Recent & Upcoming Talks

ISLa is a novel specification language and fuzzer generating system inputs from grammars and constraints. It lets you specify input constraints like “a variable has to be defined before it is used”; “the ‘file name’ block must be 100 bytes long,” or “the number of columns in all CSV rows must be identical.” We show that a few ISLa constraints suffice to produce 100% semantically valid inputs while still maintaining input diversity. ISLa can also parse and precisely validate; inputs against semantic constraints. On top, our ISLearn prototype mines constraints from existing examples based on a catalog of common patterns. The resulting constraints can then again be used for fuzzing and parsing.

Changing software without breaking it! How to use Abstract Execution and REFINITY to automatically prove properties of program transformation rules.

REFINITY is a workbench for modeling statement-level transformation rules on Java programs with the aim to formally verify their …

In this tutorial session colocated with the International Conference on integrated Formal Methods (iFM), I gave a 30-minutes talk …

We propose the trace modality, a concept to uniformly express a wide range of program verification problems. To demonstrate its …

We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter …