[FT17] Bernd Finkbeiner and Hazem Torfah. The Density of Linear-time Properties. ATVA 2017.
[FHST17] Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring Hyperproperties. RV 2017.
[AFFST17] Florian-Michael Adolf, Peter Faymonville, Bernd Finkbeiner, Sebastian Schirmer, and Christoph Torens. Stream Runtime Monitoring on UAS. RV 2017.
[W17b] Alexander Weinert. VLDL Satisfiability and Model Checking via Tree Automata. arXiv.
[FHS17] Bernd Finkbeiner, Christopher Hahn, and Marvin Stenger. EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties. CAV 2017.
[FFT17] Peter Faymonville, Bernd Finkbeiner, Leander Tentrup. BoSy: An Experimentation Framework for Bounded Synthesis. CAV 2017.
[T17] Leander Tentrup. On Expansion and Resolution in CEGAR Based QBF Solving. CAV 2017.
[FGHO17] Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Symbolic vs. Bounded Synthesis for Petri Games. SYNT 2017.
[Z17b] Martin Zimmermann. Finite-state Strategies in Delay Games. arXiv.
[W17] Alexander Weinert. Quantitative Reductions and Infinite Vertex-Ranked Games. arXiv.
[DBBFH17] Pedro R. D’Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, and Holger Hermanns. Is your software on dope? ⋆ Formal analysis of surreptitiously “enhanced” programs. ESOP 2017.
[BHMRZ17] Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann. Bounding Average-energy Games. FoSSaCS 2017.
[FFRT17] Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, Leander Tentrup. Encodings of Bounded Synthesis. TACAS 2017.
[FKPS17] Bernd Finkbeiner, Felix Klein, Ruzica Piskac and Mark Santolucito. Vehicle Platooning Simulations with Functional Reactive Programming. SCAV.
[FZ17a] Peter Faymonville and Martin Zimmermann. Parametric Linear Dynamic Logic. Information and Computation.
[FZ17] Bernd Finkbeiner and Martin Zimmermann. The First-Order Logic of Hyperproperties. STACS 2017.
[TAFS17] Christoph Torens, Florian-Michael Adolf, Peter Faymonville, Sebastian Schirmer. Towards Intelligent System Health Management using Runtime Monitoring. AIAA Information Systems-AIAA Infotech @ Aerospace. Grapevine, Texas.
[Z17] Martin Zimmermann. Games with Costs and Delays. arXiv.

[WZ16b] Alexander Weinert, Martin Zimmermann. Visibly Linear Dynamic Logic. FSTTCS 2016.
[KlZ16a] Felix Klein and Martin Zimmermann. Prompt Delay. FSTTCS 2016.
[PWita16] Peter Wita. Provable State-Space Minimization of Büchi Automata arising from LTL Specifications. Bachelor Thesis.
[SYNTCOMP16] Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Perez, Jean-Francois Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker. The Third Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants and Results. SYNT 2016.
[JB16] Swen Jacobs, Roderick Bloem. The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond. SYNT 2016.
[JKS16] Swen Jacobs, Felix Klein and Sebastian Schirmer. A High-Level LTL Synthesis Format: TLSF v1.1. SYNT 2016.
[Z16] Martin Zimmermann. Delay Games with WMSO+U Winning Conditions. RAIRO – ITA.
[Sch16] Sebastian Schirmer. Runtime Monitoring with Lola. Master Thesis.
[LLZ16] Kim G. Larsen, Simon Laursen, Martin Zimmermann. Limit Your Consumption! Finding Bounds in Average-energy Games. QAPL 2016.
[BHMRZ16] Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann. Bounding Average-energy Games. arXiv.
[FZ16b] Bernd Finkbeiner and Martin Zimmermann. The First-Order Logic of Hyperproperties. arXiv.
[FT16] Bernd Finkbeiner and Hazem Torfah. Synthesizing Skeletons for Reactive Systems. ATVA 2016.
[FSM16] Bernd Finkbeiner, Helmut Seidl, and Christian Müller. Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. ATVA 2016.
[BDFH16] Gilles Barthe, Pedro R. D’Argenio, Bernd Finkbeiner, Holger Hermanns. Facets of Software Doping. ISOLA 2016.
[FO16] Bernd Finkbeiner and Ernst-Rüdiger Olderog. Petri Games: Synthesis of Distributed Systems with Causal Memory. Information and Computation.
[FFST16] Peter Faymonville, Bernd Finkbeiner, Sebastian Schirmer and Hazem Torfah. A Stream-based Specification Language for Network Monitoring. RV 2016.
[JTZ16] Swen Jacobs, Leander Tentrup and Martin Zimmermann. Distributed PROMPT-LTL Synthesis. GandALF 2016.
[TWZ16] Leander Tentrup, Alexander Weinert, Martin Zimmermann. Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time. GandALF 2016.
[WZ16a] Alexander Weinert and Martin Zimmermann. Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. CSL 2016.
[KZ16] Felix Klein and Martin Zimmermann. How Much Lookahead is Needed to Win Infinite Games?. LMCS.
[FH16] Bernd Finkbeiner and Christopher Hahn. Deciding Hyperproperties. CONCUR 2016.
[BBJ16] Roderick Bloem, Nicolas Braud-Santoni, Swen Jacobs. Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems. CAV 2016.
[FK16] Bernd Finkbeiner and Felix Klein. Bounded Cycle Synthesis. CAV 2016.
[Hec16] Jesko Hecking-Harbusch. Equivalence of Petri Games. Master Thesis.
[T16b] Leander Tentrup. Non-prenex QBF Solving Using Abstraction. SAT 2016.
[BJKKRVW16] Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder. Decidability in Parameterized Verification. ACM SIGACT News.
[F16] Bernd Finkbeiner. Synthesis of Reactive Systems. MOD’15.
[T16a] Leander Tentrup. Solving QBF by Abstraction. arXiv:1604.06752.
[WZ16] Alexander Weinert and Martin Zimmermann. Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. arXiv:1604.05543.
[SYNTCOMP14] Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker. The First Reactive Synthesis Competition (SYNTCOMP 2014). STTT.
[KlZ16] Felix Klein and Martin Zimmermann. Prompt Delay. arxiv:1602.05045.
[SYNTCOMP15] Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker. The Second Reactive Synthesis Competition (SYNTCOMP 2015). SYNT 2015.
[AJK16] Simon Außerlechner, Swen Jacobs, Ayrat Khalimov. Tight Cutoffs for Guarded Protocols with Fairness. VMCAI 2016.

[WZ15] Alexander Weinert, Martin Zimmermann. Visibly Linear Dynamic Logic. arXiv:1512.05177.
[HTWZ15] Florian Horn, Wolfgang Thomas, Nico Wallmeier Martin Zimmermann. Optimal Strategy Synthesis for Request-Response Games. RAIRO – ITA.
[TWZ15] Leander Tentrup, Alexander Weinert, Martin Zimmermann. Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time. arXiv:1511.09450.
[RT15] Markus N. Rabe and Leander Tentrup. CAQE: A Certifying QBF Solver. FMCAD 2015.
[LLZ15] Kim G. Larsen, Simon Laursen, Martin Zimmermann. Limit Your Consumption! Finding Bounds in Average-energy Games. arXiv:1510.05774.
[AWWA15] Loris D’Antoni, Matthew Weaver, Alexander Weinert, Rajeev Alur. Automata Tutor and what we learned from building an online teaching tool. BEATCS 117.
[MTHueneberg15] Mark Timon Hüneberg. Optimizing LOLA Specifications. Bachelor Thesis.
[BJKKRVW15] Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures in Distributed Computing Theory.
[Z15c] Martin Zimmermann. Unbounded Lookahead in WMSO+U Games. arXiv:1509.07495.
[JTZ15] Swen Jacobs, Leander Tentrup and Martin Zimmermann. Distributed PROMPT-LTL Synthesis. arXiv:1509.05144.
[Z15b] Martin Zimmermann. Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL. GandALF 2015.
[Gut15] Carolyn Guthoff. Bounded Synthesis of Distributed Architectures. Bachelor Thesis.
[F15] Bernd Finkbeiner. Bounded Synthesis for Petri Games. Correct System Design 2015.
[KlZ15b] Felix Klein and Martin Zimmermann. What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead. CSL 2015.
[W15b] Alexander Weinert. Analyzing Arithmetic Prolog Programs by Symbolic Execution. Master Thesis.
[FT15] Bernd Finkbeiner and Leander Tentrup. Detecting Unrealizability of Distributed Fault-tolerant Systems. LMCS.
[FGO15] Bernd Finkbeiner, Manuel Gieseking, and Ernst-Rüdiger Olderog. ADAM: Causality-Based Synthesis of Distributed Systems. CAV 2015.
[FRS15] Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL*. CAV 2015.
[Z15a] Martin Zimmermann. Delay Games with WMSO+U Winning Conditions. CSR 2015.
[KlZ15a] Felix Klein and Martin Zimmermann. How much lookahead is needed to win infinite games?. ICALP 2015.
[W15a] Alexander Weinert. Problem Generation for DFA Construction. Technical Report UCB/EECS-2015-170.
[Z15] Martin Zimmermann. Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL. arXiv:1505.06953.
[FFRT15] Thomas Bauereiss, Abhishek Bichhawat, Iulia Bolosteanu, Peter Faymonville, Bernd Finkbeiner, Deepak Garg, Richard Gay, Sergey Grebenshchikov, Christian Hammer, Dieter Hutter, Ondřej Kunčar, Peter Lammich, Heiko Mantel, Christian Müller, Andrei Popescu, Markus Rabe, Vineet Rajani, Helmut Seidl, Markus Tasch, Leander Tentrup. Poster: Security in Web-Based Workflows. IEEE S&P 2015.
[Hec15] Jesko Hecking-Harbusch. A Game-Based Semantics for CSP. Bachelor Thesis.
[Hor15] Kai Hornung. Monitoring First-order Parametric Linear-time Temporal Logic. Bachelor Thesis.
[N15] Jennifer Niederländer. Approximate LTL Model Counting. Bachelor Thesis.
[BCJK15] Roderick Bloem, Krishnendu Chatterjee, Swen Jacobs, Robert Könighofer. Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information. TACAS 2015.
[KlZ15] Felix Klein and Martin Zimmermann. What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead. arXiv:1504.02627.

[Z14] Martin Zimmermann. Delay Games with WMSO+U Winning Conditions. arXiv:1412.3978.
[KlZ14] Felix Klein and Martin Zimmermann. How much lookahead is needed to win infinite games?. arXiv:1412.3701.
[TZ14] Hazem Torfah and Martin Zimmermann. The Complexity of Counting Models of Linear-time Temporal Logic. FSTTCS 2014.
[NRZ14] Daniel Neider, Roman Rabinovich, Martin Zimmermann. Down the Borel Hierarchy: Solving Muller Games via Safety Games. TCS.
[FR14] Bernd Finkbeiner, Markus N. Rabe. The Linear-Hyper-Branching Spectrum of Temporal Logics. it.
[FO14] Bernd Finkbeiner, Ernst-Rüdiger Olderog. Petri Games: Synthesis of Distributed Systems with Causal Memory. GandALF 2014.
[FZ14a] Peter Faymonville, Martin Zimmermann. Parametric Linear Dynamic Logic. GandALF 2014.
[RWKYH14] Markus N. Rabe, Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov, and Youssef Hamadi. Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains. QEST 2014.
[TZ14a] Hazem Torfah and Martin Zimmermann. The Complexity of Counting Models of Linear-time Temporal Logic. arXiv:1408.5752.
[FTe14c] Bernd Finkbeiner and Leander Tentrup. Fast DQBF Refutation (full version). AVACS Technical Report No. 97.
[FTe14b] Bernd Finkbeiner and Leander Tentrup. Fast DQBF Refutation. SAT 2014.
[KF14] Andrey Kupriyanov and Bernd Finkbeiner. Causal Termination of Multi-threaded Programs. CAV 2014.
[FZ14] Nathanaël Fijalkow and Martin Zimmermann. Parity and Streett Games with Costs. LMCS.
[HTWZ14] Florian Horn, Wolfgang Thomas, Nico Wallmeier and Martin Zimmermann. Optimal Strategy Synthesis for Request-Response Games. Technical report arXiv:1406.4648.
[DF14] Werner Damm and Bernd Finkbeiner. Automatic Compositional Synthesis of Distributed Systems. FM 2014.
[RLP14] Markus N. Rabe, Peter Lammich, and Andrei Popescu. A shallow embedding of HyperCTL*. AFP.
[CFKMRS14] Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal Logics for Hyperproperties. POST14.
[FTe14] Bernd Finkbeiner and Leander Tentrup. Detecting Unrealizable Specifications of Distributed Systems. TACAS 2014.
[FT14] Bernd Finkbeiner and Hazem Torfah. Counting Models of Linear-time Temporal Logic. LATA 2014.
[CFKMRS14arXiv] Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal Logics for Hyperproperties. arXiv.
[FFP14] Peter Faymonville and Bernd Finkbeiner and Doron Peled. Monitoring Parametric Temporal Logic. VMCAI 2014.

[KSF13] Máté Kovács, Helmut Seidl and Bernd Finkbeiner. Relational Abstract Interpretation for the Verification of 2-Hypersafety Properties. CCS 2013.
[Ehl13] Rüdiger Ehlers. Symmetric and Efficient Synthesis. PhD Thesis.
[FS13] Bernd Finkbeiner and Sven Schewe. Bounded Synthesis. STTT.
[KF13] Andrey Kupriyanov and Bernd Finkbeiner. Causality-Based Verification of Multi-threaded Programs. CONCUR 2013.
[Z13] Martin Zimmermann. Optimal Bounds in Parametric LTL Games. TCS.
[FRS13] Bernd Finkbeiner, Markus N. Rabe, César Sánchez. A Temporal Logic for Hyperproperties. arXiv.
[DF13] Rayna Dimitrova and Bernd Finkbeiner. Lossy Channel Games under Incomplete Information. SR 2013.
[RS13] Markus N. Rabe and Sven Schewe. Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games. TCS.

[FZ12c] Nathanaël Fijalkow and Martin Zimmermann. Cost-Parity and Cost-Streett Games. FSTTCS 2012.
[EKH12] Rüdiger Ehlers, Robert Könighofer, and Georg Hofferek. Symbolically Synthesizing Small Circuits. FMCAD 2012.
[KF12] Lars Kuhtz and Bernd Finkbeiner. Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds. LMCS.
[DFR12] Rayna Dimitrova, Bernd Finkbeiner and Markus N. Rabe. Monitoring Temporal Information Flow. ISoLA 2012.
[GR12] Sergio Giro and Markus N. Rabe. Verification of Partial-Information Probabilistic Systems Using Counterexample-Guided Refinements. ATVA 2012.
[BELM12] Bernd Becker, Rüdiger Ehlers, Matthew Lewis, and Paolo Marin. ALLQBF Solving by Computational Learning. ATVA 2012.
[FZ12d] Nathanaël Fijalkow and Martin Zimmermann. Parity and Streett Games with Costs. Technical report arXiv:1207.0663.
[DF12] Rayna Dimitrova and Bernd Finkbeiner. Counterexample-guided Synthesis of Observation Predicates. FORMATS 2012.
[PF12] Hans-Jörg Peter and Bernd Finkbeiner. The Complexity of Bounded Synthesis for Timed Control with Partial Observability. FORMATS 2012.
[NRZ12] Daniel Neider, Roman Rabinovich, Martin Zimmermann. Down the Borel Hierarchy: Solving Muller Games via Safety Games. GandALF 2012.
[FZ12b] Wladimir Fridman and Martin Zimmermann. Playing Pushdown Parity Games in a Hurry. GandALF 2012.
[Ehl12b] Rüdiger Ehlers. ACTL ∩ LTL Synthesis. CAV 2012.
[EM12] Rüdiger Ehlers and Daniela Moldovan. Sparse Positional Strategies for Safety Games. SYNT 2012.
[GEFP12] Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner, and Hans-Jörg Peter. FlexRay for Avionics: Automatic Verification with Parametric Physical Layers. I@A 2012.
[GEFP12a] Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner, and Hans-Jörg Peter. Automatic Protocol Verification with Parametric Physical Layers. AVACS Technical Report No. 86.
[FZ12a] John Fearnley and Martin Zimmermann. Playing Muller Games in a Hurry. IJFCS.
[FP12] Bernd Finkbeiner and Hans-Jörg Peter. Template-based Controller Synthesis for Timed Systems. TACAS 2012.
[Ehl12a] Rüdiger Ehlers. Symbolic Bounded Synthesis. FMSD. Extended journal version of [Ehl10c].
[FJ12] Bernd Finkbeiner and Swen Jacobs. Lazy Synthesis. VMCAI 2012.
[DFKRS12] Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe, and Helmut Seidl. Model Checking Information Flow in Reactive Systems. VMCAI 2012. RS3 Best Paper Award 2011/2012.
[Z12] Martin Zimmermann. Solving Infinite Games with Bounds. RWTH Aachen University. PhD Thesis.

[FRSZ11] John Fearnley, Markus N. Rabe, Sven Schewe and Lijun Zhang. Efficient Approximation of Optimal Control for Continuous-Time Markov Games. FSTTCS 2011.
[EF11b] Rüdiger Ehlers and Bernd Finkbeiner. Monitoring Realizability. RV 2011.
[KF11b] Lars Kuhtz and Bernd Finkbeiner. Weak Kripke Structures and LTL. CONCUR 2011.
[FLZ11] Wladimir Fridman and Christof Löding, and Martin Zimmermann. Degrees of Lookahead in Context-free Infinite Games. CSL 2011.
[Ehl11d] Rüdiger Ehlers. Small witnesses, accepting lassos and winning strategies in omega-automata and games. AVACS Technical Report No. 80, SFB/TR 14 AVACS, also appeared as arXiv/CoRR: 1108.0315.
[RS11] Markus N. Rabe and Sven Schewe. Finite Optimal Control for Time-bounded Reachability in CTMDPs and Continuous-time Markov Games. Acta Informatica.
[PEM11] Hans-Jörg Peter, Rüdiger Ehlers, and Robert Mattmüller. Synthia: Verification and Synthesis for Timed Automata. CAV 2011.
[NRZ11] Daniel Neider and Rabinovich, Roman and Martin Zimmermann. Solving Muller Games via Safety Games. Technical Report AIB-2011-14, RWTH Aachen University.
[Z11] Martin Zimmermann. Optimal Bounds in Parametric LTL Games. GandALF 2011.
[DF11] Werner Damm and Bernd Finkbeiner. Does It Pay to Extend the Perimeter of a World Model?. FM 2011.
[EF11] Rüdiger Ehlers and Bernd Finkbeiner. Reactive Safety. GandALF 2011.
[Ehl11c] Rüdiger Ehlers. Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis. NFM 2011.
[Ehl11b] Rüdiger Ehlers. Unbeast: Symbolic Bounded Synthesis. TACAS 2011.
[Ehl11a] Rüdiger Ehlers. Experimental Aspects of Synthesis. iWIGP 2011.

[K10] Lars Kuhtz. Model Checking Finite Paths and Trees. PhD Thesis.
[FLZ10] Wladimir Fridman and Christof Löding, and Martin Zimmermann. Degrees of Lookahead in Context-free Infinite Games. Technical Report AIB-2010-20, RWTH Aachen University.
[EFGP10] Rüdiger Ehlers, Daniel Fass, Michael Gerke, and Hans-Jörg Peter. Fully Symbolic Timed Model Checking using Constraint Matrix Diagrams. RTSS 2010.
[Ger10] Michael Gerke. Zone State Diagrams. Master Thesis.
[EGP10] Rüdiger Ehlers, Michael Gerke, and Hans-Jörg Peter. Making the Right Cut in Model Checking Data-Intensive Timed Systems. ICFEM 2010.
[RSZ10] Markus N. Rabe, Sven Schewe, and Lijun Zhang. Efficient Approximation of Optimal Control for Markov Games – early arXiv version. arXiv/CoRR: 1011.0397.
[EF10] Rüdiger Ehlers and Bernd Finkbeiner. On the Virtue of Patience: Minimizing Büchi Automata. SPIN 2010.
[GEFP10] Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner, and Hans-Jörg Peter. Model Checking the FlexRay Physical Layer Protocol. FMICS 2010.
[EMP10] Rüdiger Ehlers, Robert Mattmüller, and Hans-Jörg Peter. Combining Symbolic Representations for Solving Timed Games. FORMATS 2010.
[FS10] Bernd Finkbeiner and Sven Schewe. Coordination Logic. CSL 2010.
[Ehl10d] Rüdiger Ehlers. Minimising Deterministic Büchi Automata Precisely using SAT Solving. SAT 2010.
[Ehl10c] Rüdiger Ehlers. Symbolic Bounded Synthesis. CAV 2010.
[FPS10] Bernd Finkbeiner, Hans-Jörg Peter, and Sven Schewe. Synthesising Certificates in Networks of Timed Automata. IET SEN 2010.
[RS10a] Markus N. Rabe, and Sven Schewe. Optimal Time-Abstract Schedulers for CTMDPs and Markov Games. QAPL, 2010.
[Z10] Martin Zimmermann. Parametric LTL Games. Technical Report AIB-2010-11, RWTH Aachen University.
[Ehl10b] Rüdiger Ehlers. Short Witnesses and Accepting Lassos in omega-automata. LATA 2010.
[RS10b] Markus N. Rabe, and Sven Schewe. Finite Optimal Control for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games. arXiv/CoRR: 1004.4005.
[DKFW10] Klaus Dräger, Andrey Kupriyanov, Bernd Finkbeiner, and Heike Wehrheim. SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. TACAS 2010.
[Ehl10a] Rüdiger Ehlers. Generalised Rabin(1) synthesis. arXiv/CoRR: 1003.1684.
[FZ10] John Fearnley and Martin Zimmermann. Playing Muller Games in a Hurry. GandALF 2010.

[PM09] Hans-Jörg Peter and Robert Mattmüller. Component-based Abstraction Refinement for Timed Controller Synthesis. RTSS 2009.
[DF09] Rayna Dimitrova and Bernd Finkbeiner. Synthesis of Fault-Tolerant Distributed Systems. ATVA 2009.
[Abel09] Andreas Abel. From Uppaal to Slab. Bachelor Thesis.
[KF09] Lars Kuhtz and Bernd Finkbeiner. LTL Path Checking is Efficiently Parallelizable. ICALP 2009. Best paper award.
[Z09c] Martin Zimmermann. Time-optimal Winning Strategies for Poset Games. CIAA 2009.
[FK09] Bernd Finkbeiner and Lars Kuhtz. Monitor Circuits for LTL with Bounded and Unbounded Future. RV 2009.
[Fas09] Daniel Fass. Clock Matrix Diagrams. Bachelor Thesis.
[Had09] Walid Haddad. Verifying Networks of Phase Event Automata. Master Thesis.
[Dah09] Daniel Dahrendorf. Symbolic Encodings of Timed Games with Incomplete Information. Master Thesis.
[Z09b] Martin Zimmermann. Time-optimal Winning Strategies for Poset Games. Technical Report AIB-2009-13, RWTH Aachen University.
[Z09a] Martin Zimmermann. Time-optimal Winning Strategies in Infinite Games. RWTH Aachen University. Diploma Thesis.

[BDFW08] Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Slicing Abstractions. FI 2008.
[DF08] Rayna Dimitrova and Bernd Finkbeiner. Abstraction Refinement for Games with Incomplete Information. FSTTCS 08.
[FPS08b] Bernd Finkbeiner, Hans-Jörg Peter, and Sven Schewe. Synthesizing Certificates in Networks of Timed Automata. RTSS 2008.
[DFP08] Klaus Dräger, Bernd Finkbeiner, and Andreas Podelski. Directed Model Checking with Distance-preserving Abstractions. STTT 2008.
[DF08b] Klaus Dräger and Bernd Finkbeiner. Subsequence Invariants. AVACS Technical Report 42.
[DF08a] Klaus Dräger and Bernd Finkbeiner. Subsequence Invariants. CONCUR 2008.
[FPS08a] Bernd Finkbeiner, Hans-Jörg Peter, and Sven Schewe. RESY: Requirement Synthesis for Compositional Model Checking. TACAS 2008.
[S08c] Sven Schewe. Synthesis of Distributed Systems. PhD Thesis.
[S08b] Sven Schewe. An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games. CSL 2008.
[DP08] Rayna Dimitrova and Andreas Podelski. Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?. VMCAI 2008.
[S08a] Sven Schewe. ATL* Satisfiability is 2EXPTIME-complete. ICALP 2008.

[E07] Franziska Ebert. Translation Validation for Optimizing Compilers. Universität des Saarlandes. Diploma Thesis.
[FGP08] Bernd Finkbeiner, Yuri Gurevich, and Alexander K. Petrenko (editors). Proceedings of the Fourth Workshop on Model Based Testing.
[FGP07] Bernd Finkbeiner, Yuri Gurevich, and Alexander K. Petrenko (editors). Proceedings of the Third Workshop on Model Based Testing.
[KDHFDPB07] Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, and Gerd Behrmann. UPPAAL/DMC – Abstraction-based Heuristics for Directed Model Checking. TACAS 2007.
[S07] Sven Schewe. Solving Parity Games in Big Steps. FSTTCS 2007.
[FS07] Bernd Finkbeiner and Sven Schewe. SMT-Based Synthesis of Distributed Systems. AFM 2007.
[SF07c] Sven Schewe and Bernd Finkbeiner. Distributed Synthesis for Alternating-Time Logics. ATVA 2007.
[BDFW07] Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Slicing Abstractions. FSEN 2007. Best paper award.
[SF07b] Sven Schewe and Bernd Finkbeiner. Bounded Synthesis. ATVA 2007.
[SF07a] Sven Schewe and Bernd Finkbeiner. Semi-Automatic Distributed Synthesis. International Journal of Foundations of Computer Science.
[Bri07] Dominik Brill. Deductive Model Checking with Transition Constraint Systems. Diploma Thesis.
[Had07] Walid Haddad. Inequality Constraints on Synchronization Counters. Bachelor Thesis.

[FGP06] Bernd Finkbeiner, Yuri Gurevich, and Alexander K. Petrenko (editors). Proceedings of the Second Workshop on Model Based Testing.
[S06] Sven Schewe. Synthesis for Probabilistic Environments. ATVA 2006.
[CK06] Amin Coja-Oghlan and Lars Kuhtz. An improved algorithm for approximating the chromatic number of Gn,p. Information Processing Letters, volume 99, issue 6, 30 September 2006, pages 234-238.
[HMS06] Malte Helmert, Robert Mattmüller, and Sven Schewe. Selective Approaches for Solving Weak Games. ATVA 2006.
[FSB06] Bernd Finkbeiner, Sven Schewe and Matthias Brill. Automatic Synthesis of Assumptions for Compositional Model Checking. FORTE 2006.
[SF06b] Sven Schewe and Bernd Finkbeiner. Satisfiability and Finite Model Property for the Alternating-Time µ-Calculus. CSL 2006.
[CZ06] Domenico Cantone and Calogero G. Zarba. A decision procedure for monotone functions over bounded and complete lattices. TARSKI 2006.
[KMZ06] Deepak Kapur, Rupak Majumdar, and Calogero G. Zarba. Interpolation for data structures. FSE 2006.
[RZ06] Silvio Ranise and Calogero G. Zarba. A theory of singly-linked lists and its extensible decision procedure. SEFM 2006.
[SF06a] Sven Schewe and Bernd Finkbeiner. Synthesis of Asynchronous Systems. LOPSTR 2006.
[DFP06] Klaus Dräger, Bernd Finkbeiner, and Andreas Podelski. Directed Model Checking with Distance-Preserving Abstractions. SPIN 2006.
[BFGS06] Howard Barringer, Bernd Finkbeiner, Yuri Gurevich, and Henny Sipma (editors). Proceedings of the Fifth Workshop on Runtime Verification.
[Fie06] Arnaud Fietzke. Learning Minimal Requirements for Compositional Verification. Bachelor Thesis.
[Bue06] Sven Bünte. Automatic Abstraction of Synchronization Sequences. Bachelor Thesis.

[Pet05] Hans-Jörg Peter. Controller Program Synthesis for Industrial Machines. Diploma Thesis.
[Reg05] Jens Regenberg. Synthesis of Reactive Systems. Diploma Thesis.
[Mau05] Tobias Maurer. Distributed Games For Reactive Systems. Diploma Thesis.
[E05] Pavel Emeliyanenko. Automatic Verification of Conditions for Absence of Interrupts. Universität des Saarlandes. Bachelor Thesis.
[M05] Ghulam Mujtaba. Monitoring Execution Traces using Metric Alternating Automata. Universität des Saarlandes. Diploma Thesis.
[FS05b] Bernd Finkbeiner and Sven Schewe. Semi-Automatic Distributed Synthesis. ATVA 2005.
[FS05a] Bernd Finkbeiner and Sven Schewe. Uniform Distributed Synthesis. LICS 2005.
[DSS+05] Ben d’Angelo, Sriram Sankaranarayanan, Cesar Sanchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, Zohar Manna. LOLA: Runtime Monitoring of Synchronous Systems. TIME 2005.
[FSS05] Bernd Finkbeiner, Sriram Sankaranarayanan and Henny Sipma. Collecting Statistics over Runtime Executions. FMSD 2005. Journal version of [FSS02].

[K04b] Lars Kuhtz. Colouring Gn,p and Spectral Techniques. Humboldt Universität zu Berlin. Diploma Thesis.
[FS04] Bernd Finkbeiner and Henny Sipma. Checking Finite Traces using Alternating Automata. FMSD 2004. Journal version of [FS01].
[CJ04] J. Creci and L. Pottier. Gb: une procédure de décision pour le système Coq. JFLA 2004.

[FSS02] Bernd Finkbeiner, Sriram Sankaranarayanan and Henny Sipma. Collecting Statistics over Runtime Executions. RV 2002.

[FK01] Bernd Finkbeiner and Ingolf Krüger. Using Message Sequence Charts for Component-Based Formal Verification. SAVCBS 2001.
[FS01] Bernd Finkbeiner and Henny Sipma. Checking Finite Traces using Alternating Automata. RV 2001.
[F01] Bernd Finkbeiner. Language Containment Checking with Nondeterministic BDDs. TACAS 2001.

[BFMS00] Anca Browne, Bernd Finkbeiner, Zohar Manna and Henny Sipma. The `Cash-Point Service’: A Verification Case Study Using STeP. FAC 2000.
[BBC+00] Nikolaj S. Bjørner, Anca Browne, Michael A. Colón, Bernd Finkbeiner, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. FMSD 2000.

[MBB+99] Zohar Manna, Nikolaj S. Bjørner, Anca Browne, Michael A. Colón, Bernd Finkbeiner, Mark Pichora, Henny B. Sipma and Tomás E. Uribe. An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. TOOLS 1999.

[MCF+98] Zohar Manna, Michael A. Colón, Bernd Finkbeiner, Henny B. Sipma and Tomás E. Uribe. Abstraction and Modular Verification of Infinite-State Reactive Systems. RTSE 1998.
[FMS98] Bernd Finkbeiner, Zohar Manna and Henny B. Sipma. Deductive Verification of Modular Systems. COMPOS 1997.