Date: Tue, 23 Sep 2003 20:54:49 -0700 From: George Necula <necula@eecs.berkeley.edu> Subject: FW: Title and abstract Message-id: <4E06A937DADC3842ACE4D3A1096A9EACB591AC@janus.EECS.Berkeley.EDU> On Monday the 29th at 4pm, Maria Sorea from SRI will speak at the PS seminar. George. -----Original Message----- From: Maria Sorea [mailto:sorea@csl.sri.com] Sent: Friday, September 19, 2003 8:42 AM To: necula@cs.berkeley.edu Cc: tah@eecs.berkeley.edu; msanvido@eecs.berkeley.edu; sorea@csl.sri.com Subject: Title and abstract George, please find below the title and the abstract for the talk on Sep 29. Thanks, Maria Title: Counterexample-Guided Model Checking Abstract: The generation of counterexamples is frequently touted as one of the primary advantages of model checking as a verification technique. However, the generation of trace-like counterexamples is limited to a small fragment of branching-time temporal logic. When model checking does succeed in verifying a property, there is typically no independently checkable witness that can be used as evidence for the verified property. We present a definition of witnesses, and, dually, counterexamples, for computation-tree logic (CTL), and describe a model checking algorithm that is based on the generation of evidence. Our model checking algorithm is local in the sense that it explores only the reachable states, and in some cases, even less than the reachable states. It partitions the given initial set of states into those that do, and those that do not satisfy the given property, with a corresponding witness and counterexample that is independently verifiable. We have built a model checker based on these ideas that works quite efficiently despite the overhead of generating evidence.
This archive was generated by hypermail 2b30 : 11/23/03 PST