Bounded model checking of high-integrity software
Sagar Chaki · 2013
Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. One of the most successful variants of model checking is Bounded Model Checking (BMC) [2] which leverages the power of state-of-the-art satisfiability (SAT) 1 and satisfiability-modulo-theory (SMT) 2 to push the boundaries of automated verification. Like model checking, BMC was developed originally for hardware, but has since been extended and applied successfully to verify sequential [4], multi-threaded [1, 10], as well as real-time software [3].