New version of the PML language and (classical) proof assistant
-
Updated
Feb 13, 2026 - OCaml
New version of the PML language and (classical) proof assistant
Evaluation task for 2024 UIUC+ undergraduate interns
Neuro-symbolic engine that uses Z3 SMT solver to formally prove behavioral equivalence between legacy and modernized code.
Dataset of equivalent and non-equivalent Dafny functions for benchmarking program equivalence checkers
An MLP-based incomplete heuristic model to predict functional counterexamples in zero-equivalent straight-line programs, bypassing the state-space explosion of formal SMT solvers.
Did behaviour change between two versions of a program, and on which inputs? A replayed witness, a proof, or an honest UNKNOWN.
To associate your repository with the program-equivalence topic, visit your repo's landing page and select "manage topics."