Abstracting and Counting Synchronizing Processes
16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015.
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.
[GREP15] Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng, "Abstracting and Counting Synchronizing Processes", 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015. |
|
