On Module-Based Abstraction and Repair of Behavioral Programs

摘要

The number of states a program has tends to grow exponentially in the size of the code. This phenomenon, known as state explosion, hinders the verification and repair of large programs. A key technique for coping with state explosion is using abstractions, where one substitutes a program's state graph with smaller over-approximations thereof. We show how module-based abstraction-refinement strategies can be applied to the verification of programs written in the recently proposed framework of Behavioral Programming. Further, we demonstrate how - by using a sought-after repair as a means of refining existing abstractions -these techniques can improve the scalability of existing program repair algorithms. Our findings are supported by a proof-of-concept tool.