Niagara

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.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.

Publications:

  1. AE-VAL: Horn clause-based Skolemizer for ∀∃-formulas , Grigory Fedyukovich, Arie Gurfinkel, and Natasha Sharygina  
  2. Automated Discovery of Simulation Between Programs ,  Grigory Fedyukovich, Arie Gurfinkel, and Natasha Sharygina
  3. Incremental Verification of Compiler Optimizations ,  Grigory Fedyukovich, Arie Gurfinkel, and Natasha Sharygina
  4. Property Directed Equivalence via Abstract Simulation ,  Grigory Fedyukovich, Arie Gurfinkel, and Natasha Sharygina