Abstract Execution: Automatically Proving Infinitely Many Programs

PhD thesis introducing a complete framework for Abstract Execution, as well a general framework for symbolic execution, model and dynamic trace logic based on the trace modality, and new safety preconditions for statement-based refactoring techniques …

From Trees to DAGs: A General Lattice Model for Symbolic Execution

Enforcing Datalog Policies with Service Automata on Distributed Version Control Systems