Markus N. Rabe

Markus N. Rabe


Markus N. Rabe

eMail: rabe at
Office: 545S, Cory Hall


I am a Postdoc at UC Berkeley working with Sanjit Seshia.

I want to enable the automatic synthesis of software from abstract specifications. Besides enhancing abstraction and automation in software development this helps to improve the safety and security of technical systems. In the following I highlight some of the areas I worked in. A relatively complete list of publications can be found on dblp and Google Scholar.

Algorithms for Quantified Boolean Formulas

I currently focus on algorithms for solving quantified boolean formulas. This problem is the key to program synthesis and has many other applications in programming languages, security, and artificial intelligence. My most recent work is an algorithm we named incremental determinization that lifts the known principles of CDCL search algorithms to the space of Skolem functions. Check out the new certifying 2QBF solver CADET.

[FFRT17] Encodings of Bounded Synthesis.
with Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup.
TACAS, 2017.
Implementation: BoSy
[RS16] Incremental Determinization.
with Sanjit Seshia.
SAT, 2016.
Implementation: CADET
[FRS15] CAQE: A Certifying QBF Solver.
with Leander Tentrup.
FMCAD 2015.
[FFRT15]  Encodings of Reactive Synthesis.
with Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup.
QUANTIFY 2015 (Workshop).

Temporal Logics for Information-flow Control

In my PhD thesis I studied specification languages and verification algorithms for information security - How can we specify what it means that a system is secure and how can we make sure that a given piece of software or hardware satisfies its specification? On a more technical level, I study the automatic analysis of system properties beyond the standard temporal logics (like LTL and CTL*), including properties from information-flow security and probabilistic properties. The common feature of these properties is that they cannot be determined by considering a single execution of the system, but instead require us to compare multiple executions. This includes hyperproperties as defined by Clarkson and Schneider. Together with my co-authors I proposed the temporal logics HyperLTL and HyperCTL* as specification languages for information-flow security and developed algorithms for the automatic verification of properties specified in HyperLTL and HyperCTL*.

[R16] A Temporal Logic Approach to Information-flow Control.
PhD Thesis.
Saarland University, 2016.
[FRS15] Algorithms for Model Checking HyperLTL and HyperCTL*.
with Bernd Finkbeiner and César Sánchez.
CAV 2015.
[FR14] The Linear-Hyper-Branching Spectrum of Temporal Logics
with Bernd Finkbeiner
Information Technology 2014
[RLP14] A Shallow Embedding of HyperCTL *
with Peter Lammich and Andrei Popescu
Archive of Formal Proofs, 2014.
[CFKMRS14]  Temporal Logics for Hyperproperties
with Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, and César Sánchez
POST 2014
Full version available at arxiv
[DFR12] Monitoring Temporal Information Flow
with Rayna Dimitrova and Bernd Finkbeiner
ISoLA 2012 (invited paper).
[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.)

Symbolic Analysis of Quantitative Models

How to find a program that satisfies its specification on the largest possible number of inputs? How to find an input to a program that maximizes the information we can observe in its output? These are very hard optimization problems as there are exponentially many points over which we optimize, and for each point the function may be hard to compute. In our recent publication at AAAI 2017 we show that there is a practical way to determine a point that is likely close to the maximum, and that it is easier than to determine the (exact) quality of a single point. The algorithm employs recent progress in approximative model counting and sampling algorithms using SAT solvers. This represents a fascinating way to merge quantitative and qualitative reasoning.

[FRS2017] Maximum Model Counting
with Daniel Fremont and Sanjit A. Seshia
Accepted at AAAI 2017
[RWKYH14]  Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains
with Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov, and Youssef Hamadi
QEST 2014

Models of Continuous Time, Probabilities, and Nondeterminism

My early research focused on variants of Markov decision processes, which are system models that combine probabilistic and nondeterministic choices. In my Bachelor thesis I studied probabilistic games with partial information, leading to a joint publication with Segio Giro. In my Master thesis I studied fundamental questions on continuous-time Markov decision processes (CTMDPs), such as the existence of optimal strategies, and algorithmic questions including efficient numerical approximation algorithms.

[FRSZ16]  Efficient Approximation of Optimal Control for Continuous-Time Markov Games
with John Fearnley, Sven Schewe, and Lijun Zhang
Information and Computation. 2016.
[RS13] Optimal Time-Abstract Schedulers for CTMDPs and
Continuous-Time Markov Games

with Sven Schewe
Theoretical Computer Science. 2013.
[GR12] Verification of partial-information probabilistic systems using counterexample-guided refinements
with Sergio Giro
ATVA 2012
[FRSZ11]  Efficient Approximation of Optimal Control for Continuous-Time Markov Games
with John Fearnley, Sven Schewe, and Lijun Zhang
[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