Recent & Upcoming Talks

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 …