Erika Ábrahám

Email: abraham@cs.rwth-aachen.de
Address: Room 4229
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21242

Prof. Dr. Dr.h.c.

Current research activities:

modeling, synthesis, and analysis of hybrid systems,
analysis of probabilistic systems, probabilistic hyperproperties,
SMT solving with a focus on real algebra,
SMT-based planning and scheduling,
energy optimization.

Curriculum vitae
Projects
Teaching
School activities
Women in Computer Science

Some further links: ACM-WE interview

Publications

Own publications

2026

Proceedings
Research software from the 27th ACM International Conference on Hybrid Systems: Computation and Control
Science of computer programming · Elsevier Science
RWTH record for Research software from the 27th ACM International Conference on Hybrid Systems: Computation and Control BibTeX for Research software from the 27th ACM International Conference on Hybrid Systems: Computation and Control
Journal article
Preface Special Issue SCICO on HSCC2024-software
Erika Abraham, Manuel Mazo Espinosa
Science of computer programming
RWTH record for Preface Special Issue SCICO on HSCC2024-software BibTeX for Preface Special Issue SCICO on HSCC2024-software
Book chapter
Probabilistic Counterexamples Through the Ages
Erika Abraham, Nils Jansen, Simon Jantsch
Principles of formal quantitative analysis
RWTH record for Probabilistic Counterexamples Through the Ages BibTeX for Probabilistic Counterexamples Through the Ages
Conference paper
Counterexample-Guided Abstraction Refinement for Star-Based Neural Network Verification
László Antal, Franz Link, Erika Ábrahám
Reachability Problems
RWTH record for Counterexample-Guided Abstraction Refinement for Star-Based Neural Network Verification BibTeX for Counterexample-Guided Abstraction Refinement for Star-Based Neural Network Verification
Conference paper
A Hyperlogic for Strategies in Stochastic Games
Carolina Gerlach, Christof Löding, Erika Abraham
Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems
RWTH record for A Hyperlogic for Strategies in Stochastic Games BibTeX for A Hyperlogic for Strategies in Stochastic Games

2025

Conference paper
Counterfactual Strategies for Markov Decision Processes
Paul Kobialka, Carolina Gerlach, Francesco Leofante, Erika Abraham, Silvia Lizeth Tapia Tarifa, Einar Broch Johnsen
Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence
RWTH record for Counterfactual Strategies for Markov Decision Processes BibTeX for Counterfactual Strategies for Markov Decision Processes
Conference paper
Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks
Jonas Stübbe, Anne Remke, Erika Abraham
27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
RWTH record for Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks BibTeX for Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks
Conference paper
ROSAR: An Adversarial Re-Training Framework for Robust Side-Scan Sonar Object Detection
Martin Aubard, László Antal, Ana Madureira, Luis F. Teixeira, Erika Abraham
2025 Symposium on Maritime Informatics and Robotics (MARIS)
RWTH record for ROSAR: An Adversarial Re-Training Framework for Robust Side-Scan Sonar Object Detection BibTeX for ROSAR: An Adversarial Re-Training Framework for Robust Side-Scan Sonar Object Detection
Conference paper
Correction to: Efficient Probabilistic Model Checking for Relational Reachability
Lina Gerlach, Tobias Winkler, Erika Abraham, Borzoo Bonakdarpour, Sebastian Junges
Computer Aided Verification
PDF of Correction to: Efficient Probabilistic Model Checking for Relational Reachability RWTH record for Correction to: Efficient Probabilistic Model Checking for Relational Reachability BibTeX for Correction to: Efficient Probabilistic Model Checking for Relational Reachability
Book chapter
WoCa Lunch: A Program for Female Students to Get Informed About PhD Studies
Milena Vujošević Janičić, Erika Abraham, Amal Mersni, Oleksandra Yeremenko, Miguel Goulão
Actions for Gender Balance in Informatics Across Europe
PDF of WoCa Lunch: A Program for Female Students to Get Informed About PhD Studies RWTH record for WoCa Lunch: A Program for Female Students to Get Informed About PhD Studies BibTeX for WoCa Lunch: A Program for Female Students to Get Informed About PhD Studies
Conference paper
Projective Delineability for Single Cell Construction
Jasper Kurt Ferdinand Nalbach, Lucas Michel, Erika Abraham, Christopher W. Brown, James H. Davenport, Matthew England, Pierre Mathonet, Naïm Zénaïdi
SC-Square 2025
PDF of Projective Delineability for Single Cell Construction RWTH record for Projective Delineability for Single Cell Construction BibTeX for Projective Delineability for Single Cell Construction
Conference paper
A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination
Jasper Kurt Ferdinand Nalbach, Erika Abraham
SC-Square 2025
PDF of A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination RWTH record for A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination BibTeX for A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination
Journal article
Artificial Intelligence based robotic applications for higher education
Isabela Drămnesc, Erika Abraham, László Antal, Péter Csóka, Nikolaos Fachantidis, Tudor Jebelean, Gábor Kusper, Konstantinos Papadopoulos
Annales mathematicae et informaticae
RWTH record for Artificial Intelligence based robotic applications for higher education BibTeX for Artificial Intelligence based robotic applications for higher education
Conference paper
Efficient Probabilistic Model Checking for Relational Reachability
Carolina Gerlach, Tobias Winkler, Erika Abraham, Borzoo Bonakdarpour, Sebastian Junges
Computer Aided Verification
PDF of Efficient Probabilistic Model Checking for Relational Reachability RWTH record for Efficient Probabilistic Model Checking for Relational Reachability BibTeX for Efficient Probabilistic Model Checking for Relational Reachability
Journal article
Reachability analysis of Hybrid Rebeca models
Fatemeh Ghassemi, Saeed Zhiany, Nesa Abbasi, Ali Hodaei, Ali Ataollahi, Jozsef Kovacs, Erika Ábrahám, Marjan Sirjani
Journal of systems architecture
RWTH record for Reachability analysis of Hybrid Rebeca models BibTeX for Reachability analysis of Hybrid Rebeca models
Proceedings
Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2023) : Special issue
Science of computer programming · Elsevier Science
RWTH record for Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2023) : Special issue BibTeX for Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2023) : Special issue
Journal article
Preface: Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2023)
Hossein Hojjat, Erika Ábrahám
Science of computer programming
RWTH record for Preface: Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2023)BibTeX for Preface: Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2023)
Preprint
Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
Carolina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour, Sebastian Junges
PDF of Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)RWTH record for Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)BibTeX for Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
Preprint
Counterfactual Strategies for Markov Decision Processes
Paul Kobialka, Carolina Gerlach, Francesco Leofante, Erika Ábrahám, Silvia Lizeth, Tapia Tarifa, Einar Brocj Johnsen
PDF of Counterfactual Strategies for Markov Decision Processes RWTH record for Counterfactual Strategies for Markov Decision Processes BibTeX for Counterfactual Strategies for Markov Decision Processes
Journal article
Generalizing neural network verification to the family of piece-wise linear activation functions
László Antal, Erika Abraham, Hana Masara
Science of Computer Programming
PDF of Generalizing neural network verification to the family of piece-wise linear activation functions RWTH record for Generalizing neural network verification to the family of piece-wise linear activation functions BibTeX for Generalizing neural network verification to the family of piece-wise linear activation functions
Journal article
Introduction to the Special Issue on QEST 2022, Part 2
Erika Ábrahám, Marco Paolieri
ACM transactions on internet technology
RWTH record for Introduction to the Special Issue on QEST 2022, Part 2 BibTeX for Introduction to the Special Issue on QEST 2022, Part 2
Journal article
FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex
Valentin Maxim Promies, Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Paul Kobialka
Logical methods in computer science
PDF of FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex RWTH record for FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex BibTeX for FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex
Journal article
Numerical Modeling and Analysis of Shadow Flicker Using Solar Path Functions for Enhanced Predictive Accuracy
Nicolai Radke, Patrick E. M. De Smet, Erika Ábrahám
Energies
PDF of Numerical Modeling and Analysis of Shadow Flicker Using Solar Path Functions for Enhanced Predictive Accuracy RWTH record for Numerical Modeling and Analysis of Shadow Flicker Using Solar Path Functions for Enhanced Predictive Accuracy BibTeX for Numerical Modeling and Analysis of Shadow Flicker Using Solar Path Functions for Enhanced Predictive Accuracy
Book chapter
(de-)Composed And More: Eager and Lazy Specifications (CAMELS) for Stochastic Hybrid Systems
Lisa Willemsen, Anne Remke, Erika Ábrahám
Principles of verification: cycling the probabilistic landscape
RWTH record for (de-)Composed And More: Eager and Lazy Specifications (CAMELS) for Stochastic Hybrid Systems BibTeX for (de-)Composed And More: Eager and Lazy Specifications (CAMELS) for Stochastic Hybrid Systems
Proceedings
Runtime verification : 24th international conference, RV 2024, Istanbul, Turkey, October 15-17, 2024 : proceedings
Springer
RWTH record for Runtime verification : 24th international conference, RV 2024, Istanbul, Turkey, October 15-17, 2024 : proceedings BibTeX for Runtime verification : 24th international conference, RV 2024, Istanbul, Turkey, October 15-17, 2024 : proceedings
Journal article
Maximizing reachability probabilities in rectangular automata with random events
Joanna Delicaris, Anne Remke, Erika Ábrahám, Stefan Schupp, Jonas Stubbe
Science of computer programming
PDF of Maximizing reachability probabilities in rectangular automata with random events RWTH record for Maximizing reachability probabilities in rectangular automata with random events BibTeX for Maximizing reachability probabilities in rectangular automata with random events
Conference paper
A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic
Valentin Maxim Promies, Erika Ábrahám
Formal methods
PDF of A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic RWTH record for A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic BibTeX for A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic

2024

Patent
Steuerung einer Versorgungstechnik eines Gebäudes mittels eines neuronalen Netzwerks
Pascal Richter, Erika Ábrahám, Ahmed Abida
RWTH record for Steuerung einer Versorgungstechnik eines Gebäudes mittels eines neuronalen Netzwerks BibTeX for Steuerung einer Versorgungstechnik eines Gebäudes mittels eines neuronalen Netzwerks
Conference paper
On Projective Delineability
Lucas Michel, Jasper Kurt Ferdinand Nalbach, Pierre Mathonet, Naïm Zénaïdi, Christopher W. Brown, Erika Ábrahám, James H. Davenport, Matthew England
2024 26th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
RWTH record for On Projective Delineability BibTeX for On Projective Delineability
Preprint
On Projective Delineability
Lucas Michel, Jasper Kurt Ferdinand Nalbach, Pierre Mathonet, Naïm Zénaïdi, Christopher W. Brown, Erika Ábrahám, James H. Davenport, Matthew England
PDF of On Projective Delineability RWTH record for On Projective Delineability BibTeX for On Projective Delineability
Preprint
Hybrid Rebeca Revisited
Fatemeh Ghassemi, Saeed Zhiany, Nesa Abbasimoghadam, Ali Hodaei, Ali Ataollahi, Jozsef Kovacs, Erika Ábrahám, Marjan Sirjani
PDF of Hybrid Rebeca Revisited RWTH record for Hybrid Rebeca Revisited BibTeX for Hybrid Rebeca Revisited
Dataset
SWDD: Sonar Wall Detection Dataset
Martin Aubard, László Antal, Ana Maria Madureira, Erika Ábrahám
Zenodo
RWTH record for SWDD: Sonar Wall Detection Dataset BibTeX for SWDD: Sonar Wall Detection Dataset
Conference paper
A European Project on AI-based Robotics
Isabela Dramnesc, Erika Ábrahám, Tudor Jebelean, Nikolaos Fachantidis, Gabor Kusper, Sorin Stratulat
2024 IEEE International Conference on Teaching, Assessment and Learning for Engineering conference proceedings
RWTH record for A European Project on AI-based Robotics BibTeX for A European Project on AI-based Robotics
Preprint
ROSAR: An Adversarial Re-Training Framework for Robust Side-Scan Sonar Object Detection
Martin Aubard, László Antal, Ana Madureira, Luis F. Teixeira, Erika Ábrahám
PDF of ROSAR: An Adversarial Re-Training Framework for Robust Side-Scan Sonar Object Detection RWTH record for ROSAR: An Adversarial Re-Training Framework for Robust Side-Scan Sonar Object Detection BibTeX for ROSAR: An Adversarial Re-Training Framework for Robust Side-Scan Sonar Object Detection
Proceedings
Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control
Association for Computing Machinery
RWTH record for Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control BibTeX for Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control
Journal article
Introduction to the Special Issue on QEST 2022, Part 1
Erika Ábrahám, Marco Paolieri
ACM transactions on modeling and computer simulation
RWTH record for Introduction to the Special Issue on QEST 2022, Part 1 BibTeX for Introduction to the Special Issue on QEST 2022, Part 1
Conference paper
Under-Approximation of a Single Algebraic Cell
Valentin Maxim Promies, Jasper Kurt Ferdinand Nalbach, Erika Ábrahám
PAAR+SC-Square 2024: Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2024
PDF of Under-Approximation of a Single Algebraic Cell RWTH record for Under-Approximation of a Single Algebraic Cell BibTeX for Under-Approximation of a Single Algebraic Cell
Preprint
Knowledge Distillation in YOLOX-ViT for Side-Scan Sonar Object Detection
Martin Aubard, László Antal, Ana Madureira, Erika Ábrahám
PDF of Knowledge Distillation in YOLOX-ViT for Side-Scan Sonar Object Detection RWTH record for Knowledge Distillation in YOLOX-ViT for Side-Scan Sonar Object Detection BibTeX for Knowledge Distillation in YOLOX-ViT for Side-Scan Sonar Object Detection
Conference paper
Merging Adjacent Cells During Single Cell Construction
Jasper Kurt Ferdinand Nalbach, Erika Ábrahám
Computer algebra in scientific computing
RWTH record for Merging Adjacent Cells During Single Cell Construction BibTeX for Merging Adjacent Cells During Single Cell Construction
Journal article
Parameter synthesis for Markov models : covering the parameter space
Sebastian Junges, Erika Ábrahám, Hans Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk
Formal methods in system design
PDF of Parameter synthesis for Markov models : covering the parameter space RWTH record for Parameter synthesis for Markov models : covering the parameter space BibTeX for Parameter synthesis for Markov models : covering the parameter space
Conference paper
SMT: Something You Must Try
Erika Ábrahám, Jószef Kovács, Anne Remke
iFM 2023
RWTH record for SMT: Something You Must Try BibTeX for SMT: Something You Must Try
Journal article
Levelwise construction of a single cylindrical algebraic cell
Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Philippe Specht, Christopher W. Brown, James H. Davenport, Matthew England
Journal of symbolic computation
PDF of Levelwise construction of a single cylindrical algebraic cell RWTH record for Levelwise construction of a single cylindrical algebraic cell BibTeX for Levelwise construction of a single cylindrical algebraic cell
Journal article
On the applicability of hybrid systems safety verification tools from the automotive perspective
Stefan Schupp, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow, Zeng Qiu
International journal on software tools for technology transfer
PDF of On the applicability of hybrid systems safety verification tools from the automotive perspective RWTH record for On the applicability of hybrid systems safety verification tools from the automotive perspective BibTeX for On the applicability of hybrid systems safety verification tools from the automotive perspective

2023

Conference paper
Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions
László Antal, Hana Masara, Erika Ábrahám
Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems
PDF of Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions RWTH record for Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions BibTeX for Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions
Conference paper
Theoretical Aspects of Computing
Erika Ábrahám, Clemens Dubslaff, Silvia Lizeth Tapia Tarifa
Theoretical Aspects of Computing – ICTAC 2023
RWTH record for Theoretical Aspects of Computing BibTeX for Theoretical Aspects of Computing
Conference paper
FMplex: A Novel Method for Solving Linear Real Arithmetic Problems
Jasper Kurt Ferdinand Nalbach, Valentin Maxim Promies, Erika Ábrahám, Paul Kobialka
Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification Udine, Italy, 18-20th September 2023
RWTH record for FMplex: A Novel Method for Solving Linear Real Arithmetic Problems BibTeX for FMplex: A Novel Method for Solving Linear Real Arithmetic Problems
Journal article
Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041)
Erika Ábrahám, Stefan Hallerstede, John Hatcliff, Danielle Stewart, Noah Abou El Wafa
Dagstuhl Reports
PDF of Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041)RWTH record for Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041)BibTeX for Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041)
Conference paper
Comparing Two Approaches to Include Stochasticity in Hybrid Automata
Lisa Willemsen, Anne Remke, Erika Ábrahám
Quantitative Evaluation of Systems
RWTH record for Comparing Two Approaches to Include Stochasticity in Hybrid Automata BibTeX for Comparing Two Approaches to Include Stochasticity in Hybrid Automata
Proceedings
Fundamentals of Software Engineering : 10th International Conference, FSEN 2023, Tehran, Iran, May 4-5, 2023, Revised Selected Papers
Springer
RWTH record for Fundamentals of Software Engineering : 10th International Conference, FSEN 2023, Tehran, Iran, May 4-5, 2023, Revised Selected Papers BibTeX for Fundamentals of Software Engineering : 10th International Conference, FSEN 2023, Tehran, Iran, May 4-5, 2023, Revised Selected Papers
Preprint
FMplex: A Novel Method for Solving Linear Real Arithmetic Problems
Jasper Kurt Ferdinand Nalbach, Valentin Maxim Promies, Erika Ábrahám, Paul Kobialka
PDF of FMplex: A Novel Method for Solving Linear Real Arithmetic Problems RWTH record for FMplex: A Novel Method for Solving Linear Real Arithmetic Problems BibTeX for FMplex: A Novel Method for Solving Linear Real Arithmetic Problems
Conference paper
Introducing Asynchronicity to Probabilistic Hyperproperties
Lina Gerlach, Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour
Quantitative Evaluation of Systems
RWTH record for Introducing Asynchronicity to Probabilistic Hyperproperties BibTeX for Introducing Asynchronicity to Probabilistic Hyperproperties
Preprint
Comparing Two Approaches to Include Stochasticity in Hybrid Automata
Lisa Willemsen, Anne Remke, Erika Ábrahám
PDF of Comparing Two Approaches to Include Stochasticity in Hybrid Automata RWTH record for Comparing Two Approaches to Include Stochasticity in Hybrid Automata BibTeX for Comparing Two Approaches to Include Stochasticity in Hybrid Automata
Preprint
Introducing Asynchronicity to Probabilistic Hyperproperties
Carolina Gerlach, Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour
PDF of Introducing Asynchronicity to Probabilistic Hyperproperties RWTH record for Introducing Asynchronicity to Probabilistic Hyperproperties BibTeX for Introducing Asynchronicity to Probabilistic Hyperproperties
Preprint
Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks
Joanna Delicaris, Stefan Schupp, Erika Ábrahám, Anne Remke
PDF of Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks RWTH record for Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks BibTeX for Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks
Proceedings
SC-Square 2023: Satisfiability Checking and Symbolic Computation 2023 : proceedings of the 8th SC-Square Workshop, co-located with the 48th International Symposium on Symbolic and Algebraic Computation (ISSAC 2023) : Tromsø, Norway, July 28, 2023
RWTH Aachen
RWTH record for SC-Square 2023: Satisfiability Checking and Symbolic Computation 2023 : proceedings of the 8th SC-Square Workshop, co-located with the 48th International Symposium on Symbolic and Algebraic Computation (ISSAC 2023) : Tromsø, Norway, July 28, 2023 BibTeX for SC-Square 2023: Satisfiability Checking and Symbolic Computation 2023 : proceedings of the 8th SC-Square Workshop, co-located with the 48th International Symposium on Symbolic and Algebraic Computation (ISSAC 2023) : Tromsø, Norway, July 28, 2023
Conference paper
Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks
Joanna Delicaris, Stefan Schupp, Erika Ábrahám, Anne Remke
Theoretical Aspects of Software Engineering
RWTH record for Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks BibTeX for Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks
Preprint
Exploiting Strict Constraints in the Cylindrical Algebraic Covering
Philipp Bär, Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Christopher W. Brown
PDF of Exploiting Strict Constraints in the Cylindrical Algebraic Covering RWTH record for Exploiting Strict Constraints in the Cylindrical Algebraic Covering BibTeX for Exploiting Strict Constraints in the Cylindrical Algebraic Covering
Conference paper
Exploiting Strict Constraints in the Cylindrical Algebraic Covering
Philipp Bär, Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Christopher Brown
SMT 2023
PDF of Exploiting Strict Constraints in the Cylindrical Algebraic Covering RWTH record for Exploiting Strict Constraints in the Cylindrical Algebraic Covering BibTeX for Exploiting Strict Constraints in the Cylindrical Algebraic Covering
Conference paper
Subtropical Satisfiability for SMT Solving
Jasper Kurt Ferdinand Nalbach, Erika Ábrahám
NASA formal methods
RWTH record for Subtropical Satisfiability for SMT Solving BibTeX for Subtropical Satisfiability for SMT Solving
Conference paper
Automated Exercise Generation for Satisfiability Checking
Erika Ábrahám, Jasper Kurt Ferdinand Nalbach, Valentin Maxim Promies
Formal methods teaching
RWTH record for Automated Exercise Generation for Satisfiability Checking BibTeX for Automated Exercise Generation for Satisfiability Checking
Conference paper
A Collision Avoidance Method for Autonomous Underwater Vehicles Based on Long Short-Term Memories
László Antal, Martin Aubard, Erika Ábrahám, Ana Madureira, Luís Madureira, Maria Costa, José Pinto, Renato Campos
Innovations in Bio-Inspired Computing and Applications
RWTH record for A Collision Avoidance Method for Autonomous Underwater Vehicles Based on Long Short-Term Memories BibTeX for A Collision Avoidance Method for Autonomous Underwater Vehicles Based on Long Short-Term Memories
Patent
Verfahren und System zur Steuerung von Lasten in einem Gebäude
Jonas Blum, Stefan Hardt, Pascal Richter, Erika Ábrahám, Ahmed Abida, Simon Klemp
RWTH record for Verfahren und System zur Steuerung von Lasten in einem Gebäude BibTeX for Verfahren und System zur Steuerung von Lasten in einem Gebäude

2022

Preprint
Levelwise construction of a single cylindrical algebraic cell
Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Philippe Specht, Christopher W. Brown, James H. Davenport, Matthew England
PDF of Levelwise construction of a single cylindrical algebraic cell RWTH record for Levelwise construction of a single cylindrical algebraic cell BibTeX for Levelwise construction of a single cylindrical algebraic cell
Journal article
Model checking hyperproperties for Markov decision processes
Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour
Information and Computation
RWTH record for Model checking hyperproperties for Markov decision processes BibTeX for Model checking hyperproperties for Markov decision processes
Proceedings
Quantitative evaluation of systems : 19th international conference, QEST 2022 Warsaw, Poland, September 12–16, 2022, proceedings
Springer
RWTH record for Quantitative evaluation of systems : 19th international conference, QEST 2022 Warsaw, Poland, September 12–16, 2022, proceedings BibTeX for Quantitative evaluation of systems : 19th international conference, QEST 2022 Warsaw, Poland, September 12–16, 2022, proceedings
Journal article
New Perspectives in Symbolic Computation and Satisfiability Checking
Erika Ábrahám, James H. Davenport, Matthew England, Alberto Griggio
Dagstuhl reports
PDF of New Perspectives in Symbolic Computation and Satisfiability Checking RWTH record for New Perspectives in Symbolic Computation and Satisfiability Checking BibTeX for New Perspectives in Symbolic Computation and Satisfiability Checking
Conference paper
Experiments with Automated Reasoning in the Class
Isabela Dramnesc, Erika Ábrahám, Tudor Jebelean, Gábor Kusper, Sorin Stratulat
Intelligent Computer Mathematics
RWTH record for Experiments with Automated Reasoning in the Class BibTeX for Experiments with Automated Reasoning in the Class
Journal article
Recent developments in theory and tool support for hybrid systems verification with HyPro
Stefan Schupp, Erika Ábrahám, Tristan Ebert
Information and Computation
PDF of Recent developments in theory and tool support for hybrid systems verification with HyPro RWTH record for Recent developments in theory and tool support for hybrid systems verification with HyPro BibTeX for Recent developments in theory and tool support for hybrid systems verification with HyPro
Conference paper
Robot Swarms as Hybrid Systems: Modelling and Verification
Stefan Schupp, Francesco Leofante, Leander Behr, Erika Ábrahám, Armando Tacchella
Proceedings The 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT, Online, 23rd August 2021
PDF of Robot Swarms as Hybrid Systems: Modelling and Verification RWTH record for Robot Swarms as Hybrid Systems: Modelling and Verification BibTeX for Robot Swarms as Hybrid Systems: Modelling and Verification
Conference paper
Acceleration Techniques for Symbolic Simulation of Railway Timetables
Rebecca Haehn, Erika Ábrahám, Niklas Kotowski
Reliability, safety, and security of railway systems
RWTH record for Acceleration Techniques for Symbolic Simulation of Railway Timetables BibTeX for Acceleration Techniques for Symbolic Simulation of Railway Timetables
Conference paper
Probabilistic Hyperproperties with Rewards
Oyendrila Dobe, Lukas Wilke, Erika Ábrahám, Borzoo Bonakdarpour, Ezio Bartocci
NASA Formal Methods
RWTH record for Probabilistic Hyperproperties with Rewards BibTeX for Probabilistic Hyperproperties with Rewards
Conference paper
HyperPCTL Model Checking by Probabilistic Decomposition
Eshita Zaman, Gianfranco Ciardo, Erika Ábrahám, Borzoo Bonakdarpour
Integrated formal methods
RWTH record for HyperPCTL Model Checking by Probabilistic Decomposition BibTeX for HyperPCTL Model Checking by Probabilistic Decomposition

2021

Conference paper
On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving
Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport
2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
RWTH record for On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving BibTeX for On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving
Preprint
On the proof complexity of MCSAT
Gereon Kremer, Erika Ábrahám, Vijay Ganesh
PDF of On the proof complexity of MCSAT RWTH record for On the proof complexity of MCSAT BibTeX for On the proof complexity of MCSAT
Preprint
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer
PDF of Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic RWTH record for Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic BibTeX for Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Conference paper
Controller verification meets controller code: a case study
Felix Freiberger, Stefan Schupp, Holger Hermanns, Erika Ábrahám
Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design
RWTH record for Controller verification meets controller code: a case study BibTeX for Controller verification meets controller code: a case study
Conference paper
HyperProb : A Model Checker for Probabilistic Hyperproperties
Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour
Formal Methods
RWTH record for HyperProb : A Model Checker for Probabilistic Hyperproperties BibTeX for HyperProb : A Model Checker for Probabilistic Hyperproperties
Conference paper
ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics
Matthias Althoff, Erika Ábrahám, Marcelo Forets, Goran Frehse, Daniel Freire, Christian Schilling, Stefan Schupp, Mark Wetzlinger
8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)
RWTH record for ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics BibTeX for ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics
Conference paper
Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies
Rebecca Haehn, Erika Ábrahám, Nils Nießen
Quantitative evaluation of systems
RWTH record for Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies BibTeX for Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies
Conference paper
Extending the Fundamental Theorem of Linear Programming for Strict Inequalities
Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Gereon Kremer
ISSAC '21
RWTH record for Extending the Fundamental Theorem of Linear Programming for Strict Inequalities BibTeX for Extending the Fundamental Theorem of Linear Programming for Strict Inequalities
Journal article
Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer
Journal of Logical and Algebraic Methods in Programming
PDF of Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings RWTH record for Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings BibTeX for Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings

2020

Preprint
New Opportunities for the Formal Proof of Computational Real Geometry?
Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks
PDF of New Opportunities for the Formal Proof of Computational Real Geometry?RWTH record for New Opportunities for the Formal Proof of Computational Real Geometry?BibTeX for New Opportunities for the Formal Proof of Computational Real Geometry?
Conference paper
New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)
Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks
PAAR+SC-Square 2020: Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020
PDF of New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)RWTH record for New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)BibTeX for New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)
Conference paper
A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata
Carina Pilch, Maurice Krause, Anne Remke, Erika Ábrahám
NASA formal methods
RWTH record for A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata BibTeX for A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata
Conference paper
Probabilistic Hyperproperties with Nondeterminism
Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe
Automated technology for verification and analysis
RWTH record for Probabilistic Hyperproperties with Nondeterminism BibTeX for Probabilistic Hyperproperties with Nondeterminism
Conference paper
Probabilistic Simulation of a Railway Timetable
Rebecca Haehn, Erika Ábrahám, Nils Nießen
20th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems
PDF of Probabilistic Simulation of a Railway Timetable RWTH record for Probabilistic Simulation of a Railway Timetable BibTeX for Probabilistic Simulation of a Railway Timetable
Conference paper
Parameter Synthesis for Probabilistic Hyperproperties
Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe
[The 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2020]
RWTH record for Parameter Synthesis for Probabilistic Hyperproperties BibTeX for Parameter Synthesis for Probabilistic Hyperproperties
Conference paper
Freight Train Scheduling in Railway Systems
Rebecca Haehn, Erika Ábrahám, Nils Nießen
Measurement, modelling, and evaluation of computing systems
RWTH record for Freight Train Scheduling in Railway Systems BibTeX for Freight Train Scheduling in Railway Systems
Preprint
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer
PDF of Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings RWTH record for Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings BibTeX for Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
Journal article
Fully Incremental Cylindrical Algebraic Decomposition
Gereon Kremer, Erika Ábrahám
Journal of symbolic computation
RWTH record for Fully Incremental Cylindrical Algebraic Decomposition BibTeX for Fully Incremental Cylindrical Algebraic Decomposition

2019

Conference paper
Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems
Francesco Leofante, Stefan Schupp, Erika Ábrahám, Armando Tacchella
Proceedings of the 33rd International ECMS Conference on Modelling and Simulation, ECMS 2019
RWTH record for Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems BibTeX for Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems
Conference paper
On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract)
Jasper Kurt Ferdinand Nalbach, Gereon Kremer, Erika Ábrahám
SC-square 2019
PDF of On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract)RWTH record for On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract)BibTeX for On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract)
Conference paper
On the Proof Complexity of MCSAT
Gereon Kremer, Erika Ábrahám, Vijay Ganesh
SC-square 2019
PDF of On the Proof Complexity of MCSAT RWTH record for On the Proof Complexity of MCSAT BibTeX for On the Proof Complexity of MCSAT
Conference paper
Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development
Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow
Formal methods for industrial critical systems ; 24th international conference, FMICS 2019, Amsterdam, The Netherlands, August 30-31, 2019
RWTH record for Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development BibTeX for Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development

2018

Conference paper
The HyDRA Tool : A Playground for the Development of Hybrid Systems Reachability Analysis Methods
Stefan Schupp, Erika Ábrahám
Proceedings of the PhD Symposium at iFM’18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’18)
RWTH record for The HyDRA Tool : A Playground for the Development of Hybrid Systems Reachability Analysis Methods BibTeX for The HyDRA Tool : A Playground for the Development of Hybrid Systems Reachability Analysis Methods
Conference paper
Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics
Erika Ábrahám
Automated Reasoning
RWTH record for Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics BibTeX for Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics
Proceedings
2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering : GE 2018 : 28 May 2018, Gothenburg, Sweden : proceedings
IEEE
RWTH record for 2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering : GE 2018 : 28 May 2018, Gothenburg, Sweden : proceedings BibTeX for 2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering : GE 2018 : 28 May 2018, Gothenburg, Sweden : proceedings
Proceedings
Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)
PDF of Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)RWTH record for Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)BibTeX for Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)
Conference paper
Evaluation of Equational Constraints for CAD in SMT Solving
Rebecca Haehn, Gereon Kremer, Erika Ábrahám
Satisfiability checking and symbolic computation
PDF of Evaluation of Equational Constraints for CAD in SMT Solving RWTH record for Evaluation of Equational Constraints for CAD in SMT Solving BibTeX for Evaluation of Equational Constraints for CAD in SMT Solving
Conference paper
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
Erika Ábrahám, Borzoo Bonakdarpour
Quantitative evaluation of systems
RWTH record for HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties BibTeX for HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
Conference paper
Task Planning with OMT: An Application to Production Logistics
Francesco Leofante, Erika Ábrahám, Armando Tacchella
Integrated formal methods
RWTH record for Task Planning with OMT: An Application to Production Logistics BibTeX for Task Planning with OMT: An Application to Production Logistics
Journal article
Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics
Francesco Leofante, Erika Ábrahám, Tim Dieter Niemüller, Gerhard Lakemeyer, Armando Tacchella
Information systems frontiers
RWTH record for Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics BibTeX for Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics
Conference paper
Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Ábrahám, Joost-Pieter Katoen
Formal Methods
RWTH record for Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations BibTeX for Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Conference paper
Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain
Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow
Formal Methods
RWTH record for Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain BibTeX for Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain
Conference paper
Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis
Stefan Schupp, Erika Ábrahám
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis RWTH record for Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis BibTeX for Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis
Conference paper
Spread the Work : Multi-threaded Safety Analysis for Hybrid Systems
Stefan Schupp, Erika Ábrahám
Software engineering and formal methods
RWTH record for Spread the Work : Multi-threaded Safety Analysis for Hybrid Systems BibTeX for Spread the Work : Multi-threaded Safety Analysis for Hybrid Systems
Journal article
Modular strategic SMT solving with SMT-RAT
Gereon Kremer, Erika Ábrahám
Acta Universitatis Sapientiae
PDF of Modular strategic SMT solving with SMT-RAT RWTH record for Modular strategic SMT solving with SMT-RAT BibTeX for Modular strategic SMT solving with SMT-RAT
Conference paper
Context-Dependent Reachability Analysis for Hybrid Systems
Stefan Schupp, Justin Winkens, Erika Ábrahám
2018 IEEE 19th International Conference on Information Reuse and Integration for Data Science
RWTH record for Context-Dependent Reachability Analysis for Hybrid Systems BibTeX for Context-Dependent Reachability Analysis for Hybrid Systems

2017

Conference paper
Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro
Jannik Hüls, Stefan Schupp, Anne Remke, Erika Ábrahám
Proceedings of the 11th EAI International Conference on Performance Evaluation Methodologies and Tools
RWTH record for Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro BibTeX for Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro
Conference paper
Towards CLIPS-based Task Execution and Monitoring with SMT-based Planning and Optimization
Tim Dieter Niemüller, Gerhard Lakemeyer, Francesco Leofante, Erika Ábrahám
Proceedings of the 5th Workshop on Planning and Robotics at ICAPS (PLANROB 2017)
PDF of Towards CLIPS-based Task Execution and Monitoring with SMT-based Planning and Optimization RWTH record for Towards CLIPS-based Task Execution and Monitoring with SMT-based Planning and Optimization BibTeX for Towards CLIPS-based Task Execution and Monitoring with SMT-based Planning and Optimization
Conference paper
SMT Solving for Arithmetic Theories: Theory and Tool Support
Erika Ábrahám, Gereon Kremer
19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
RWTH record for SMT Solving for Arithmetic Theories: Theory and Tool Support BibTeX for SMT Solving for Arithmetic Theories: Theory and Tool Support
Proceedings
Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017
[Open Publishing Association]
PDF of Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017 RWTH record for Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017 BibTeX for Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017
Conference paper
Preface
Erika Ábrahám, Sergiy Bogomolov
Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis
RWTH record for Preface BibTeX for Preface
Conference paper
Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization
Tim Dieter Niemüller, Gerhard Lakemeyer, Francesco Leofante, Erika Ábrahám
27th International Conference on Automated Planning and Scheduling June 19-23, 2017, Pittsburgh, USA
PDF of Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization RWTH record for Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization BibTeX for Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization
Journal article
Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071)
Erika Ábrahám, Hadas Kress-Gazit, Lorenzo Natale, Armando Tacchella
Dagstuhl Reports
PDF of Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071)RWTH record for Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071)BibTeX for Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071)
Proceedings
Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017
[Open Publishing Association]
RWTH record for Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017 BibTeX for Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017
Conference paper
On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories
Francesco Leofante, Erika Ábrahám, Tim Dieter Niemüller, Gerhard Lakemeyer, Armando Tacchella
2017 IEEE International Conference on Information Reuse and Integration
RWTH record for On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories BibTeX for On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories
Conference paper
SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces
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
ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017
RWTH record for SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces BibTeX for SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces
Proceedings
Bridging two communities to solve real problems : SC2 2016 : First Workshop on Satisfiability Checking and Symbolic Computation : FETOPEN-CSA SC2 Workshop 1 : September 24, 2016 : affiliated with the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016) : Timisoara, Romania
RWTH Aachen
RWTH record for Bridging two communities to solve real problems : SC2 2016 : First Workshop on Satisfiability Checking and Symbolic Computation : FETOPEN-CSA SC2 Workshop 1 : September 24, 2016 : affiliated with the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016) : Timisoara, Romania BibTeX for Bridging two communities to solve real problems : SC2 2016 : First Workshop on Satisfiability Checking and Symbolic Computation : FETOPEN-CSA SC2 Workshop 1 : September 24, 2016 : affiliated with the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016) : Timisoara, Romania
Conference paper
Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving
Tarik Viehmann, Gereon Kremer, Erika Ábrahám
[2nd International Workshop on Satisfiability Checking and Symbolic Computation, SC2, 2017-07-29 - 2017-07-29, Kaiserslautern, Germany
PDF of Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving RWTH record for Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving BibTeX for Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving
Conference paper
Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework
Erika Ábrahám, Jasper Kurt Ferdinand Nalbach, Gereon Kremer
Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), Kaiserslautern, Germany, July 29, 2017
RWTH record for Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework BibTeX for Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework
Conference paper
Techniques and Tools for Hybrid Systems Reachability Analysis
Erika Ábrahám
Numerical Software Verification
PDF of Techniques and Tools for Hybrid Systems Reachability Analysis RWTH record for Techniques and Tools for Hybrid Systems Reachability Analysis BibTeX for Techniques and Tools for Hybrid Systems Reachability Analysis
Conference paper
HyPro : A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis
Stefan Schupp, Erika Ábrahám, Ibtissem Ben Makhlouf, Stefan Kowalewski
NASA formal methods
RWTH record for HyPro : A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis BibTeX for HyPro : A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis
Conference paper
Divide and Conquer : Variable Set Separation in Hybrid Systems Reachability Analysis
Stefan Schupp, Johanna Nellen, Erika Ábrahám
Proceedings 15th Workshop on Quantitative Aspects of Programming Languages and Systems
RWTH record for Divide and Conquer : Variable Set Separation in Hybrid Systems Reachability Analysis BibTeX for Divide and Conquer : Variable Set Separation in Hybrid Systems Reachability Analysis

2016

Preprint
Satisfiability checking and symbolic computation
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
PDF of Satisfiability checking and symbolic computation RWTH record for Satisfiability checking and symbolic computation BibTeX for Satisfiability checking and symbolic computation
Conference paper
Symbolic Computation Techniques in Satisfiability Checking
Erika Ábrahám
18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
RWTH record for Symbolic Computation Techniques in Satisfiability Checking BibTeX for Symbolic Computation Techniques in Satisfiability Checking
Journal article
Satisfiability checking and symbolic computation
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
ACM Communications in computer algebra
RWTH record for Satisfiability checking and symbolic computation BibTeX for Satisfiability checking and symbolic computation
Journal article
Symbolic Computation and Satisfiability Checking : Report of Dagstuhl Seminar 15471
Erika Ábrahám, Pascal Fontaine, Thomas Sturm, Dongming Wang
Dagstuhl reports
PDF of Symbolic Computation and Satisfiability Checking : Report of Dagstuhl Seminar 15471 RWTH record for Symbolic Computation and Satisfiability Checking : Report of Dagstuhl Seminar 15471 BibTeX for Symbolic Computation and Satisfiability Checking : Report of Dagstuhl Seminar 15471
Conference paper
Parameter synthesis for probabilistic systems
Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám
MBMV 2016
PDF of Parameter synthesis for probabilistic systems RWTH record for Parameter synthesis for probabilistic systems BibTeX for Parameter synthesis for probabilistic systems
Proceedings
Integrated formal methods : 12th international conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016 : proceedings
Springer International Publishing ; Imprint: Springer
RWTH record for Integrated formal methods : 12th international conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016 : proceedings BibTeX for Integrated formal methods : 12th international conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016 : proceedings
Proceedings
Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR) : April 11, 2016, Vienna, Austria : held as part of CPS Week, April 11-14, 2016, Vienna, Austria
IEEE
RWTH record for Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR) : April 11, 2016, Vienna, Austria : held as part of CPS Week, April 11-14, 2016, Vienna, Austria BibTeX for Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR) : April 11, 2016, Vienna, Austria : held as part of CPS Week, April 11-14, 2016, Vienna, Austria
Conference paper
Satisfiability Checking : Theory and Applications
Erika Ábrahám, Gereon Kremer
Software engineering and formal methods
RWTH record for Satisfiability Checking : Theory and Applications BibTeX for Satisfiability Checking : Theory and Applications
Conference paper
Heliostat Field Layout Optimization with Evolutionary Algorithms
Pascal Richter, David Laukamp, Levin Gerdes, Martin Frank, Erika Ábrahám
GCAI 2016
RWTH record for Heliostat Field Layout Optimization with Evolutionary Algorithms BibTeX for Heliostat Field Layout Optimization with Evolutionary Algorithms
Book
Theory and practice of formal methods : essays dedicated to Frank de Boer on the occasion of his 60th birthday
Springer International Publishing ; Imprint: Springer
RWTH record for Theory and practice of formal methods : essays dedicated to Frank de Boer on the occasion of his 60th birthday BibTeX for Theory and practice of formal methods : essays dedicated to Frank de Boer on the occasion of his 60th birthday
Conference paper
Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots
Francesco Leofante, Simone Vuotto, Erika Ábrahám, Armando Tacchella, Nils Jansen
Leveraging applications of formal methods, verification and validation
RWTH record for Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots BibTeX for Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots
Conference paper
Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies
Erika Ábrahám, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro
Dependable software engineering
RWTH record for Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies BibTeX for Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies
Conference paper
SC2 : Satisfiability Checking Meets Symbolic Computation
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
Intelligent Computer Mathematics
RWTH record for SC2 : Satisfiability Checking Meets Symbolic Computation BibTeX for SC2 : Satisfiability Checking Meets Symbolic Computation
Journal article
Some recent advances in automated analysis
Erika Ábrahám, Klaus Havelund
International journal on software tools for technology transfer
RWTH record for Some recent advances in automated analysis BibTeX for Some recent advances in automated analysis
Journal article
Two CEGAR-based approaches for the safety verification of PLC-controlled plants
Johanna Nellen, Kai Driessen, Martin Neuhäußer, Erika Ábrahám, Benedikt Wolters
Information systems frontiers
RWTH record for Two CEGAR-based approaches for the safety verification of PLC-controlled plants BibTeX for Two CEGAR-based approaches for the safety verification of PLC-controlled plants
Conference paper
A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
Gereon Kremer, Florian Corzilius, Erika Ábrahám
Computer algebra in scientific computing
PDF of A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic RWTH record for A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic BibTeX for A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
Journal article
Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis
Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, Erika Ábrahám
IMA journal of mathematical control and information
RWTH record for Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis BibTeX for Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis
Journal article
Observable Interface Behaviour and Inheritance
Erika Ábrahám, Thi Mai Thuong Tran, Martin Steffen
Mathematical structures in computer science
RWTH record for Observable Interface Behaviour and Inheritance BibTeX for Observable Interface Behaviour and Inheritance
Conference paper
Multi-objective optimization of solar tower power plants
Pascal Richter, Martin Frank, Erika Ábrahám
Progress in industrial mathematics at ECMI 2014
RWTH record for Multi-objective optimization of solar tower power plants BibTeX for Multi-objective optimization of solar tower power plants

2015

Conference paper
Learning-based Control Strategies for Hybrid Electric Vehicles
Sascha Geulen, Martina Josevski, Johanna Nellen, Janosch Fuchs, Lukas Stephan Michael Netz, Benedikt Wolters, Dirk Abel, Erika Ábrahám, Walter Unger
2015 IEEE Conference on Control Applications (CCA 2015)
RWTH record for Learning-based Control Strategies for Hybrid Electric Vehicles BibTeX for Learning-based Control Strategies for Hybrid Electric Vehicles
Conference paper
Preparing HPC Applications for Exascale: Challenges and Recommendations
Erika Ábrahám, Costas Bekas, Ivona Brandic, Samir Genaim, Einar Broch Johnsen, Ivan Kondov, Sabri Pllana, Achim Streit
Proceedings
RWTH record for Preparing HPC Applications for Exascale: Challenges and Recommendations BibTeX for Preparing HPC Applications for Exascale: Challenges and Recommendations
Conference paper
Online Lernen als Kontrollstrategie in Hybridfahrzeugen
Sascha Geulen, Martina Joševski, Johanna Nellen, Janosch Fuchs, Lukas Stephan Michael Netz, Benedikt Wolters, Erika Ábrahám, Walter Unger, Dirk Abel
Autoreg 2015
RWTH record for Online Lernen als Kontrollstrategie in Hybridfahrzeugen BibTeX for Online Lernen als Kontrollstrategie in Hybridfahrzeugen
Preprint
Challenges and Recommendations for Preparing HPC Applications for Exascale
Erika Ábrahám, Costas Bekas, Ivona Brandic, Samir Genaim, Einar Broch Johnsen, Ivan Kondov, Sabri Pllana, Achim Streit
PDF of Challenges and Recommendations for Preparing HPC Applications for Exascale RWTH record for Challenges and Recommendations for Preparing HPC Applications for Exascale BibTeX for Challenges and Recommendations for Preparing HPC Applications for Exascale
Conference paper
A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs
Johanna Nellen, Benedikt Wolters, Lukas Stephan Michael Netz, Sascha Geulen, Erika Ábrahám
GCAI 2015
RWTH record for A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs BibTeX for A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs
Conference paper
Flow* 1.2: More Effective to Play with Hybrid Systems
Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám
ARCH14-15. 1st and 2nd International Workshop on Applied veRication for Continuous and Hybrid Systems
RWTH record for Flow* 1.2: More Effective to Play with Hybrid Systems BibTeX for Flow* 1.2: More Effective to Play with Hybrid Systems
Conference paper
Current Challenges in the Verification of Hybrid Systems
Stefan Schupp, Erika Ábrahám, Xin Chen, Ibtissem Ben Makhlouf, Goran Frehse, Sriram Sankaranarayanan, Stefan Kowalewski
Cyber physical systems
RWTH record for Current Challenges in the Verification of Hybrid Systems BibTeX for Current Challenges in the Verification of Hybrid Systems
Conference paper
PROPhESY : A PRObabilistic ParamEter SYnthesis Tool
Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám
Computer aided verification
RWTH record for PROPhESY : A PRObabilistic ParamEter SYnthesis Tool BibTeX for PROPhESY : A PRObabilistic ParamEter SYnthesis Tool
Book chapter
A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata
Johanna Nellen, Erika Ábrahám, Benedikt Wolters
Formalisms for Reuse and Systems Integration
RWTH record for A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata BibTeX for A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata
Conference paper
A Greedy Approach for the Efficient Repair of Stochastic Models
Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen
NASA Formal Methods
RWTH record for A Greedy Approach for the Efficient Repair of Stochastic Models BibTeX for A Greedy Approach for the Efficient Repair of Stochastic Models
Conference paper
SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám
Theory and Applications of Satisfiability Testing
RWTH record for SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving BibTeX for SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Conference paper
Building Bridges between Symbolic Computation and Satisfiability Checking
Erika Ábrahám
Proceedings of the 14th International Symposium on Symbolic and Algebraic Computation ; Bath, United Kingdom July 06 -09, 2015 ; ISSAC 2015
RWTH record for Building Bridges between Symbolic Computation and Satisfiability Checking BibTeX for Building Bridges between Symbolic Computation and Satisfiability Checking
Conference paper
A Benchmark Suite for Hybrid Systems Reachability Analysis
Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse, Stefan Kowalewski
NASA Formal Methods ; 7th International Symposium, NFM 2015, Pasadena, Calif., USA, April 27-29, 2015, Proceedings
RWTH record for A Benchmark Suite for Hybrid Systems Reachability Analysis BibTeX for A Benchmark Suite for Hybrid Systems Reachability Analysis
Conference paper
Counterexamples for Expected Rewards
Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
FM 2015: formal methods
RWTH record for Counterexamples for Expected Rewards BibTeX for Counterexamples for Expected Rewards
Journal article
High-level Counterexamples for Probabilistic Automata
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
Logical methods in computer science
PDF of High-level Counterexamples for Probabilistic Automata RWTH record for High-level Counterexamples for Probabilistic Automata BibTeX for High-level Counterexamples for Probabilistic Automata

2014

Proceedings
Tools and Algorithms for the Construction and Analysis of Systems : 20th international conference, TACAS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5 - 13, 2014 ; proceedings
Springer
RWTH record for Tools and Algorithms for the Construction and Analysis of Systems : 20th international conference, TACAS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5 - 13, 2014 ; proceedings BibTeX for Tools and Algorithms for the Construction and Analysis of Systems : 20th international conference, TACAS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5 - 13, 2014 ; proceedings
Journal article
Randomized Timed and Hybrid Models for Critical Infrastructures
Dagstuhl Reports
PDF of Randomized Timed and Hybrid Models for Critical Infrastructures RWTH record for Randomized Timed and Hybrid Models for Critical Infrastructures BibTeX for Randomized Timed and Hybrid Models for Critical Infrastructures
Conference paper
Counterexample Generation for Hybrid Automata
Johanna Nellen, Erika Ábrahám, Xin Chen, Pieter Collins
Formal techniques for safety-critical systems
RWTH record for Counterexample Generation for Hybrid Automata BibTeX for Counterexample Generation for Hybrid Automata
Conference paper
A CEGAR Approach for the Reachability Analysis of PLC-controlled Chemical Plants
Johanna Nellen, Erika Ábrahám
2014 IEEE 15th International Conference on Information Reuse and Integration (IRI)
RWTH record for A CEGAR Approach for the Reachability Analysis of PLC-controlled Chemical Plants BibTeX for A CEGAR Approach for the Reachability Analysis of PLC-controlled Chemical Plants
Proceedings
Formal techniques for distributed objects, components, and systems : 34th IFIP WG 6.1 international conference, FORTE 2014, held as part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3 - 5, 2014 ; proceedings
Springer
RWTH record for Formal techniques for distributed objects, components, and systems : 34th IFIP WG 6.1 international conference, FORTE 2014, held as part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3 - 5, 2014 ; proceedings BibTeX for Formal techniques for distributed objects, components, and systems : 34th IFIP WG 6.1 international conference, FORTE 2014, held as part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3 - 5, 2014 ; proceedings
Conference paper
Accelerating Parametric Probabilistic Verification
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Quantitative evaluation of systems
RWTH record for Accelerating Parametric Probabilistic Verification BibTeX for Accelerating Parametric Probabilistic Verification
Conference paper
Fast Debugging of PRISM Models
Hans Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
Automated technology for verification and analysis
RWTH record for Fast Debugging of PRISM Models BibTeX for Fast Debugging of PRISM Models
Journal article
Minimal counterexamples for linear-time probabilistic verification
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Theoretical computer science
RWTH record for Minimal counterexamples for linear-time probabilistic verification BibTeX for Minimal counterexamples for linear-time probabilistic verification
Journal article
Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám
Science of computer programming
RWTH record for Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?BibTeX for Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?
Journal article
Symbolic counterexample generation for large discrete-time Markov chains
Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster
Science of computer programming
RWTH record for Symbolic counterexample generation for large discrete-time Markov chains BibTeX for Symbolic counterexample generation for large discrete-time Markov chains
Journal article
Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories
Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky
Science of computer programming
RWTH record for Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories BibTeX for Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories
Conference paper
Under-approximate Flowpipes for Non-linear Continuous Systems
Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám
2014 formal methods in computer-aided design (FMCAD 2014)
RWTH record for Under-approximate Flowpipes for Non-linear Continuous Systems BibTeX for Under-approximate Flowpipes for Non-linear Continuous Systems
Conference paper
Maybe or Maybe not : Contributions to Stochastic Verification
Ralf Wimmer, Erika Ábrahám
Aspekte der Technischen Informatik
RWTH record for Maybe or Maybe not : Contributions to Stochastic Verification BibTeX for Maybe or Maybe not : Contributions to Stochastic Verification
Conference paper
Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey
Erika Ábrahám, Bernd Becker, Hans Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer
Formal methods for executable software models
RWTH record for Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey BibTeX for Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey

2013

Conference paper
From Statistical Model Checking to Statistical Model Inference : Characterizing the Effect of Process Variations in Analog Circuits
Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Fabio Somenzi, Erika Ábrahám
2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2013)
RWTH record for From Statistical Model Checking to Statistical Model Inference : Characterizing the Effect of Process Variations in Analog Circuits BibTeX for From Statistical Model Checking to Statistical Model Inference : Characterizing the Effect of Process Variations in Analog Circuits
Preprint
Accelerating Parametric Probabilistic Verification
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
PDF of Accelerating Parametric Probabilistic Verification RWTH record for Accelerating Parametric Probabilistic Verification BibTeX for Accelerating Parametric Probabilistic Verification
Book chapter
On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers
Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám
Aachener Informatik-Berichte
PDF of On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers RWTH record for On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers BibTeX for On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers
Conference paper
On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers
Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám
Algebraic informatics
RWTH record for On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers BibTeX for On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers
Conference paper
High-level Counterexamples for Probabilistic Automata
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Quantitative evaluation of systems
RWTH record for High-level Counterexamples for Probabilistic Automata BibTeX for High-level Counterexamples for Probabilistic Automata
Conference paper
Lyapunov Function Synthesis using Handelman Representations
Sriram Sankaranarayanan, Xin Chen, Erika Ábrahám
9th IFAC Symposium on Nonlinear Control Systems 2013
RWTH record for Lyapunov Function Synthesis using Handelman Representations BibTeX for Lyapunov Function Synthesis using Handelman Representations
Conference paper
Stochastic Bounded Model Checking : Bounded Rewards and Compositionality
Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
RWTH record for Stochastic Bounded Model Checking : Bounded Rewards and Compositionality BibTeX for Stochastic Bounded Model Checking : Bounded Rewards and Compositionality
Conference paper
Flow*: An Analyzer for Non-Linear Hybrid Systems
Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan
Computer aided verification
RWTH record for Flow*: An Analyzer for Non-Linear Hybrid Systems BibTeX for Flow*: An Analyzer for Non-Linear Hybrid Systems
Conference paper
A Timed CTL Model Checker for Real-Time Maude
Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky
Algebra and Coalgebra in Computer Science
RWTH record for A Timed CTL Model Checker for Real-Time Maude BibTeX for A Timed CTL Model Checker for Real-Time Maude
Conference paper
Empirical Flowpipe Constructions for Analog Circuits
Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám
Workshop on Frontiers in Analog CAD (FAC'13) ; [Co-located with the International Solid-State Circuits Conference ISSCC], February 14-15, 2013, David Brower Center, Berkeley, CA
PDF of Empirical Flowpipe Constructions for Analog Circuits RWTH record for Empirical Flowpipe Constructions for Analog Circuits BibTeX for Empirical Flowpipe Constructions for Analog Circuits
Conference paper
A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker
Automated Deduction
RWTH record for A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition BibTeX for A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
Preprint
High-level Counterexamples for Probabilistic Automata
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
PDF of High-level Counterexamples for Probabilistic Automata RWTH record for High-level Counterexamples for Probabilistic Automata BibTeX for High-level Counterexamples for Probabilistic Automata

2012

Conference paper
Timed CTL Model Checking in Real-Time Maude
Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky
Rewriting logic and its applications
RWTH record for Timed CTL Model Checking in Real-Time Maude BibTeX for Timed CTL Model Checking in Real-Time Maude
Conference paper
The COMICS Tool : Computing Minimal Counterexamples for DTMCs
Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Automated technology for verification and analysis
RWTH record for The COMICS Tool : Computing Minimal Counterexamples for DTMCs BibTeX for The COMICS Tool : Computing Minimal Counterexamples for DTMCs
Conference paper
Taylor Model Over-approximations for Flowpipe : Guard Intersections
Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan
5th International Workshop on Numerical Software Verification (NSV'12)
RWTH record for Taylor Model Over-approximations for Flowpipe : Guard Intersections BibTeX for Taylor Model Over-approximations for Flowpipe : Guard Intersections
Conference paper
Symbolic Counterexample Generation for Discrete-time Markov Chains
Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker
Formal aspects of component software
RWTH record for Symbolic Counterexample Generation for Discrete-time Markov Chains BibTeX for Symbolic Counterexample Generation for Discrete-time Markov Chains
Conference paper
Taylor Model Flowpipe Construction for Non-linear Hybrid Systems
Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan
Proceedings of the 33rd IEEE Real-Time Systems Symposium (RTSS'12)
RWTH record for Taylor Model Flowpipe Construction for Non-linear Hybrid Systems BibTeX for Taylor Model Flowpipe Construction for Non-linear Hybrid Systems
Conference paper
SMT-RAT : An SMT-Compliant Nonlinear Real Arithmetic Toolbox
Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika Ábrahám
Theory and applications of satisfiability testing
RWTH record for SMT-RAT : An SMT-Compliant Nonlinear Real Arithmetic Toolbox BibTeX for SMT-RAT : An SMT-Compliant Nonlinear Real Arithmetic Toolbox
Conference paper
Hybrid Sequential Function Charts
Johanna Nellen, Erika Ábrahám
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
PDF of Hybrid Sequential Function Charts RWTH record for Hybrid Sequential Function Charts BibTeX for Hybrid Sequential Function Charts
Conference paper
Some Like It Very Hot : Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám
Rewriting logic and its applications
RWTH record for Some Like It Very Hot : Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude BibTeX for Some Like It Very Hot : Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude
Conference paper
Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems
Xin Chen, Erika Ábrahám
Computer aided systems theory - EUROCAST 2011
RWTH record for Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems BibTeX for Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems
Technical report
The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains
Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
PDF of The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains RWTH record for The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains BibTeX for The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains
Conference paper
Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
RWTH record for Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties BibTeX for Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties
Technical report
Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
PDF of Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes RWTH record for Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes BibTeX for Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes
Conference paper
Minimal Critical Subsystems for Discrete-Time Markov Models
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen
Tools and algorithms for the construction and analysis of systems
RWTH record for Minimal Critical Subsystems for Discrete-Time Markov Models BibTeX for Minimal Critical Subsystems for Discrete-Time Markov Models

2011

Conference paper
SMT-based Counterexample Generation for Markov Chains
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
RWTH record for SMT-based Counterexample Generation for Markov Chains BibTeX for SMT-based Counterexample Generation for Markov Chains
Journal article
Parallel SAT Solving in Bounded Model Checking
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde
Journal of logic and computation
RWTH record for Parallel SAT Solving in Bounded Model Checking BibTeX for Parallel SAT Solving in Bounded Model Checking
Conference paper
Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám
Software engineering and formal methods
RWTH record for Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude BibTeX for Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude
Conference paper
Hierarchical counterexamples for discrete-time markov chains
Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Automated technolgoy for verification and analysis
RWTH record for Hierarchical counterexamples for discrete-time markov chains BibTeX for Hierarchical counterexamples for discrete-time markov chains
Conference paper
Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
Formal techniques for distributed systems
RWTH record for Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking BibTeX for Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking
Conference paper
Efficient bounded reachability computation for rectangular automata
Xin Chen, Erika Ábrahám, Goran Frehse
Reachability problems
RWTH record for Efficient bounded reachability computation for rectangular automata BibTeX for Efficient bounded reachability computation for rectangular automata
Conference paper
Formal modeling and analysis of hybrid systems in rewriting logic using higher-order numerical methods and discrete-event detection
Muhammad Fadlisyah, P. C. Olveczky, Erika Ábrahám
2011 CSI International Symposium on Computer Science and Software Engineering (CSSE 2011)
RWTH record for Formal modeling and analysis of hybrid systems in rewriting logic using higher-order numerical methods and discrete-event detection BibTeX for Formal modeling and analysis of hybrid systems in rewriting logic using higher-order numerical methods and discrete-event detection
Conference paper
Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks
Pascal Richter, Erika Ábrahám, Gabriel Morin
Adaptive and natural computing algorithms
RWTH record for Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks BibTeX for Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks
Conference paper
GiNaCRA: A C++ Library for Real Algebraic Computations
Ulrich Loup, Erika Ábrahám
NASA formal methods
RWTH record for GiNaCRA: A C++ Library for Real Algebraic Computations BibTeX for GiNaCRA: A C++ Library for Real Algebraic Computations
Conference paper
Virtual Substitution for SMT-Solving
Florian Corzilius, Erika Ábrahám
Fundamentals of computation theory
RWTH record for Virtual Substitution for SMT-Solving BibTeX for Virtual Substitution for SMT-Solving
Conference paper
I-RiSC : an SMT-Compliant Solver for the Existential Fragment of Real Algebra
Ulrich Loup, Erika Ábrahám
Algebraic informatics
RWTH record for I-RiSC : an SMT-Compliant Solver for the Existential Fragment of Real Algebra BibTeX for I-RiSC : an SMT-Compliant Solver for the Existential Fragment of Real Algebra

2010

Journal article
Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems
Muhammad Fadlisyah, Erika Ábrahám, Peter Csaba Ölveczky
Electronic notes in theoretical computer science
RWTH record for Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems BibTeX for Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems
Journal article
The Scalasca performance toolset architecture
Markus Geimer, Felix Gerd Eugen Wolf, Brian J. N. Wylie, Erika Ábrahám, Daniel Becker, Bernd Mohr
Concurrency and computation
RWTH record for The Scalasca performance toolset architecture BibTeX for The Scalasca performance toolset architecture
Conference paper
Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications
Daniela Lepri, Peter Csaba Ölveczky, Erika Ábrahám
Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010): Longyearbyen, April 6-9, 2010
RWTH record for Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications BibTeX for Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications
Conference paper
A Rewriting-Logic-Based Technique for Modeling Thermal Systems
Muhammad Fadlisyah, Erika Ábrahám, Daniela Lepri, Peter Csaba Ölveczky
Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010): Longyearbyen, April 6-9, 2010
RWTH record for A Rewriting-Logic-Based Technique for Modeling Thermal Systems BibTeX for A Rewriting-Logic-Based Technique for Modeling Thermal Systems
Conference paper
SMT-Solving in the Analysis and Synthesis of Hybrid Systems
Erika Ábrahám, Ulrich Loup, Florian Corzilius, Thomas Sturm
Verification over discrete-continuous boundaries
RWTH record for SMT-Solving in the Analysis and Synthesis of Hybrid Systems BibTeX for SMT-Solving in the Analysis and Synthesis of Hybrid Systems
Conference paper
Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik
Erika Ábrahám, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Ulrik Schroeder
DeLFI 2010
PDF of Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik RWTH record for Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik BibTeX for Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik
Conference paper
Exploiting Different Strategies for the Parallelization of an SMT Solver
Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker
13. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
RWTH record for Exploiting Different Strategies for the Parallelization of an SMT Solver BibTeX for Exploiting Different Strategies for the Parallelization of an SMT Solver
Conference paper
DTMC Model Checking by SCC Reduction
Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Proceedings
RWTH record for DTMC Model Checking by SCC Reduction BibTeX for DTMC Model Checking by SCC Reduction
Conference paper
Synthesis of Behavioral Controllers for DES: Increasing Efficiency
Kai Bollue, Michaela Slaats, Erika Ábrahám, Wolfgang Thomas, Dirk Abel
WODES 2010
RWTH record for Synthesis of Behavioral Controllers for DES: Increasing Efficiency BibTeX for Synthesis of Behavioral Controllers for DES: Increasing Efficiency

2009

Journal article
Behavioral interface description of an object-oriented language with futures and promises
Erika Ábrahám, Immo Grabe, Andreas Grüner, Martin Steffen
The journal of logic and algebraic programming
RWTH record for Behavioral interface description of an object-oriented language with futures and promises BibTeX for Behavioral interface description of an object-oriented language with futures and promises
Conference paper
SMT-Solving for the First-Order Theory of the Reals
Erika Ábrahám, Ulrich Loup
Algorithms and Applications for Next Generation SAT Solvers
RWTH record for SMT-Solving for the First-Order Theory of the Reals BibTeX for SMT-Solving for the First-Order Theory of the Reals
Conference paper
Picoso - A Parallel Interval Constraint Solver
Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker
Proceedings of the 2009 International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2009
RWTH record for Picoso - A Parallel Interval Constraint Solver BibTeX for Picoso - A Parallel Interval Constraint Solver

2008

Journal article
Abstract Interface Behavior of Object-Oriented Languages with Monitors
Erika Ábrahám, Andreas Grüner, Martin Steffen
Theory of computing systems
RWTH record for Abstract Interface Behavior of Object-Oriented Languages with Monitors BibTeX for Abstract Interface Behavior of Object-Oriented Languages with Monitors
Journal article
A Deductive Proof System for Multithreaded Java with Exceptions
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen
Fundamenta informaticae
RWTH record for A Deductive Proof System for Multithreaded Java with Exceptions BibTeX for A Deductive Proof System for Multithreaded Java with Exceptions
Journal article
Heap-abstraction for an object-oriented calculus with thread classes
Erika Ábrahám, Andreas Grüner, Martin Steffen
Software and systems modeling
RWTH record for Heap-abstraction for an object-oriented calculus with thread classes BibTeX for Heap-abstraction for an object-oriented calculus with thread classes
Conference paper
Usage of the SCALASCA toolset for scalable performance analysis of large-scale parallel applications
Felix Gerd Eugen Wolf, Brian J. N. Wylie, Erika Ábrahám, Daniel Becker, Wolfgang Frings, Karl Fürlinger, Markus Geimer, Marc-André Hermanns, Bernd Mohr, Shirley Moore, Matthias Pfeifer, Zoltán Péter Szebenyi
Tools for high performance computing
RWTH record for Usage of the SCALASCA toolset for scalable performance analysis of large-scale parallel applications BibTeX for Usage of the SCALASCA toolset for scalable performance analysis of large-scale parallel applications

2007

Conference paper
On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata
Marc Herbstritt, Bernd Becker, Erika Ábrahám, Christian Herde
2007 IEEE design and diagnostics of electronic circuits and systems
RWTH record for On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata BibTeX for On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata
Conference paper
Parallel SAT solving in bounded model checking
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde
Formal methods: applications and technology ; 11th international workshop, FMICS 2006, and 5th international workshop, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006 ; revised selected papers
RWTH record for Parallel SAT solving in bounded model checking BibTeX for Parallel SAT solving in bounded model checking

2006

Journal article
Bounded model checking with parametric data structures
Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen
Electronic notes in theoretical computer science
RWTH record for Bounded model checking with parametric data structures BibTeX for Bounded model checking with parametric data structures
Conference paper
Memory-aware bounded model checking for linear hybrid systems
Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
RWTH record for Memory-aware bounded model checking for linear hybrid systems BibTeX for Memory-aware bounded model checking for linear hybrid systems
Conference paper
Dynamic heap-abstraction for open, object-oriented systems with thread classes
Erika Ábrahám, Andreas Grüner, Martin Steffen
Logical approaches to computational barriers
RWTH record for Dynamic heap-abstraction for open, object-oriented systems with thread classes BibTeX for Dynamic heap-abstraction for open, object-oriented systems with thread classes
Conference paper
Abstract interface behavior of object-oriented languages with monitors
Erika Ábrahám, Andreas Grüner, Martin Steffen
Formal methods for open object-based distributed systems
RWTH record for Abstract interface behavior of object-oriented languages with monitors BibTeX for Abstract interface behavior of object-oriented languages with monitors

2005

Journal article
An Assertion-Based Proof System for Multithreaded Java
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen
Theoretical computer science
RWTH record for An Assertion-Based Proof System for Multithreaded Java BibTeX for An Assertion-Based Proof System for Multithreaded Java
Conference paper
Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes
Erika Ábrahám, Andreas Grüner, Martin Steffen
COSMICAH 2005
RWTH record for Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes BibTeX for Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes
Conference paper
Optimizing Bounded Model Checking for Linear Hybrid Systems
Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen
Verification, model checking, and abstract interpretation
RWTH record for Optimizing Bounded Model Checking for Linear Hybrid Systems BibTeX for Optimizing Bounded Model Checking for Linear Hybrid Systems
Conference paper
A Fully Abstract Trace Semantics for UML Components
Frank S. de Boer, Marcello Bonsangue, Martin Steffen, Erika Ábrahám
Formal methods for components and objects
RWTH record for A Fully Abstract Trace Semantics for UML Components BibTeX for A Fully Abstract Trace Semantics for UML Components
Conference paper
Observability, Connectivity, and Replay in a Sequential Calculus of Classes
Erika Ábrahám, Frank S. de Boer, Marcello Bonsangue, Andreas Grüner, Martin Steffen
Formal methods for components and objects
RWTH record for Observability, Connectivity, and Replay in a Sequential Calculus of Classes BibTeX for Observability, Connectivity, and Replay in a Sequential Calculus of Classes
Conference paper
Inductive Proof Outlines for Exceptions in Multithreaded Java
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen
Proceedings of the First IPM International Workshop on Foundations of Software Engineering (FSEN 2005)
RWTH record for Inductive Proof Outlines for Exceptions in Multithreaded Java BibTeX for Inductive Proof Outlines for Exceptions in Multithreaded Java
Conference paper
Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes
Erika Ábrahám, Marcello Bonsangue, Frank S. de Boer, Martin Steffen
Theoretical aspects of computing - ICTAC 2004
RWTH record for Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes BibTeX for Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes

Supervised theses

2026

PhD thesis
Probabilistic hyperlogics: extensions and efficient model checking
Lina Gerlach
RWTH Aachen University
Advisers: Erika Abraham, Rayna Dimitrova
PDF of Probabilistic hyperlogics: extensions and efficient model checking RWTH record for Probabilistic hyperlogics: extensions and efficient model checking BibTeX for Probabilistic hyperlogics: extensions and efficient model checking
PhD thesis
Synthesis and analysis of neural-network-based control in cyber-physical systems
László Antal
RWTH Aachen University
Advisers: Erika Ábrahám, Ana Maria Madureira
PDF of Synthesis and analysis of neural-network-based control in cyber-physical systems RWTH record for Synthesis and analysis of neural-network-based control in cyber-physical systems BibTeX for Synthesis and analysis of neural-network-based control in cyber-physical systems

2025

PhD thesis
Cylindrical algebraic decomposition based methods in satisfiability modulo non-linear real arithmetic
Jasper Kurt Ferdinand Nalbach
RWTH Aachen University
Advisers: Erika Abraham, James H. Davenport
PDF of Cylindrical algebraic decomposition based methods in satisfiability modulo non-linear real arithmetic RWTH record for Cylindrical algebraic decomposition based methods in satisfiability modulo non-linear real arithmetic BibTeX for Cylindrical algebraic decomposition based methods in satisfiability modulo non-linear real arithmetic

2024

Bachelor’s thesis
Testing the applicability of robustness evaluation methods for neural networks on nonlinear real arithmetic problems using α-β-CROWN and foolbox
Julia Walczak
RWTH Aachen University
Advisers: Thomas Noll, Erika Abraham
Consultants: Christopher Jan-Steffen Brix
RWTH record for Testing the applicability of robustness evaluation methods for neural networks on nonlinear real arithmetic problems using α-β-CROWN and foolbox BibTeX for Testing the applicability of robustness evaluation methods for neural networks on nonlinear real arithmetic problems using α-β-CROWN and foolbox
Bachelor’s thesis
Proving termination of probabilistic recursive programs via SMT-solving
Leo Mommers
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Erika Ábrahám
Consultants: Tobias Winkler
PDF of Proving termination of probabilistic recursive programs via SMT-solving RWTH record for Proving termination of probabilistic recursive programs via SMT-solving BibTeX for Proving termination of probabilistic recursive programs via SMT-solving

2023

Master’s thesis
Generate elaborative feedback for novices’ programming exercises based on interaction data
Johanna Tolzmann
RWTH Aachen University
Advisers: Ulrik Schroeder, Erika Ábrahám
Consultants: Annabell Brocker
PDF of Generate elaborative feedback for novices’ programming exercises based on interaction data RWTH record for Generate elaborative feedback for novices’ programming exercises based on interaction data BibTeX for Generate elaborative feedback for novices’ programming exercises based on interaction data
Bachelor’s thesis
Exploiting strict constraints in the computation of cylindrical algebraic coverings
Philipp Bär
RWTH Aachen University
Advisers: Erika Ábrahám, Jürgen Giesl
Consultants: Jasper Kurt Ferdinand Nalbach
PDF of Exploiting strict constraints in the computation of cylindrical algebraic coverings RWTH record for Exploiting strict constraints in the computation of cylindrical algebraic coverings BibTeX for Exploiting strict constraints in the computation of cylindrical algebraic coverings

2022

PhD thesis
Optimisation and analysis of railway timetables under consideration of uncertainties
Rebecca Haehn
RWTH Aachen University
Advisers: Erika Ábrahám, Nils Nießen, Anne Remke
PDF of Optimisation and analysis of railway timetables under consideration of uncertainties RWTH record for Optimisation and analysis of railway timetables under consideration of uncertainties BibTeX for Optimisation and analysis of railway timetables under consideration of uncertainties

2021

Master’s thesis
Accelerating symbolic simulation to analyze the effect of delays in train timetables
Niklas Kotowski
RWTH Aachen University
Advisers: Erika Ábrahám, Thomas Noll
Consultants: Rebecca Haehn
PDF of Accelerating symbolic simulation to analyze the effect of delays in train timetables RWTH record for Accelerating symbolic simulation to analyze the effect of delays in train timetables BibTeX for Accelerating symbolic simulation to analyze the effect of delays in train timetables
PhD thesis
Determinization and ambiguity of classical and probabilistic Büchi automata
Anton Pirogov
RWTH Aachen University
Advisers: Christof Löding, Erika Ábrahám, Sven Schewe
PDF of Determinization and ambiguity of classical and probabilistic Büchi automata RWTH record for Determinization and ambiguity of classical and probabilistic Büchi automata BibTeX for Determinization and ambiguity of classical and probabilistic Büchi automata

2020

Master’s thesis
A novel adaption of the Simplex algorithm for linear real arithmetic
Jasper Kurt Ferdinand Nalbach
RWTH Aachen University
Advisers: Erika Ábrahám, Christina Maria Katharina Büsing
Consultants: Gereon Kremer
PDF of A novel adaption of the Simplex algorithm for linear real arithmetic RWTH record for A novel adaption of the Simplex algorithm for linear real arithmetic BibTeX for A novel adaption of the Simplex algorithm for linear real arithmetic
Master’s thesis
Parameter synthesis in probabilistic timed automata
Bram Kohlen
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Erika Ábrahám
Consultants: Jip Josephine Spel
RWTH record for Parameter synthesis in probabilistic timed automata BibTeX for Parameter synthesis in probabilistic timed automata
PhD thesis
Optimal planning modulo theories
Francesco Leofante
RWTH Aachen University
Advisers: Erika Ábrahám, Armando Tacchella
PDF of Optimal planning modulo theories RWTH record for Optimal planning modulo theories BibTeX for Optimal planning modulo theories
PhD thesis
Cylindrical algebraic decomposition for nonlinear arithmetic problems
Gereon Kremer
RWTH Aachen University
Advisers: Erika Ábrahám, James H. Davenport, Viktor Levandovskyy
PDF of Cylindrical algebraic decomposition for nonlinear arithmetic problems RWTH record for Cylindrical algebraic decomposition for nonlinear arithmetic problems BibTeX for Cylindrical algebraic decomposition for nonlinear arithmetic problems

2019

PhD thesis
State set representations and their usage in the reachability analysis of hybrid systems
Stefan Schupp
RWTH Aachen University
Advisers: Erika Ábrahám, Goran Frehse
PDF of State set representations and their usage in the reachability analysis of hybrid systems RWTH record for State set representations and their usage in the reachability analysis of hybrid systems BibTeX for State set representations and their usage in the reachability analysis of hybrid systems

2018

PhD thesis
On solving real-algebraic formulas in a satisfiability-modulo-theories framework
Ulrich Loup
RWTH Aachen University
Advisers: Erika Ábrahám, Viktor Levandovskyy, Thomas Sturm
PDF of On solving real-algebraic formulas in a satisfiability-modulo-theories framework RWTH record for On solving real-algebraic formulas in a satisfiability-modulo-theories framework BibTeX for On solving real-algebraic formulas in a satisfiability-modulo-theories framework
PhD thesis
Differentiation of numerical simulations with embedded nonlinear systems and integrals
Niloofar Safiran
RWTH Aachen University
Advisers: Uwe Naumann, Erika Ábrahám
PDF of Differentiation of numerical simulations with embedded nonlinear systems and integrals RWTH record for Differentiation of numerical simulations with embedded nonlinear systems and integrals BibTeX for Differentiation of numerical simulations with embedded nonlinear systems and integrals

2017

PhD thesis
Berechnung und Bewertung der Gesamtleistungsfähigkeit von Eisenbahnnetzen
Christian Meirich
Rheinisch-Westfälische Technische Hochschule Aachen
Advisers: Nils Nießen, Erika Ábrahám
PDF of Berechnung und Bewertung der Gesamtleistungsfähigkeit von Eisenbahnnetzen RWTH record for Berechnung und Bewertung der Gesamtleistungsfähigkeit von Eisenbahnnetzen BibTeX for Berechnung und Bewertung der Gesamtleistungsfähigkeit von Eisenbahnnetzen

2016

PhD thesis
Integrating virtual substitution into strategic SMT solving
Florian Corzilius
RWTH Aachen University
Advisers: Erika Ábrahám, Pascal Fontaine
PDF of Integrating virtual substitution into strategic SMT solving RWTH record for Integrating virtual substitution into strategic SMT solving BibTeX for Integrating virtual substitution into strategic SMT solving
PhD thesis
Analysis and synthesis of hybrid systems in engineering applications
Johanna Nellen
RWTH Aachen University
Advisers: Erika Ábrahám, Walter Unger
PDF of Analysis and synthesis of hybrid systems in engineering applications RWTH record for Analysis and synthesis of hybrid systems in engineering applications BibTeX for Analysis and synthesis of hybrid systems in engineering applications

2015

PhD thesis
Counterexamples in probabilistic verification
Nils Jansen
Aachen, Techn. Hochsch.
Advisers: Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen
PDF of Counterexamples in probabilistic verification RWTH record for Counterexamples in probabilistic verification BibTeX for Counterexamples in probabilistic verification
PhD thesis
Reachability analysis of non-linear hybrid systems using Taylor Models
Xin Chen
RWTH Aachen University
Advisers: Erika Ábrahám, Sriram Sankaranarayanan
PDF of Reachability analysis of non-linear hybrid systems using Taylor Models RWTH record for Reachability analysis of non-linear hybrid systems using Taylor Models BibTeX for Reachability analysis of non-linear hybrid systems using Taylor Models

2011

Thesis
Webbasierte konstruktivistische Lernumgebung für PHP und Datenbanken
Till Königshofen
Rheinisch-Westfälische Technische Hochschule Aachen
Advisers: Ulrik Schroeder, Erika Ábrahám, Thiemo Leonhardt, Daniel Herding
RWTH record for Webbasierte konstruktivistische Lernumgebung für PHP und Datenbanken BibTeX for Webbasierte konstruktivistische Lernumgebung für PHP und Datenbanken

All records on RWTH Publications