IC Monday Seminar : "Algorithmic Software Verification for Data Structures"
Event details
| Date | 21.03.2011 |
| Hour | 16:15 |
| Speaker | Dr. Pavol Cerny, IST Austria - IC Faculty candidate |
| Location |
INM 202
|
| Category | Conferences - Seminars |
Abstract : Algorithmic methods for software verification have been very successful in verifying sequential properties of control-oriented programs such as device drivers. The main challenges currently include verification of concurrent and data-oriented programs. In particular, concurrent data structures are notoriously difficult to implement correctly. Algorithmic software verification is an especially effective analysis method in this case, as the difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. In this talk, I will focus on algorithms for verifying properties of both sequential and concurrent programs accessing heap-based data structures. First, I will present streaming string transducers, a robust, expressive, and analyzable model of programs. The pre/post condition checking and equivalence checking problems are decidable for streaming string transducers, and the expressiveness of the model is the same as that of MSO transductions. Second, I will show how these results lead to algorithms for assertion checking and for checking functional equivalence for a class of sequential programs. This class includes common list-manipulating routines, such as insert, delete, and reverse. Third, I will present an algorithm for verifying linearizability for a class of concurrent programs which covers many of the common implementation techniques, such as fine-grained locking, and optimistic, lazy, and lock-free synchronization. The tool COLT implements the algorithm, and was used to verify (and find bugs in) a representative sample of Java implementations of the concurrent set data structure. Bio: Pavol Cerny is a postdoctoral researcher at IST Austria. He obtained his PhD in Computer Science from the University of Pennsylvania in 2009 and a DEA diploma from Ecole normale superieure, Paris, France in 2003. His current research interests are in formal methods and programming languages, in particular in algorithmic verification for concurrent software and in quantitative program synthesis. He also worked on a new programming model for data parallel programs, on verification of software security, and on security analysis of electronic voting machines.
Links
Practical information
- General public
- Free
Contact
- Christine Moscioni