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.


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

  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).