Assume, Guarantee or Repair -- A Regular Framework for Non Regular Properties (full version)
Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald

TL;DR
This paper introduces AGR, a framework that verifies and repairs communication programs with complex properties using a learning-based assume-guarantee reasoning approach, effectively handling infinite-state systems.
Contribution
It presents a novel integrated verification and repair framework for communication programs with complex properties, utilizing a learning-based assume-guarantee method and finite abstractions.
Findings
Achieved compact correctness proofs in experiments
Performed quick repairs on communication protocols
Effectively handled infinite-state systems with complex properties
Abstract
We present Assume-Guarantee-Repair (AGR) - a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs - these are simple C-like programs, extended with synchronous actions over communication channels. Our method, which consists of a learning-based approach to assume-guarantee reasoning, performs verification and repair simultaneously: in every iteration, AGR either makes another step towards proving that the (current) system satisfies the required properties, or alters the system in a way that brings it closer to satisfying the properties. To handle infinite-state systems we build finite abstractions, for which we check the satisfaction of complex properties that contain first-order constraints, using both syntactic and semantic-aware methods. We implemented AGR and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
