Leander Tentrup

Contact

Leander Tentrup

Reactive Systems Group
Universität des Saarlandes
eMail: tentrup at cs.uni-saarland.de

About me

I was a Ph.D. student in the Reactive Systems Group at the Computer Science Department at Saarland University.
I defended my thesis Symbolic Reactive Synthesis in November 2019.
My solvers won the reactive synthesis competition and the Competitive evaluation of QBF solvers.

Publications

[CFST19]

Verifying Hyperliveness

Norine Coenen, Bernd Finkbeiner, Cesar Sanchez, Leander Tentrup
31st International Conference on Computer-Aided Verification (CAV 2019).

[FFS+19b]

StreamLAB: Stream-based Monitoring of Cyber-physical Systems

Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger, Leander Tentrup, Hazem Torfah
31st International Conference on Computer-Aided Verification (CAV 2019).

[TR19]

Clausal Abstraction for DQBF

Leander Tentrup, Markus N. Rabe
22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019).

[FHST19]

Monitoring Hyperproperties

Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, Leander Tentrup
Formal Methods in System Design (FMSD).

[TR19a]

Clausal Abstraction for DQBF (full version)

Leander Tentrup, Markus N. Rabe
Full version of SAT 2019 paper

[HST19]

Constraint-based Monitoring of Hyperproperties

Christopher Hahn, Marvin Stenger, Leander Tentrup
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019).

[JTZ18]

Distributed synthesis for parameterized temporal logics

Swen Jacobs, Leander Tentrup, Martin Zimmermann
Information and Computation, Volume 262, Part 2

[HT18]

Solving QBF by Abstraction

Jesko Hecking-Harbusch, Leander Tentrup
9th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2018)
Implementation

[FHLST18]

Synthesizing Reactive Systems from Hyperproperties

Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, Leander Tentrup
30th International Conference on Computer Aided Verification (CAV 2018)

[RTRS18]

Understanding and Extending Incremental Determinization for 2QBF

Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia
30th International Conference on Computer Aided Verification (CAV 2018)

[FHST18]

RVHyper: A Runtime Verification Tool for Temporal Hyperproperties

Bernd Finkbeiner, Christopher Hahn, Marvin Stenger and Leander Tentrup
24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)

[FHST17]

Monitoring Hyperproperties

Bernd Finkbeiner, Christopher Hahn, Marvin Stenger and Leander Tentrup
17th International Conference on Runtime Verification (RV 2017)

[T17]

On Expansion and Resolution in CEGAR Based QBF Solving

Leander Tentrup
29th International Conference on Computer Aided Verification (CAV 2017)
Implementation

[FFT17]

BoSy: An Experimentation Framework for Bounded Synthesis

Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup
29th International Conference on Computer Aided Verification (CAV 2017)
Implementation

[FFRT17]

Encodings of Bounded Synthesis

Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup
23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017)
Implementation

[JTZ16]

Distributed PROMPT-LTL Synthesis

Swen Jacobs, Leander Tentrup, and Martin Zimmermann
7th International Symposium on Games, Automata, and Formal Verification (GandALF 2016)

[TWZ16]

Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time

Leander Tentrup, Alexander Weinert, and Martin Zimmermann
7th International Symposium on Games, Automata, and Formal Verification (GandALF 2016)

[T16]

Non-prenex QBF Solving Using Abstraction

Leander Tentrup
19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016)
Implementation

[RT15]

CAQE: A Certifying QBF Solver

Markus N. Rabe and Leander Tentrup
15th International Conference on Formal Methods in Computer-aided Design (FMCAD 2015)
Implementation

[FT15]

Detecting Unrealizability of Distributed Fault-tolerant Systems

Bernd Finkbeiner and Leander Tentrup
LMCS Special Issue.

[FTe14c]

Fast DQBF Refutation (full version)

Bernd Finkbeiner and Leander Tentrup
AVACS Technical Report No. 97.

[FTe14b]

Fast DQBF Refutation

Bernd Finkbeiner and Leander Tentrup
17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014).

[FTe14]

Detecting Unrealizable Specifications of Distributed Systems

Bernd Finkbeiner and Leander Tentrup
20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014).

Tools

bunsat is a DQBF solver based on the bounded unsatisfiability method.
realizer is a simple safety game solver.
CAQE is a certifying solver for quantified Boolean formulas (QBF) based on the CEGAR-based clausal abstraction algorithm.
QuAbS is a certifying solver for quantified Boolean formulas (QBF) based on a CEGAR-based abstraction algorithm.
SafetySynth is a synthesis tool for safety specifications.
BoSy is a synthesis tool based on symbolic encodings of bounded synthesis.

Teaching

Winter 2018/19	Seminar Advisor for Hyperproperties.
Summer 2018	Tutor for Embedded Systems.
Summer 2018	Seminar Advisor for Formal Verification of Security Protocols.
Winter 2016/17	Tutor for Verification.
Summer 2016	Tutor for Embedded Systems.
Summer 2015	Assistant for Recursion Theory.
Summer 2014	Assistant for Embedded Systems.
Summer 2014	Seminar Advisor for Advanced Topics in Infinite Games
Winter 2013/14	Proseminar Advisor Time Machine.
Summer 2013	Assistant for Verification.
Summer 2012	Student Teaching Assistant for Concurrent Programming at the Dependable Systems Chair.
Winter 2011/12	Student Teaching Assistant for Basics of Algorithms and Data Structures at the MPI Informatik.
Summer 2011	Student Teaching Assistant for Programming 2 at the Compiler Design Lab.
Winter 2010/11	Student Teaching Assistant for Programming 1 at the Programming Systems Lab.
Winter 2010/11	Student Teaching Assistant for System Architecture at the Institute for Computer Architecture and Parallel Computing Lab.