Markus N. Rabe

Markus N. Rabe

Contact

Markus N. Rabe

eMail: rabe at berkeley.edu
Office: 545S, Cory Hall

I am a Postdoc at UC Berkeley working with Sanjit Seshia on the specification, verification, and synthesis of systems. The goal is to automate the construction of correct and secure systems through a new generation of automated reasoning techniques.

Main Publications

[RS16] Incremental Determinization
with Sanjit Seshia.
SAT, 2016.
Implementation: CADET
[FRS2017]  Maximum Model Counting
with Daniel Fremont and Sanjit A. Seshia
AAAI 2017
Implementation
[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

A complete list of publications can be found on dblp and Google Scholar.

Research summaries

Reasoning in Quantified Logics

Many of the challenging problems in computer science can be formulated as a quantified logical problem. Algorithms in this area will hence impact a broad range of applications. For example, quantified reasoning will enable the automatic synthesis of programs from abstract, declarative specifications, which will allow programmers to focus on the "what" instead of the "how". Thereby, we will be able to improve the safety and security of the systems we build and change how we approach computer programming.

Our recent work on quantified Boolean formulas (QBF) introduced a new algorithmic principle for reasoning in quantified logics [RS16], which helped to solve several benchmark problems from verification and synthesis for the first time. Besides providing an effective solution method for many quantified problems, our algorithm is able to provide proofs for its results - and its proofs are order of magnitude smaller than those of earlier algorithms.

My QBF solver CADET was awarded the second place in the 2QBF track of QBFEVAL'17. Check it out!

In an earlier line of work, Leander Tentrup and I created the QBF solver CAQE, which implements a variant of the counter-example guided abstraction refinement (CEGAR) algorithm [RT15]. It won the first place in the main track of QBFEVAL'17.

[R17] A Resolution-style Proof System for DQBF
SAT, 2017.
Errata
[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
[RT15] CAQE: A Certifying QBF Solver
with Leander Tentrup.
FMCAD 2015.
Implementation

Specification Languages for Security

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.
Implementation
[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
Implementation
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.)

Reasoning about Quantities

How to estimate the maximum of a function with less computation than it takes to evaluate the function at any single point? In our recent publication [FRS17] we present a probabilistic approximation optimization that estimates the maximum of arbitrary functions in the (very general) complexity class #P. The algorithm requires only polynomially many calls to an NP oracle and is thus much faster than to exactly evaluate the function to optimize at any single point. For this result, we extended ideas from approximate sampling that go back to Stockmeyer and Jerrum, Valiant, and Vazirani. For the implementation and our experiments, we exploiting recent progress in practical algorithms for approximative model counting and sampling algorithms using SAT solvers. This represents a fascinating way to merge quantitative and qualitative reasoning.

[FRS17] 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
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