Message-Id: <200104070103.SAA12237@ic.EECS.Berkeley.EDU> Subject: Interesting seminar Date: Fri, 06 Apr 2001 18:03:41 -0700 From: Tom Henzinger <tah@ic.eecs.berkeley.edu> ------- Forwarded Message Return-Path: tah Received: from localhost (fmang@localhost) by ic.EECS.Berkeley.EDU (8.8.5/8.8.8) with ESMTP id QAA10107; Fri, 6 Apr 2001 16:51:33 -0700 (PDT) Date: Fri, 6 Apr 2001 16:51:33 -0700 (PDT) From: Freddy Mang <fmang@ic.EECS.Berkeley.EDU> To: <cad-seminar@ic.EECS.Berkeley.EDU> cc: Freddy Mang <fmang@ic.EECS.Berkeley.EDU> Subject: CAD Seminar next Wednesday (4/11): Dr. Shaz Qadeer Message-ID: <Pine.OSF.4.33.0104061647510.10344-100000@ic.EECS.Berkeley.EDU> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Speaker: Dr. Shaz Qadeer, Compaq Systems Research Center Title: Predicate abstraction for software verification Date: 11 April 2001 (next Wednesday) Time: 5:00pm - 6:00pm Venue: Hogan Room (531 Cory Hall) Abstract: A completely automatic method for software verification is impossible since the problem is undecidable in general. Existing semi-automatic techniques that require annotations, such as loop invariants, from the programmer have had limited acceptance because the annotation burden on programmers is perceived to be excessive. In this talk, I will describe a method to infer loop invariants for programs written in a general-purpose programming language. We have implemented this method and used it to verify the exported procedure "create" from the implementation of a file system Frangipani. Our method for inferring loop invariants has several nice features compared to previous methods. First, it can infer loop invariants with universal quantifications; this is critical in the verification of Frangipani whose specification comprises a number of assertions on unbounded data. Second, the method is based on forward analysis; it analyzes a loop in the context of the code preceding it resulting in more precision. At the core of our algorithm is predicate abstraction, a technique for characterizing a program in terms of how it transforms the truth values of a finite set of predicates. I will describe a novel algorithm for constructing the abstraction of a concrete set of states in terms of the predicates. I will also describe experimental results showing that our algorithm is more efficient in practice than existing algorithms. Bio: Shaz Qadeer received a B.Tech. from the Indian Institute of Technology Kanpur in 1994. He received an M.S. and a Ph.D. from University of California at Berkeley in 1997 and 1999 respectively. Since November 1999, he has been at Compaq Systems Research Center. He is interested in the formal design and analysis of hardware and concurrent software systems, model checking and automated theorem proving. ------- End of Forwarded Message
This archive was generated by hypermail 2b30 : 11/04/02 PST