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. The detailed explanation 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.