1

Certified Abstract Cost Analysis

A program containing placeholders for unspecified statements or expressions is called an abstract (or schematic) program. Placeholder symbols occur naturally in program transformation rules, as used in refactoring, compilation, optimization, or …

Safer Parallelization

Adapting sequential legacy software to parallel environments can not only save time and money, but additionally avoids the loss of valuable domain knowledge hidden in existing code. A common parallelization approach is the use of standardized …

REFINITY to Model and Prove Program Transformation Rules

REFINITY is a workbench for modeling statement-level transformation rules on Java programs with the aim to formally verify their correctness. It is based on Abstract Execution, a verification framework for abstract programs with a high degree of …

Abstract Execution

We propose a new static software analysis principle called *Abstract Execution*, generalizing Symbolic Execution: While the latter analyzes all possible execution paths of a *specific program*, Abstract Execution analyzes a *partially unspecified …

The Trace Modality

We propose the *trace modality*, a concept to uniformly express a wide range of program verification problems. To demonstrate its usefulness, we formalize several program verification problems in it: Functional Verification, Information Flow …

Modular, Correct Compilation with Automatic Soundness Proofs

Assessing the Coverage of Formal Specifications

Proposes a symbolic-execution based approach to measure how much of an implementation is covered by a formal specification, or, in other words, the strength of a specification.

A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows

A General Lattice Model for Merging Symbolic Execution Branches