We have developed an approach that combines efforts on unbounded property directed equivalence checking and simulation synthesis. A brief explanation can be found here.

So far, we have the following research results:

  • AE-VAL algorithm (ext.abstractslides) to decide validity and Skolemize Forall-Exists formulas in FOL

  • SimAbs algorithm (paperexperimentsslides) to automatically discover simulation relation between programs

  • OptVerify algorithm (paperexperiments) to migrate safety proofs across evolution boundaries

  • PDE and ASSI algorithms (paperslides) to establish Property Directed Equivalence between programs using Abstract Simulations

The repository of our implementation is available here.