News
21.10.2015

No lecture on Nov. 19, 2015There will be no lecture/exercise group on Thursday, November 19, 2015. 
Formal Engineering of Digital and Hybrid Systems
Audience
This advanced course addresses Bachelor and Master students in Computer Science, Bioinformatics, CuK or Computerlinguistics. Background in the module Verification are of advantage but not mandatory.
Topic
The main topic of this lecture is to show how verification techniques can be applied to realworld systems. The main challenge is hereby to cope with the state space explosion problem: The size of the state space typically grows exponentially in the number of components. For instance, a circuit with 64 flipflops can contain up to 2^{64} =18446744073709551616 states. If all these states have to be traversed only once during verification and visiting a single state takes 1 ns, the traversal still needs more than 500 years! This severely limits all algorithms relying on an explicit state space representation (i.e. a representation which lists all states and transitions of the system) to rather small state spaces.
Symbolic methods, in contrast, represent states and transitions as solutions of formulas or as paths in a directed graph. This has the advantage that the size of the representation can be smaller by orders of magnitude than the represented state space. However, this requires dedicated algorithms which can directly work on such symbolic representations and whose running time only depends on the size of the representation and not on the size of the represented state space.
In this lecture, we will look into different symbolic data structures and algorithms like ordered binary decision diagrams, (linear) andinverter graphs, SAT and QBF formulas, difference bound matrices, ... and show how they can be used to verify not only digital circuits, but also timed automata and linear hybrid systems.
Credits:
6 ECTS points (3 hours of lecture, 1 hour of tutorials, and some exercises every week).
Time and location:
Tuesday 1416 and Thursday 1012 in the seminar room 015 in building E1 3