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
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
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.