| 2025 | CADE | More is Less: Adding Polynomials for Faster Explanations in NLSAT. | Valentin Promies, Jasper Nalbach, Erika brahm, Paul Wagner |
| 2025 | CAV | Efficient Probabilistic Model Checking for Relational Reachability. | Lina Gerlach, Tobias Winkler, Erika brahm, Borzoo Bonakdarpour, Sebastian Junges |
| 2025 | IJCAI | Counterfactual Strategies for Markov Decision Processes. | Paul Kobialka, Lina Gerlach, Francesco Leofante, Erika brahm, Silvia Lizeth Tapia Tarifa, Einar Broch Johnsen |
| 2025 | SYNASC | Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks. | Jonas Stbbe, Anne Remke, Erika brahm |
| 2024 | CASC | Merging Adjacent Cells During Single Cell Construction. | Jasper Nalbach, Erika brahm |
| 2024 | FM | A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic. | Valentin Promies, Erika brahm |
| 2024 | SYNASC | On Projective Delineability. | Lucas Michel, Jasper Nalbach, Pierre Mathonet, Nam Znadi, Christopher W. Brown, Erika brahm, James H. Davenport, Matthew England |
| 2023 | IFM | SMT: Something You Must Try. | Erika brahm, Jzsef Kovcs, Anne Remke |
| 2023 | TASE | Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks. | Joanna Delicaris, Stefan Schupp, Erika brahm, Anne Remke |
| 2022 | IFM | HyperPCTL Model Checking by Probabilistic Decomposition. | Eshita Zaman, Gianfranco Ciardo, Erika brahm, Borzoo Bonakdarpour |
| 2021 | FM | HyperProb: A Model Checker for Probabilistic Hyperproperties. | Oyendrila Dobe, Erika brahm, Ezio Bartocci, Borzoo Bonakdarpour |
| 2021 | ISSAC | Extending the Fundamental Theorem of Linear Programming for Strict Inequalities. | Jasper Nalbach, Erika brahm, Gereon Kremer |
| 2021 | MEMOCODE | Controller verification meets controller code: a case study. | Felix Freiberger, Stefan Schupp, Holger Hermanns, Erika brahm |
| 2021 | SYNASC | On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving. | Gereon Kremer, Erika brahm, Matthew England, James H. Davenport |
| 2020 | ATMOS | Probabilistic Simulation of a Railway Timetable. | Rebecca Haehn, Erika brahm, Nils Nieen |
| 2020 | ATVA | Probabilistic Hyperproperties with Nondeterminism. | Erika brahm, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe |
| 2020 | CADE | New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract). | Erika brahm, James H. Davenport, Matthew England, Gereon Kremer, Zak Tonks |
| 2020 | IJCAI | Optimal Planning Modulo Theories. | Francesco Leofante, Enrico Giunchiglia, Erika brahm, Armando Tacchella |
| 2020 | LPAR | Parameter Synthesis for Probabilistic Hyperproperties. | Erika brahm, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe |
| 2019 | ECMS | Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems. | Francesco Leofante, Stefan Schupp, Erika brahm, Armando Tacchella |
| 2019 | FMICS | Multiple Analyses, Requirements Once: - Simplifying Testing and Verification in Automotive Model-Based Development. | Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika brahm, Md Tawhid Bin Waez, Thomas Rambow |
| 2018 | FM | Verifying Auto-generated C Code from Simulink - An Experience Report in the Automotive Domain. | Philipp Berger, Joost-Pieter Katoen, Erika brahm, Md Tawhid Bin Waez, Thomas Rambow |
| 2018 | FM | Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations. | Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika brahm, Joost-Pieter Katoen |
| 2018 | IRI | Context-Dependent Reachability Analysis for Hybrid Systems. | Stefan Schupp, Justin Winkens, Erika brahm |
| 2018 | IFM | Task Planning with OMT: An Application to Production Logistics. | Francesco Leofante, Erika brahm, Armando Tacchella |
| 2018 | SEFM | Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems. | Stefan Schupp, Erika brahm |
| 2018 | TACAS | Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis. | Stefan Schupp, Erika brahm |
| 2017 | CADE | SC-square: when Satisfiability Checking and Symbolic Computation join forces. | Erika brahm, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler |
| 2017 | IRI | On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories. | Francesco Leofante, Erika brahm, Tim Niemueller, Gerhard Lakemeyer, Armando Tacchella |
| 2017 | ISSAC | Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. | Erika brahm, Jasper Nalbach, Gereon Kremer |
| 2017 | ISSAC | Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. | Tarik Viehmann, Gereon Kremer, Erika brahm |
| 2017 | SYNASC | SMT Solving for Arithmetic Theories: Theory and Tool Support. | Erika brahm, Gereon Kremer |
| 2016 | CASC | A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic. | Gereon Kremer, Florian Corzilius, Erika brahm |
| 2016 | ISoLA | Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots. | Francesco Leofante, Simone Vuotto, Erika brahm, Armando Tacchella, Nils Jansen |
| 2016 | SEFM | Satisfiability Checking: Theory and Applications. | Erika brahm, Gereon Kremer |
| 2016 | SETTA | Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies. | Erika brahm, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro |
| 2016 | SYNASC | Symbolic Computation Techniques in Satisfiability Checking. | Erika brahm |
| 2015 | CAV | PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. | Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, Erika brahm |
| 2015 | FM | Counterexamples for Expected Rewards. | Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika brahm, Joost-Pieter Katoen, Bernd Becker |
| 2015 | ISSAC | Building Bridges between Symbolic Computation and Satisfiability Checking. | Erika brahm |
| 2015 | SAT | SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. | Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika brahm |
| 2014 | ATVA | Fast Debugging of PRISM Models. | Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika brahm, Joost-Pieter Katoen |
| 2014 | FMCAD | Under-approximate flowpipes for non-linear continuous systems. | Xin Chen, Sriram Sankaranarayanan, Erika brahm |
| 2014 | IRI | A CEGAR approach for the reachability analysis of PLC-controlled chemical plants. | Johanna Nellen, Erika brahm |
| 2013 | CADE | A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition. | Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika brahm, Bernd Becker |
| 2013 | CALCO | A Timed CTL Model Checker for Real-Time Maude. | Daniela Lepri, Erika brahm, Peter Csaba lveczky |
| 2013 | CAV | Flow*: An Analyzer for Non-linear Hybrid Systems. | Xin Chen, Erika brahm, Sriram Sankaranarayanan |
| 2013 | ICCAD | From statistical model checking to statistical model inference: characterizing the effect of process variations in analog circuits. | Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi, Xin Chen, Erika brahm |
| 2012 | ATVA | The COMICS Tool - Computing Minimal Counterexamples for DTMCs. | Nils Jansen, Erika brahm, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker |
| 2012 | RTSS | Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. | Xin Chen, Erika brahm, Sriram Sankaranarayanan |
| 2012 | SAT | SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox - (Tool Presentation). | Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika brahm |
| 2012 | TACAS | Minimal Critical Subsystems for Discrete-Time Markov Models. | Ralf Wimmer, Nils Jansen, Erika brahm, Bernd Becker, Joost-Pieter Katoen |
| 2011 | ATVA | Hierarchical Counterexamples for Discrete-Time Markov Chains. | Nils Jansen, Erika brahm, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker |
| 2011 | FCT | Virtual Substitution for SMT-Solving. | Florian Corzilius, Erika brahm |
| 2011 | FORTE | Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking. | Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika brahm |
| 2011 | SEFM | Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude. | Muhammad Fadlisyah, Peter Csaba lveczky, Erika brahm |
| 2009 | PDPTA | Picoso - A Parallel Interval Constraint Solver. | Natalia Kalinnik, Tobias Schubert, Erika brahm, Ralf Wimmer, Bernd Becker |
| 2007 | DDECS | On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata. | Marc Herbstritt, Bernd Becker, Erika brahm, Christian Herde |
| 2006 | CiE | Heap-Abstraction for an Object-Oriented Calculus with Thread Classes. | Erika brahm, Andreas Grner, Martin Steffen |
| 2006 | FMICS | Parallel SAT Solving in Bounded Model Checking. | Erika brahm, Tobias Schubert, Bernd Becker, Martin Frnzle, Christian Herde |
| 2005 | VMCAI | Optimizing Bounded Model Checking for Linear Hybrid Systems. | Erika brahm, Bernd Becker, Felix Klaedtke, Martin Steffen |
| 2004 | ICTAC | Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes. | Erika brahm, Marcello M. Bonsangue, Frank S. de Boer, Martin Steffen |