We have developed an approach that combines efforts on unbounded property directed equivalence checking and simulation synthesis. A brief explanation can be found here, and a detailed technical report can be found here.
So far, we have the following research results:
- AE-VAL algorithm (ext.abstract, slides) to decide validity and Skolemize Forall-Exists formulas in FOL
- SimAbs algorithm (paper, experiments, slides) to automatically discover simulation relation between programs
- OptVerify algorithm (paper, experiments) to migrate safety proofs across evolution boundaries
- PDE and ASSI algorithms (paper, slides) to establish Property Directed Equivalence between programs using Abstract Simulations
The repository of our implementation is available here.