Showing 2026 · cs.PLShow all
2 papers · 2 filters
cs.PL2026
Scenario Proofs for Verification of Distributed Protocols
Zhendong Ang, George Pîrlea, Umang Mathur
Formal verification of distributed protocols is still dominated by inductive-invariant proofs, whose central challenge is discovering strengthening assertions that rule out unreach…
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…