From: Rupak Majumdar <rupak@EECS.Berkeley.EDU> Message-Id: <200211211832.KAA02753@ic.EECS.Berkeley.EDU> Subject: [ESD-Seminar] Harald Ruess on Monday Nov 25, 4 pm Date: Thu, 21 Nov 2002 10:32:58 -0800 (PST) Electronic Systems Design Seminar http://www-cad.eecs.berkeley.edu/esd-seminar 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.
This archive was generated by hypermail 2b30 : 11/21/02 PST