| 10:00 | Muralidhar Talupur (CMU Pittsburgh) | Model Checking Protocols without Atomicity Assumptions |
| Formally verifying intricate parameterized systems such as mutual exclusion protocols and cache coherence protocols is very hard. While theorem proving based approaches require manual guidance, automatic methods like model checking can be used for these protocols under severe restrictions, namely that all protocol actions take place atomically. In this talk we will briefly outline a new method that allows us to apply model checking automatically to these systems without any restrictions. Using this method we have verified intricate mutual exclusion protocols like Szymanski's and the Bakery algorithm. | ||
| 10:30 | Javier Esparza (Universität Stuttgart) | Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems |
| Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this talk, this concept is investigated in the context of sequential (possibly recursive) programs whose statements are given as BDDs. It is examined how Craig interpolants can be computed efficiently in this case and a new, special type of interpolants is proposed. Moreover, it is shown how to treat multiple counterexamples in one refinement cycle. We have implemented this approach as an extension of the model checker Moped and report on experiments. | ||
| 11:00 | Kaffeepause | |
| 11:15 | Helmut Veith (TU München) | Verification Beyond Single-Pass Model Checking |
| 11:45 | Stefan Schwoon (Universität Stuttgart) | Model-Checking für Authorisierungsprobleme |
| Kellerautomaten haben sich als geeignetes Modell für prozedurale Programme erwiesen, weswegen Algorithmen für die entsprechenden Model-Checking-Probleme in den letzten Jahren eingehend untersucht wurden. Für diese Algorithmen hat sich eine neue, überraschende Anwendung ergeben im Bereich der Authorisierung mit Hilfe von SPKI/SDSI. Der Vortrag stellt diese Anwendung vor und geht auf die speziellen Fragestellungen ein, die sich in diesem Zusammenhang ergeben. | ||
| 12:00 | Mittagspause | |
| 14:00 | Wolfram Büttner (OneSpin Solutions) | Is Formal Verification Bound to Remain a Junior Partner of Simulation? |
|
After decades of research the late eighties and the nineties have
produced a number of "checkers" verifying complex aspects of
industrial designs and thus raising the attention of early
adopters. These achievements, however, have not led to wide
adoption. The generally accepted explanation of this resistance is the
required methodology change and the lacking ease of use. We see a more
fundamental reason in the difficulty to set up a compelling value
proposition based on isolated proven theorems. With the advent of assertion-based verification the first two of the above obstacles are being successfully tackled. In this framework formal verification is piggybacking on advanced and established simulation platforms. We foresee as a next step in the evolution of formal verification fully formal solutions for important functional verification tasks. Similar to formal equivalence checking these solutions will excel by extreme quality and improved productivity. This claim is exemplified by reporting about the formal verification of an industrial embedded processor within a large national initiative involving industry and academia. | ||
| 15:00 | Jan Johannsen (LMU München) | Bounded Model Checking for the Linear Time Mu-Calculus |
| The linear time mu-calculus muTL is an extension of LTL that is capable of expressing all omega-regular properties. We present a bounded model checking encoding of muTL into SAT, and report on experiments to use this encoding for the SAT-based verification of regular proerties. | ||
| 15:30 | Andrey Rybalchenko (Max-Planck-Institut für Informatik, Saarbrücken) | Termination Proofs for Systems Code |
| Termination of (operating) system components is crucial for the successful system behavior. We present the main building blocks of our tool for the automated termination proofs of C code fragments (containing nested loops, gotos, mutually recursive function calls, pointer aliasing etc). These blocks are transition invariants, transition predicate abstraction, and abstraction refinement for termination. Transition invariants are auxiliary assertions for proving termination that can be computed by least fixed point iteration. We apply transition predicate abstraction to make such iteration effective. We discover the relevant transition predicates from counterexamples. Finally, we describe how we extend the SLAM software model checker to automatically compute transition invariants, which gives us a tool for proving termination of C programs. Joint work with Byron Cook and Andreas Podelski. | ||
| 16:00 | Kaffeepause | |
| 16:30 | Michael Weber (TH Aachen) | Parallel Model Checking |
| We give a general introduction to parallel model checking, and describe its ingredients and challenges by example of algorithms for fragments of the mu-calculus. | ||
| 17:00 | Martin Leucker (TU München) | Don't Know in the mu-calculus |
| This work presents game-based model checking for abstract models with respect to specifications in mu-calculus, interpreted over a 3-valued semantics. If the model checking result is indefinite (don't know), the abstract model is refined, based on an analysis of the cause for this result. For finite concrete models our abstraction-refinement is fully automatic and guaranteed to terminate with a definite result true or false. | ||
| 17:30 | Martin Lange (LMU München) | Model Checking Non-Regular Properties |
| The modal mu-calculus captures exactly the bisimulation-invariant regular tree languages. Hence, properties expressed in formulas of its fragments like LTL or CTL for instance are only regular. We present temporal logics whose expressive power reaches beyond that of the modal mu-calculus and survey known result about these with a focus on their model checking problems - due to the undecidability of satisfiability. | ||