Erika Ábrahám | Theory of Hybrid Systems

Email: 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

Publications

2023
[bibtex] @misc{VSSLG2023, title = {Verfahren und System zur Steuerung von Lasten in einem Gebäude}, author = {Jonas Blum and Stefan Hardt and Pascal Richter and Erika Ábrahám and Ahmed Abida and Simon Klemp}, pages = {17 Seiten : Illustrationen}, type = {Patent}, year = {2023}, url = { https://publications.rwth-aachen.de/record/953391}, }× [issue]	Jonas Blum, Stefan Hardt, Pascal Richter, Erika Ábrahám, Ahmed Abida, Simon Klemp. Verfahren und System zur Steuerung von Lasten in einem Gebäude, 17 Seiten : Illustrationen, 2023.
[bibtex] @unpublished{L2023, title = {Levelwise construction of a single cylindrical algebraic cell}, author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Philippe Specht and Christopher W. Brown and James H. Davenport and Matthew England}, type = {Preprint}, year = {2023}, doi = {10.48550/arXiv.2212.09309}, url = { https://arxiv.org/abs/2212.09309}, }× [issue]	Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Philippe Specht, Christopher W. Brown, James H. Davenport, Matthew England. Levelwise construction of a single cylindrical algebraic cell, 2023. https://arxiv.org/abs/2212.09309
[bibtex] @conference{ACAMAUVBLSTM2023, title = {A Collision Avoidance Method for Autonomous Underwater Vehicles Based on Long Short-Term Memories}, author = {László Antal and Martin Aubard and Erika Ábrahám and Ana Madureira and Luís Madureira and Maria Costa and José Pinto and Renato Campos}, publisher = {Springer}, booktitle = {Lecture Notes in Networks and Systems}, volume = {649}, pages = {448-457}, type = {Conference Paper}, year = {2023}, doi = {10.1007/978-3-031-27499-2_42}, url = { https://publications.rwth-aachen.de/record/955843}, }× [issue]	László Antal, Martin Aubard, Erika Ábrahám, Ana Madureira, Luís Madureira, Maria Costa, José Pinto, Renato Campos. A Collision Avoidance Method for Autonomous Underwater Vehicles Based on Long Short-Term Memories, 13th International Conference on Innovations in Bio-Inspired Computing and Applications (IBICA22), Volume 649 of Lecture Notes in Networks and Systems, 448-457, Springer, 2023.
[bibtex] @conference{AEGSC2023, title = {Automated Exercise Generation for Satisfiability Checking}, author = {Erika Ábrahám and Jasper Nalbach and Valentin Maxim Promies}, publisher = {Springer}, booktitle = {LNCS}, volume = {13962}, pages = {1-16}, type = {Conference Paper}, year = {2023}, doi = {10.1007/978-3-031-27534-0_1}, url = { https://publications.rwth-aachen.de/record/957774}, }× [issue]	Erika Ábrahám, Jasper Nalbach, Valentin Maxim Promies. Automated Exercise Generation for Satisfiability Checking, 5th International Workshop on Formal Methods Teaching (FMTea 2023), Volume 13962 of LNCS, 1-16, Springer, 2023.
2022
[bibtex] @conference{HMCPD2022, title = {HyperPCTL Model Checking by Probabilistic Decomposition}, author = {Eshita Zaman and Gianfranco Ciardo and Erika Ábrahám and Borzoo Bonakdarpour}, publisher = {Springer}, booktitle = {LNCS}, volume = {13274, Formal methods}, pages = {209-226}, type = {Conference Paper}, year = {2022}, doi = {10.1007/978-3-031-07727-2_12}, url = { https://publications.rwth-aachen.de/record/850268}, }× [issue]	Eshita Zaman, Gianfranco Ciardo, Erika Ábrahám, Borzoo Bonakdarpour. HyperPCTL Model Checking by Probabilistic Decomposition, 17. International Conference on integrated Formal Methods (IFM 2022), Volume 13274, Formal methods of LNCS, 209-226, Springer, 2022.
[bibtex] @conference{PHR2022, title = {Probabilistic Hyperproperties with Rewards}, author = {Oyendrila Dobe and Lukas Wilke and Erika Ábrahám and Borzoo Bonakdarpour and Ezio Bartocci}, publisher = {Springer}, booktitle = {LNCS}, volume = {13260}, pages = {656-673}, type = {Conference Paper}, year = {2022}, doi = {10.1007/978-3-031-06773-0_35}, url = { https://publications.rwth-aachen.de/record/850269}, }× [issue]	Oyendrila Dobe, Lukas Wilke, Erika Ábrahám, Borzoo Bonakdarpour, Ezio Bartocci. Probabilistic Hyperproperties with Rewards, 14. International Symposium NASA Formal Methods (NFM 2022), Volume 13260 of LNCS, 656-673, Springer, 2022.
[bibtex] @conference{ATSSRT2022, title = {Acceleration Techniques for Symbolic Simulation of Railway Timetables}, author = {Rebecca Haehn and Erika Ábrahám and Niklas Kotowski}, publisher = {Springer}, booktitle = {LNCS}, volume = {13294}, pages = {46-62}, type = {Conference Paper}, year = {2022}, doi = {10.1007/978-3-031-05814-1_4}, url = { https://publications.rwth-aachen.de/record/850270}, }× [issue]	Rebecca Haehn, Erika Ábrahám, Niklas Kotowski. Acceleration Techniques for Symbolic Simulation of Railway Timetables, 4. International Conference on Reliability, Safety and Security of Railway Systems (RSSRail 2022), Volume 13294 of LNCS, 46-62, Springer, 2022.
[bibtex] @unpublished{RSHSMV2022, title = {Robot Swarms as Hybrid Systems: Modelling and Verification}, author = {Stefan Schupp and Francesco Leofante and Leander Behr and Erika Ábrahám and Armando Tacchella}, type = {Preprint}, year = {2022}, doi = {10.48550/arXiv.2207.06758}, url = { https://arxiv.org/abs/2207.06758}, }× [issue]	Stefan Schupp, Francesco Leofante, Leander Behr, Erika Ábrahám, Armando Tacchella. Robot Swarms as Hybrid Systems: Modelling and Verification, 2022. https://arxiv.org/abs/2207.06758
[bibtex] @article{RH2022, title = {Recent developments in theory and tool support for hybrid systems verification with HyPro}, author = {Stefan Schupp and Erika Ábrahám and Tristan Ebert}, publisher = {Elsevier}, journal = {Information and Computation}, volume = {289(Part A)}, pages = {pages 104945}, type = {Journal Article}, year = {2022}, doi = {10.1016/j.ic.2022.104945}, url = { https://publications.rwth-aachen.de/record/850718}, }× [issue]	Stefan Schupp, Erika Ábrahám, Tristan Ebert. Recent developments in theory and tool support for hybrid systems verification with HyPro, Information and Computation 289 (Part A), pages 104945, Elsevier, 2022.
[bibtex] @conference{EARC2022, title = {Experiments with Automated Reasoning in the Class}, author = {Isabela Dramnesc and Erika Ábrahám and Tudor Jebelean and Gábor Kusper and Sorin Stratulat}, publisher = {Springer}, booktitle = {Lecture Notes in Artificial Intelligence}, volume = {13467}, pages = {287-304}, type = {Conference Paper}, year = {2022}, doi = {10.1007/978-3-031-16681-5_20}, url = { https://publications.rwth-aachen.de/record/854208}, }× [issue]	Isabela Dramnesc, Erika Ábrahám, Tudor Jebelean, Gábor Kusper, Sorin Stratulat. Experiments with Automated Reasoning in the Class, Intelligent Computer Mathematics - 15. International Conference (CICM 2022), Volume 13467 of Lecture Notes in Artificial Intelligence, 287-304, Springer, 2022.
[bibtex] @article{NPSCSC2022, title = {New Perspectives in Symbolic Computation and Satisfiability Checking}, author = {Erika Ábrahám and James H. Davenport and Matthew England and Alberto Griggio}, publisher = {Schloss Dagstuhl}, journal = {Dagstuhl reports}, volume = {12(2)}, pages = {pages 67-86}, type = {Journal Article}, year = {2022}, doi = {10.4230/DagRep.12.2.67}, url = { https://publications.rwth-aachen.de/record/854210}, }× [issue]	Erika Ábrahám, James H. Davenport, Matthew England, Alberto Griggio. New Perspectives in Symbolic Computation and Satisfiability Checking, Dagstuhl reports 12 (2), pages 67-86, Schloss Dagstuhl, 2022.
[bibtex] @proceedings{Q2022, title = {Quantitative evaluation of systems}, author = {}, editor = {Erika Ábrahám and Marco Paolieri}, publisher = {Springer}, booktitle = {LNCS}, volume = {13479}, pages = {XVII, 399 Seiten : Illustrationen}, type = {Proceeding Article}, year = {2022}, doi = {10.1007/978-3-031-16336-4}, url = { https://publications.rwth-aachen.de/record/854216}, }× [issue]	. Quantitative evaluation of systems, Volume 13479 of LNCS, XVII, 399 Seiten : Illustrationen, Springer, 2022.
[bibtex] @article{MM2022, title = {Model checking hyperproperties for Markov decision processes}, author = {Oyendrila Dobe and Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour}, publisher = {Elsevier}, journal = {Information and Computation}, volume = {289(Part B)}, pages = {pages 104978}, type = {Journal Article}, year = {2022}, doi = {10.1016/j.ic.2022.104978}, url = { https://publications.rwth-aachen.de/record/861552}, }× [issue]	Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour. Model checking hyperproperties for Markov decision processes, Information and Computation 289 (Part B), pages 104978, Elsevier, 2022.
2021
[bibtex] @article{D2021, title = {Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings}, author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer}, publisher = {Elsevier Science}, journal = {Journal of Logical and Algebraic Methods in Programming}, volume = {119}, pages = {pages 100633}, type = {Journal Article}, year = {2021}, doi = {10.1016/j.jlamp.2020.100633}, url = { https://publications.rwth-aachen.de/record/816049}, }× [issue]	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.
[bibtex] @conference{EFTLPSI2021, title = {Extending the Fundamental Theorem of Linear Programming for Strict Inequalities}, author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Gereon Kremer}, publisher = {Association for Computing Machinery}, booktitle = {ACM Conferences}, pages = {313-320}, type = {Conference Paper}, year = {2021}, doi = {10.1145/3452143.3465538}, url = { https://publications.rwth-aachen.de/record/823081}, }× [issue]	Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Gereon Kremer. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities, International Symposium on Symbolic and Algebraic Computation (ISSAC '21), ACM Conferences, 313-320, Association for Computing Machinery, 2021.
[bibtex] @conference{SSRTUCSD2021, title = {Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies}, author = {Rebecca Haehn and Erika Ábrahám and Nils Nießen}, publisher = {Springer}, booktitle = {LNCS}, volume = {12846}, pages = {257-275}, type = {Conference Paper}, year = {2021}, doi = {10.1007/978-3-030-85172-9_14}, url = { https://publications.rwth-aachen.de/record/825264}, }× [issue]	Rebecca Haehn, Erika Ábrahám, Nils Nießen. Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies, 18. International Conference on Quantitative Evaluation of Systems (QEST 2021), Volume 12846 of LNCS, 257-275, Springer, 2021.
[bibtex] @conference{ACCRCHSLCD2021, title = {ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics}, author = {Matthias Althoff and Erika Ábrahám and Marcelo Forets and Goran Frehse and Daniel Freire and Christian Schilling and Stefan Schupp and Mark Wetzlinger}, booktitle = {EPiC Series in Computing}, volume = {80}, pages = {1-31}, type = {Conference Paper}, year = {2021}, doi = {10.29007/lhbw}, url = { https://publications.rwth-aachen.de/record/841832}, }× [issue]	Matthias Althoff, Erika Ábrahám, Marcelo Forets, Goran Frehse, Daniel Freire, Christian Schilling, Stefan Schupp, Mark Wetzlinger. ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics, 8. International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Volume 80 of EPiC Series in Computing, 1-31, 2021.
[bibtex] @inbook{HAMCPH2021, title = {HyperProb: A Model Checker for Probabilistic Hyperproperties}, author = {Oyendrila Dobe and Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour}, publisher = {Springer}, booktitle = {LNCS}, volume = {13047}, pages = {657-666}, type = {Book Chapter}, year = {2021}, doi = {10.1007/978-3-030-90870-6_35}, url = { https://publications.rwth-aachen.de/record/841833}, }× [issue]	Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour. HyperProb: A Model Checker for Probabilistic Hyperproperties, Volume 13047 of LNCS, 657-666, Springer, 2021.
[bibtex] @conference{C2021, title = {Controller verification meets controller code: a case study}, author = {Felix Freiberger and Stefan Schupp and Holger Hermanns and Erika Ábrahám}, publisher = {Association for Computing Machinery}, booktitle = {ACM conferences}, pages = {98-103}, type = {Conference Paper}, year = {2021}, doi = {10.1145/3487212.3487337}, url = { https://publications.rwth-aachen.de/record/841835}, }× [issue]	Felix Freiberger, Stefan Schupp, Holger Hermanns, Erika Ábrahám. Controller verification meets controller code: a case study, 19. International Conference on Formal Methods and Models for System Design (MEMOCODE 21), ACM conferences, 98-103, Association for Computing Machinery, 2021.
[bibtex] @unpublished{PUSTCQFNLRA2021, title = {Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic}, author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer}, pages = {5 Seiten}, type = {Preprint}, year = {2021}, url = { https://arxiv.org/abs/2108.05320}, }× [issue]	Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic, 5 Seiten, 2021. https://arxiv.org/abs/2108.05320
[bibtex] @unpublished{OM2021, title = {On the proof complexity of MCSAT}, author = {Gereon Kremer and Erika Ábrahám and Vijay Ganesh}, type = {Preprint}, year = {2021}, url = { https://arxiv.org/abs/2109.01585}, }× [issue]	Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the proof complexity of MCSAT, 2021. https://arxiv.org/abs/2109.01585
[bibtex] @conference{OICACSMTS2021, title = {On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving}, author = {Gereon Kremer and Erika Ábrahám and Matthew England and James H. Davenport}, publisher = {IEEE}, pages = {37-39}, type = {Conference Paper}, year = {2021}, doi = {10.1109/SYNASC54541.2021.00018}, url = { https://publications.rwth-aachen.de/record/846648}, }× [issue]	Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport. On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving, 23. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 37-39, IEEE, 2021.
2020
[bibtex] @unpublished{DCNLRACCDSUCAC2020, title = {Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings}, author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer}, publisher = {Elsevier Science}, pages = {41 Seiten}, type = {Preprint}, year = {2020}, url = { https://arxiv.org/abs/2003.05633}, }× [issue]	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, 41 Seiten, Elsevier Science, 2020. https://arxiv.org/abs/2003.05633
[bibtex] @conference{FTSRS2020, title = {Freight Train Scheduling in Railway Systems}, author = {Rebecca Haehn and Erika Ábrahám and Nils Nießen}, publisher = {Springer}, booktitle = {LNCS}, volume = {12040}, pages = {225-241}, type = {Conference Paper}, year = {2020}, doi = {10.1007/978-3-030-43024-5_14}, url = { https://publications.rwth-aachen.de/record/789633}, }× [issue]	Rebecca Haehn, Erika Ábrahám, Nils Nießen. Freight Train Scheduling in Railway Systems, 20. International Conference on Measurement, Modelling and Evaluation of Computing Systems (MMB 2020), Volume 12040 of LNCS, 225-241, Springer, 2020.
[bibtex] @conference{PSPH2020, title = {Parameter Synthesis for Probabilistic Hyperproperties}, author = {Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour and Oyendrila Dobe}, booktitle = {EPiC Series in Computing}, volume = {73}, pages = {12-31}, type = {Conference Paper}, year = {2020}, doi = {10.29007/37lf}, url = { https://publications.rwth-aachen.de/record/792181}, }× [issue]	Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe. Parameter Synthesis for Probabilistic Hyperproperties, 23. International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2020), Volume 73 of EPiC Series in Computing, 12-31, 2020.
[bibtex] @conference{PSRT2020, title = {Probabilistic Simulation of a Railway Timetable}, author = {Rebecca Haehn and Erika Ábrahám and Nils Nießen}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, booktitle = {OpenAccess Series in Informatics (OASIcs)}, volume = {85}, pages = {16:1-16:14}, type = {Conference Paper}, year = {2020}, doi = {10.4230/OASICS.ATMOS.2020.16}, url = { https://publications.rwth-aachen.de/record/807139}, }× [issue]	Rebecca Haehn, Erika Ábrahám, Nils Nießen. Probabilistic Simulation of a Railway Timetable, 20. Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2020), Volume 85 of OpenAccess Series in Informatics (OASIcs), 16:1-16:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
[bibtex] @conference{PHN2020, title = {Probabilistic Hyperproperties with Nondeterminism}, author = {Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour and Oyendrila Dobe}, publisher = {Springer}, booktitle = {LNCS}, volume = {12302}, pages = {518-534}, type = {Conference Paper}, year = {2020}, doi = {10.1007/978-3-030-59152-6_29}, url = { https://publications.rwth-aachen.de/record/833949}, }× [issue]	Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe. Probabilistic Hyperproperties with Nondeterminism, International Symposium on Automated Technology for Verification and Analysis (ATVA 2020), Volume 12302 of LNCS, 518-534, Springer, 2020.
[bibtex] @conference{ATHPNSFSSHA2020, title = {A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata}, author = {Carina Pilch and Maurice Krause and Anne Remke and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {12229}, pages = {381-400}, type = {Conference Paper}, year = {2020}, doi = {10.1007/978-3-030-55754-6_23}, url = { https://publications.rwth-aachen.de/record/833951}, }× [issue]	Carina Pilch, Maurice Krause, Anne Remke, Erika Ábrahám. A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata, 12. NASA Formal Methods Symposium (NFM 2020), Volume 12229 of LNCS, 381-400, Springer, 2020.
[bibtex] @misc{NOFPCRGEA2020, title = {New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)}, author = {Erika Ábrahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {2752}, pages = {178-188}, type = {Invited Abstract}, year = {2020}, doi = {10.18154/RWTH-2021-09565}, url = { https://publications.rwth-aachen.de/record/833961}, }× [issue]	Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks. New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract), Volume 2752 of CEUR Workshop Proceedings, 178-188, RWTH Aachen, 2020.
[bibtex] @unpublished{NOFPCRG2020, title = {New Opportunities for the Formal Proof of Computational Real Geometry?}, author = {Erika Ábrahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks}, pages = {14 Seiten}, type = {Preprint}, year = {2020}, url = { https://arxiv.org/abs/2004.04034}, }× [issue]	Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks. New Opportunities for the Formal Proof of Computational Real Geometry?, 14 Seiten, 2020. https://arxiv.org/abs/2004.04034
2019
[bibtex] @conference{MAROSTVAMBD2019, title = {Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development}, author = {Philipp Berger and Johanna Nellen and Joost-Pieter Katoen and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow}, publisher = {Springer}, booktitle = {LNCS}, volume = {11687}, pages = {59-75}, type = {Conference Paper}, year = {2019}, doi = {10.1007/978-3-030-27008-7_4}, url = { https://publications.rwth-aachen.de/record/767285}, }× [issue]	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, 24. International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019), Volume 11687 of LNCS, 59-75, Springer, 2019.
[bibtex] @conference{OPCM2019, title = {On the Proof Complexity of MCSAT}, author = {Gereon Kremer and Erika Ábrahám and Vijay Ganesh}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {2460}, pages = {10 Seiten}, type = {Conference Paper}, year = {2019}, url = { https://publications.rwth-aachen.de/record/771621}, }× [issue]	Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the Proof Complexity of MCSAT, 4. Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 10 Seiten, RWTH Aachen, 2019.
[bibtex] @conference{OVOMNRA2019, title = {On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract)}, author = {Jasper Kurt Ferdinand Nalbach and Gereon Kremer and Erika Ábrahám}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {2460}, pages = {7 Seiten}, type = {Conference Paper}, year = {2019}, doi = {10.18154/RWTH-CONV-240068}, url = { https://publications.rwth-aachen.de/record/771622}, }× [issue]	Jasper Kurt Ferdinand Nalbach, Gereon Kremer, Erika Ábrahám. On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract), 4. Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 7 Seiten, RWTH Aachen, 2019.
[bibtex] @conference{ECFSRVRAIHS2019, title = {Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems}, author = {Francesco Leofante and Stefan Schupp and Erika Ábrahám and Armando Tacchella}, publisher = {European Council for Modelling and Simulation}, pages = {7 Seiten}, type = {Conference Paper}, year = {2019}, doi = {10.7148/2019-0407}, url = { https://publications.rwth-aachen.de/record/771665}, }× [issue]	Francesco Leofante, Stefan Schupp, Erika Ábrahám, Armando Tacchella. Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems, 33. International ECMS Conference on Modelling and Simulation (ECMS 2019), 7 Seiten, European Council for Modelling and Simulation, 2019.
[bibtex] @article{FICAD2019, title = {Fully Incremental Cylindrical Algebraic Decomposition}, author = {Gereon Kremer and Erika Ábrahám}, publisher = {Elsevier}, journal = {Journal of symbolic computation}, volume = {100}, pages = {pages 11-37}, type = {Journal Article}, year = {2019}, doi = {10.1016/j.jsc.2019.07.018}, url = { https://publications.rwth-aachen.de/record/780485}, }× [issue]	Gereon Kremer, Erika Ábrahám. Fully Incremental Cylindrical Algebraic Decomposition, Journal of symbolic computation 100, pages 11-37, Elsevier, 2019.
2018
[bibtex] @conference{CDRAHS2018, title = {Context-Dependent Reachability Analysis for Hybrid Systems}, author = {Stefan Schupp and Justin Winkens and Erika Ábrahám}, publisher = {IEEE}, pages = {518-525}, type = {Conference Paper}, year = {2018}, doi = {10.1109/IRI.2018.00082}, url = { https://publications.rwth-aachen.de/record/735730}, }× [issue]	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.
[bibtex] @article{MSSR2018, title = {Modular strategic SMT solving with SMT-RAT}, author = {Gereon Kremer and Erika Ábrahám}, publisher = {De Gruyter Open}, journal = {Acta Universitatis Sapientiae / Informatica}, volume = {10(1)}, pages = {pages 5-25}, type = {Journal Article}, year = {2018}, doi = {10.2478/ausi-2018-0001}, url = { https://publications.rwth-aachen.de/record/735737}, }× [issue]	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.
[bibtex] @conference{SWMSAHS2018, title = {Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems}, author = {Stefan Schupp and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {10886}, pages = {89-104}, type = {Conference Paper}, year = {2018}, doi = {10.1007/978-3-319-92970-5_6}, url = { https://publications.rwth-aachen.de/record/741983}, }× [issue]	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.
[bibtex] @conference{EDERHSRA2018, title = {Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis}, author = {Stefan Schupp and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {10806, Part 2}, pages = {287-302}, type = {Conference Paper}, year = {2018}, doi = {10.1007/978-3-319-89963-3_17}, url = { https://publications.rwth-aachen.de/record/745466}, }× [issue]	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.
[bibtex] @conference{VACCSAERAD2018, title = {Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain}, author = {Philipp Berger and Joost-Pieter Katoen and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow}, publisher = {Springer}, booktitle = {LNCS}, volume = {10951}, type = {Conference Paper}, year = {2018}, doi = {10.1007/978-3-319-95582-7_18}, url = { https://publications.rwth-aachen.de/record/753075}, }× [issue]	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, 22. International Symposium on Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.
[bibtex] @conference{FVASCMETCER2018, title = {Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations}, author = {Johanna Nellen and Thomas Rambow and Md Tawhid Bin Waez and Erika Ábrahám and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {10951}, type = {Conference Paper}, year = {2018}, doi = {10.1007/978-3-319-95582-7_23}, url = { https://publications.rwth-aachen.de/record/753076}, }× [issue]	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, 22. International Symposium on Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.
[bibtex] @article{ISEOPMRSL2018, title = {Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics}, author = {Francesco Leofante and Erika Ábrahám and Tim Dieter Niemüller and Gerhard Lakemeyer and Armando Tacchella}, publisher = {Kluwer}, journal = {Information systems frontiers}, volume = {21(1)}, pages = {pages 87-107}, type = {Journal Article}, year = {2018}, doi = {10.1007/s10796-018-9858-3}, url = { https://publications.rwth-aachen.de/record/753080}, }× [issue]	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, Kluwer, 2018.
[bibtex] @conference{TPOAAPL2018, title = {Task Planning with OMT: An Application to Production Logistics}, author = {Francesco Leofante and Erika Ábrahám and Armando Tacchella}, publisher = {Springer}, booktitle = {LNCS}, volume = {11023, Programming and Software Engineering}, pages = {316-325}, type = {Conference Paper}, year = {2018}, doi = {10.1007/978-3-319-98938-9_18}, url = { https://publications.rwth-aachen.de/record/753083}, }× [issue]	Francesco Leofante, Erika Ábrahám, Armando Tacchella. 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.
[bibtex] @conference{HATLPH2018, title = {HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties}, author = {Erika Ábrahám and Borzoo Bonakdarpour}, publisher = {Springer}, booktitle = {LNCS}, volume = {11024, Theoretical Computer Science and General Issues}, type = {Conference Paper}, year = {2018}, doi = {10.1007/978-3-319-99154-2_2}, url = { https://publications.rwth-aachen.de/record/753085}, }× [issue]	Erika Ábrahám, Borzoo Bonakdarpour. 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.
[bibtex] @conference{EECCSS2018, title = {Evaluation of Equational Constraints for CAD in SMT Solving}, author = {Rebecca Haehn and Gereon Kremer and Erika Ábrahám}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {2189}, pages = {[19]-32}, type = {Conference Paper}, year = {2018}, url = { https://publications.rwth-aachen.de/record/753088}, }× [issue]	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.
[bibtex] @proceedings{PPSFMATAP2018, title = {Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)}, author = {}, editor = {Erika Ábrahám and Silvia Lizeth Taipa Tarifa}, booktitle = {Research report / University of Oslo}, volume = {483}, type = {Proceeding Article}, year = {2018}, doi = {10.18154/RWTH-CONV-236485}, url = { https://publications.rwth-aachen.de/record/753093}, }× [issue]	. 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.
[bibtex] @proceedings{AIIWGESEG2018, title = {2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering: GE 2018}, author = {}, editor = {Erika Ábrahám and Elisabetta Di Nitto and Raffaela Mirandola}, publisher = {IEEE}, type = {Proceeding Article}, year = {2018}, url = { https://publications.rwth-aachen.de/record/753094}, }× [issue]	. 2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering: GE 2018, IEEE, 2018.
[bibtex] @misc{SCTSSMBMEH2018, title = {Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics}, author = {Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {10900}, pages = {XII-XII}, type = {Invited Abstract}, year = {2018}, url = { https://publications.rwth-aachen.de/record/753095}, }× [issue]	Erika Ábrahám. Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics, Volume 10900 of LNCS, XII-XII, Springer, 2018.
[bibtex] @conference{THTAPDHSRAM2018, title = {The HyDRA Tool: A Playground for the Development of Hybrid Systems Reachability Analysis Methods}, author = {Stefan Schupp and Erika Ábrahám}, publisher = {Oslo University}, booktitle = {Research report}, volume = {483}, pages = {2 Seiten}, type = {Conference Paper}, year = {2018}, url = { https://publications.rwth-aachen.de/record/767299}, }× [issue]	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
[bibtex] @article{S2017, title = {Satisfiability checking and symbolic computation}, author = {Erika Ábrahám and P. Fontaine and S. Forrest and A. Griggio and D. Kroening and W. M. Seiler and T. Sturm and J. Abbott and B. Becker and A. M. Bigatti and M. Brain and B. Buchberger and A. Cimatti and J. H. Davenport and M. England}, publisher = {ACM}, journal = {ACM Communications in computer algebra}, volume = {50(4)}, pages = {pages 145-147}, type = {Journal Article}, year = {2017}, doi = {10.1145/3055282.3055285}, url = { https://publications.rwth-aachen.de/record/688933}, }× [issue]	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 50 (4), pages 145-147, ACM, 2017.
[bibtex] @conference{DCVSSHSRA2017, title = {Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis}, author = {Stefan Schupp and Johanna Nellen and Erika Ábrahám}, publisher = {[Open Publishing Association]}, booktitle = {EPTCS}, volume = {250}, pages = {1-14}, type = {Conference Paper}, year = {2017}, doi = {10.4204/EPTCS.250.1}, url = { https://publications.rwth-aachen.de/record/696075}, }× [issue]	Stefan Schupp, Johanna Nellen, Erika Ábrahám. Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis, 15. Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2017), Volume 250 of EPTCS, 1-14, [Open Publishing Association], 2017.
[bibtex] @conference{HACLSSRHSRA2017, title = {HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis}, author = {Stefan Schupp and Erika Ábrahám and Ibtissem Ben Makhlouf and Stefan Kowalewski}, publisher = {Springer}, booktitle = {LNCS}, volume = {10227}, pages = {288-294}, type = {Conference Paper}, year = {2017}, doi = {10.1007/978-3-319-57288-8_20}, url = { https://publications.rwth-aachen.de/record/696076}, }× [issue]	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, 288-294, Springer, 2017.
[bibtex] @conference{TTHSRA2017, title = {Techniques and Tools for Hybrid Systems Reachability Analysis}, author = {Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {10381}, pages = {XVI-XVII}, type = {Conference Paper}, year = {2017}, url = { https://publications.rwth-aachen.de/record/696135}, }× [issue]	Erika Ábrahám. Techniques and Tools for Hybrid Systems Reachability Analysis, 10. International Workshop on Numerical Software Verification (NSV 2017), Volume 10381 of LNCS, XVI-XVII, Springer, 2017.
[bibtex] @conference{EVSMMCSCF2017, title = {Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework}, author = {Erika Ábrahám and Jasper Kurt Ferdinand Nalbach and Gereon Kremer}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {1974}, pages = {12 Seiten}, type = {Conference Paper}, year = {2017}, url = { https://publications.rwth-aachen.de/record/713477}, }× [issue]	Erika Ábrahám, Jasper Kurt Ferdinand Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework, 2. International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 12 Seiten, RWTH Aachen, 2017.
[bibtex] @conference{CDPOCADSS2017, title = {Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving}, author = {Tarik Viehmann and Gereon Kremer and Erika Ábrahám}, publisher = {RWTH Aachen}, booktitle = {CEUR Workshop Proceedings}, volume = {1974}, pages = {15 Seiten}, type = {Conference Paper}, year = {2017}, url = { https://publications.rwth-aachen.de/record/713479}, }× [issue]	Tarik Viehmann, Gereon Kremer, Erika Ábrahám. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving, 2. International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 15 Seiten, RWTH Aachen, 2017.
[bibtex] @proceedings{BS2017, title = {Bridging two communities to solve real problems: SC2 2016}, author = {}, editor = {Erika Ábrahám and James H. Davenport and Pascal Fontaine}, publisher = {RWTH Aachen}, booktitle = {CEUR workshop proceedings}, volume = {1804}, pages = {1 Online-Ressource : Illustrationen}, type = {Proceeding Article}, year = {2017}, url = { https://publications.rwth-aachen.de/record/713481}, }× [issue]	. Bridging two communities to solve real problems: SC2 2016, Volume 1804 of CEUR workshop proceedings, 1 Online-Ressource : Illustrationen, RWTH Aachen, 2017.
[bibtex] @conference{SSCSC2017, title = {SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces}, author = {Erika Ábrahám and John Abbott and Bernd Becker and Anna M. Bigatti and Martin Brain and Alessandro Cimatti and James H. Davenport and Matthew England and Pascal Fontaine and Stephen Forrest and Vijay Ganesh and Alberto Griggio and Daniel Kroening and Werner M. Seiler}, publisher = {EasyChair}, booktitle = {EPiC Series in Computing}, volume = {51}, pages = {6-10}, type = {Conference Paper}, year = {2017}, doi = {10.29007/p319}, url = { https://publications.rwth-aachen.de/record/713487}, }× [issue]	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, 1. International Workshop on Automated Reasoning: Challenges, Applications, Directions (ARCADE 2017), Volume 51 of EPiC Series in Computing, 6-10, EasyChair, 2017.
[bibtex] @conference{OSGQPRFLSOMT2017, title = {On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories}, author = {Francesco Leofante and Erika Ábrahám and Tim Dieter Niemüller and Gerhard Lakemeyer and Armando Tacchella}, publisher = {IEEE}, pages = {403-410}, type = {Conference Paper}, year = {2017}, doi = {10.1109/IRI.2017.67}, url = { https://publications.rwth-aachen.de/record/713493}, }× [issue]	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), 403-410, IEEE, 2017.
[bibtex] @proceedings{PIWSNMRA2017, title = {Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis}, author = {}, editor = {Erika Ábrahám and Sergiy Bogomolov}, publisher = {[Open Publishing Association]}, booktitle = {EPTCS}, volume = {247}, pages = {1 Online-Ressource : Illustrationen}, type = {Proceeding Article}, year = {2017}, url = { https://publications.rwth-aachen.de/record/713497}, }× [issue]	. Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, Volume 247 of EPTCS, 1 Online-Ressource : Illustrationen, [Open Publishing Association], 2017.
[bibtex] @article{CAERASDS2017, title = {Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071)}, author = {Armando Tacchella}, editor = {Erika Ábrahám and Hadas Kress-Gazit and Lorenzo Natale}, publisher = {Schloss Dagstuhl}, journal = {Dagstuhl Reports}, volume = {7(2)}, pages = {pages 48-63}, type = {Journal Article}, year = {2017}, doi = {10.4230/DagRep.7.2.48}, url = { https://publications.rwth-aachen.de/record/713498}, }× [issue]	Armando Tacchella. Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071), Dagstuhl Reports 7 (2), pages 48-63, Schloss Dagstuhl, 2017.
[bibtex] @conference{TCTEMSDO2017, title = {Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization}, author = {Tim Dieter Niemüller and Gerhard Lakemeyer and Francesco Leofante and Erika Ábrahám}, pages = {60-67}, type = {Conference Paper}, year = {2017}, url = { https://publications.rwth-aachen.de/record/713532}, }× [issue]	Tim Dieter Niemüller, Gerhard Lakemeyer, Francesco Leofante, Erika Ábrahám. Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization, 5. Workshop on Planning and Robotics (PlanRob 2017), 60-67, 2017.
[bibtex] @conference{P2017, title = {Preface}, author = {Erika Ábrahám and Sergiy Bogomolov}, publisher = {[Open Publishing Association]}, booktitle = {EPTCS}, volume = {247}, type = {Conference Paper}, year = {2017}, url = { https://publications.rwth-aachen.de/record/720626}, }× [issue]	Erika Ábrahám, Sergiy Bogomolov. Preface, 3. International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), Volume 247 of EPTCS, [Open Publishing Association], 2017.
[bibtex] @unpublished{PIWSNMRA2017, title = {Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis}, author = {}, editor = {Erika Ábrahám and Sergiy Bogomolov}, publisher = {[Open Publishing Association]}, pages = {1 Online-Ressource : Illustrationen}, type = {Preprint}, year = {2017}, doi = {10.4204/EPTCS.247}, url = { https://arxiv.org/abs/1704.02421}, }× [issue]	. Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, 1 Online-Ressource : Illustrationen, [Open Publishing Association], 2017. https://arxiv.org/abs/1704.02421
[bibtex] @conference{SSATTTS2017, title = {SMT Solving for Arithmetic Theories: Theory and Tool Support}, author = {Erika Ábrahám and Gereon Kremer}, publisher = {IEEE}, pages = {1-8}, type = {Conference Paper}, year = {2017}, doi = {10.1109/SYNASC.2017.00009}, url = { https://publications.rwth-aachen.de/record/780487}, }× [issue]	Erika Ábrahám, Gereon Kremer. SMT Solving for Arithmetic Theories: Theory and Tool Support, 19. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), 1-8, IEEE, 2017.
[bibtex] @conference{TCTEMSPO2017, title = {Towards CLIPS-based Task Execution and Monitoring with SMT-based Planning and Optimization}, author = {Tim Dieter Niemüller and Gerhard Lakemeyer and Francesco Leofante and Erika Ábrahám}, type = {Conference Paper}, year = {2017}, url = { https://publications.rwth-aachen.de/record/809638}, }× [issue]	Tim Dieter Niemüller, Gerhard Lakemeyer, Francesco Leofante, Erika Ábrahám. Towards CLIPS-based Task Execution and Monitoring with SMT-based Planning and Optimization, 5. Workshop on Planning and Robotics at ICAPS (PLANROB 2017), 2017.
[bibtex] @conference{AHPH2017, title = {Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro}, author = {Jannik Hüls and Stefan Schupp and Anne Remke and Erika Ábrahám}, publisher = {ACM}, booktitle = {ICPS: ACM international conference proceeding series}, pages = {178-185}, type = {Conference Paper}, year = {2017}, doi = {10.1145/3150928.3150938}, url = { https://publications.rwth-aachen.de/record/814253}, }× [issue]	Jannik Hüls, Stefan Schupp, Anne Remke, Erika Ábrahám. Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro, 11. EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS 2017), ICPS: ACM international conference proceeding series, 178-185, ACM, 2017.
2016
[bibtex] @article{LL2016, title = {Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis}, author = {Mohamed Amin Ben Sassi and Sriram Sankaranarayanan and Xin Chen and Erika Ábrahám}, publisher = {Univ. Press}, journal = {IMA journal of mathematical control and information}, volume = {33(3)}, pages = {pages 723-756}, type = {Journal Article}, year = {2016}, doi = {10.1093/imamci/dnv003}, url = { https://publications.rwth-aachen.de/record/571421}, }× [issue]	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.
[bibtex] @conference{AGBBAIASMNIA2016, title = {A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic}, author = {Gereon Kremer and Florian Corzilius and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {9890}, pages = {315-335}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-45641-6_21}, url = { https://publications.rwth-aachen.de/record/670551}, }× [issue]	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, 315-335, Springer, 2016.
[bibtex] @article{TCP2016, title = {Two CEGAR-based approaches for the safety verification of PLC-controlled plants}, author = {Johanna Nellen and Kai Driessen and Martin Neuhäußer and Erika Ábrahám and Benedikt Wolters}, publisher = {Springer}, journal = {Information systems frontiers}, volume = {18(5)}, pages = {pages 927-952}, type = {Journal Article}, year = {2016}, doi = {10.1007/s10796-016-9671-9}, url = { https://publications.rwth-aachen.de/record/670652}, }× [issue]	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 18 (5), pages 927-952, Springer, 2016.
[bibtex] @article{S2016, title = {Some recent advances in automated analysis}, author = {Erika Ábrahám and Klaus Havelund}, publisher = {Springer}, journal = {International journal on software tools for technology transfer}, volume = {18(2)}, pages = {pages 121-128}, type = {Journal Article}, year = {2016}, doi = {10.1007/s10009-015-0403-0}, url = { https://publications.rwth-aachen.de/record/679253}, }× [issue]	Erika Ábrahám, Klaus Havelund. Some recent advances in automated analysis, International journal on software tools for technology transfer 18 (2), pages 121-128, Springer, 2016.
[bibtex] @conference{SSCMSC2016, title = {SC2: Satisfiability Checking Meets Symbolic Computation}, author = {Erika Ábrahám and John Abbott and Bernd Becker and Anna M. Bigatti and Martin Brain and Bruno Buchberger and Alessandro Cimatti and James H. Davenport and Matthew England and Pascal Fontaine and Stephen Forrest and Alberto Griggio and Daniel Kroening and Werner M. Seiler and Thomas Sturm}, publisher = {Springer}, booktitle = {LNCS}, volume = {9791}, pages = {28-43}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-42547-4_3}, url = { https://publications.rwth-aachen.de/record/681150}, }× [issue]	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, 9. International Conference on Intelligent Computer Mathematics (CICM 2016), Volume 9791 of LNCS, 28-43, Springer, 2016.
[bibtex] @conference{ZOFDOUSCT2016, title = {Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies}, author = {Erika Ábrahám and Florian Corzilius and Einar Broch Johnsen and Gereon Kremer and Jacopo Mauro}, publisher = {Springer}, booktitle = {LNCS}, volume = {9984}, pages = {229-245}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-47677-3_15}, url = { https://publications.rwth-aachen.de/record/681504}, }× [issue]	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, 229-245, Springer, 2016.
[bibtex] @conference{CSRMASSUHR2016, title = {Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots}, author = {Francesco Leofante and Simone Vuotto and Erika Ábrahám and Armando Tacchella and Nils Jansen}, publisher = {Springer}, booktitle = {LNCS}, volume = {9952}, pages = {496-514}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-47166-2_34}, url = { https://publications.rwth-aachen.de/record/682004}, }× [issue]	Francesco Leofante, Simone Vuotto, Erika Ábrahám, Armando Tacchella, Nils Jansen. Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots, 7. International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), Volume 9952 of LNCS, 496-514, Springer, 2016.
[bibtex] @book{TFB2016, title = {Theory and practice of formal methods: essays dedicated to Frank de Boer on the occasion of his 60th birthday}, author = {}, editor = {Erika Ábrahám and Marcello Bonsangue and Einar Broch Johnsen}, publisher = {Springer}, booktitle = {LNCS}, volume = {9660}, pages = {XII, 427 Seiten : Illustrationen}, type = {Book}, year = {2016}, doi = {10.1007/978-3-319-30734-3}, url = { https://publications.rwth-aachen.de/record/683000}, }× [issue]	Erika Ábrahám (ed), Marcello Bonsangue (ed), Einar Broch Johnsen (ed). Theory and practice of formal methods: essays dedicated to Frank de Boer on the occasion of his 60th birthday, Volume 9660 of LNCS, XII, 427 Seiten : Illustrationen, Springer, 2016.
[bibtex] @conference{HFLOEA2016, title = {Heliostat Field Layout Optimization with Evolutionary Algorithms}, author = {Pascal Richter and David Laukamp and Levin Gerdes and Martin Frank and Erika Ábrahám}, publisher = {[Cool Press Ltd]}, booktitle = {EPiC Series in Computing}, volume = {41}, pages = {240-252}, type = {Conference Paper}, year = {2016}, url = { https://publications.rwth-aachen.de/record/683003}, }× [issue]	Pascal Richter, David Laukamp, Levin Gerdes, Martin Frank, Erika Ábrahám. Heliostat Field Layout Optimization with Evolutionary Algorithms, 2. GlobalConference on Artifcial Intelligence (GCAI 2016), Volume 41 of EPiC Series in Computing, 240-252, [Cool Press Ltd], 2016.
[bibtex] @conference{SCTA2016, title = {Satisfiability Checking: Theory and Applications}, author = {Erika Ábrahám and Gereon Kremer}, publisher = {Springer}, booktitle = {LNCS}, volume = {9763}, pages = {9-23}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-41591-8_2}, url = { https://publications.rwth-aachen.de/record/683011}, }× [issue]	Erika Ábrahám, Gereon Kremer. Satisfiability Checking: Theory and Applications, Software Engineering and Formal Methods : 14. International Conference (SEFM 2016), Volume 9763 of LNCS, 9-23, Springer, 2016.
[bibtex] @book{PWSNMRAS2016, title = {Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR)}, author = {}, editor = {Erika Ábrahám and Sergiy Bogomolov}, publisher = {IEEE}, type = {Book}, year = {2016}, doi = {10.1109/SNR.2016.7479374}, url = { https://publications.rwth-aachen.de/record/683014}, }× [issue]	Erika Ábrahám (ed), Sergiy Bogomolov (ed). Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), IEEE, 2016.
[bibtex] @book{I2016, title = {Integrated formal methods}, author = {}, editor = {Erika Ábrahám and Marieke Huisman}, publisher = {Springer}, booktitle = {LNCS}, volume = {9681}, pages = {XIV, 538 Seiten : Illustrationen, Diagramme}, type = {Book}, year = {2016}, doi = {10.1007/978-3-319-33693-0}, url = { https://publications.rwth-aachen.de/record/683017}, }× [issue]	Erika Ábrahám (ed), Marieke Huisman (ed). Integrated formal methods, Volume 9681 of LNCS, XIV, 538 Seiten : Illustrationen, Diagramme, Springer, 2016.
[bibtex] @conference{P2016, title = {Parameter synthesis for probabilistic systems}, author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám}, publisher = {Albert-Ludwigs-Universität}, pages = {72-74}, type = {Conference Paper}, year = {2016}, doi = {10.6094/UNIFR/10639}, url = { https://publications.rwth-aachen.de/record/683021}, }× [issue]	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.
[bibtex] @article{SCSCRDS2016, title = {Symbolic Computation and Satisfiability Checking: Report of Dagstuhl Seminar 15471}, author = {Erika Ábrahám and Pascal Fontaine and Thomas Sturm and Dongming Wang}, publisher = {Schloss Dagstuhl}, journal = {Dagstuhl reports}, volume = {5(11)}, pages = {pages 71-89}, type = {Journal Article}, year = {2016}, doi = {10.4230/DagRep.5.11.71}, url = { https://publications.rwth-aachen.de/record/683051}, }× [issue]	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, Schloss Dagstuhl, 2016.
[bibtex] @conference{SCTSC2016, title = {Symbolic Computation Techniques in Satisfiability Checking}, author = {Erika Ábrahám}, publisher = {IEEE}, pages = {3-10}, type = {Conference Paper}, year = {2016}, doi = {10.1109/SYNASC.2016.014}, url = { https://publications.rwth-aachen.de/record/696073}, }× [issue]	Erika Ábrahám. Symbolic Computation Techniques in Satisfiability Checking, 18. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 3-10, IEEE, 2016.
[bibtex] @unpublished{S2016, title = {Satisfiability checking and symbolic computation}, author = {Erika Ábrahám and P. Fontaine and S. Forrest and A. Griggio and D. Kroening and W. M. Seiler and T. Sturm and J. Abbott and B. Becker and A. M. Bigatti and M. Brain and B. Buchberger and A. Cimatti and J. H. Davenport and M. England}, pages = {3 Seiten : Illustrationen}, type = {Preprint}, year = {2016}, url = { https://arxiv.org/abs/1607.06945}, }× [issue]	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, 3 Seiten : Illustrationen, 2016. https://arxiv.org/abs/1607.06945
2015
[bibtex] @article{HCPA2015, title = {High-level Counterexamples for Probabilistic Automata}, author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen}, publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig}, journal = {Logical methods in computer science}, volume = {11(1)}, pages = {pages 15}, type = {Journal Article}, year = {2015}, doi = {10.2168/LMCS-11(1:15)2015}, url = { https://publications.rwth-aachen.de/record/540624}, }× [issue]	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, Department of Theoretical Computer Science, Technical University of Braunschweig, 2015.
[bibtex] @conference{CER2015, title = {Counterexamples for Expected Rewards}, author = {Tim Quatmann and Nils Jansen and Hans Christian Dehnert and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, publisher = {Springer}, booktitle = {LNCS}, volume = {9109}, pages = {435-452}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-19249-9_27}, url = { https://publications.rwth-aachen.de/record/541095}, }× [issue]	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.
[bibtex] @conference{ABSHSRA2015, title = {A Benchmark Suite for Hybrid Systems Reachability Analysis}, author = {Xin Chen and Stefan Schupp and Ibtissem Ben Makhlouf and Erika Ábrahám and Goran Frehse and Stefan Kowalewski}, publisher = {Springer}, booktitle = {LNCS}, volume = {9058}, pages = {408-414}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-17524-9_29}, url = { https://publications.rwth-aachen.de/record/541100}, }× [issue]	Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse, Stefan Kowalewski. A Benchmark Suite for Hybrid Systems Reachability Analysis, 7. International Symposium Formal Methods (NFM 2015), Volume 9058 of LNCS, 408-414, Springer, 2015.
[bibtex] @conference{BBSCSC2015, title = {Building Bridges between Symbolic Computation and Satisfiability Checking}, author = {Erika Ábrahám}, publisher = {ACM Press}, pages = {6 S.}, type = {Conference Paper}, year = {2015}, doi = {10.1145/2755996.2756636}, url = { https://publications.rwth-aachen.de/record/561679}, }× [issue]	Erika Ábrahám. Building Bridges between Symbolic Computation and Satisfiability Checking, 14. International Symposium on Symbolic and Algebraic Computation (ISSAC'15), 6 S., ACM Press, 2015.
[bibtex] @conference{SROSCTSPSS2015, title = {SMT-RAT: an Open Source C++ Toolbox for Strategic and Parallel SMT Solving}, author = {Florian Corzilius and Gereon Kremer and Sebastian Junges and Stefan Schupp and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {9340}, pages = {360-368}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-24318-4_26}, url = { https://publications.rwth-aachen.de/record/561680}, }× [issue]	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, 360-368, Springer, 2015.
[bibtex] @conference{AGAERSM2015, title = {A Greedy Approach for the Efficient Repair of Stochastic Models}, author = {Shashank Pathak and Erika Ábrahám and Nils Jansen and Armando Tacchella and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {9058}, pages = {295-309}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-17524-9_21}, url = { https://publications.rwth-aachen.de/record/561930}, }× [issue]	Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, 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.
[bibtex] @inbook{ACTRAPCPUHA2015, title = {A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata}, author = {Johanna Nellen and Erika Ábrahám and Benedikt Wolters}, publisher = {Springer}, booktitle = {Advances in Intelligent Systems and Computing}, volume = {346}, pages = {55-78}, type = {Book Chapter}, year = {2015}, doi = {10.1007/978-3-319-16577-6_3}, url = { https://publications.rwth-aachen.de/record/561931}, }× [issue]	Johanna Nellen, Erika Ábrahám, Benedikt Wolters. A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata, Volume 346 of Advances in Intelligent Systems and Computing, 55-78, Springer, 2015.
[bibtex] @conference{PAPPST2015, title = {PROPhESY: A PRObabilistic ParamEter SYnthesis Tool}, author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {9206}, pages = {214-231}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-21690-4_13}, url = { https://publications.rwth-aachen.de/record/564236}, }× [issue]	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.
[bibtex] @conference{CCVHS2015, title = {Current Challenges in the Verification of Hybrid Systems}, author = {Stefan Schupp and Erika Ábrahám and Xin Chen and Ibtissem Ben Makhlouf and Goran Frehse and Sriram Sankaranarayanan and Stefan Kowalewski}, publisher = {Springer}, booktitle = {LNCS}, volume = {9361}, pages = {8-24}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-25141-7_2}, url = { https://publications.rwth-aachen.de/record/564375}, }× [issue]	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] @conference{FMEPHS2015, title = {Flow* 1.2: More Effective to Play with Hybrid Systems}, author = {Xin Chen and Sriram Sankaranarayanan and Erika Ábrahám}, publisher = {EasyChair}, booktitle = {EPiC Series in Computer Science}, volume = {34}, pages = {152-159}, type = {Conference Paper}, year = {2015}, url = { https://publications.rwth-aachen.de/record/565595}, }× [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.
[bibtex] @conference{AGACSEMPP2015, title = {A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs}, author = {Johanna Nellen and Benedikt Wolters and Lukas Stephan Michael Netz and Sascha Geulen and Erika Ábrahám}, publisher = {EasyChair}, booktitle = {EPiC series in computing}, volume = {36}, pages = {196-214}, type = {Conference Paper}, year = {2015}, url = { https://publications.rwth-aachen.de/record/565596}, }× [issue]	Johanna Nellen, Benedikt Wolters, Lukas Stephan Michael Netz, Sascha Geulen, Erika Ábrahám, Martina Joševski, Dirk Abel. A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs, 1. Global Conference on Artificial Intelligence (GCAI'15), Volume 36 of EPiC series in computing, 196-214, EasyChair, 2015.
[bibtex] @unpublished{CRPHAE2015, title = {Challenges and Recommendations for Preparing HPC Applications for Exascale}, author = {Erika Ábrahám and Costas Bekas and Ivona Brandic and Samir Genaim and Einar Broch Johnsen and Ivan Kondov and Sabri Pllana and Achim Streit}, pages = {6 Seiten}, type = {Preprint}, year = {2015}, url = { https://arxiv.org/abs/1503.06974}, }× [issue]	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, 6 Seiten, 2015. https://arxiv.org/abs/1503.06974
[bibtex] @conference{OLKH2015, title = {Online Lernen als Kontrollstrategie in Hybridfahrzeugen}, author = {Sascha Geulen and Martina Joševski and Johanna Nellen and Janosch Fuchs and Lukas Stephan Michael Netz and Benedikt Wolters and Erika Ábrahám and Walter Unger and Dirk Abel}, publisher = {VDI-Verl.}, booktitle = {VDI-Berichte}, volume = {2233}, pages = {101-112}, type = {Conference Paper}, year = {2015}, url = { https://publications.rwth-aachen.de/record/571422}, }× [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.
[bibtex] @conference{PHAECR2015, title = {Preparing HPC Applications for Exascale: Challenges and Recommendations}, author = {Erika Ábrahám and Costas Bekas and Ivona Brandic and Samir Genaim and Einar Broch Johnsen and Ivan Kondov and Sabri Pllana and Achim Streit}, publisher = {IEEE}, pages = {401-406}, type = {Conference Paper}, year = {2015}, doi = {10.1109/NBiS.2015.61}, url = { https://publications.rwth-aachen.de/record/571423}, }× [issue]	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, 18. International Conference on Network-Based Information Systems (NBiS 2015), 401-406, IEEE, 2015.
[bibtex] @conference{LCSHEV2015, title = {Learning-based Control Strategies for Hybrid Electric Vehicles}, author = {Sascha Geulen and Martina Josevski and Johanna Nellen and Janosch Fuchs and Lukas Stephan Michael Netz and Benedikt Wolters and Dirk Abel and Erika Ábrahám and Walter Unger}, publisher = {IEEE}, pages = {1722-1728}, type = {Conference Paper}, year = {2015}, doi = {10.1109/CCA.2015.7320858}, url = { https://publications.rwth-aachen.de/record/667226}, }× [issue]	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
[bibtex] @conference{CGDTMMAIS2014, title = {Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey}, author = {Erika Ábrahám and Bernd Becker and Hans Christian Dehnert and Nils Jansen and Joost-Pieter Katoen and Ralf Wimmer}, publisher = {Springer}, booktitle = {LNCS}, volume = {8483}, pages = {65-121}, type = {Conference Paper}, year = {2014}, doi = {10.1007/978-3-319-07317-0_3}, url = { https://publications.rwth-aachen.de/record/443312}, }× [issue]	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.
[bibtex] @conference{MMCSV2014, title = {Maybe or Maybe not: Contributions to Stochastic Verification}, author = {Ralf Wimmer and Erika Ábrahám}, publisher = {Monsenstein und Vannerdat}, pages = {119-127}, type = {Conference Paper}, year = {2014}, url = { https://publications.rwth-aachen.de/record/443585}, }× [issue]	Ralf Wimmer, Erika Ábrahám. Maybe or Maybe not: Contributions to Stochastic Verification, Aspekte der Technischen Informatik : Festschrift zum 60. Geburtstag von Bernd Becker, 119-127, Monsenstein und Vannerdat, 2014.
[bibtex] @conference{UFNCS2014, title = {Under-approximate Flowpipes for Non-linear Continuous Systems}, author = {Xin Chen and Sriram Sankaranarayanan and Erika Ábrahám}, publisher = {IEEE}, booktitle = {ACM Other conferences}, pages = {59-66}, type = {Conference Paper}, year = {2014}, url = { https://publications.rwth-aachen.de/record/444150}, }× [issue]	Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám. Under-approximate Flowpipes for Non-linear Continuous Systems, 2014 Formale Methoden im Computer Aided Design (FMCAD 2014), ACM Other conferences, 59-66, IEEE, 2014.
[bibtex] @conference{M2014, title = {Multi-objective optimization of solar tower power plants}, author = {Pascal Richter and Martin Frank and Erika Ábrahám}, publisher = {Springer}, booktitle = {Mathematics in industry}, type = {Conference Paper}, year = {2014}, url = { https://publications.rwth-aachen.de/record/444449}, }× [issue]	Pascal Richter, Martin Frank, Erika Ábrahám. Multi-objective optimization of solar tower power plants, 18. European Conference on Mathematics for Industry (ECMI'14), Mathematics in industry, Springer, 2014.
[bibtex] @article{SCTCMCTKSRTRT2014, title = {Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories}, author = {Daniela Lepri and Erika Ábrahám and Peter Csaba Ölveczky}, publisher = {Elsevier}, journal = {Science of computer programming}, volume = {99}, pages = {pages 128-192}, type = {Journal Article}, year = {2014}, doi = {10.1016/j.scico.2014.06.006}, url = { https://publications.rwth-aachen.de/record/445441}, }× [issue]	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, Elsevier, 2014.
[bibtex] @article{SM2014, title = {Symbolic counterexample generation for large discrete-time Markov chains}, author = {Nils Jansen and Ralf Wimmer and Erika Ábrahám and Barna Zajzon and Joost-Pieter Katoen and Bernd Becker and Johann Schuster}, publisher = {Elsevier}, journal = {Science of computer programming}, volume = {91(Part A)}, pages = {pages 90-114}, type = {Journal Article}, year = {2014}, doi = {10.1016/j.scico.2014.02.001}, url = { https://publications.rwth-aachen.de/record/445537}, }× [issue]	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.
[bibtex] @article{FHMWSWC2014, title = {Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?}, author = {Muhammad Fadlisyah and Peter Csaba Ölveczky and Erika Ábrahám}, publisher = {Elsevier}, journal = {Science of computer programming}, type = {Journal Article}, year = {2014}, doi = {10.1016/j.scico.2014.06.010}, url = { https://publications.rwth-aachen.de/record/445943}, }× [issue]	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, Elsevier, 2014.
[bibtex] @article{M2014, title = {Minimal counterexamples for linear-time probabilistic verification}, author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, publisher = {Elsevier}, journal = {Theoretical computer science}, volume = {549}, pages = {pages 61-100}, type = {Journal Article}, year = {2014}, doi = {10.1016/j.tcs.2014.06.020}, url = { https://publications.rwth-aachen.de/record/447343}, }× [issue]	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.
[bibtex] @conference{FDPM2014, title = {Fast Debugging of PRISM Models}, author = {Hans Christian Dehnert and Nils Jansen and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {8837}, pages = {146-162}, type = {Conference Paper}, year = {2014}, doi = {10.1007/978-3-319-11936-6_11}, url = { https://publications.rwth-aachen.de/record/460136}, }× [issue]	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.
[bibtex] @conference{APPV2014, title = {Accelerating Parametric Probabilistic Verification}, author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, publisher = {Springer}, booktitle = {LNCS}, volume = {8657}, pages = {404-420}, type = {Conference Paper}, year = {2014}, doi = {10.1007/978-3-319-10696-0_31}, url = { https://publications.rwth-aachen.de/record/540007}, }× [issue]	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.
[bibtex] @book{F2014, title = {Formal techniques for distributed objects, components, and systems}, author = {}, editor = {Erika Ábrahám and Catuscia Palamidessi}, publisher = {Springer}, booktitle = {LNCS}, volume = {8461}, pages = {XII, 299 S.}, type = {Book}, year = {2014}, doi = {10.1007/978-3-662-43613-4}, url = { https://publications.rwth-aachen.de/record/561681}, }× [issue]	Erika Ábrahám (ed), Catuscia Palamidessi (ed). Formal techniques for distributed objects, components, and systems, Volume 8461 of LNCS, XII, 299 S., Springer, 2014.
[bibtex] @article{OIBI2014, title = {Observable Interface Behaviour and Inheritance}, author = {Erika Ábrahám and Thi Mai Thuong Tran and Martin Steffen}, publisher = {Cambridge Univ. Press}, journal = {Mathematical structures in computer science}, volume = {26(Special Issue 03)}, pages = {pages 561-605}, type = {Journal Article}, year = {2014}, doi = {10.1017/S0960129514000255}, url = { https://publications.rwth-aachen.de/record/561682}, }× [issue]	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.
[bibtex] @conference{ACARAPCP2014, title = {A CEGAR Approach for the Reachability Analysis of PLC-controlled Chemical Plants}, author = {Johanna Nellen and Erika Ábrahám}, publisher = {IEEE}, pages = {500-507}, type = {Conference Paper}, year = {2014}, doi = {10.1109/IRI.2014.7051930}, url = { https://publications.rwth-aachen.de/record/561928}, }× [issue]	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), 500-507, IEEE, 2014.
[bibtex] @conference{CGHA2014, title = {Counterexample Generation for Hybrid Automata}, author = {Johanna Nellen and Erika Ábrahám and Xin Chen and Pieter Collins}, publisher = {Springer}, booktitle = {Communications in Computer and Information Science}, volume = {419}, pages = {88-106}, type = {Conference Paper}, year = {2014}, doi = {10.1007/978-3-319-05416-2_7}, url = { https://publications.rwth-aachen.de/record/561929}, }× [issue]	Johanna Nellen, Erika Ábrahám, Xin Chen, Pieter Collins. 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.
[bibtex] @article{RTHMCI2014, title = {Randomized Timed and Hybrid Models for Critical Infrastructures}, author = {}, editor = {Erika Ábrahám and Alberto Avritzer and Anne Remke and William H. Sanders}, publisher = {Schloss Dagstuhl}, journal = {Dagstuhl Reports}, volume = {4(1)}, pages = {pages 37-82}, type = {Journal Article}, year = {2014}, doi = {10.4230/DagRep.4.1.36}, url = { https://publications.rwth-aachen.de/record/564382}, }× [issue]	. Randomized Timed and Hybrid Models for Critical Infrastructures, Dagstuhl Reports 4 (1), pages 37-82, Schloss Dagstuhl, 2014.
[bibtex] @book{TACAS2014, title = {Tools and Algorithms for the Construction and Analysis of Systems}, author = {}, editor = {Erika Ábrahám and Klaus Havelund}, publisher = {Springer}, booktitle = {LNCS}, volume = {8413}, pages = {XVIII, 652 S. : graph. Darst.}, type = {Book}, year = {2014}, doi = {10.1007/978-3-642-54862-8}, url = { https://publications.rwth-aachen.de/record/564383}, }× [issue]	Erika Ábrahám (ed), Klaus Havelund (ed). Tools and Algorithms for the Construction and Analysis of Systems, Volume 8413 of LNCS, XVIII, 652 S. : graph. Darst., Springer, 2014.
2013
[bibtex] @unpublished{HCPA2013, title = {High-level Counterexamples for Probabilistic Automata}, author = {Ralf Wimmer and Nils Jansen and Andreas Vorpahl and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, publisher = {Cornell University}, type = {Preprint}, year = {2013}, url = { https://arxiv.org/abs/1305.5055}, }× [issue]	Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata, Cornell University, 2013. https://arxiv.org/abs/1305.5055
[bibtex] @conference{ASICPCAD2013, title = {A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition}, author = {Ulrich Loup and Karsten Scheibler and Florian Corzilius and Erika Ábrahám and Bernd Becker}, publisher = {Springer}, booktitle = {LNCS}, volume = {7898}, pages = {193-207}, type = {Conference Paper}, year = {2013}, doi = {10.1007/978-3-642-38574-2_13}, url = { https://publications.rwth-aachen.de/record/207654}, }× [issue]	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, 193-207, Springer, 2013.
[bibtex] @conference{EFCAC2013, title = {Empirical Flowpipe Constructions for Analog Circuits}, author = {Yan Zhang and Xin Chen and Sriram Sankaranarayanan and Erika Ábrahám}, type = {Conference Paper}, year = {2013}, url = { https://publications.rwth-aachen.de/record/209164}, }× [issue]	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] @conference{ATCMCRTM2013, title = {A Timed CTL Model Checker for Real-Time Maude}, author = {Daniela Lepri and Erika Ábrahám and Peter Csaba Ölveczky}, publisher = {Springer}, booktitle = {LNCS}, volume = {8089}, pages = {334-339}, type = {Conference Paper}, year = {2013}, doi = {10.1007/978-3-642-40206-7_27}, url = { https://publications.rwth-aachen.de/record/225701}, }× [issue]	Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky. A Timed CTL Model Checker for Real-Time Maude, Algebra and Coalgebra in Computer Science : 5. International Conference (CALCO 2013), Volume 8089 of LNCS, 334-339, Springer, 2013.
[bibtex] @conference{FAANLHS2013, title = {Flow*: An Analyzer for Non-Linear Hybrid Systems}, author = {Xin Chen and Erika Ábrahám and Sriram Sankaranarayanan}, publisher = {Springer}, booktitle = {LNCS}, volume = {8044}, pages = {258-263}, type = {Conference Paper}, year = {2013}, doi = {10.1007/978-3-642-39799-8_18}, url = { https://publications.rwth-aachen.de/record/225803}, }× [issue]	Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan. Flow: An Analyzer for Non-Linear Hybrid Systems*, Computer aided verification : 25. International conference (CAV), Volume 8044 of LNCS, 258-263, Springer, 2013.
[bibtex] @conference{SBMCBRC2013, title = {Stochastic Bounded Model Checking: Bounded Rewards and Compositionality}, author = {Bettina Braitling and Ralf Wimmer and Bernd Becker and Erika Ábrahám}, publisher = {Univ., ITMZ}, pages = {243-254}, type = {Conference Paper}, year = {2013}, url = { https://publications.rwth-aachen.de/record/226121}, }× [issue]	Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám. Stochastic Bounded Model Checking: Bounded Rewards and Compositionality, MBMV 2013, 243-254, Univ., ITMZ, 2013.
[bibtex] @conference{LFSHR2013, title = {Lyapunov Function Synthesis using Handelman Representations}, author = {Sriram Sankaranarayanan and Xin Chen and Erika Ábrahám}, publisher = {Elsevier}, booktitle = {Nonlinear Control Systems}, volume = {9,1}, pages = {576-581}, type = {Conference Paper}, year = {2013}, doi = {10.3182/20130904-3-FR-2041.00198}, url = { https://publications.rwth-aachen.de/record/226223}, }× [issue]	Sriram Sankaranarayanan, Xin Chen, Erika Ábrahám. Lyapunov Function Synthesis using Handelman Representations, 9. IFAC Symposium on Nonlinear Control Systems 2013, Volume 9,1 of Nonlinear Control Systems, 576-581, Elsevier, 2013.
[bibtex] @conference{HCPA2013, title = {High-level Counterexamples for Probabilistic Automata}, author = {Ralf Wimmer and Nils Jansen and Andreas Vorpahl and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, publisher = {Springer}, booktitle = {LNCS}, volume = {8054}, pages = {39-54}, type = {Conference Paper}, year = {2013}, doi = {10.1007/978-3-642-40196-1_4}, url = { https://publications.rwth-aachen.de/record/226401}, }× [issue]	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.
[bibtex] @conference{OGBCSMTSRN2013, title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers}, author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {8080}, pages = {186-198}, type = {Conference Paper}, year = {2013}, doi = {10.1007/978-3-642-40663-8_18}, url = { https://publications.rwth-aachen.de/record/226897}, }× [issue]	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 : 5. international conference (CAI 2013), Volume 8080 of LNCS, 186-198, Springer, 2013.
[bibtex] @techreport{OGBCSMTSRN2013, title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers}, author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám}, publisher = {Shaker [u.a.]}, booktitle = {Aachener Informatik-Berichte : AIB}, volume = {2013,08}, pages = {3-21}, type = {Tech Report}, year = {2013}, url = { https://publications.rwth-aachen.de/record/228582}, }× [issue]	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, 3-21, Shaker [u.a.], 2013.
[bibtex] @unpublished{APPV2013, title = {Accelerating Parametric Probabilistic Verification}, author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, pages = {21 Seiten}, type = {Preprint}, year = {2013}, url = { https://arxiv.org/abs/1312.3979}, }× [issue]	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
[bibtex] @conference{FSMCSMICEPVAC2013, title = {From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits}, author = {Yan Zhang and Xin Chen and Sriram Sankaranarayanan and Fabio Somenzi and Erika Ábrahám}, publisher = {IEEE}, pages = {662-669}, type = {Conference Paper}, year = {2013}, doi = {10.1109/ICCAD.2013.6691186}, url = { https://publications.rwth-aachen.de/record/444173}, }× [issue]	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), 662-669, IEEE, 2013.
2012
[bibtex] @conference{MCSDTMM2012, title = {Minimal Critical Subsystems for Discrete-Time Markov Models}, author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Bernd Becker and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {7214}, pages = {299-314}, type = {Conference Paper}, year = {2012}, doi = {10.1007/978-3-642-28756-5_21}, url = { https://publications.rwth-aachen.de/record/128454}, }× [issue]	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.
[bibtex] @techreport{MCRRPMDP2012, title = {Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes}, author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, booktitle = {Reports of SFB/TR 14 AVACS}, volume = {88}, type = {Tech Report}, year = {2012}, url = { https://publications.rwth-aachen.de/record/197366}, }× [issue]	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] @conference{MCSCRDP2012, title = {Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties}, author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, publisher = {Kovač}, booktitle = {Schriftenreihe Forschungsergebnisse zur Informatik}, volume = {68}, pages = {169-180}, type = {Conference Paper}, year = {2012}, url = { https://publications.rwth-aachen.de/record/198077}, }× [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.
[bibtex] @conference{CDARSHS2012, title = {Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems}, author = {Xin Chen and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {6927}, pages = {535-542}, type = {Conference Paper}, year = {2012}, doi = {10.1007/978-3-642-27549-4_69}, url = { https://publications.rwth-aachen.de/record/207001}, }× [issue]	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, 535-542, Springer, 2012.
2011
[bibtex] @conference{IRSCSEFRA2011, title = {I-RiSC: an SMT-Compliant Solver for the Existential Fragment of Real Algebra}, author = {Ulrich Loup and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {6742}, pages = {230-246}, type = {Conference Paper}, year = {2011}, doi = {10.1007/978-3-642-21493-6_15}, url = { https://publications.rwth-aachen.de/record/100365}, }× [issue]	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.
[bibtex] @conference{VSSS2011, title = {Virtual Substitution for SMT-Solving}, author = {Florian Corzilius and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {6914}, pages = {360-371}, type = {Conference Paper}, year = {2011}, doi = {10.1007/978-3-642-22953-4_31}, url = { https://publications.rwth-aachen.de/record/116784}, }× [issue]	Florian Corzilius, Erika Ábrahám. Virtual Substitution for SMT-Solving, Fundamentals of computation theory:18th international symposium, FCT 2011 (FCT 2011), Volume 6914 of LNCS, 360-371, Springer, 2011.
[bibtex] @conference{GACLRAC2011, title = {GiNaCRA: A C++ Library for Real Algebraic Computations}, author = {Ulrich Loup and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {6617}, pages = {512-517}, type = {Conference Paper}, year = {2011}, doi = {10.1007/978-3-642-20398-5_41}, url = { https://publications.rwth-aachen.de/record/124551}, }× [issue]	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.
[bibtex] @conference{E2011, title = {Efficient bounded reachability computation for rectangular automata}, author = {Xin Chen and Erika Ábrahám and Goran Frehse}, publisher = {Springer}, booktitle = {LNCS}, volume = {6945}, pages = {139-152}, type = {Conference Paper}, year = {2011}, doi = {10.1007/978-3-642-24288-5_13}, url = { https://publications.rwth-aachen.de/record/127806}, }× [issue]	Xin Chen, Erika Ábrahám, Goran Frehse. Efficient bounded reachability computation for rectangular automata, Reachability problems : 5. international workshop (RP 2011), Volume 6945 of LNCS, 139-152, Springer, 2011.
[bibtex] @conference{CGMCUSBBMC2011, title = {Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking}, author = {Bettina Braitling and Ralf Wimmer and Bernd Becker and Nils Jansen and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {6722}, pages = {75-89}, type = {Conference Paper}, year = {2011}, doi = {10.1007/978-3-642-21461-5_5}, url = { https://publications.rwth-aachen.de/record/127839}, }× [issue]	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.
[bibtex] @conference{H2011, title = {Hierarchical counterexamples for discrete-time markov chains}, author = {Nils Jansen and Erika Ábrahám and Jens Katelaan and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker}, publisher = {Springer}, booktitle = {LNCS}, volume = {6996}, pages = {443-452}, type = {Conference Paper}, year = {2011}, doi = {10.1007/978-3-642-24372-1_33}, url = { https://publications.rwth-aachen.de/record/128557}, }× [issue]	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] @conference{SCGMC2011, title = {SMT-based Counterexample Generation for Markov Chains}, author = {Bettina Braitling and Ralf Wimmer and Bernd Becker and Nils Jansen and Erika Ábrahám}, publisher = {OFFIS}, pages = {19-28}, type = {Conference Paper}, year = {2011}, url = { https://publications.rwth-aachen.de/record/564234}, }× [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
[bibtex] @conference{DMCSR2010, title = {DTMC Model Checking by SCC Reduction}, author = {Erika Ábrahám and Nils Jansen and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker}, publisher = {IEEE Computer Society}, pages = {37-46}, type = {Conference Paper}, year = {2010}, doi = {10.1109/QEST.2010.13}, url = { https://publications.rwth-aachen.de/record/119427}, }× [issue]	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.
[bibtex] @article{ASSNMRLBFAIHS2010, title = {Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems}, author = {Muhammad Fadlisyah and Erika Ábrahám and Peter Csaba Ölveczky}, publisher = {Elsevier Science}, journal = {Electronic notes in theoretical computer science}, volume = {274}, pages = {pages 17-32}, type = {Journal Article}, year = {2010}, doi = {10.1016/j.entcs.2011.07.004}, url = { https://publications.rwth-aachen.de/record/170101}, }× [issue]	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 274, pages 17-32, Elsevier Science, 2010.
2007
[bibtex] @inbook{PS2007, title = {Parallel SAT solving in bounded model checking}, author = {Erika Ábrahám and Tobias Schubert and Bernd Becker and Martin Fränzle and Christian Herde}, publisher = {Springer}, booktitle = {LNCS}, volume = {4346}, pages = {301-315}, type = {Book Chapter}, year = {2007}, doi = {10.1007/978-3-540-70952-7_21}, url = { https://publications.rwth-aachen.de/record/88690}, }× [issue]	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.
[bibtex] @conference{OVSSLBMCLHA2007, title = {On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata}, author = {Marc Herbstritt and Bernd Becker and Erika Ábrahám and Christian Herde}, publisher = {IEEE Service Center}, pages = {391-396}, type = {Conference Paper}, year = {2007}, doi = {10.1109/DDECS.2007.4295318}, url = { https://publications.rwth-aachen.de/record/119470}, }× [issue]	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
[bibtex] @conference{A2006, title = {Abstract interface behavior of object-oriented languages with monitors}, author = {Erika Ábrahám and Andreas Grüner and Martin Steffen}, publisher = {Springer}, booktitle = {LNCS}, volume = {4037}, pages = {218-232}, type = {Conference Paper}, year = {2006}, doi = {10.1007/11768869}, url = { https://publications.rwth-aachen.de/record/111866}, }× [issue]	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.
[bibtex] @conference{D2006, title = {Dynamic heap-abstraction for open, object-oriented systems with thread classes}, author = {Erika Ábrahám and Andreas Grüner and Martin Steffen}, publisher = {Springer}, booktitle = {LNCS}, volume = {3988}, pages = {1-10}, type = {Conference Paper}, year = {2006}, doi = {10.1007/11780342_1}, url = { https://publications.rwth-aachen.de/record/113855}, }× [issue]	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] @conference{M2006, title = {Memory-aware bounded model checking for linear hybrid systems}, author = {Erika Ábrahám and Marc Herbstritt and Bernd Becker and Martin Steffen}, publisher = {Fraunhofer-Institut für Integrierte Schaltungen, Außenstelle Entwurfsautomatisierung}, pages = {153-162}, type = {Conference Paper}, year = {2006}, url = { https://publications.rwth-aachen.de/record/116300}, }× [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.
[bibtex] @article{B2006, title = {Bounded model checking with parametric data structures}, author = {Erika Ábrahám and Marc Herbstritt and Bernd Becker and Martin Steffen}, publisher = {Elsevier}, journal = {Electronic notes in theoretical computer science}, volume = {174(3)}, pages = {pages 3-16}, type = {Journal Article}, year = {2006}, doi = {10.1016/j.entcs.2006.12.019}, url = { https://publications.rwth-aachen.de/record/157630}, }× [issue]	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
[bibtex] @conference{OCFACCC2005, title = {Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes}, author = {Erika Ábrahám and Marcello Bonsangue and Frank S. de Boer and Martin Steffen}, publisher = {Springer}, booktitle = {LNCS}, volume = {3407}, pages = {37-51}, type = {Conference Paper}, year = {2005}, doi = {10.1007/b107116}, url = { https://publications.rwth-aachen.de/record/119436}, }× [issue]	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.
[bibtex] @conference{IPOEMJ2005, title = {Inductive Proof Outlines for Exceptions in Multithreaded Java}, author = {Erika Ábrahám and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, publisher = {Elsevier}, booktitle = {Electronic notes in theoretical computer science}, volume = {159}, pages = {281-297}, type = {Conference Paper}, year = {2005}, doi = {10.1016/j.entcs.2005.12.072}, url = { https://publications.rwth-aachen.de/record/119437}, }× [issue]	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.
[bibtex] @conference{OCRSCC2005, title = {Observability, Connectivity, and Replay in a Sequential Calculus of Classes}, author = {Erika Ábrahám and Frank S. de Boer and Marcello Bonsangue and Andreas Grüner and Martin Steffen}, publisher = {Springer}, booktitle = {LNCS}, volume = {3657 : Tutorial}, pages = {296-316}, type = {Conference Paper}, year = {2005}, doi = {10.1007/11561163}, url = { https://publications.rwth-aachen.de/record/119439}, }× [issue]	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.
[bibtex] @conference{AFATSUC2005, title = {A Fully Abstract Trace Semantics for UML Components}, author = {Frank S. de Boer and Marcello Bonsangue and Martin Steffen and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {3657 : Tutorial}, pages = {49-69}, type = {Conference Paper}, year = {2005}, doi = {10.1007/11561163_3}, url = { https://publications.rwth-aachen.de/record/119440}, }× [issue]	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.
[bibtex] @conference{OBMCLHS2005, title = {Optimizing Bounded Model Checking for Linear Hybrid Systems}, author = {Erika Ábrahám and Bernd Becker and Felix Klaedtke and Martin Steffen}, publisher = {Springer}, booktitle = {LNCS}, volume = {3385}, pages = {396-412}, type = {Conference Paper}, year = {2005}, doi = {10.1007/978-3-540-30579-8_26}, url = { https://publications.rwth-aachen.de/record/119443}, }× [issue]	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] @conference{DHAOOOSTC2005, title = {Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes}, author = {Erika Ábrahám and Andreas Grüner and Martin Steffen}, publisher = {Queen Mary, University of London, Department of Computer Science}, booktitle = {Research report / Queen Mary, University of London, Department of Computer Science}, volume = {RR-05-04}, pages = {47-61}, type = {Conference Paper}, year = {2005}, url = { https://publications.rwth-aachen.de/record/119469}, }× [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.
[bibtex] @article{AABPSMJ2005, title = {An Assertion-Based Proof System for Multithreaded Java}, author = {Erika Ábrahám and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, publisher = {Elsevier}, journal = {Theoretical computer science}, volume = {331(2/3)}, pages = {pages 251-290}, type = {Journal Article}, year = {2005}, doi = {10.1016/j.tcs.2004.09.019}, url = { https://publications.rwth-aachen.de/record/170083}, }× [issue]	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.