research
∙
07/31/2023
Towards Formal Verification of a TPM Software Stack
The Trusted Platform Module (TPM) is a cryptoprocessor designed to prote...
share
research
∙
07/24/2023
Execution at RISC: Stealth JOP Attacks on RISC-V Applications
RISC-V is a recently developed open instruction set architecture gaining...
research
∙
11/26/2022
An Efficient Black-Box Support of Advanced Coverage Criteria for Klee
Dynamic symbolic execution (DSE) is a powerful test generation approach ...
research
∙
11/26/2022
Control-Flow Integrity at RISC: Attacking RISC-V by Jump-Oriented Programming
RISC-V is an open instruction set architecture recently developed for em...
research
∙
02/21/2022
Certified Verification of Relational Properties
The use of function contracts to specify the behavior of functions often...
research
∙
11/25/2019
Abstract Compilation for Verification of Numerical Accuracy Properties
Verification of numerical accuracy properties in modern software remains...
research
∙
11/26/2018
MetAcsl: Specification and Verification of High-Level Properties
Modular deductive verification is a powerful technique capable to show t...
research
∙
01/21/2018
Static and Dynamic Verification of Relational Properties on Self-Composed C Code
Function contracts are a well-established way of formally specifying the...
research
∙
01/21/2018
Self-composition to Prove Relational Properties in Annotated C Program
Deductive verification provides a powerful tool to show functional prope...
research
∙
08/29/2017
Freeing Testers from Polluting Test Objectives
Testing is the primary approach for detecting software defects. A major ...
research
∙
08/24/2017