Seminar: Symbolic Model Checking in the Analysis of Critical Systems
Schedule
Seminar: Prof. Dr. Stefan Leue, Alina Bey
Thursday 15:15 - 16:45 Room: PZ 902
| Session | Date | Topic |
|---|---|---|
| 0.1 | 22.10.2015 | Initial Meeting, Formalities, Topic Distribution |
| 0.2 | 29.10.2015 | How To Seminar |
Description
Contents
Model Checking is a technique to determine whether the state-transition model (Kripke structure) for some software or hardware system satisfies a given specification, typically formalized using some form of temporal logic. This seminar will present various methods, techniques and tools in the realm of symbolic model checking. In symbolic model checking, the transition system is encoded in the form of an Ordered Binary Decision Diagram (OBDD), a canoncial representation for boolean functions. This representation can then be used to either perform fixpoint-based CTL or LTL mode checking, or to translate the model into a SAT problem and to perform bounded model checking on it.
Participants
Bachelor Computer Science level standing in Logic, Theory of Computaton, Programming and Software Engineering
Subject Area
Informatik der Systeme / Angewandte Informatik
Contents / Syllabus
The participants will be equipped with a deeper understanding of Symbolic Model Checking.
Seminar taught entirely in English.
Seminar presentation (appr. 30 mins.) and seminar report (appr. 10 pages)
The grading schemes can be found here:
Literature
Will be announced
Credits
SWS: 2
ECTS-points: 4
Topics
Basic Techniques
- Boolean Systems
- Analysis of Boolean Programs
- Verifying LTL Properties of Bytecode with Symbolic Execution
- Efficient Generation and Represantation of Failure Lists out of an Information Flux Model for Modeling Safety Critical Systems
- Symbolic Model Checking without BDDs
Timed Systems
Equivalences
- Model Checking Process Equivalences
- Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs
- A Computationally Complete Symbolic Attacker for Equivalence Properties
Fixed-Point Logic
- The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols
- Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic