SymmPa: a Software Model Checker for Replicated Concurrent Programs

SymmPa is a CEGAR-based tool for automatically verifying safety properties of concurrent C programs. SymmPa targets replicated concurrent programs, where many threads execute the same function. Scalability is achieved through predicate abstraction and symmetry reduction; the former curbs data explosion, while the latter exploits the structure of replicated programs to reduce state space explosion arising from thread interleavings.

For questions about SymmPa contact alastair.donaldson@imperial.ac.uk, michael.tautschnig@cs.ox.ac.uk or alexander.kaiser@cs.ox.ac.uk.

Obtaining and Using the Tool

SymmPa has been integrated with SatAbs 3.1 and Boom. To use the new features for replicated concurrent programs, use the --concurrency option. For best possible performance of the Boom, rename the boom binary shipped in the SatAbs archive to bboom and download this boom binary (Linux x86-64).

We had previously published a prototype as part of the foundational CAV'11 paper. Although we do still support the special modelling constructs described on that page, but

POSIX threads (pthread) can now be used instead of non-portable __CPROVER_ASYNC_ labels or __CPROVER_atomic_begin/__CPROVER_atomic_end;
the new refinement techniques should make manual predicate annotation unnecessary.

Experimental Results

For our experiments we used an 8-core Intel 64bit system running Ubuntu 10.04.3. We do expect, however, that the experiments are reproducible on any Linux system.

Our experiments were performed using the CPROVER Benchmarking Toolkit. To repeat our experiments, download symmpa.tar.gz and symmpa.cprover-bm.tar.gz and proceed as described on the CPROVER Benchmarking Toolkit's web page.

For reference, all our log files and detailed results are available online as well: