RelationalReasoning

Two program runs, one relation.
Verification and proof automation.

two arrays, one relation

GArel

Try the browser playground for BiArel examples and relational cost checks.

Open playground
Research project

Relational CellMorphing

Automated relational verification for array programs through cell morphing, prophecy, and CHC solving.

Slides Evaluation Logic GitHub
Course platform

ProgramAnalysis

Practice material for verification
and proof automation.

Open the bootcamp