Automatic verification of concurrent programs remains a critical
and open problem. One key challenge in verifying such programs is
reasoning soundly about all possible interleavings of the two threads. Previous work addresses this challenge by considering each interleaving at a time.
In this work, we propose a novel automatic verifier, named
NESTER, that refutes all interleavings of a pair of paths at once, using DAG interpolants. These are then combined using the Lazy Interpolants strategy of McMillan.
NESTER can also verify a safety property for program runs with procedure calls and returns in which the calls and returns of threads are well-nested. This has been implemented to target Java Virtual Machine bytecode and has been used to verify or find counterexamples
to critical safety properties in a collection of open concurrency benchmarks.
Best,
Qinheping Hu
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}