| [BF24d] |
Raven Beutner, Bernd Finkbeiner. Checking Satisfiability of Hyperproperties using First-Order Logic. ATVA 2024. |
| [CNFW24] |
Arthur Correnson, Tobias Niessen, Bernd Finkbeiner, Georg Weissenbacher. Finding ∀∃ Hyperbugs using Symbolic Execution. OOPSLA 2024. |
| [BFKS24] |
Jan Baumeister, Bernd Finkbeiner, Florian Kohn, Frederik Scheerer. A Tutorial on Stream-Based Monitoring. FM 2024. |
| [BFG24] |
Raven Beutner, Bernd Finkbeiner, Angelina Göbl. Visualizing Game-Based Certificates for Hyperproperty Verification. FM 2024. Distinguished Paper. |
| [FMM24] |
Bernd Finkbeiner, Niklas Metzger, and Yoram Moses. Information Flow Guided Synthesis with Unbounded Communication. CAV 2024. |
| [BHBF24] |
Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner. Syntax-Guided Automated Program Repair for Hyperproperties. CAV 2024. |
| [BFKLMST24] |
Jan Baumeister, Bernd Finkbeiner, Florian Kohn, Florian Löhr, Guido Manfredi, Sebastian Schirmer, Christoph Torens. Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-Learned. CAV 2024. |
| [FFMS24f] |
Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger, and Julian Siber. Synthesis of Temporal Causality. CAV 2024. |
| [BF24c] |
Raven Beutner, Bernd Finkbeiner. Non-Deterministic Planning for Hyperproperty Verification. ICAPS 2024. |
| [SSJDFS24a] |
Sebastian Schirmer, Jasdeep Singh, Emily Jensen, Johann Dauer, Bernd Finkbeiner, Sriram Sankaranarayanan. Temporal Behavior Trees: Robustness and Segmentation. HSCC 2024. |
| [SSJDFS24b] |
Sebastian Schirmer, Jasdeep Singh, Emily Jensen, Johann Dauer, Bernd Finkbeiner, Sriram Sankaranarayanan. Temporal Behavior Trees — Segmentation. HSCC 2024. |
| [BF24b] |
Raven Beutner, Bernd Finkbeiner. Hyper Strategy Logic. AAMAS 2024. |
| [BFFM24] |
Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger. Monitoring Second-Order Hyperproperties. AAMAS 2024. |
| [CHOS24] |
Matthias Cosler, Christopher Hahn, Ayham Omar, Frederik Schmitt. NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis. TACAS 2024. |
| [B24] |
Raven Beutner. Automated Software Verification of Hyperliveness. TACAS 2024. |
| [BF24a] |
Raven Beutner, Bernd Finkbeiner. On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing. AAAI 2024. |
| [Ghanem24] |
Mohamed Ghanem. NeuRes: A Neural Resolution Prover of Unsatisfiability. Master Thesis. |
| [JFLA24] |
Arthur Correnson. À la recherche de tous les vrais bugs. JFLA 2024. |
| [Correnson24] |
Arthur Correnson. Formal Verification of Symbolic Bug Finders. Master Thesis. |
| [TNSDBKFML24] |
Christoph Torens, Pranav Nagarajan, Sebastian Schirmer, Johann Dauer, Jan Baumeister, Florian Kohn, Bernd Finkbeiner, Guido Manfredi, Florian Löhr. Certification Aspects of Runtime Assurance for Urban Air Mobility. SCITECH 2024. |
| [CS23] |
Arthur Correnson, Dominic Steinhoefel. Engineering a Formally Verified Automated Bug Finder. ESEC/FSE 2023. FSE Best Artifact Award. |
| [BFFS23] |
Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Julian Siber. Checking and Sketching Causes on Temporal Sequences. ATVA 2023. |
| [FKS23] |
Bernd Finkbeiner, Florian Kohn, and Malte Schledjewski. Leveraging Static Analysis: An IDE for RTLola. ATVA 2023. |
| [FHKP23] |
Bernd Finkbeiner, Jana Hofmann, Florian Kohn, and Noemi Passing. Reactive Synthesis of Smart Contract Control Flows. ATVA 2023. |
| [FO23] |
Bernd Finkbeiner and Ernst-Rüdiger Olderog. Concurrent Hyperproperties. Theories of Programming and Formal Methods 2023. |
| [BFFM23] |
Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger. Second-Order Hyperproperties. CAV 2023. |
| [CHMST23] |
Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, Caroline Trippel. nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models. CAV 2023. |
| [CFHT23] |
Norine Coenen, Bernd Finkbeiner, Jana Hofmann, Julia Tillman. Smart Contract Synthesis Modulo Hyperproperties. CSF 2023. CSF Distinguished Paper Award 2023. |
| [BF23c] |
Raven Beutner, Bernd Finkbeiner. Model Checking Omega-Regular Hyperproperties with AutoHyperQ. LPAR 2023. |
| [FS23] |
Bernd Finkbeiner and Julian Siber. Counterfactuals Modulo Temporal Logics. LPAR 2023. |
| [BF23b] |
Raven Beutner, Bernd Finkbeiner. HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems. LMCS 2023. |
| [FFHL23] |
Bernd Finkbeiner, Hadar Frenkel, Jana Hofmann, Janine Lohse. Automata-Based Software Model Checking of Hyperproperties. NFM 2023. |
| [CSHF23] |
Matthias Cosler, Frederik Schmitt, Christopher Hahn, Bernd Finkbeiner. Iterative Circuit Repair Against Formal Specifications. ICLR 2023. |
| [F23] |
Bernd Finkbeiner. Logics and Algorithms for Hyperproperties. ACM SIGLOG News 2023. |
| [BF23a] |
Raven Beutner, Bernd Finkbeiner. AutoHyper: Explicit-State Model Checking for HyperLTL. TACAS 2023. SCP Best Paper Award. |
| [FFZ23] |
Dana Fisman, Hadar Frenkel and Sandra Zilles. Inferring Symbolic Automata. LMCS. |
| [BDFRST23] |
Jan Baumeister, Johann C. Dauer, Bernd Finkbeiner, Kristin Y. Rozier, Sebastian Schirmer, and Christoph Torens. A Hierarchy of Monitoring Properties for Autonomous Systems. SciTech. |
| [FGRS22] |
Hadar Frenkel, Orna Grumberg, Bat-Chen Rothenberg and Sarai Sheinvald. Automated Program Repair Using Formal Verification Techniques. Principles of Systems Design Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. |
| [FP22b] |
Bernd Finkbeiner, Noemi Passing. Synthesizing Dominant Strategies for Liveness. FSTTCS 2022. |
| [CFF+22] |
Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Niklas Metzger, and Julian Siber. Temporal Causality in Reactive Systems. ATVA 2022. |
| [FGPS22] |
Hadar Frenkel, Orna Grumberg, Corina Pasareanu and Sarai Sheinvald. Assume, Guarantee or Repair – a Regular Framework for non-Regular Properties. STTT. |
| [BFGS22] |
Jan Baumeister, Bernd Finkbeiner, Stefan Gumhold, and Malte Schledjewski.. Real-time Visualization of Stream-based Monitoring Data.. RV 2022. |
| [FS22] |
Hadar Frenkel and Sarai Sheinvald. Realizable and Context-Free Hyperlanguages. GandALF 2022. |
| [Cosler22] |
Matthias Cosler. Repairing Circuits with Transformers. Master Thesis. |
| [FMM22] |
Bernd Finkbeiner, Niklas Metzger, and Yoram Moses. Information Flow Guided Synthesis. CAV 2022. |
| [CDF+22] |
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger, and Julian Siber. Explaining Hyperproperty Violations. CAV 2022. |
| [BF22b] |
Raven Beutner, Bernd Finkbeiner. Software Verification of Hyperproperties Beyond k-Safety. CAV 2022. CAV Distinguished Paper Award 2022. |
| [BF22a] |
Raven Beutner, Bernd Finkbeiner. Prophecy Variables for Hyperproperty Verification. CSF 2022. |
| [BCFHK22] |
Raven Beutner, David Carral, Bernd Finkbeiner, Jana Hofmann, Markus Krötzsch. Deciding Hyperproperties Combined with Functional Specifications. LICS 2022. |
| [BDFS22] |
Jan Baumeister, Johann C. Dauer, Bernd Finkbeiner, Sebastian Schirmer.. Monitoring with Verified Guarantees. STTT22. |
| [FGP22] |
Bernd Finkbeiner, Gideon Geier, Noemi Passing. Specification decomposition for reactive synthesis. ISSE 2022. |
| [BOZ22] |
Raven Beutner, C.H. Luke Ong, Fabian Zaiser. Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming. PLDI 2022. |
| [CFPS22] |
Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, Mark Santolucito. Can reactive synthesis and syntax-guided synthesis be friends?. PLDI 2022. |
| [FBies22] |
Florian Bies. Complete Bounded Model Checking for Hyperproperties. Bachelor Thesis. |
| [FMPSS22] |
Bernd Finkbeiner, Kaushik Mallik, Noemi Passing, Malte Schledjewski, Anne-Kathrin Schmuck. BOCoSy: Small but Powerful Symbolic Output-Feedback Control. HSCC 2022. |
| [Omar22] |
Ayham Omar. Predicting Timed Traces With Neural Networks. Bachelor Thesis. |
| [FFKK22] |
Bernd Finkbeiner, Martin Fränzle, Florian Kohn, Paul Kröger. A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation. Algorithms 2022. |
| [FP22a] |
Bernd Finkbeiner, Noemi Passing. Compositional synthesis of modular systems. ISSE 2022. |
| [FKM22] |
Bernd Finkbeiner, Felix Klein, Niklas Metzger. Live synthesis. ISSE 2022. |
| [FHP22] |
Bernd Finkbeiner, Philippe Heim, Noemi Passing. Temporal Stream Logic modulo Theories. FoSSaCS 2022. |
| [FGHO22] |
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog. Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory. CSL 2022. |
| [FFZ22] |
Dana Fisman, Hadar Frenkel and Sandra Zilles. Inferring Symbolic Automata. CSL 2022. |
| [Kreber22] |
Jens Kreber. Generating and Solving Temporal Logic Problems with Adversarial Transformers. Master Thesis. |
| [GDG+22] |
Mohamed Ghanem, Fadi Dawoud, Habiba Gamal, Eslam Soliman, Hossam Sharara, Tamer El-Batt. FLoBC: A Decentralized Blockchain-Based Federated Learning Framework. BCCA 2022. |
| [Linn22] |
Jonas Linn. Refinement of TSL Specifications for LTL Synthesis. Bachelor Thesis. |
| [Lohse22] |
Janine Lohse. Model Checking Temporal Stream Logic and Hyper-Temporal Stream Logic. Bachelor Thesis. |
| [Aumann22] |
Jan-Robin Aumann. Modularization of code in RTLola. Bachelor Thesis. |
| [Hec21] |
Jesko Hecking-Harbusch. Synthesis of Asynchronous Distributed Systems from Global Specifications. PhD Thesis. |
| [VHFKY21] |
Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, Fan Yang. Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity. FSTTCS 2021. |
| [SHRF21] |
Frederik Schmitt, Christopher Hahn, Markus N. Rabe, Bernd Finkbeiner. Neural Circuit Synthesis from Specification Patterns. NeurIPS 2021. |
| [HCM+21] |
Tom Horak, Norine Coenen, Niklas Metzger, Christopher Hahn, Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd Finkbeiner, Raimund Dachselt. Visual Analysis of Hyperproperties for Understanding Model Checking Results. VIS 2021. |
| [CFHHS21] |
Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Yannick Schillo. Runtime Enforcement of Hyperproperties. ATVA 2021. |
| [FKM21] |
Bernd Finkbeiner, Felix Klein, Niklas Metzger. Live Synthesis. ATVA 2021. |
| [FP21] |
Bernd Finkbeiner, Noemi Passing. Compositional Synthesis of Modular Systems. ATVA 2021. |
| [DFS21] |
Johann C. Dauer, Bernd Finkbeiner, and Sebastian Schirmer. Monitoring with Verified Guarantees. RV 2021. |
| [SHKRF21] |
Frederik Schmitt, Christopher Hahn, Jens U. Kreber, Markus N. Rabe, Bernd Finkbeiner. Deep Learning for Temporal Logics. AITP 2021. Extended Abstract. |
| [BF21] |
Raven Beutner, Bernd Finkbeiner. A Temporal Logic for Strategic Hyperproperties. CONCUR 2021. |
| [BCFFJS21] |
Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch, Julian Siber. Causality-Based Game Solving. CAV 2021. Watch the 5 minute presentation and the 25 minute presentation. |
| [BCBFS21] |
Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and Cesar Sanchez. A Temporal Logic for Asynchronous Hyperproperties. CAV 2021. Watch the 5 minute presentation and the 25 minute presentation. |
| [BO21] |
Raven Beutner, Luke Ong. On Probabilistic Termination of Functional Programs with Continuous Distributions. PLDI 2021. |
| [FGP21] |
Bernd Finkbeiner, Gideon Geier, Noemi Passing. Specification Decomposition for Reactive Synthesis. NFM 2021. |
| [BFKOPS21] |
Jan Baumeister, Bernd Finkbeiner, Matthis Kruse, Stefan Oswald, Noemi Passing, Maximilian Schwenger. Automatic Optimizations for Runtime Verification Specifications. MT-CPS 2021. |
| [FKSS21] |
Bernd Finkbeiner, Andreas Keller, Jessica Schmidt, Maximilian Schwenger. Robust Monitoring for Medical Cyber-Physical Systems. MedCPS 2021. |
| [HSKRF21] |
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, Bernd Finkbeiner. Teaching Temporal Logics to Neural Networks. ICLR 2021. |
| [BFHKSS21] |
Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian A. Köhl, Yannik Schnitzer, Maximilian Schwenger. RTLola on Board: Testing Real Driving Emissions on your Phone. TACAS 2021. |
| [GHY21] |
Manuel Gieseking, Jesko Hecking-Harbusch, Ann Yanich. A Web Interface for Petri Nets with Transits and Petri Games. TACAS 2021. |
| [Siber21] |
Julian Siber. Causal Solving of Reachability Games. Master Thesis. |
| [Ger21] |
Michael Gerke. Modeling and Verifying the FlexRay Physical Layer Protocol with Reachability Checking of Timed Automata. PhD Thesis. |
| [JSchmidt21] |
Jessica Aline Schmidt. Robust Monitoring of Medical Cyber-Physical Systems. Bachelor Thesis. |
| [F21] |
Bernd Finkbeiner. Model Checking Algorithms for Hyperproperties. VMCAI 2021. |
| [Laichner21] |
Julia Laichner. Timing is Key – A WCET Analysis of RTLola. Bachelor Thesis. |
| [Scheerer21] |
Frederik Scheerer. Monitoring Smart Contracts with RTLola. Bachelor Thesis. |
| [Engel21] |
Simon Engel. Bounded Model Checking for PHL. Bachelor Thesis. |
| [DFT20] |
Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah. Probabilistic Hyperproperties of Markov Decision Processes. ATVA 2020. |
| [BFT20] |
Tom Baumeister, Bernd Finkbeiner, Hazem Torfah. Explainable Reactive Synthesis. ATVA 2020. |
| [FGHO20b] |
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog. Model Checking Branching Properties on Petri Nets with Transits. ATVA 2020. |
| [FP20] |
Bernd Finkbeiner, Noemi Passing. Dependency-based Compositional Synthesis. ATVA 2020. |
| [BFKS20] |
Jan Baumeister, Bernd Finkbeiner, Matthis Kruse, Maximilian Schwenger. Automatic Optimizations for Stream-based Monitoring Languages. RV 2020. |
| [FOPS20] |
Bernd Finkbeiner, Stefan Oswald, Noemi Passing, Maximilian Schwenger. Verified Rust Monitors for Lola Specifications. RV 2020. |
| [Schwenger20] |
Maximilian Schwenger. Monitoring Cyber-Physical Systems: From Design to Integration. RV 2020. |
| [Kle20] |
Felix Klein. Synthesizing Stream Control. PhD Thesis. |
| [CFHH20] |
Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann. The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective. KR 2020. |
| [BF20] |
Borzoo Bonakdarpour, Bernd Finkbeiner. Controller Synthesis for Hyperproperties. CSF 2020. |
| [HSKRF20] |
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, Bernd Finkbeiner. Transformers Generalize to the Semantics of Logics. arxiv preprint. |
| [BFSST20] |
Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer, Maximilian Schwenger, Christoph Torens. RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft. CAV 2020. |
| [FGHO20a] |
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog. AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL. CAV 2020. |
| [FHHT20] |
Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, Leander Tentrup. Realizing Omega-regular Hyperproperties. CAV 2020. |
| [FGPS20] |
Hadar Frenkel, Orna Grumberg, Corina Pasareanu and Sarai Sheinvald. Assume, Guarantee or Repair. TACAS 2020. |
| [FSS20] |
Bernd Finkbeiner, Jessica Schmidt, Maximilian Schwenger. Simplex Architecture Meets RTLola. MT-CPS 2020. |
| [MNSTWZ20] |
Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada, Alexander Weinert, Martin Zimmermann. From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics. HSCC 2020. |
| [CGerstacker20] |
Carsten Gerstacker. Specification-Aided Trajectory Prediction with RNNs. Master Thesis. |
| [FHST20] |
Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, Leander Tentrup. Efficient monitoring of hyperproperties using prefix trees. STTT 2020. |
| [SOswald20] |
Stefan Oswald. Verifiable Runtime Monitor Generation for Lola Specifications. Bachelor Thesis. |
| [Baumeister20] |
Jan Baumeister. Tracing Correctness: A Practical Approach to Traceable Runtime Monitoring. Master Thesis. |
| [SMF20] |
Helmut Seidl, Christian Müller, Bernd Finkbeiner. How to Win First-Order Safety Games. VMCAI 2020. |
| [Tillman20] |
Julia Tillman. Temporal Stream Logic for Hyperproperties. Bachelor Thesis. |
| [Tor19] |
Hazem Torfah. Model Counting for Reactive Systems. PhD Thesis. |
| [Ten19] |
Leander Tentrup. Symbolic Reactive Synthesis. PhD Thesis. |
| [FHLST19] |
Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, Leander Tentrup. Synthesis from Hyperproperties. Acta Informatica. |
| [T19] |
Hazem Torfah. Stream-based Monitors for Real-time Properties. RV 2019 @ FM’19. |
| [BF19] |
Borzoo Bonakdarpour, Bernd Finkbeiner. Program Repair for Hyperproperties. ATVA 2019. |
| [HM19] |
Jesko Hecking-Harbusch, Niklas Metzger. Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems. ATVA 2019. |
| [FGHO19] |
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog. Model Checking Data Flows in Concurrent Network Updates. ATVA 2019. |
| [DFT19b] |
Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah. Approximate Automata for Omega-regular Languages. ATVA 2019. |
| [GHKF19] |
Gideon Geier, Philippe Heim, Felix Klein, Bernd Finkbeiner. Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications. FMCAD 2019. |
| [BFST19b] |
Jan Baumeister, Bernd Finkbeiner, Maximilian Schwenger, Hazem Torfah. On the Similarities of Aircraft and Humans: Monitoring CPS with StreamLAB. CyberCardia 2019. |
| [BFST19a] |
Jan Baumeister, Bernd Finkbeiner, Maximilian Schwenger, Hazem Torfah. FPGA Stream-Monitoring of Real-time Properties. EMSOFT 2019. |
| [H19] |
Christopher Hahn. Algorithms for Monitoring Hyperproperties. RV 2019 @ FM’19. |
| [Kohn19] |
Florian Kohn. A Stream-based Approach to Network Intrusion Detection. Bachelor Thesis. |
| [Coenen19] |
Norine Coenen. Verifying Hyperliveness. Master Thesis. |
| [Schwenger19] |
Maximilian Schwenger. Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS. Master Thesis. |
| [Bungert19] |
Paul Bungert. Monitoring Hybrid Automata. Bachelor Thesis. |
| [Cosler19] |
Matthias Cosler. Towards Synthesizing Smart Contracts: Reducing ATL* Synthesis to HyperLTL Synthesis. Bachelor Thesis. |
| [BFH19] |
Raven Beutner, Bernd Finkbeiner, Jesko Hecking-Harbusch. Translating Asynchronous Games for Distributed Synthesis. CONCUR 2019. |
| [FKPS19b] |
Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito. Synthesizing Functional Reactive Programs. Haskell 2019. |
| [Beutner19] |
Raven Beutner. Translating Asynchronous Games for Distributed Synthesis. Bachelor Thesis. |
| [CFST19] |
Norine Coenen, Bernd Finkbeiner, Cesar Sanchez, Leander Tentrup. Verifying Hyperliveness. CAV 2019. |
| [DFT19] |
Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah. Synthesizing Approximate Implementations for Unrealizable Specifications. CAV 2019. |
| [FKPS19a] |
Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito. Temporal Stream Logic: Synthesis beyond the Bools. CAV 2019. |
| [FFS+19b] |
Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger, Leander Tentrup, Hazem Torfah. StreamLAB: Stream-based Monitoring of Cyber-physical Systems. CAV 2019. |
| [Leidinger19] |
Hendrik Leidinger. Learning Desired Behavior for Causality Analysis. Master Thesis. |
| [TR19] |
Leander Tentrup, Markus N. Rabe. Clausal Abstraction for DQBF. SAT 2019. |
| [FHST19] |
Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, Leander Tentrup. Monitoring Hyperproperties. FMSD. Extended journal version of [FHST17]. |
| [FHT19] |
Bernd Finkbeiner, Lennart Haas, Hazem Torfah. Canonical Representations of k-Safety Hyperproperties. CSF 2019. |
| [CFHH19] |
Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann. The Hierarchy of Hyperlogics. LICS 2019. |
| [Fay19] |
Peter Faymonville. Monitoring with Parameters. PhD Thesis. |
| [TR19a] |
Leander Tentrup, Markus N. Rabe. Clausal Abstraction for DQBF. arXiv. |
| [FFS+19a] |
Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Leander Tentrup, Hazem Torfah. Real-time Stream Monitoring with StreamLAB. MT-CPS 2019. |
| [Wei19] |
Alexander Weinert. Optimality and Resilience in Parity Games. PhD Thesis. |
| [HST19] |
Christopher Hahn, Marvin Stenger, Leander Tentrup. Constraint-based Monitoring of Hyperproperties. TACAS 2019. |
| [Siber19] |
Julian Siber. Causality-Based Model Checking for Real-Time Systems. Bachelor Thesis. |
| [Rosenhauer19] |
Christoph Rosenhauer. Compiling Lola 2.0 to C. Bachelor Thesis. |
| [Schmitt19] |
Sanny Schmitt. Generating Concurrency-preserving Petri Games. Bachelor Thesis. |
| [WZ18] |
Alexander Weinert, Martin Zimmermann. Visibly Linear Dynamic Logic. TCS 747. |
| [FGS19] |
Hadar Frenkel, Orna Grumberg and Sarai Sheinvald. An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains. Journal of Automated Reasoning (2019). NFM 2017 special issue. |
| [FKG18] |
Bernd Finkbeiner, Felix Klein, Carsten Gerstacker. Bounded Synthesis of Reactive Programs. ATVA 2018. |
| [JS18b] |
Swen Jacobs, Mouhammad Sakr. A Symbolic Algorithm for Lazy Synthesis of Eager Strategies. ATVA 2018. |
| [FHH18] |
Bernd Finkbeiner, Christopher Hahn, Tobias Hans. MGHyper: Checking Satisfiability of HyperLTL formulas beyond the ∃*∀* Fragment. ATVA 2018. |
| [Hofmann18] |
Marvin Hofmann. Runtime Verification of Critical Web-based Systems with Lola. Bachelor Thesis. |
| [JTZ18] |
Swen Jacobs, Leander Tentrup, Martin Zimmermann. Distributed Synthesis for Parameterized Temporal Logics. Information and Computation. |
| [W18] |
Alexander Weinert. Quantitative Reductions and Infinite Vertex-Ranked Games. GandALF 2018. |
| [Wita18] |
Peter Wita. Bounded Synthesis for Past LTL. Master Thesis. |
| [HT18] |
Jesko Hecking-Harbusch, Leander Tentrup. Solving QBF by Abstraction. GandALF 2018. |
| [HMMZ18b] |
Matthew Hague, Roland Meyer, Sebastian Muskalla, Martin Zimmermann. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. MFCS 2018. |
| [KMVZ18] |
Andreas Krebs, Arne Meier, Jonni Virtema, Martin Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. MFCS 2018. |
| [SWZ18b] |
Sven Schewe, Alexander Weinert, Martin Zimmermann. Parity Games with Weights. CSL 2018. |
| [NWZ18b] |
Daniel Neider, Alexander Weinert, Martin Zimmermann. Synthesizing Optimally Resilient Controllers. CSL 2018. |
| [NWZ18] |
Daniel Neider, Alexander Weinert, Martin Zimmermann. Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free. arXiv. |
| [FHLST18] |
Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, Leander Tentrup. Synthesizing Reactive Systems from Hyperproperties. CAV 2018. |
| [RTRS18] |
Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia. Understanding and Extending Incremental Determinization for 2QBF. CAV 2018. |
| [FHT18] |
Bernd Finkbeiner, Christopher Hahn, Hazem Torfah. Model Checking Quantitative Hyperproperties. CAV 2018. |
| [BF18] |
Borzoo Bonakdarpour, Bernd Finkbeiner. The Complexity of Monitoring Hyperproperties. CSF 2018. |
| [Heinen18] |
Jens Heinen. Model Checking Timed Hyperproperties. Master Thesis. |
| [HMMZ18] |
Matthew Hague, Roland Meyer, Sebastian Muskalla, Martin Zimmermann. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. arXiv. |
| [KGT18] |
Hadas Kress-Gazit, Hazem Torfah. The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems. CREST 2018. |
| [SWZ18] |
Sven Schewe, Alexander Weinert, Martin Zimmermann. Parity Games with Weights. arXiv. |
| [Z18] |
Martin Zimmermann. Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL. Acta Informatica. |
| [TZ18] |
Hazem Torfah and Martin Zimmermann. The Complexity of Counting Models of Linear-time Temporal Logic. Acta Informatica. |
| [FHST18] |
Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, Leander Tentrup. RVHyper: A Runtime Verification Tool for Temporal Hyperproperties. TACAS 2018. |
| [Hans18] |
Tobias Hans. MGHyper: Checking Satisfiability of HyperLTL Formulas beyond the ∃*∀*-Fragment. Bachelor Thesis. |
| [Lukert18] |
Philip Lukert. HyperLTL Synthesis. Bachelor Thesis. |
| [JS18a] |
Swen Jacobs, Mouhammad Sakr. Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity. VMCAI 2018. |
| [SYNT17] |
Dana Fisman and Swen Jacobs (editors). Proceedings of the Sixth Workshop on Synthesis. SYNT 2017. |
| [SYNTCOMP17] |
Swen Jacobs, Nicolas Basset, Roderick Bloem, Romain Brenguier, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Thibaud Michaud, Guillermo A. Perez, Jean-Francois Raskin, Ocan Sankur, Leander Tentrup. The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants and Results. SYNT 2017. |
| [CGerstacker17] |
Carsten Gerstacker. Bounded Synthesis of Reactive Programs. Bachelor Thesis. |
| [MKoehl17] |
Maximilian Köhl. From Knowledge- to Belief-Based Programming for Mobile Ad-Hoc Networks. Bachelor Thesis. |
| [FMSZ17] |
Bernd Finkbeiner, Christian Müller, Helmut Seidl and Eugen Zălinescu. Verifying Security Policies in Multi-agent Workflows with Loops. CCS 2017. RS3 Best Paper Award 2016/2017. |
| [Baumeister17] |
Jan Baumeister. Encodings of Bounded Synthesis of Distributed Systems. Bachelor Thesis. |
| [Met17] |
Niklas Metzger. Bounded Synthesis of Petri Games with True Concurrency Firing Semantics. Bachelor Thesis. |
| [FKl17] |
Bernd Finkbeiner and Felix Klein. Reactive Synthesis: Towards Output-Sensitive Algorithms. IOS Press. |
| [EF17] |
Ruediger Ehlers and Bernd Finkbeiner. Symmetric Synthesis. FSTTCS 2017. |
| [W17c] |
Alexander Weinert. VLDL Satisfiability and Model Checking via Tree Automata. FSTTCS 2017. |
| [FG17] |
Bernd Finkbeiner and Paul Gölz. Synthesis in Distributed Environments. FSTTCS 2017. |
| [FKu17] |
Bernd Finkbeiner and Andrey Kupriyanov. Causality-based Model Checking. CREST 2017. |
| [FT17] |
Bernd Finkbeiner and Hazem Torfah. The Density of Linear-time Properties. ATVA 2017. |
| [F17] |
Bernd Finkbeiner. Temporal Hyperproperties. Bulletin of EATCS. |
| [Z17c] |
Martin Zimmermann. Finite-state Strategies in Delay Games. GandALF 2017. |
| [WZ17] |
Alexander Weinert and Martin Zimmermann. Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. LMCS. |
| [DWZ17] |
Daniel Neider, Alexander Weinert, Martin Zimmermann. Synthesizing Optimally Resilient Controllers. arXiv. |
| [FHST17] |
Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring Hyperproperties. RV 2017. Extended journal version available at [FHST19]. |
| [AFFST17] |
Florian-Michael Adolf, Peter Faymonville, Bernd Finkbeiner, Sebastian Schirmer, and Christoph Torens. Stream Runtime Monitoring on UAS. RV 2017. |
| [Z17d] |
Martin Zimmermann. Games with Costs and Delays. LICS 2017. |
| [Hahn17] |
Christopher Hahn. Satisfiability and Monitoring of Hyperproperties. Master Thesis. |
| [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. |
| [KMVZ17] |
Andreas Krebs, Arne Meier, Jonni Virtema, Martin Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. arXiv. |
| [JTZ17] |
Swen Jacobs, Leander Tentrup, Martin Zimmermann. Distributed Synthesis for Parameterized Temporal Logics. arXiv. |
| [Z17b] |
Sarah Winter and 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. |
| [FGS17] |
Hadar Frenkel, Orna Grumberg and Sarai Sheinvald. An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data. NFM 2017. |
| [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. |
| [Kup16] |
Andrey Kupriyanov. Causality-based Verification. PhD Thesis. |
| [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. |
| [DFR16] |
Werner Damm, Bernd Finkbeiner, Astrid Rakow. What You Really Need To Know About Your Neighbor. SYNT 2016. |
| [FK16] |
Bernd Finkbeiner and Felix Klein. Bounded Cycle Synthesis. CAV 2016. |
| [Hec16] |
Jesko Hecking-Harbusch. Equivalence of Petri Games. Master Thesis. |
| [T16] |
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. IOS Press. |
| [WZ16] |
Alexander Weinert and Martin Zimmermann. Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. arXiv:1604.05543. |
| [Rab16] |
Markus N. Rabe. A Temporal Logic Approach to Information-flow Control. PhD Thesis. |
| [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. |
| [Coenen16] |
Norine Coenen. A Proof System for HyperLTL. Bachelor Thesis. |
| [Hahn16] |
Christopher Hahn. Deciding HyperLTL. Bachelor Thesis. |
| [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. |
| [Dim14] |
Rayna Dimitrova. Synthesis and Control of Infinite-State Systems with Partial Observability. PhD Thesis. |
| [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. |
| [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, Bernd Finkbeiner, and Doron Peled. Monitoring Parametric Temporal Logic. VMCAI 2014. |
| [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. |
| [Dra11] |
Klaus Dräger. Subsequence Invariants. PhD Thesis. |
| [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. |
| [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. |
