Assume , Guarantee or Repair Student submission

We present Assume-Guarantee-Repair (AGR) – a novel framework which not only verifies that a program is error-free, but also repairs the program, in case the verification fails. We consider simple C-like programs, extended with synchronous communication actions over communication channels. Our method uses compositional approach to modularly check the system for errors, and to repair it. We fulfill the two tasks simultaneously: in every iteration of the procedure, we either make another step towards proving safety of the (current) system, or remove the current vulnerability in a way that brings it closer to being safe. We manage to handle infinite-state systems by using a finite abstract representation. We describe our method and demonstrate the effectiveness of AGR on several examples using existing SMT solvers, learning, and reachability analysis tools.