Teaching material
Tutorials
Tutorial papers and slides on the methods my group works with.
Parameterized systems
-
View abstraction
Abstraction technique for verifying systems with an unbounded number of components.
-
Parameterized systems
Dagstuhl 2007
A collection of the techniques we have designed for verification of parameterized systems.
-
Monotonic abstraction
RP 2008 · SOFSEM 2010
A lightweight description of parameterized verification, in two alternative presentations.
Infinite-state systems
-
Well-quasi-ordered transition systems
BSL 2010
A detailed description of our methods for model checking of infinite-state systems.
Paper (PDF) Slides, MOVEP 2016 (PDF) Slides, MOVEP 2016 (Keynote)
-
Regular model checking
STTT 2012
An introduction to representing states as words and transitions as transducers.
-
Infinite-state Markov chains
CONCUR 2011
Framework for model checking of Markov chains induced by Petri nets, Turing machines, communicating processes and others.
Time and cost
-
Timed push-down automata
QFM 2012
Push-down automata extended with time.
-
Priced timed Petri nets
INFINITY 2012
Checking coverability properties for Petri nets extended with both time and prices.
-
Priced discrete-timed Petri nets
LIAFA 2009
Analysis of priced discrete-timed Petri nets.
Programs and data structures
-
Heap-manipulating programs
Dagstuhl 2008
Symbolic backward reachability analysis for verification of programs with pointers.