3 papers
cs.SE2026
Certified Program Synthesis with a Multi-Modal Verifier
Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein +5
Certified program synthesis (aka vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of their alignment from a…
cs.PL2026
Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
Ziyi Yang, George Pîrlea, Ilya Sergey
We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system…
cs.PL2024
Small Scale Reflection for the Working Lean User
Vladimir Gladshtein, George Pîrlea, Ilya Sergey
We present the design and implementation of the Small Scale Reflection proof methodology and tactic language (a.k.a. SSR) for the Lean 4 proof assistant. Like its Coq predecessor S…