|
 |
Bounded Model Checking: From Refutation to Verification
Harald Ruess
SRI
Monday, November 25th, 2002, 4:00pm-5:00pm
540AB Cory Hall (DOP Center Classroom)
|
Abstract
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.
Speaker
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.
|
