We introduce a novel verification method for multi-threaded programs that is fully automated and enables scalable compositional reasoning in reference [2] below. To achieve full automation, our technique supports abstraction refinement, which we realize with another research contribution, a constraint solver for Horn clauses over linear arithmetic constraints. We extend this method from safety to termination properties in [5] and published a tool paper describing our implementation of these algorithms in the most prestigious verification conference [4]. We solve two additional challenges in handling abstraction of control-flow [1] and solving Horn clauses in the presence of uninterpreted functions [3].
This project has been carried at the Technical University Munich and is joint work with Ashutosh Gupta and Andrey Rybalchenko.