(2022) Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties.
|
Text
s10009-022-00669-9.pdf Download (1MB) | Preview |
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 evaluated it on various communication protocols. Our experiments present compact proofs of correctness and quick repairs.
| Item Type: | Article |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Depositing User: | Hadar Frenkel |
| Date Deposited: | 13 Oct 2022 07:54 |
| Last Modified: | 13 Oct 2022 07:54 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3825 |
Actions
Actions (login required)
 |
View Item |