Publications | Theory of Hybrid Systems

0
[bibtex]	Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer. Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings, Journal of Logical and Algebraic Methods in Programming .
2019
[bibtex]	Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development, 24th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019), Volume 11687 of LNCS, pages 59-75, Springer, 2019.
[bibtex]	Jasper Nalbach, Gereon Kremer, Erika Ábrahám. On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract), 4th Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 7 pages, RWTH Aachen, 2019.
[bibtex]	Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the Proof Complexity of MCSAT, 4th Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 10 pages, RWTH Aachen, 2019.
[bibtex]	Francesco Leofante, Stefan Schupp, Erika Ábrahám, Armando Tacchella. Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems, 33rd International ECMS Conference on Modelling and Simulation (ECMS 2019), 7 pages, European Council for Modelling and Simulation, 2019.
[bibtex]	Stefan Schupp. State set representations and their usage in the reachability analysis of hybrid systems, PhD Thesis, RWTH Aachen University, 217 pages, 2019.
[bibtex]	Gereon Lukas Kremer, Erika Ábrahám. Fully Incremental Cylindrical Algebraic Decomposition, Journal of symbolic computation ??, pages S0747717119300847, 2019.
2018
[bibtex]	Erika Ábrahám, Silvia Lizeth Taipa Tarifa. Proceedings of the PhD Symposium at iFM'18 on Formal Methods, Volume 483 of Research report / University of Oslo, 2018.
[bibtex]	Francesco Leofante, Erika Ábrahám, Armando Tacchella. Task Planning with OMT: An Application to Production Logistics, 14th International Conference on Integrated Formal Methods (IFM 2018), Volume 11023 of Programming and Software Engineering, pages 316-325, Springer, 2018.
[bibtex]	Stefan Schupp, Erika Ábrahám. The HyDRA Tool : A Playground for the Development of Hybrid Systems Reachability Analysis Methods, PhD Symposium at iFM’18 on Formal Methods (PhD-iFM’18), Volume 483 of Research report, 2 pages, Oslo University, 2018.
[bibtex]	Erika Ábrahám, Borzoo Bonakdarpour. HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties, 15th International Conference on Quantitative Evaluation of Systems (QEST 2018), LNCS, Springer, 2018.
[bibtex]	Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Ábrahám, Joost-Pieter Katoen. Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations, 22nd International Symposium on Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.
[bibtex]	Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain, 22nd International Symposium of Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.
[bibtex]	Erika Ábrahám. Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics, Federated Logic Conference (FloC 2018), Volume 10900 of LNCS, pages XII-XII, Springer, 2018.
[bibtex]	Rebecca Haehn, Gereon Kremer, Erika Ábrahám. Evaluation of Equational Constraints for CAD in SMT Solving, 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference (SC-Square 2018), Volume 2189 of CEUR Workshop Proceedings, pages 19-32, RWTH Aachen, 2018.
[bibtex]	Stefan Schupp, Justin Winkens, Erika Ábrahám. Context-Dependent Reachability Analysis for Hybrid Systems, 2018 IEEE International Conference on Information Reuse and Integration for Data Science (IRI 2018), pages 518-525, IEEE, 2018.
[bibtex]	Stefan Schupp, Erika Ábrahám. Spread the Work : Multi-threaded Safety Analysis for Hybrid Systems, 16th International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, pages 89-104, Springer, 2018.
[bibtex]	Erika Ábrahám, Elisabetta Di Nitto, Raffaela Mirandola. 2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering (GE 2018), IEEE, 2018.
[bibtex]	Stefan Schupp, Erika Ábrahám. Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806, Part 2 of LNCS, pages 287-302, Springer, 2018.
[bibtex]	Francesco Leofante, Erika Ábrahám, Tim Dieter Niemüller, Gerhard Lakemeyer, Armando Tacchella. Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics, Information systems frontiers 21 (1), pages 87-107, 2018.
[bibtex]	Niloofar Safiran. Differentiation of numerical simulations with embedded nonlinear systems and integrals, PhD Thesis, RWTH Aachen University, 163 pages, 2018.
[bibtex]	Gereon Kremer, Erika Ábrahám. Modular strategic SMT solving with SMT-RAT, Acta Universitatis Sapientiae / Informatica 10 (1), pages 5-25, 2018.
[bibtex]	Ulrich Loup. On solving real-algebraic formulas in a satisfiability-modulo-theories framework, PhD Thesis, RWTH Aachen University, 222 pages, 2018.
2017
[bibtex]	Erika Ábrahám, Gereon Lukas Kremer. SMT Solving for Arithmetic Theories: Theory and Tool Support, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), pages 1-8, IEEE, 2017.
[bibtex]	Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler. SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions (ARCADE 2017), Volume 51 of EPiC Series in Computing, pages 6-10, EasyChair, 2017.
[bibtex]	Francesco Leofante, Erika Ábrahám, Tim Dieter Niemüller, Gerhard Lakemeyer, Armando Tacchella. On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories, 2017 IEEE International Conference on Information Reuse and Integration (IRI) (IRI 2017), pages 403-410, IEEE, 2017.
[bibtex]	Erika Ábrahám, Jasper Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework, 2nd International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 12 pages, RWTH Aachen, 2017.
[bibtex]	Tarik Viehmann, Gereon Kremer, Erika Ábrahám. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving, 2nd International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 15 pages, RWTH Aachen, 2017.
[bibtex]	Erika Ábrahám. Techniques and Tools for Hybrid Systems Reachability Analysis, The 10th International Workshop on Numerical Software Verification (NSV 2017), Volume 10381 of LNCS, pages XVI-XVII, Springer, 2017.
[bibtex]	Tim Dieter Niemüller, Gerhard Lakemeyer, Francesco Leofante, Erika Ábrahám. Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization, 5th Workshop on Planning and Robotics (PlanRob 2017), pages 60-67, 2017.
[bibtex]	Stefan Schupp, Erika Ábrahám, Ibtissem Ben Makhlouf, Stefan Kowalewski. HyPro : A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis, NASA Formal Methods (NFM) Symposium (NFM 2017), Volume 10227 of LNCS, pages 288-294, Springer, 2017.
[bibtex]	Stefan Schupp, Johanna Nellen, Erika Ábrahám. Divide and Conquer : Variable Set Separation in Hybrid Systems Reachability Analysis, 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2017), Volume 250 of EPTCS, pages 1-14, [Open Publishing Association], 2017.
[bibtex]	Erika Ábrahám, Sergiy Bogomolov. Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, Volume 247 of EPTCS, , [Open Publishing Association], 2017.
[bibtex]	Erika Ábrahám, Sergiy Bogomolov. Preface, 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), Volume 247 of EPTCS, [Open Publishing Association], 2017.
[bibtex]	Erika Ábrahám, Sergiy Bogomolov. Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017, [Open Publishing Association], 2017. arXiv:1704.02421
[bibtex]	Erika Ábrahám, Hadas Kress-Gazit, Lorenzo Natale, Armando Tacchella. Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071), Dagstuhl Reports 7 (2), pages 48-63, 2017.
[bibtex]	Christian Meirich. Berechnung und Bewertung der Gesamtleistungsfähigkeit von Eisenbahnnetzen, PhD Thesis, Rheinisch-Westfälische Technische Hochschule Aachen, 221 pages, 2017.
2016
[bibtex]	Erika Ábrahám, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro. Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies, International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016), Volume 9984 of LNCS, pages 229-245, Springer, 2016.
[bibtex]	Francesco Leofante, Simone Vuotto, Erika Ábrahám, Armando Tacchella, Nils Jansen. Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), Volume 9952 of LNCS, pages 496-514, Springer, 2016.
[bibtex]	Pascal Richter, David Laukamp, Levin Gerdes, Martin Frank, Erika Ábrahám. Heliostat Field Layout Optimization with Evolutionary Algorithms, 2nd GlobalConference on Artifcial Intelligence (GCAI 2016), Volume 41 of EPiC Series in Computing, pages 240-252, [Cool Press Ltd], 2016.
2017
[bibtex]	Erika Ábrahám, James H. Davenport, Pascal Fontaine. Bridging two communities to solve real problems (SC2 2016), Volume 1804 of CEUR workshop proceedings, , RWTH Aachen, 2017.
2016
[bibtex]	Erika Ábrahám. Symbolic Computation Techniques in Satisfiability Checking, 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pages 3-10, IEEE, 2016.
[bibtex]	Gereon Kremer, Florian Corzilius, Erika Ábrahám. A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic, International Workshop on Computer Algebra in Scientific Computing (CASC16), Volume 9890 of LNCS, pages 315-335, Springer, 2016.
2015
[bibtex]	Erika Ábrahám, Costas Bekas, Ivona Brandic, Samir Genaim, Einar Broch Johnsen, Ivan Kondov, Sabri Pllana, Achim Streit. Challenges and Recommendations for Preparing HPC Applications for Exascale, 2015. arXiv:1503.06974
2016
[bibtex]	Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. SC2 : Satisfiability Checking Meets Symbolic Computation, 9th International Conference on Intelligent Computer Mathematics (CICM 2016), Volume 9791 of LNCS, pages 28-43, Springer, 2016.
[bibtex]	Erika Ábrahám, Gereon Kremer. Satisfiability Checking : Theory and Applications, Software Engineering and Formal Methods : 14th International Conference (SEFM 2016), Volume 9763 of LNCS, pages 9-23, Springer, 2016.
[bibtex]	Erika Ábrahám, Marieke Huisman. Integrated formal methods : 12th international conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016 : proceedings, Volume 9681 of LNCS, pages XIV, 538 Seiten : Illustrationen, Diagramme, Springer, 2016.
[bibtex]	Erika Ábrahám, Sergiy Bogomolov. Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR) : April 11, 2016, Vienna, Austria : held as part of CPS Week, April 11-14, 2016, Vienna, Austria, IEEE, 2016.
[bibtex]	Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), pages 72-74, Albert-Ludwigs-Universität, 2016.
[bibtex]	Florian Corzilius. Integrating virtual substitution into strategic SMT solving, PhD Thesis, RWTH Aachen University, 186 pages, 2016.
2017
[bibtex]	Erika Ábrahám, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W. M. Seiler, T. Sturm, J. Abbott, B. Becker, A. M. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J. H. Davenport, M. England. Satisfiability checking and symbolic computation, ACM Communications in computer algebra : ACM CCA 50 (4), pages 145-147, 2017.
2016
[bibtex]	Johanna Nellen, Kai Driessen, Martin Neuhäußer, Erika Ábrahám, Benedikt Wolters. Two CEGAR-based approaches for the safety verification of PLC-controlled plants, Information systems frontiers : ISF 18 (5), pages 927-952, 2016.
[bibtex]	Erika Ábrahám, Marcello Bonsangue, Einar Broch Johnsen. Theory and practice of formal methods : essays dedicated to Frank de Boer on the occasion of his 60th birthday, Volume 9660 of LNCS, pages XII, 427 Seiten : Illustrationen, Springer, 2016.
[bibtex]	Johanna Nellen. Analysis and synthesis of hybrid systems in engineering applications, PhD Thesis, RWTH Aachen University, 168 pages, 2016.
[bibtex]	Erika Ábrahám, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W. M. Seiler, T. Sturm, J. Abbott, B. Becker, A. M. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J. H. Davenport, M. England. Satisfiability checking and symbolic computation, 2016. arXiv:1607.06945
[bibtex]	Erika Ábrahám, Pascal Fontaine, Thomas Sturm, Dongming Wang. Symbolic Computation and Satisfiability Checking : Report of Dagstuhl Seminar 15471, Dagstuhl reports 5 (11), pages 71-89, 2016.
2015
[bibtex]	Johanna Nellen, Benedikt Wolters, Lukas Netz, Sascha Geulen, Erika Ábrahám, Martina Joševski, Dirk Abel. A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs, 1st Global Conference on Artificial Intelligence (GCAI'15), Volume 36 of EPiC Series in Computer Science, pages 196-214, EasyChair, 2015.
[bibtex]	Stefan Schupp, Erika Ábrahám, Xin Chen, Ibtissem Ben Makhlouf, Goran Frehse, Sriram Sankaranarayanan, Stefan Kowalewski. Current Challenges in the Verification of Hybrid Systems, 5th Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy 2015), Volume 9361 of LNCS, pages 8-24, Springer, 2015.
[bibtex]	Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám. SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving, International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Volume 9340 of LNCS, pages 360-368, Springer, 2015.
[bibtex]	Sascha Geulen, Martina Josevski, Johanna Nellen, Janosch Fuchs, Lukas Netz, Benedikt Wolters, Dirk Abel, Erika Ábrahám, Walter Unger. Learning-based Control Strategies for Hybrid Electric Vehicles, 2015 IEEE Conference on Control Applications (CCA), pages 1722-1728, IEEE, 2015.
[bibtex]	Erika Ábrahám, Costas Bekas, Ivona Brandic, Samir Genaim, Einar Broch Johnsen, Ivan Kondov, Sabri Pllana, Achim Streit. Preparing HPC Applications for Exascale: Challenges and Recommendations, 18th International Conference on Network-Based Information Systems (NBiS 2015), pages 401-406, IEEE, 2015.
[bibtex]	Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. PROPhESY : A PRObabilistic ParamEter SYnthesis Tool, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, pages 214-231, Springer, 2015.
[bibtex]	Erika Ábrahám. Building Bridges between Symbolic Computation and Satisfiability Checking, 14th International Symposium on Symbolic and Algebraic Computation (ISSAC'15), pages 6 S., ACM Press, 2015.
[bibtex]	Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards, 20th international symposium Formal Methods (FM 2015), Volume 9109 of LNCS, pages 435-452, Springer, 2015.
[bibtex]	Sascha Geulen, Martina Joševski, Johanna Nellen, Janosch Fuchs, Lukas Netz, Benedikt Wolters, Erika Ábrahám, Walter Unger, Dirk Abel. Online Lernen als Kontrollstrategie in Hybridfahrzeugen, 7th VDI/VDE Fachtagung AUTOREG: Auf dem Weg zum automatisierten Fahren (AUTOREG'15), Volume 2233 of VDI-Berichte, pages 101-112, VDI-Verl., 2015.
[bibtex]	Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse, Stefan Kowalewski. A Benchmark Suite for Hybrid Systems Reachability Analysis, 7th International Symposium Formal Methods (NFM 2015), Volume 9058 of LNCS, pages 408-414, Springer, 2015.
[bibtex]	Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen. A Greedy Approach for the Efficient Repair of Stochastic Models, 7th NASA Formal Methods Symposium (NFM'15), Volume 9058 of LNCS, pages 295-309, Springer, 2015.
[bibtex]	Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám. Flow 1.2: More Effective to Play with Hybrid Systems*, 1st and 2nd Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH'15), Volume 34 of EPiC Series in Computer Science, pages 152-159, EasyChair, 2015.
[bibtex]	Xin Chen. Reachability analysis of non-linear hybrid systems using Taylor Models, PhD Thesis, RWTH Aachen University, Volume 2015, 09 of Aachener Informatik Berichte, pages 166 S. : graph. Darst., Publikationsserver der RWTH Aachen University, 2015.
[bibtex]	Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen. High-level Counterexamples for Probabilistic Automata, Logical methods in computer science 11 (1), pages 15, 2015.
2016
[bibtex]	Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, Erika Ábrahám. Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis, IMA journal of mathematical control and information 33 (3), pages 723-756, 2016.
2015
[bibtex]	Johanna Nellen, Erika Ábrahám, Benedikt Wolters. A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata, Formalisms for Reuse and Systems Integration / edited by Thouraya Bouabana-Tebibel, Stuart H. Rubin, Volume 346 of Advances in Intelligent Systems and Computing, pages 55-78, Springer, 2015.
[bibtex]	Nils Jansen. Counterexamples in probabilistic verification, PhD Thesis, Aachen, Techn. Hochsch., pages XI, 224 S.S. . graph. Darst., Publikationsserver der RWTH Aachen University, 2015.
2014
[bibtex]	Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 11th International Conference on Quantitative Evaluation of Systems (QEST 2014), Volume 8657 of LNCS, pages 404-420, Springer, 2014.
[bibtex]	Johanna Nellen, Erika Ábrahám. A CEGAR Approach for the Reachability Analysis of PLC-controlled Chemical Plants, 2014 IEEE International Conference on Information Reuse and Integration (IRI'14), pages 500-507, IEEE, 2014.
[bibtex]	Erika Ábrahám, Catuscia Palamidessi. Formal techniques for distributed objects, components, and systems : 34th IFIP WG 6.1 international conference, FORTE 2014, held as part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3 - 5, 2014 ; proceedings, Volume 8461 of LNCS, pages XII, 299 S., Springer, 2014.
[bibtex]	Erika Ábrahám, Klaus Havelund. Tools and Algorithms for the Construction and Analysis of Systems : 20th international conference, TACAS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5 - 13, 2014 ; proceedings, Volume 8413 of LNCS, pages XVIII, 652 S. : graph. Darst., Springer, 2014.
2016
[bibtex]	Erika Ábrahám, Klaus Havelund. Some recent advances in automated analysis, International journal on software tools for technology transfer : STTT 18 (2), pages 121-128, 2016.
2014
[bibtex]	Erika Ábrahám, Alberto Avritzer, Anne Remke, William H. Sanders. Randomized Timed and Hybrid Models for Critical Infrastructures, Dagstuhl Reports 4 (1), pages 37-82, 2014.
[bibtex]	Erika Ábrahám, Bernd Becker, Hans Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer. Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey, Formal methods for executable software models (SFM 2014), Volume 8483 of LNCS, pages 65-121, Springer, 2014.
[bibtex]	Ralf Wimmer, Erika Ábrahám. Maybe or Maybe not : Contributions to Stochastic Verification, Aspekte der Technischen Informatik, pages 119-127, Monsenstein und Vannerdat, 2014.
[bibtex]	Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám. Under-approximate Flowpipes for Non-linear Continuous Systems, Proc. of Formal Methods in Computer-Aided Design (FMCAD'14), pages 59-66, IEEE/ACM, 2014.
[bibtex]	Pascal Richter, Martin Frank, Erika Ábrahám. Multi-objective optimization of solar tower power plants, Proc. of the 18th European Conference on Mathematics for Industry (ECMI'14), Mathematics in industry, Springer, 2014.
[bibtex]	Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky. Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories, Science of computer programming 99, pages 128-192, 2014.
[bibtex]	Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster. Symbolic counterexample generation for large discrete-time Markov chains, Science of computer programming 91 (Part A), pages 90-114, 2014.
[bibtex]	Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám. Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?, Science of computer programming , 2014.
[bibtex]	Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal counterexamples for linear-time probabilistic verification, Theoretical computer science 549, pages 61-100, 2014.
[bibtex]	Hans Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen. Fast Debugging of PRISM Models, Automated technology for verification and analysis (ATVA 2014), Volume 8837 of LNCS, pages 146-162, Springer, 2014.
[bibtex]	Erika Ábrahám, Thi Mai Thuong Tran, Martin Steffen. Observable Interface Behaviour and Inheritance, Mathematical structures in computer science : MSCS 26 (Special Issue 03), pages 561-605, 2014.
[bibtex]	Johanna Nellen, Erika Ábrahám, Xin Chen, Pieter Collins. Counterexample Generation for Hybrid Automata, Second International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'13), Volume 419 of Communications in Computer and Information Science, pages 88-106, Springer, 2014.
2013
[bibtex]	Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata, Cornell University, 2013. arXiv:1305.5055
[bibtex]	Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition, Automated Deduction, Volume 7898 of LNCS, pages 193-207, Springer, 2013.
[bibtex]	Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám. Empirical Flowpipe Constructions for Analog Circuits, Workshop on Frontiers in Analog CAD (FAC'13), 2013.
[bibtex]	Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky. A Timed CTL Model Checker for Real-Time Maude, Algebra and Coalgebra in Computer Science (CALCO 2013), Volume 8089 of LNCS, pages 334-339, Springer, 2013.
[bibtex]	Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan. Flow: An Analyzer for Non-Linear Hybrid Systems*, Computer aided verification (CAV 2013), Volume 8044 of LNCS, pages 258-263, Springer, 2013.
[bibtex]	Sriram Sankaranarayanan, Xin Chen, Erika Ábrahám. Lyapunov Function Synthesis using Handelman Representations, 9th IFAC Symposium on Nonlinear Control Systems 2013, Volume 9,1 of Nonlinear Control Systems, pages 576-581, Elsevier, 2013.
[bibtex]	Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám. Stochastic Bounded Model Checking : Bounded Rewards and Compositionality, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2013), pages 243-254, Univ., ITMZ, 2013.
[bibtex]	Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Algebraic informatics (CAI 2013), Volume 8080 of LNCS, pages 186-198, Springer, 2013.
[bibtex]	Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 2013,08 of Aachener Informatik-Berichte : AIB, pages 3-21, Shaker [u.a.], 2013.
[bibtex]	Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 2013. arXiv:1312.3979
[bibtex]	Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Fabio Somenzi, Erika Ábrahám. From Statistical Model Checking to Statistical Model Inference : Characterizing the Effect of Process Variations in Analog Circuits, 2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2013), pages 662-669, IEEE, 2013.
[bibtex]	Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata, Quantitative evaluation of systems (QEST 2013), Volume 8054 of LNCS, pages 39-54, Springer, 2013.
2012
[bibtex]	Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám. Some Like It Very Hot : Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude, Rewriting logic and its applications (WRLA 2012), Volume 7571 of LNCS, pages 139-161, Springer, 2012.
[bibtex]	Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes, Volume 88 of Reports of SFB/TR 14 AVACS, 2012.
[bibtex]	Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2012), Volume 68 of Schriftenreihe Forschungsergebnisse zur Informatik, pages 169-180, Kovač, 2012.
[bibtex]	Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains, Cornell Univ., 2012. arXiv:1206.0603v1
[bibtex]	Xin Chen, Erika Ábrahám. Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems, Computer aided systems theory - EUROCAST 2011, Volume 6927 of LNCS, pages 535-542, Springer, 2012.
[bibtex]	Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker. Symbolic Counterexample Generation for Discrete-time Markov Chains, Formal aspects of component software (FACS 2012), Springer eBook collection : Computer science, pages 134-151, Springer, 2012.
[bibtex]	Johanna Nellen, Erika Ábrahám. Hybrid Sequential Function Charts, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2012), Volume 68 of Schriftenreihe Forschungsergebnisse zur Informatik, pages 109-120, Kovač, 2012.
[bibtex]	Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika Ábrahám. SMT-RAT : An SMT-Compliant Nonlinear Real Arithmetic Toolbox, Theory and applications of satisfiability testing, Volume 7317 of LNCS, pages 442-448, Springer, 2012.
[bibtex]	Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems, Proceedings of the 33rd IEEE Real-Time Systems Symposium (RTSS'12), Volume 2012 of Real-Time Systems Symposium-Proceedings, pages 183-192, IEEE Computer Soc., 2012.
[bibtex]	Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan. Taylor Model Over-approximations for Flowpipe : Guard Intersections, 5th International Workshop on Numerical Software Verification (NSV'12), 2012.
[bibtex]	Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool : Computing Minimal Counterexamples for DTMCs, Automated technology for verification and analysis (ATVA 2012), Volume 7561 of LNCS, pages 349-353, Springer, 2012.
[bibtex]	Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky. Timed CTL Model Checking in Real-Time Maude, Rewriting logic and its applications (WRLA 2012), Volume 7571 of LNCS, pages 182-200, Springer, 2012.
[bibtex]	Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen. Minimal Critical Subsystems for Discrete-Time Markov Models, Tools and algorithms for the construction and analysis of systems (TACAS 2012), Volume 7214 of LNCS, pages 299-314, Springer, 2012.
2011
[bibtex]	Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám. SMT-based Counterexample Generation for Markov Chains, Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'11), pages 19-28, OFFIS, 2011.
[bibtex]	Till Königshofen. Webbasierte konstruktivistische Lernumgebung für PHP und Datenbanken, Diploma Thesis, Rheinisch-Westfälische Technische Hochschule Aachen, pages 159 S. : graph. Darst., 2011.
[bibtex]	Muhammad Fadlisyah, P. C. Olveczky, Erika Ábrahám. Formal modeling and analysis of hybrid systems in rewriting logic using higher-order numerical methods and discrete-event detection, 2011 CSI International Symposium on Computer Science and Software Engineering (CSSE 2011), pages 1-8, 2011.
[bibtex]	Florian Corzilius, Erika Ábrahám. Virtual Substitution for SMT-Solving, Fundamentals of computation theory (FCT 2011), Volume 6914 of LNCS, pages 360-371, Springer, 2011.
[bibtex]	Ulrich Loup, Erika Ábrahám. GiNaCRA: A C++ Library for Real Algebraic Computations, NASA formal methods (NFM 2011), Volume 6617 of LNCS, pages 512-517, Springer, 2011.
[bibtex]	Pascal Richter, Erika Ábrahám, Gabriel Morin. Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks, Adaptive and natural computing algorithms (ICANNGA 2011), Volume 6593 of LNCS, pages 190-199, Springer, 2011.
[bibtex]	Ulrich Loup, Erika Ábrahám. I-RiSC : an SMT-Compliant Solver for the Existential Fragment of Real Algebra, Algebraic informatics (CAI 2011), Volume 6742 of LNCS, pages 230-246, Springer, 2011.
[bibtex]	Xin Chen, Erika Ábrahám, Goran Frehse. Efficient bounded reachability computation for rectangular automata, Reachability problems (RP 2011), Volume 6945 of LNCS, pages 139-152, Springer, 2011.
[bibtex]	Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám. Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking, Formal techniques for distributed systems (FORTE 2011), Volume 6722 of LNCS, pages 75-89, Springer, 2011.
[bibtex]	Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical counterexamples for discrete-time markov chains, Automated technolgoy for verification and analysis (ATVA 2011), Volume 6996 of LNCS, pages 443-452, Springer, 2011.
[bibtex]	Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám. Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude, Software engineering and formal methods (SEFM 2011), Volume 7041 of LNCS, pages 415-430, Springer, 2011.
[bibtex]	Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde. Parallel SAT Solving in Bounded Model Checking, Journal of logic and computation 21 (1), pages 5-21, 2011.
2010
[bibtex]	Muhammad Fadlisyah, Erika Ábrahám, Peter Csaba Ölveczky. Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems, Electronic notes in theoretical computer science : ENTCS 274, pages 17-32, 2010.
[bibtex]	Markus Geimer, Felix Gerd Eugen Wolf, Brian J. N. Wylie, Erika Ábrahám, Daniel Becker, Bernd Mohr. The Scalasca performance toolset architecture, Concurrency and computation : practice & experience 22.2010 (6 : Special issue), pages 702-719, 2010.
[bibtex]	Daniela Lepri, Peter Csaba Ölveczky, Erika Ábrahám. Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications, Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), Volume 36 of EPTCS, pages 117-136, NICTA, 2010.
[bibtex]	Muhammad Fadlisyah, Erika Ábrahám, Daniela Lepri, Peter Csaba Ölveczky. A Rewriting-Logic-Based Technique for Modeling Thermal Systems, Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), Volume 36 of EPTCS, pages 82-100, NICTA, 2010.
[bibtex]	Erika Ábrahám, Ulrich Loup, Florian Corzilius, Thomas Sturm. SMT-Solving in the Analysis and Synthesis of Hybrid Systems, Verification over discrete-continuous boundaries, Volume 10271 of Dagstuhl Seminar Proceedings, pages 9 S., Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2010.
[bibtex]	Erika Ábrahám, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Ulrik Schroeder. Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik, DeLFI 2010, Volume 169 of GI-Edition lecture notes in informatics : P, Proceedings, pages 239-251, Ges. für Informatik, 2010.
[bibtex]	Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker. Exploiting Different Strategies for the Parallelization of an SMT Solver, 13. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pages 97-106, Fraunhofer Verl., 2010.
[bibtex]	Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. DTMC Model Checking by SCC Reduction, Proceedings / Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010), pages 37-46, IEEE Computer Society, 2010.
[bibtex]	Kai Bollue, Michaela Slaats, Erika Ábrahám, Wolfgang Thomas, Dirk Abel. Synthesis of Behavioral Controllers for DES: Increasing Efficiency, pages 30-37, IFAC, 2010.
2009
[bibtex]	Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker. Picoso - A Parallel Interval Constraint Solver, Proceedings of the 2009 International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2009, pages 473-479, CSREA Press, 2009.
[bibtex]	Erika Ábrahám, Immo Grabe, Andreas Grüner, Martin Steffen. Behavioral interface description of an object-oriented language with futures and promises, The journal of logic and algebraic programming 78 (7), pages 491-518, 2009.
[bibtex]	Erika Ábrahám, Ulrich Loup. SMT-Solving for the First-Order Theory of the Reals, Algorithms and Applications for Next Generation SAT Solvers, Volume 09461 of Dagstuhl Seminar Proceedings, pages 7 S., Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2009.
2008
[bibtex]	Erika Ábrahám, Andreas Grüner, Martin Steffen. Abstract Interface Behavior of Object-Oriented Languages with Monitors, Theory of computing systems 43 (3/4), pages 322-361, 2008.
[bibtex]	Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. A Deductive Proof System for Multithreaded Java with Exceptions, Fundamenta informaticae 82 (4), pages 391-463, 2008.
[bibtex]	Erika Ábrahám, Andreas Grüner, Martin Steffen. Heap-abstraction for an object-oriented calculus with thread classes, Software and systems modeling 7 (2), pages 177-208, 2008.
[bibtex]	Felix Gerd Eugen Wolf, Brian J. N. Wylie, Erika Ábrahám, Daniel Becker, Wolfgang Frings, Karl Fürlinger, Markus Geimer, Marc-André Hermanns, Bernd Mohr, Shirley Moore, Matthias Pfeifer, Zoltán Péter Szebenyi. Usage of the SCALASCA toolset for scalable performance analysis of large-scale parallel applications, Tools for high performance computing, pages 157-167, Springer, 2008.
2007
[bibtex]	Marc Herbstritt, Bernd Becker, Erika Ábrahám, Christian Herde. On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata, 2007 IEEE design and diagnostics of electronic circuits and systems, pages 391-396, IEEE Service Center, 2007.
[bibtex]	Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde. Parallel SAT solving in bounded model checking, Formal methods, Volume 4346 of LNCS, pages 301-315, Springer, 2007.
2006
[bibtex]	Erika Ábrahám, Andreas Grüner, Martin Steffen. Abstract interface behavior of object-oriented languages with monitors, Formal methods for open object-based distributed systems, Volume 4037 of LNCS, pages 218-232, Springer, 2006.
[bibtex]	Erika Ábrahám, Andreas Grüner, Martin Steffen. Dynamic heap-abstraction for open, object-oriented systems with thread classes, Logical approaches to computational barriers, Volume 3988 of LNCS, pages 1-10, Springer, 2006.
[bibtex]	Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen. Memory-aware bounded model checking for linear hybrid systems, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pages 153-162, Fraunhofer-Institut für Integrierte Schaltungen, Außenstelle Entwurfsautomatisierung, 2006.
[bibtex]	Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen. Bounded model checking with parametric data structures, Electronic notes in theoretical computer science : ENTCS 174 (3), pages 3-16, 2006.
2005
[bibtex]	Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. An Assertion-Based Proof System for Multithreaded Java, Theoretical computer science 331 (2/3), pages 251-290, 2005.
[bibtex]	Erika Ábrahám, Andreas Grüner, Martin Steffen. Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes, COSMICAH 2005, Volume RR-05-04 of Research report / Queen Mary, University of London, Department of Computer Science, pages 47-61, Queen Mary, University of London, Department of Computer Science, 2005.
[bibtex]	Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen. Optimizing Bounded Model Checking for Linear Hybrid Systems, Verification, model checking, and abstract interpretation (VMCAI 2005), Volume 3385 of LNCS, pages 396-412, Springer, 2005.
[bibtex]	Frank S. de Boer, Marcello Bonsangue, Martin Steffen, Erika Ábrahám. A Fully Abstract Trace Semantics for UML Components, Formal methods for components and objects (FMCO 2004), Volume 3657 : Tutorial of LNCS, pages 49-69, Springer, 2005.
[bibtex]	Erika Ábrahám, Frank S. de Boer, Marcello Bonsangue, Andreas Grüner, Martin Steffen. Observability, Connectivity, and Replay in a Sequential Calculus of Classes, Formal methods for components and objects (FMCO 2004), Volume 3657 : Tutorial of LNCS, pages 296-316, Springer, 2005.
[bibtex]	Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Inductive Proof Outlines for Exceptions in Multithreaded Java, Proceedings of the First IPM International Workshop on Foundations of Software Engineering (FSEN 2005), Volume 159 of Electronic notes in theoretical computer science, pages 281-297, Elsevier, 2005.
[bibtex]	Erika Ábrahám, Marcello Bonsangue, Frank S. de Boer, Martin Steffen. Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes, Theoretical aspects of computing - ICTAC 2004, Volume 3407 of LNCS, pages 37-51, Springer, 2005.