« Tech talk video: Efficient Implementation of Property Directed Reachability | Main | New tech talk video: Formalizing Haskell 98 in the K semantic framework »

Tech Talk: Efficient Implementation of Property Directed Reachability 

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual date and time for this talk, it is on Monday, 6 February 2012, at 10am.

title: Efficient Implementation of Property Directed Reachability

speaker: Alan Mishchenko

time: Monday, 6 February 2012, 10:00am

Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)


Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.

Relevant links: the paper, slides for the talk.

bio: Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998. Currently, Alan is an Associate Researcher at University of California, Berkeley. His research interests are in developing computationally efficient methods for logic synthesis and verification.

Reader Comments

There are no comments for this journal entry. To create a new comment, use the form below.

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>