symex-formally-formalized

Coq formalization of Symbolic Execution Formally Explained.

Build

The included Makefile (created for Coq 8.16.1) should allow just

make

To update the Makefile use

coq_makefile -f _CoqProject -o Makefile

Table of Contents

Formalization of de Boer et al.

• BasicConcrete formalizes section 2. Basic symbolic execution for simple arithmetic and boolean expression with integer valuations.
  • Syntax and notation for expressions is in Expr
  • Notation and lemmas about maps used for substitution and valuation are in Maps
• Recursion formalizes 3. Recursion – an extension of the basic language with procedure calls.
• OOP contains an incomplete formalization of 4. Object orientation.

The approach to syntax and transition relation semantics is based on Programming Language Foundations

Extensions

• Trace Semantics introduces trace semantics for the language with procedures
  • Notation and lemmas about traces are in Traces
  • Some examples of programs and their traces are found in examples
• Parallel Traces adds a parallel composition operator to the base language with trace semantics. Additionally contains some preliminary results about reduction of trace sets.
  • The base language with a parallel operator is in Parallel
• Context Reduction contains an alternative approach to syntax based on reductions in a context inspired by Mechanized Semantics
• Partial Order Reduction formalizes partial order reduction of symbolic execution in the context reduction style
  • Some examples of programs and their traces with and without POR are found in examples
• Program Logics contains some notes on program logics for Parallel. In particular the DL from sympaths and Einar's simple parallel logic

Other

• PLACES contains a talk proposal to PLACES 2023