This is the home of the research project Niagara. We develop 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.