Markus N. Rabe

Markus N. Rabe

Contact

Markus N. Rabe (Ph.D. Student)

Reactive Systems Group
Universität des Saarlandes
Phone: +49 681 302 5637
eMail: rabe at cs.uni-saarland.de
Building: E 1.3 Room: 507

I just moved to UC Berkeley. Please find my new homepage here.

Research

I study model checking problems for system properties beyond LTL and CTL*, including properties from information-flow security and also probabilistic properties. Their common feature is that they cannot be determined by considering a single execution of the system. I focus on their automatic verification using automata-theory and symbolic model checking techniques.

Publications

[RT15] CAQE: A Certifying QBF Solver.
with Leander Tentrup.
FMCAD 2015.
Implementation: CAQE
[FRS15] Algorithms for Model Checking HyperLTL and HyperCTL*.
with Bernd Finkbeiner and César Sánchez.
CAV 2015.
Implementation
[FR14] The Linear-Hyper-Branching Spectrum of Temporal Logics
with Bernd Finkbeiner
Information Technology 2014
[RWKYH14] Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains
with Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov, and Youssef Hamadi
Accepted at QEST 2014
[RLP14] A Shallow Embedding of HyperCTL *
with Peter Lammich and Andrei Popescu
Archive of Formal Proofs
[CFKMRS14] Temporal Logics for Hyperproperties
with Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, and César Sánchez
POST 2014
Implementation
Full version available at arxiv
[FRS13] A Temporal Logic for Hyperproperties
with Bernd Finkbeiner and César Sánchez
arXiv preprint, arXiv:1306.6657.
[RS13] Optimal Time-Abstract Schedulers for CTMDPs and
Continuous-Time Markov Games
with Sven Schewe.
Theoretical Computer Science.
[DFR12] Monitoring Temporal Information Flow
with Rayna Dimitrova and Bernd Finkbeiner
ISoLA 2012 (invited paper).
[GR12] Verification of partial-information probabilistic systems using counterexample-guided refinements
with Sergio Giro
ATVA 2012
[DFKRS12] Model Checking Information Flow in Reactive Systems
with Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, and Helmut Seidl
VMCAI 2012
Won the RS3 Best Paper Award! (Best among 27 papers of the RS3 project.)
[FRSZ11] Efficient Approximation of Optimal Control for Continuous-Time Markov Games
with John Fearnley, Sven Schewe, and Lijun Zhang
FSTTCS 2011
[RS11] Finite Optimal Control for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games
with Sven Schewe
Acta Informatica, vol. 48, 2011
[RS10] Optimal Time-Abstract Schedulers for CTMDPs and Markov Games
with Sven Schewe
Quantitative Aspects of Programming Languages (QAPL) 2010

Teaching

SS 2012 Embedded Systems.
WS 2011/12 Proseminar: Softwarezuverlässigkeit.
SS 2011 Seminar: Games, Synthesis and Robotics.
SS 2010 Assistant for Programmierung 1.
SS 2008 Student assistant for Concurrent Programming at the Dependable Systems Chair.
WS 2007/08 Student assistant for a preparatory course.
SS 2007 Student assistant for Programmierung 2 at the Software Engineering Chair.
WS 2006/07 Student assistant for Programmierung 1 at the Programming Systems Lab.
WS 2006/07 Student assistant for a preparatory course helping new students to catch up to university level math.