icon-carat-right menu search cmu-wordmark

Spacer

Software
Spacer is an algorithmic framework for SMT-based software model checking using proofs and counterexamples.
Publisher

Bitbucket

Abstract

SPACER, Software Proof-Based Abstraction with CounterExample-Based Refinement, is an algorithmic framework for SMT-based software model checking using proofs and counterexamples.