Authors: Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng
Abstract: We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. This is beyond the capabilities of current automatic verification techniques. For this purpose, we define an original logic that mixes variables refering to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build an original nested counter example based refinement scheme for establishing correctness (expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.
In Proceedings of the the 16th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI 2014.
Last version (pdf)