Electronic Systems Design Seminar
We present the foundation of bounded model checking for infinite-state
systems. Given a program M over an infinite state type, a linear temporal
logic formula PHI with domain-specific constraints over program states, and an
upper bound k, this procedure determines if there is a falsifying path of length k
to the hypothesis that M satisfies the specification PHI. The resulting satisfiability
problems are effectively solved using a combination of a propositional SAT checker with
domain-specific decision procedures. Our verification engine is lazy in that
propositional abstractions of Boolean constraint formulas are incrementally refined
by generating lemmas on demand from an automated analysis of spurious counterexamples
using theorem proving. Using iterated induction, bounded model checking is then
used to verify safety properties.
This is a joint work with Leonardo de Moura and Maria Sorea.
Harald Ruess works mainly on the application of logic for analyzing computational systems, on the development of decision procedures, and on verifying cryptographic protocols. He received a Msc in CS from SDSU (1990) and a mathematics degree (1991) and a PhD in CS from the Universitaet Ulm (1995). The topic of his thesis was on reflection in type theory. During my postdoctoral studies at SRI he performed large-scale hardware verifications using the PVS verification system. After returning to U. Ulm as an assistent professor, he joined SRI as a member of staff in late 1998.