Date: Fri, 11 Jan 2002 12:54:32 -0800 (PST) From: Ranjit Jhala <jhala@ic.eecs.berkeley.edu> Subject: Reminder: POPL Practice Talk Message-ID: <Pine.LNX.4.33.0201111253310.1752-100000@edalap09.eecs.berkeley.edu> A gentle reminder: today at 2 pm. 380 Soda. Thanks! -Ranjit. > Hi, > I am giving a practice talk for POPL (different from Zhendong's > ...) on "Lazy Abstraction" on: > Friday 11th Jan, Soda 380, at 2:00 Pm. > I guess some of you've heard this before but I'd really appreciate > it if you could come down and give me some feedback. > Thanks! > -Ranjit Jhala. > > Abstract: > One approach to model checking software is based on the > abstract-check-refine paradigm: build an abstract model, then check > the desired property, and if the check fails, refine the model and > start over. We introduce the concept of lazy abstraction to integrate > and optimize the three phases of the abstract-check-refine loop. Lazy > abstraction continuously builds and refines a single abstract model on > demand, driven by the model checker, so that different parts of the > model may exhibit different degrees of precision, namely just enough > to verify the desired property. We present an algorithm for model > checking safety properties using lazy abstraction and describe an > implementation of the algorithm applied to C programs. We also give an > abstract characterization of the infinite-state systems for which the > algorithm finds a safety-witnessing finite-state model whenever such a > model exists. > > Tom Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre. > > >
This archive was generated by hypermail 2b30 : 11/04/02 PST