Electronic Systems Design Seminar


Bounded Model Checking: From Refutation to Verification

Harald Ruess

Monday, November 25th, 2002, 4:00pm-5:00pm
540AB Cory Hall (DOP Center Classroom)


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.

©2002-2018 U.C. Regents