- abraham at cs.rwth-aachen.de
- Address
- Room 4229
Ahornstraße 55
D-52074 Aachen - Phone
- +49 241 80 21242
Current research activities:
- modeling, synthesis, and analysis of hybrid systems,
- analysis of probabilistic systems, probabilistic hyperproperties,
- SMT solving with a focus on real algebra,
- SMT-based planning and scheduling,
- energy optimization.
Curriculum vitae
Projects
Teaching
School activities
Women in Computer Science
Some further links: ACM-WE interview
Publications
2024 | |
---|---|
![]() |
Erika Ábrahám, Hans Christian Hensel, , Joost-Pieter Katoen, Tim Quatmann, . Parameter synthesis for Markov models: covering the parameter space, Formal methods in system design 62 (1/3), pages 181-259, Springer, 2024. | ,
2021 | |
![]() ![]() |
Erika Ábrahám, James H. 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 119, pages 100633, Elsevier Science, 2021. |
2019 | |
![]() |
Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Ábrahám, , . Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development, 24. International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019), Volume 11687 of LNCS, 59-75, Springer, 2019. |
2018 | |
![]() |
Stefan Schupp, Justin Winkens, Erika Ábrahám. Context-Dependent Reachability Analysis for Hybrid Systems, IEEE 19. International Conference on Information Reuse and Integration for Data Science (IRI 2018), 518-525, IEEE, 2018. |
![]() ![]() |
Gereon Kremer, Erika Ábrahám. Modular strategic SMT solving with SMT-RAT, Acta Universitatis Sapientiae / Informatica 10 (1), pages 5-25, De Gruyter Open, 2018. |
![]() |
Stefan Schupp, Erika Ábrahám. Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems, 16. International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, 89-104, Springer, 2018. |
![]() ![]() |
Stefan Schupp, Erika Ábrahám. Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis, 24. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806, Part 2 of LNCS, 287-302, Springer, 2018. |
![]() |
Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, , . Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain, 22. International Symposium on Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018. |
![]() |
Johanna Nellen, , , Erika Ábrahám, Joost-Pieter Katoen. Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations, 22. International Symposium on Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018. |
![]() |
Francesco Leofante, Erika Ábrahám, Tim Dieter Niemüller, Gerhard Lakemeyer, . Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics, Information systems frontiers 21 (1), pages 87-107, Kluwer, 2018. |
![]() |
Francesco Leofante, Erika Ábrahám, . Task Planning with OMT: An Application to Production Logistics, 14. International Conference on Integrated Formal Methods (IFM 2018), Volume 11023, Programming and Software Engineering of LNCS, 316-325, Springer, 2018. |
![]() |
Erika Ábrahám, . HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties, 15. International Conference on Quantitative Evaluation of Systems (QEST 2018), Volume 11024, Theoretical Computer Science and General Issues of LNCS, Springer, 2018. |
![]() |
Rebecca Haehn, Gereon Kremer, Erika Ábrahám. Evaluation of Equational Constraints for CAD in SMT Solving, 3. Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference (SC-Square 2018), Volume 2189 of CEUR Workshop Proceedings, [19]-32, RWTH Aachen, 2018. |
![]() ![]() |
Erika Ábrahám (ed), Silvia Lizeth Taipa Tarifa (ed). Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18), Volume 483 of Research report / University of Oslo, 2018. |
![]() |
Erika Ábrahám (ed), Elisabetta Di Nitto (ed), . 2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering: GE 2018, IEEE, 2018. |
![]() |
Erika Ábrahám. Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics, Volume 10900 of LNCS, XII-XII, Springer, 2018. |
![]() |
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 Seiten, Oslo University, 2018. |
2017 | |
![]() |
Erika Ábrahám, , , , , , , , , , , , , , . Satisfiability checking and symbolic computation, ACM Communications in computer algebra 50 (4), pages 145-147, ACM, 2017. |
2016 | |
![]() |
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, Univ. Press, 2016. |
![]() ![]() |
Hans 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), 72-74, Albert-Ludwigs-Universität, 2016. |
![]() |
Erika Ábrahám, , , , , , , , , , , , , , . Satisfiability checking and symbolic computation, 3 Seiten : Illustrationen, 2016. https://arxiv.org/abs/1607.06945 |
2015 | |
![]() ![]() |
Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen. High-level Counterexamples for Probabilistic Automata, Logical methods in computer science 11 (1), pages 15, Department of Theoretical Computer Science, Technical University of Braunschweig, 2015. | ,
![]() |
Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards, 20. international symposium Formal Methods (FM 2015), Volume 9109 of LNCS, 435-452, Springer, 2015. |
![]() |
Erika Ábrahám, Nils Jansen, , Joost-Pieter Katoen. A Greedy Approach for the Efficient Repair of Stochastic Models, 7. NASA Formal Methods Symposium (NFM'15), Volume 9058 of LNCS, 295-309, Springer, 2015. | ,
![]() |
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, 214-231, Springer, 2015. |
![]() |
Stefan Schupp, Erika Ábrahám, Xin Chen, Ibtissem Ben Makhlouf, Goran Frehse, Sriram Sankaranarayanan, Stefan Kowalewski. Current Challenges in the Verification of Hybrid Systems, 5. Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy 2015), Volume 9361 of LNCS, 8-24, Springer, 2015. |
[bibtex] [issue] | Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám. Flow* 1.2: More Effective to Play with Hybrid Systems, 1. and 2nd Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH'15), Volume 34 of EPiC Series in Computer Science, 152-159, EasyChair, 2015. |
![]() |
Erika Ábrahám, , , , , , , Achim Streit. Challenges and Recommendations for Preparing HPC Applications for Exascale, 6 Seiten, 2015. https://arxiv.org/abs/1503.06974 |
[bibtex] [issue] | Sascha Geulen, Martina Joševski, Johanna Nellen, Janosch Fuchs, Lukas Stephan Michael Netz, Benedikt Wolters, Erika Ábrahám, Walter Unger, Dirk Abel. Online Lernen als Kontrollstrategie in Hybridfahrzeugen, AUTOREG 2015 - Auf dem Weg zum automatisierten Fahren, 7. Fachtagung (AUTOREG 2015), Volume 2233 of VDI-Berichte, 101-112, VDI-Verl., 2015. |
![]() |
Erika Ábrahám, , , , , , , Achim Streit. Preparing HPC Applications for Exascale: Challenges and Recommendations, 18. International Conference on Network-Based Information Systems (NBiS 2015), 401-406, IEEE, 2015. |
![]() |
Sascha Geulen, Martina Josevski, Johanna Nellen, Janosch Fuchs, Lukas Stephan Michael 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), 1722-1728, IEEE, 2015. |
2014 | |
![]() |
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, 65-121, Springer, 2014. |
![]() |
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, Elsevier, 2014. |
![]() |
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, Elsevier, 2014. |
![]() |
Hans Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen. Fast Debugging of PRISM Models, Automated technology for verification and analysis : 12th international symposium (ATVA 2014), Volume 8837 of LNCS, 146-162, Springer, 2014. |
![]() |
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 11. International Conference on Quantitative Evaluation of Systems (QEST 2014), Volume 8657 of LNCS, 404-420, Springer, 2014. |
![]() |
Erika Ábrahám (ed), . Formal techniques for distributed objects, components, and systems, Volume 8461 of LNCS, XII, 299 S., Springer, 2014. |
![]() |
Erika Ábrahám, Thi Mai Thuong Tran, Martin Steffen. Observable Interface Behaviour and Inheritance, Mathematical structures in computer science 26 (Special Issue 03), pages 561-605, Cambridge Univ. Press, 2014. |
![]() |
Johanna Nellen, Erika Ábrahám, Xin Chen, . Counterexample Generation for Hybrid Automata, 2. International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'13), Volume 419 of Communications in Computer and Information Science, 88-106, Springer, 2014. |
2013 | |
![]() |
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata, Quantitative evaluation of systems : 10. international conference (QEST 2013), Volume 8054 of LNCS, 39-54, Springer, 2013. |
![]() |
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 21 Seiten, 2013. https://arxiv.org/abs/1312.3979 |
2012 | |
![]() |
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 : 18. international conference (TACAS 2012), Volume 7214 of LNCS, 299-314, Springer, 2012. |
![]() |
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] [issue] | Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties, 15. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2012), Volume 68 of Schriftenreihe Forschungsergebnisse zur Informatik, 169-180, Kovač, 2012. |
2011 | |
![]() |
Ulrich Loup, Erika Ábrahám. I-RiSC: an SMT-Compliant Solver for the Existential Fragment of Real Algebra, 4. international conference: Algebraic informatics (CAI 2011), Volume 6742 of LNCS, 230-246, Springer, 2011. |
![]() |
Ulrich Loup, Erika Ábrahám. GiNaCRA: A C++ Library for Real Algebraic Computations, 3. International Symposium NASA Formal Methods (NFM 2011), Volume 6617 of LNCS, 512-517, Springer, 2011. |
![]() |
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám. Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking, 13. IFIP WG 6.1 international conference (FORTE 2011), Volume 6722 of LNCS, 75-89, Springer, 2011. |
![]() |
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 : 9. international symposium (ATVA 2011), Volume 6996 of LNCS, 443-452, Springer, 2011. |
[bibtex] [issue] | 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), 19-28, OFFIS, 2011. |
2010 | |
![]() |
Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. DTMC Model Checking by SCC Reduction, 7. International Conference on the Quantitative Evaluation of Systems (QEST 2010), 37-46, IEEE Computer Society, 2010. |
2007 | |
![]() |
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde. Parallel SAT solving in bounded model checking, Volume 4346 of LNCS, 301-315, Springer, 2007. |
![]() |
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, 391-396, IEEE Service Center, 2007. |
2006 | |
![]() |
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, 218-232, Springer, 2006. |
![]() |
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, 1-10, Springer, 2006. |
[bibtex] [issue] | 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, 153-162, Fraunhofer-Institut für Integrierte Schaltungen, Außenstelle Entwurfsautomatisierung, 2006. |
![]() |
Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen. Bounded model checking with parametric data structures, Electronic notes in theoretical computer science 174 (3), pages 3-16, Elsevier, 2006. |
2005 | |
![]() |
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, 37-51, Springer, 2005. |
![]() |
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, 281-297, Elsevier, 2005. |
![]() |
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, 296-316, Springer, 2005. |
![]() |
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, 49-69, Springer, 2005. |
![]() |
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, 396-412, Springer, 2005. |
[bibtex] [issue] | 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, 47-61, Queen Mary, University of London, Department of Computer Science, 2005. |
![]() |
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, Elsevier, 2005. |