I/O Efficient Algorithms for Verification
I/O-efficient algorithms were introduced for computational problems involving manipulation of massive amounts of data. In the area of I/O-efficient algorithms the main goal is exactly to develop algorithms that minimize the number of block transfers (I/Os) used to solve a given problem. Given the context of formal verification, we explore possibilities of applying I/O efficient techniques to (distributed) model checking algorithms. We are particularly interested in I/O efficient algorithms for cycle detection and accepting cycle detection problems that are the core algorithmic problems to be solved in most practical model checking approaches.Researchers
Lubos Brim (project leader), Jiri Barnat, Pavel Simecek , Martin Smerek
Publications
S. Edelkamp, P. Sanders, and P. Simecek: Semi-External LTL Model-Checking. CAV 2008, Princeton.
J. Barnat, L. Brim, P. Simecek, and M. Weber: Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. TACAS 2008, Budapest.
J. Barnat, L. Brim, and P. Simecek: I/O-Efficient Accepting Cycle Detection. CAV 2007, Berlin.
J. Barnat, L. Brim, and P. Simecek: LTL model checking with I/O-Efficient Accepting Cycle Detection. Technical Report FIMU-RS-2007-01, Masaryk University, Faculty of Informatics, Brno, Czech Republic, January 2007.
[ paper PDF | paper PS ]Meetings
The group meets each Monday at 15:30 in Room B404.