SPACER

SPACER stands for Software Proof-based Abstraction with CounterExample-based Refinement. It is a new algorithmic framework for SMT-based software model checking using proofs and counterexamples.

Publications

1. SMT-Based Model Checking for Recursive Programs, Anvesh Komuravelli, Arie Gurfinkel and Sagar Chaki, CAV 2014 (arxiv|pdf|slides|video).

   • Source Code available from this fork of Z3
   • Download (old) binaries: Linux x86-64 OS X x86-64
   • Benchmarks
     • SLAM Benchmarks from SV-COMP repository
     • Python script to generate the Boolean Program from Bebop paper for a given number of procedures
     • Horn-SMT files for the C programs from SV-COMP 2014 are available here
     • Horn-SMT example where GPDR diverges for bounded call-stack

2. Automated Abstraction in SMT-Based Unbounded Software Model Checking, Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki and Edmund M. Clarke, CAV 2013 (arxiv|pdf|slides).

   • New version of tool: spacer v1.1. Works with latest unstable version of Z3, as of July 2, 2013.
   • Download the tool: spacer v0.1. Tested on Ubuntu 64bit 12.04.1. See README file for details.
   • Benchmarks from Software Verification Competition (SV-COMP) are available from the competition repository.
   • SV-COMP benchmarks in SMT2 format (required to run SPACER) are available at https://bitbucket.org/arieg/svb/downloads/svcomp13-full-smt.zip.
   • Experimental Results
     • Z3: down counter and up counter.
     • SPACER: down counter, up counter, PBA-only, and State-Abstraction