Publications-New

Split title: 'On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract)'
Fixed Title: 'On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract)'
Split title: 'Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development'
Fixed Title: 'Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development'
Split title: 'Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)'
Fixed Title: 'Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)'
Split title: 'The HyDRA Tool : A Playground for the Development of Hybrid Systems Reachability Analysis Methods'
Fixed Title: 'The HyDRA Tool: A Playground for the Development of Hybrid Systems Reachability Analysis Methods'
Split title: 'Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics'
Fixed Title: 'Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics'
Split title: '2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering : GE 2018 : 28 May 2018, Gothenburg, Sweden : proceedings'
Fixed Title: '2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering: GE 2018'
Split title: 'HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties'
Fixed Title: 'HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties'
Split title: 'Task Planning with OMT: An Application to Production Logistics'
Fixed Title: 'Task Planning with OMT: An Application to Production Logistics'
Split title: 'Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations'
Fixed Title: 'Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations'
Split title: 'Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain'
Fixed Title: 'Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain'
Split title: 'Spread the Work : Multi-threaded Safety Analysis for Hybrid Systems'
Fixed Title: 'Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems'
Split title: 'SMT Solving for Arithmetic Theories: Theory and Tool Support'
Fixed Title: 'SMT Solving for Arithmetic Theories: Theory and Tool Support'
Split title: 'Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017'
Fixed Title: 'Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis'
Split title: 'Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017'
Fixed Title: 'Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis'
Split title: 'SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces'
Fixed Title: 'SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces'
Split title: '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'
Fixed Title: 'Bridging two communities to solve real problems: SC2 2016'
Split title: 'HyPro : A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis'
Fixed Title: 'HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis'
Split title: 'Divide and Conquer : Variable Set Separation in Hybrid Systems Reachability Analysis'
Fixed Title: 'Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis'
Split title: 'Symbolic Computation and Satisfiability Checking : Report of Dagstuhl Seminar 15471'
Fixed Title: 'Symbolic Computation and Satisfiability Checking: Report of Dagstuhl Seminar 15471'
Split title: 'Integrated formal methods : 12th international conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016 : proceedings'
Fixed Title: 'Integrated formal methods'
Split title: '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'
Fixed Title: 'Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR)'
Split title: 'Satisfiability Checking : Theory and Applications'
Fixed Title: 'Satisfiability Checking: Theory and Applications'
Split title: 'Theory and practice of formal methods : essays dedicated to Frank de Boer on the occasion of his 60th birthday'
Fixed Title: 'Theory and practice of formal methods: essays dedicated to Frank de Boer on the occasion of his 60th birthday'
Split title: 'Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies'
Fixed Title: 'Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies'
Split title: 'SC2 : Satisfiability Checking Meets Symbolic Computation'
Fixed Title: 'SC2: Satisfiability Checking Meets Symbolic Computation'
Split title: 'Preparing HPC Applications for Exascale: Challenges and Recommendations'
Fixed Title: 'Preparing HPC Applications for Exascale: Challenges and Recommendations'
Split title: 'Flow* 1.2: More Effective to Play with Hybrid Systems'
Fixed Title: 'Flow* 1.2: More Effective to Play with Hybrid Systems'
Split title: 'PROPhESY : A PRObabilistic ParamEter SYnthesis Tool'
Fixed Title: 'PROPhESY: A PRObabilistic ParamEter SYnthesis Tool'
Split title: 'SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving'
Fixed Title: 'SMT-RAT: an Open Source C++ Toolbox for Strategic and Parallel SMT Solving'
Split title: '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'
Fixed Title: 'Tools and Algorithms for the Construction and Analysis of Systems'
Split title: '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'
Fixed Title: 'Formal techniques for distributed objects, components, and systems'
Split title: 'Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?'
Fixed Title: 'Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?'
Split title: 'Maybe or Maybe not : Contributions to Stochastic Verification'
Fixed Title: 'Maybe or Maybe not: Contributions to Stochastic Verification'
Split title: 'Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey'
Fixed Title: 'Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey'
Split title: 'From Statistical Model Checking to Statistical Model Inference : Characterizing the Effect of Process Variations in Analog Circuits'
Fixed Title: 'From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits'
Split title: 'Stochastic Bounded Model Checking : Bounded Rewards and Compositionality'
Fixed Title: 'Stochastic Bounded Model Checking: Bounded Rewards and Compositionality'
Split title: 'Flow*: An Analyzer for Non-Linear Hybrid Systems'
Fixed Title: 'Flow*: An Analyzer for Non-Linear Hybrid Systems'
Split title: 'The COMICS Tool : Computing Minimal Counterexamples for DTMCs'
Fixed Title: 'The COMICS Tool: Computing Minimal Counterexamples for DTMCs'
Split title: 'Taylor Model Over-approximations for Flowpipe : Guard Intersections'
Fixed Title: 'Taylor Model Over-approximations for Flowpipe: Guard Intersections'
Split title: 'SMT-RAT : An SMT-Compliant Nonlinear Real Arithmetic Toolbox'
Fixed Title: 'SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox'
Split title: 'Some Like It Very Hot : Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude'
Fixed Title: 'Some Like It Very Hot: Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude'
Split title: 'The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains'
Fixed Title: 'The COMICS Tool: Computing Minimal Counterexamples for Discrete-time Markov Chains'
Split title: 'GiNaCRA: A C++ Library for Real Algebraic Computations'
Fixed Title: 'GiNaCRA: A C++ Library for Real Algebraic Computations'
Split title: 'I-RiSC : an SMT-Compliant Solver for the Existential Fragment of Real Algebra'
Fixed Title: 'I-RiSC: an SMT-Compliant Solver for the Existential Fragment of Real Algebra'
Split title: 'Synthesis of Behavioral Controllers for DES: Increasing Efficiency'
Fixed Title: 'Synthesis of Behavioral Controllers for DES: Increasing Efficiency'
2021
[bibtex]
@conference{SSRTUCSD2021,
title = {Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies},
author = {Rebecca Haehn and Erika Ábrahám and Nils Nießen},
publisher = {Springer},
pages = {257-275},
type = {Conference Paper},
year = {2021},
url = { https://publications.rwth-aachen.de/record/825264},
}×
[issue]
Rebecca Haehn, Erika Ábrahám, Nils Nießen. Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies, 18th International Conference on Quantitative Evaluation of SysTems (QEST 2021), 257-275, Springer, 2021.
DOI fulltext PDF [bibtex]
@article{D2021,
title = {Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
publisher = {Elsevier Science},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {119},
pages = {pages 100633},
type = {Journal Article},
year = {2021},
doi = {10.1016/j.jlamp.2020.100633},
url = { https://publications.rwth-aachen.de/record/816049},
}×
[issue]
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Journal of Logical and Algebraic Methods in Programming 119, pages 100633, Elsevier Science, 2021.
DOI fulltext PDF [bibtex]
@phdthesis{DB2021,
title = {Determinization and ambiguity of classical and probabilistic Büchi automata},
author = {Anton Pirogov},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2021},
doi = {10.18154/RWTH-2021-02027},
url = { https://publications.rwth-aachen.de/record/813936},
}×
[issue]
Anton Pirogov. Determinization and ambiguity of classical and probabilistic Büchi automata, PhD Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, Diagramme, RWTH Aachen University, 2021.
DOI [bibtex]
@conference{EFTLPSI2021,
title = {Extending the Fundamental Theorem of Linear Programming for Strict Inequalities},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Gereon Kremer},
publisher = {Association for Computing Machinery},
booktitle = {ACM Conferences},
pages = {313-320},
type = {Conference Paper},
year = {2021},
doi = {10.1145/3452143.3465538},
url = { https://publications.rwth-aachen.de/record/823081},
}×
[issue]
Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Gereon Kremer. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities, ISSAC '21: International Symposium on Symbolic and Algebraic Computation (ISSAC '21), ACM Conferences, 313-320, Association for Computing Machinery, 2021.
2020
DOI fulltext PDF [bibtex]
@masterthesis{AS2020,
title = {A novel adaption of the Simplex algorithm for linear real arithmetic},
author = {Jasper Kurt Ferdinand Nalbach},
institution = {RWTH Aachen University},
pages = {79 Seiten},
type = {Master Thesis},
year = {2020},
doi = {10.18154/RWTH-2021-04303},
url = { https://publications.rwth-aachen.de/record/818122},
}×
[issue]
Jasper Kurt Ferdinand Nalbach, Gereon Kremer. A novel adaption of the Simplex algorithm for linear real arithmetic, Master Thesis, RWTH Aachen University, 79 Seiten, 2020.
[bibtex]
@masterthesis{P2020,
title = {Parameter synthesis in probabilistic timed automata},
author = {Bram Kohlen},
institution = {RWTH Aachen University},
pages = {91 Seiten},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/811856},
}×
[issue]
Bram Kohlen, Jip Josephine Spel. Parameter synthesis in probabilistic timed automata, Master Thesis, RWTH Aachen University, 91 Seiten, 2020.
DOI fulltext PDF [bibtex]
@phdthesis{O2020,
title = {Optimal planning modulo theories},
author = {Francesco Leofante},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (96 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-06076},
url = { https://publications.rwth-aachen.de/record/792387},
}×
[issue]
Francesco Leofante. Optimal planning modulo theories, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (96 Seiten) : Illustrationen, Diagramme, 2020.
DOI fulltext PDF [bibtex]
@phdthesis{C2020,
title = {Cylindrical algebraic decomposition for nonlinear arithmetic problems},
author = {Gereon Kremer},
booktitle = {Aachener Informatik-Berichte},
volume = {2020-04},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-05913},
url = { https://publications.rwth-aachen.de/record/792185},
}×
[issue]
Gereon Kremer. Cylindrical algebraic decomposition for nonlinear arithmetic problems, PhD Thesis, RWTH Aachen University, Volume 2020-04 of Aachener Informatik-Berichte, 1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme, 2020.
DOI fulltext PDF [bibtex]
@conference{PSPH2020,
title = {Parameter Synthesis for Probabilistic Hyperproperties},
author = {Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour and Oyendrila Dobe},
booktitle = {EPiC Series in Computing},
volume = {73},
pages = {12-31},
type = {Conference Paper},
year = {2020},
doi = {10.29007/37lf},
url = { https://publications.rwth-aachen.de/record/792181},
}×
[issue]
Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe. Parameter Synthesis for Probabilistic Hyperproperties, The 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2020), Volume 73 of EPiC Series in Computing, 12-31, 2020.
DOI [bibtex]
@conference{FTSRS2020,
title = {Freight Train Scheduling in Railway Systems},
author = {Rebecca Haehn and Erika Ábrahám and Nils Nießen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12040},
pages = {225-241},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-43024-5_14},
url = { https://publications.rwth-aachen.de/record/789633},
}×
[issue]
Rebecca Haehn, Erika Ábrahám, Nils Nießen. Freight Train Scheduling in Railway Systems, 20th International Conference on Measurement, Modelling and Evaluation of Computing Systems (MMB 2020), Volume 12040 of LNCS, 225-241, Springer, 2020.
arXiv:2003.05633 [bibtex]
@unpublished{DCNLRACCDSUCAC2020,
title = {Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
publisher = {Elsevier Science},
pages = {41 Seiten},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2003.05633},
}×
[issue]
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings, 41 Seiten, Elsevier Science, 2020. https://arxiv.org/abs/2003.05633
2019
DOI fulltext PDF [bibtex]
@phdthesis{S2019,
title = {State set representations and their usage in the reachability analysis of hybrid systems},
author = {Stefan Schupp},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (217 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2019},
doi = {10.18154/RWTH-2019-08875},
url = { https://publications.rwth-aachen.de/record/767529},
}×
[issue]
Stefan Schupp. State set representations and their usage in the reachability analysis of hybrid systems, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (217 Seiten) : Illustrationen, Diagramme, 2019.
DOI [bibtex]
@conference{MAROSTVAMBD2019,
title = {Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development},
author = {Philipp Berger and Johanna Nellen and Joost-Pieter Katoen and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow},
publisher = {Springer},
booktitle = {LNCS},
volume = {11687},
pages = {59-75},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-27008-7_4},
url = { https://publications.rwth-aachen.de/record/767285},
}×
[issue]
Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development, 24th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019), Volume 11687 of LNCS, 59-75, Springer, 2019.
DOI [bibtex]
@conference{ECFSRVRAIHS2019,
title = {Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems},
author = {Francesco Leofante and Stefan Schupp and Erika Ábrahám and Armando Tacchella},
publisher = {European Council for Modelling and Simulation},
pages = {7 Seiten},
type = {Conference Paper},
year = {2019},
doi = {10.7148/2019-0407},
url = { https://publications.rwth-aachen.de/record/771665},
}×
[issue]
Francesco Leofante, Stefan Schupp, Erika Ábrahám, Armando Tacchella. Engineering Controllers For Swarm Robotics Via Reachability Analysis In Hybrid Systems, 33rd International ECMS Conference on Modelling and Simulation (ECMS 2019), 7 Seiten, European Council for Modelling and Simulation, 2019.
fulltext PDF [bibtex]
@conference{OPCM2019,
title = {On the Proof Complexity of MCSAT},
author = {Gereon Kremer and Erika Ábrahám and Vijay Ganesh},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {2460},
pages = {10 Seiten},
type = {Conference Paper},
year = {2019},
url = { https://publications.rwth-aachen.de/record/771621},
}×
[issue]
Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the Proof Complexity of MCSAT, 4th Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 10 Seiten, RWTH Aachen, 2019.
DOI fulltext PDF [bibtex]
@conference{OVOMNRA2019,
title = {On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract)},
author = {Jasper Kurt Ferdinand Nalbach and Gereon Kremer and Erika Ábrahám},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {2460},
pages = {7 Seiten},
type = {Conference Paper},
year = {2019},
doi = {10.18154/RWTH-CONV-240068},
url = { https://publications.rwth-aachen.de/record/771622},
}×
[issue]
Jasper Kurt Ferdinand Nalbach, Gereon Kremer, Erika Ábrahám. On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract), 4th Workshop on Satisfiability Checking and Symbolic Computation (SC-square), Volume 2460 of CEUR Workshop Proceedings, 7 Seiten, RWTH Aachen, 2019.
DOI [bibtex]
@article{FICAD2019,
title = {Fully Incremental Cylindrical Algebraic Decomposition},
author = {Gereon Kremer and Erika Ábrahám},
publisher = {Elsevier},
journal = {Journal of symbolic computation},
volume = {100},
pages = {pages 11-37},
type = {Journal Article},
year = {2019},
doi = {10.1016/j.jsc.2019.07.018},
url = { https://publications.rwth-aachen.de/record/780485},
}×
[issue]
Gereon Kremer, Erika Ábrahám. Fully Incremental Cylindrical Algebraic Decomposition, Journal of symbolic computation 100, pages 11-37, Elsevier, 2019.
2018
DOI [bibtex]
@conference{TPOAAPL2018,
title = {Task Planning with OMT: An Application to Production Logistics},
author = {Francesco Leofante and Erika Ábrahám and Armando Tacchella},
publisher = {Springer},
booktitle = {Programming and Software Engineering},
volume = {11023},
pages = {316-325},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-98938-9_18},
url = { https://publications.rwth-aachen.de/record/753083},
}×
[issue]
Francesco Leofante, Erika Ábrahám, Armando Tacchella. Task Planning with OMT: An Application to Production Logistics, 14th International Conference on Integrated Formal Methods (IFM 2018), Volume 11023 of Programming and Software Engineering, 316-325, Springer, 2018.
DOI [bibtex]
@conference{CDRAHS2018,
title = {Context-Dependent Reachability Analysis for Hybrid Systems},
author = {Stefan Schupp and Justin Winkens and Erika Ábrahám},
publisher = {IEEE},
pages = {518-525},
type = {Conference Paper},
year = {2018},
doi = {10.1109/IRI.2018.00082},
url = { https://publications.rwth-aachen.de/record/735730},
}×
[issue]
Stefan Schupp, Justin Winkens, Erika Ábrahám. Context-Dependent Reachability Analysis for Hybrid Systems, 2018 IEEE International Conference on Information Reuse and Integration for Data Science (IRI 2018), 518-525, IEEE, 2018.
DOI fulltext PDF [bibtex]
@article{MSSR2018,
title = {Modular strategic SMT solving with SMT-RAT},
author = {Gereon Kremer and Erika Ábrahám},
publisher = {De Gruyter Open},
journal = {Acta Universitatis Sapientiae / Informatica},
volume = {10(1)},
pages = {pages 5-25},
type = {Journal Article},
year = {2018},
doi = {10.2478/ausi-2018-0001},
url = { https://publications.rwth-aachen.de/record/735737},
}×
[issue]
Gereon Kremer, Erika Ábrahám. Modular strategic SMT solving with SMT-RAT, Acta Universitatis Sapientiae / Informatica 10 (1), pages 5-25, De Gruyter Open, 2018.
DOI [bibtex]
@conference{SWMSAHS2018,
title = {Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems},
author = {Stefan Schupp and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {10886},
pages = {89-104},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-92970-5_6},
url = { https://publications.rwth-aachen.de/record/741983},
}×
[issue]
Stefan Schupp, Erika Ábrahám. Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems, 16th International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, 89-104, Springer, 2018.
DOI fulltext PDF [bibtex]
@conference{EDERHSRA2018,
title = {Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis},
author = {Stefan Schupp and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {10806, Part 2},
pages = {287-302},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-89963-3_17},
url = { https://publications.rwth-aachen.de/record/745466},
}×
[issue]
Stefan Schupp, Erika Ábrahám. Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806, Part 2 of LNCS, 287-302, Springer, 2018.
DOI [bibtex]
@conference{VACCSAERAD2018,
title = {Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain},
author = {Philipp Berger and Joost-Pieter Katoen and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow},
publisher = {Springer},
booktitle = {LNCS},
volume = {10951},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-95582-7_18},
url = { https://publications.rwth-aachen.de/record/753075},
}×
[issue]
Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain, 22nd International Symposium of Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.
DOI [bibtex]
@conference{FVASCMETCER2018,
title = {Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations},
author = {Johanna Nellen and Thomas Rambow and Md Tawhid Bin Waez and Erika Ábrahám and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10951},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-95582-7_23},
url = { https://publications.rwth-aachen.de/record/753076},
}×
[issue]
Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Ábrahám, Joost-Pieter Katoen. Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations, 22nd International Symposium on Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.
DOI fulltext PDF [bibtex]
@phdthesis{D2018,
title = {Differentiation of numerical simulations with embedded nonlinear systems and integrals},
author = {Niloofar Safiran},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (iv, 163 Seiten) : Illustrationen},
type = {PhD Thesis},
year = {2018},
doi = {10.18154/RWTH-2018-223992},
url = { https://publications.rwth-aachen.de/record/723136},
}×
[issue]
Niloofar Safiran. Differentiation of numerical simulations with embedded nonlinear systems and integrals, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (iv, 163 Seiten) : Illustrationen, 2018.
DOI [bibtex]
@conference{HATLPH2018,
title = {HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties},
author = {Erika Ábrahám and Borzoo Bonakdarpour},
publisher = {Springer},
booktitle = {LNCS},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-99154-2_2},
url = { https://publications.rwth-aachen.de/record/753085},
}×
[issue]
Erika Ábrahám, Borzoo Bonakdarpour. HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties, 15th International Conference on Quantitative Evaluation of Systems (QEST 2018), LNCS, Springer, 2018.
fulltext PDF [bibtex]
@conference{EECCSS2018,
title = {Evaluation of Equational Constraints for CAD in SMT Solving},
author = {Rebecca Haehn and Gereon Kremer and Erika Ábrahám},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {2189},
pages = {[19]-32},
type = {Conference Paper},
year = {2018},
url = { https://publications.rwth-aachen.de/record/753088},
}×
[issue]
Rebecca Haehn, Gereon Kremer, Erika Ábrahám. Evaluation of Equational Constraints for CAD in SMT Solving, 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference (SC-Square 2018), Volume 2189 of CEUR Workshop Proceedings, [19]-32, RWTH Aachen, 2018.
fulltext PDF [bibtex]
@proceedings{AIIWGESEG2018,
title = {2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering: GE 2018},
author = {},
editor = {Erika Ábrahám and Elisabetta Di Nitto and Raffaela Mirandola},
publisher = {IEEE},
type = {Proceeding Article},
year = {2018},
url = { https://publications.rwth-aachen.de/record/753094},
}×
[issue]
. 2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering: GE 2018, IEEE, 2018.
fulltext PDF [bibtex]
@misc{SCTSSMBMEH2018,
title = {Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics},
author = {Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {10900},
pages = {XII-XII},
type = {Invited Abstract},
year = {2018},
url = { https://publications.rwth-aachen.de/record/753095},
}×
[issue]
Erika Ábrahám. Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics, Volume 10900 of LNCS, XII-XII, Springer, 2018.
fulltext PDF [bibtex]
@conference{THTAPDHSRAM2018,
title = {The HyDRA Tool: A Playground for the Development of Hybrid Systems Reachability Analysis Methods},
author = {Stefan Schupp and Erika Ábrahám},
publisher = {Oslo University},
booktitle = {Research report},
volume = {483},
pages = {2 Seiten},
type = {Conference Paper},
year = {2018},
url = { https://publications.rwth-aachen.de/record/767299},
}×
[issue]
Stefan Schupp, Erika Ábrahám. The HyDRA Tool: A Playground for the Development of Hybrid Systems Reachability Analysis Methods, PhD Symposium at iFM’18 on Formal Methods (PhD-iFM’18), Volume 483 of Research report, 2 Seiten, Oslo University, 2018.
DOI fulltext PDF [bibtex]
@phdthesis{O2018,
title = {On solving real-algebraic formulas in a satisfiability-modulo-theories framework},
author = {Ulrich Loup},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (ii, 222 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2018},
doi = {10.18154/RWTH-2018-231963},
url = { https://publications.rwth-aachen.de/record/752239},
}×
[issue]
Ulrich Loup. On solving real-algebraic formulas in a satisfiability-modulo-theories framework, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (ii, 222 Seiten) : Illustrationen, Diagramme, 2018.
DOI [bibtex]
@article{ISEOPMRSL2018,
title = {Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics},
author = {Francesco Leofante and Erika Ábrahám and Tim Dieter Niemüller and Gerhard Lakemeyer and Armando Tacchella},
publisher = {Kluwer},
journal = {Information systems frontiers},
volume = {21(1)},
pages = {pages 87-107},
type = {Journal Article},
year = {2018},
doi = {10.1007/s10796-018-9858-3},
url = { https://publications.rwth-aachen.de/record/753080},
}×
[issue]
Francesco Leofante, Erika Ábrahám, Tim Dieter Niemüller, Gerhard Lakemeyer, Armando Tacchella. Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics, Information systems frontiers 21 (1), pages 87-107, Kluwer, 2018.
DOI fulltext PDF [bibtex]
@proceedings{PPSFMATAP2018,
title = {Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)},
author = {},
editor = {Erika Ábrahám and Silvia Lizeth Taipa Tarifa},
booktitle = {Research report / University of Oslo},
volume = {483},
type = {Proceeding Article},
year = {2018},
doi = {10.18154/RWTH-CONV-236485},
url = { https://publications.rwth-aachen.de/record/753093},
}×
[issue]
. Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18), Volume 483 of Research report / University of Oslo, 2018.
2017
[bibtex]
@proceedings{BS2017,
title = {Bridging two communities to solve real problems: SC2 2016},
author = {},
editor = {Erika Ábrahám and James H. Davenport and Pascal Fontaine},
publisher = {RWTH Aachen},
booktitle = {CEUR workshop proceedings},
volume = {1804},
pages = {1 Online-Ressource : Illustrationen},
type = {Proceeding Article},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713481},
}×
[issue]
. Bridging two communities to solve real problems: SC2 2016, Volume 1804 of CEUR workshop proceedings, 1 Online-Ressource : Illustrationen, RWTH Aachen, 2017.
DOI [bibtex]
@article{S2017,
title = {Satisfiability checking and symbolic computation},
author = {Erika Ábrahám and P. Fontaine and S. Forrest and A. Griggio and D. Kroening and W. M. Seiler and T. Sturm and J. Abbott and B. Becker and A. M. Bigatti and M. Brain and B. Buchberger and A. Cimatti and J. H. Davenport and M. England},
publisher = {ACM},
journal = {ACM Communications in computer algebra},
volume = {50(4)},
pages = {pages 145-147},
type = {Journal Article},
year = {2017},
doi = {10.1145/3055282.3055285},
url = { https://publications.rwth-aachen.de/record/688933},
}×
[issue]
Erika Ábrahám, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W. M. Seiler, T. Sturm, J. Abbott, B. Becker, A. M. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J. H. Davenport, M. England. Satisfiability checking and symbolic computation, ACM Communications in computer algebra 50 (4), pages 145-147, ACM, 2017.
DOI [bibtex]
@conference{DCVSSHSRA2017,
title = {Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis},
author = {Stefan Schupp and Johanna Nellen and Erika Ábrahám},
publisher = {[Open Publishing Association]},
booktitle = {EPTCS},
volume = {250},
pages = {1-14},
type = {Conference Paper},
year = {2017},
doi = {10.4204/EPTCS.250.1},
url = { https://publications.rwth-aachen.de/record/696075},
}×
[issue]
Stefan Schupp, Johanna Nellen, Erika Ábrahám. Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis, 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2017), Volume 250 of EPTCS, 1-14, [Open Publishing Association], 2017.
DOI [bibtex]
@conference{HACLSSRHSRA2017,
title = {HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis},
author = {Stefan Schupp and Erika Ábrahám and Ibtissem Ben Makhlouf and Stefan Kowalewski},
publisher = {Springer},
booktitle = {LNCS},
volume = {10227},
pages = {288-294},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-57288-8_20},
url = { https://publications.rwth-aachen.de/record/696076},
}×
[issue]
Stefan Schupp, Erika Ábrahám, Ibtissem Ben Makhlouf, Stefan Kowalewski. HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis, NASA Formal Methods (NFM) Symposium (NFM 2017), Volume 10227 of LNCS, 288-294, Springer, 2017.
DOI fulltext PDF [bibtex]
@phdthesis{BBGE2017,
title = {Berechnung und Bewertung der Gesamtleistungsfähigkeit von Eisenbahnnetzen},
author = {Christian Meirich},
institution = {Rheinisch-Westfälische Technische Hochschule Aachen},
pages = {1 Online-Ressource (221 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2017},
doi = {10.18154/RWTH-2017-06606},
url = { https://publications.rwth-aachen.de/record/696083},
}×
[issue]
Christian Meirich. Berechnung und Bewertung der Gesamtleistungsfähigkeit von Eisenbahnnetzen, PhD Thesis, Rheinisch-Westfälische Technische Hochschule Aachen, 1 Online-Ressource (221 Seiten) : Illustrationen, Diagramme, 2017.
fulltext PDF [bibtex]
@conference{TTHSRA2017,
title = {Techniques and Tools for Hybrid Systems Reachability Analysis},
author = {Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {10381},
pages = {XVI-XVII},
type = {Conference Paper},
year = {2017},
url = { https://publications.rwth-aachen.de/record/696135},
}×
[issue]
Erika Ábrahám. Techniques and Tools for Hybrid Systems Reachability Analysis, The 10th International Workshop on Numerical Software Verification (NSV 2017), Volume 10381 of LNCS, XVI-XVII, Springer, 2017.
[bibtex]
@conference{EVSMMCSCF2017,
title = {Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework},
author = {Erika Ábrahám and Jasper Kurt Ferdinand Nalbach and Gereon Kremer},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {1974},
pages = {12 Seiten},
type = {Conference Paper},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713477},
}×
[issue]
Erika Ábrahám, Jasper Kurt Ferdinand Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework, 2nd International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 12 Seiten, RWTH Aachen, 2017.
fulltext PDF [bibtex]
@conference{CDPOCADSS2017,
title = {Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving},
author = {Tarik Viehmann and Gereon Kremer and Erika Ábrahám},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {1974},
pages = {15 Seiten},
type = {Conference Paper},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713479},
}×
[issue]
Tarik Viehmann, Gereon Kremer, Erika Ábrahám. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving, 2nd International Workshop on Satisfiability Checking and Symbolic Computation (SC2), Volume 1974 of CEUR Workshop Proceedings, 15 Seiten, RWTH Aachen, 2017.
fulltext PDF [bibtex]
@conference{TCTEMSDO2017,
title = {Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization},
author = {Tim Dieter Niemüller and Gerhard Lakemeyer and Francesco Leofante and Erika Ábrahám},
pages = {60-67},
type = {Conference Paper},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713532},
}×
[issue]
Tim Dieter Niemüller, Gerhard Lakemeyer, Francesco Leofante, Erika Ábrahám. Towards CLIPS-based Task Execution and Monitoring with SMT-based Decision Optimization, 5th Workshop on Planning and Robotics (PlanRob 2017), 60-67, 2017.
DOI [bibtex]
@conference{SSCSC2017,
title = {SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces},
author = {Erika Ábrahám and John Abbott and Bernd Becker and Anna M. Bigatti and Martin Brain and Alessandro Cimatti and James H. Davenport and Matthew England and Pascal Fontaine and Stephen Forrest and Vijay Ganesh and Alberto Griggio and Daniel Kroening and Werner M. Seiler},
publisher = {EasyChair},
booktitle = {EPiC Series in Computing},
volume = {51},
pages = {6-10},
type = {Conference Paper},
year = {2017},
doi = {10.29007/p319},
url = { https://publications.rwth-aachen.de/record/713487},
}×
[issue]
Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler. SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions (ARCADE 2017), Volume 51 of EPiC Series in Computing, 6-10, EasyChair, 2017.
DOI arXiv:1704.02421 [bibtex]
@unpublished{PIWSNMRA2017,
title = {Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis},
author = {},
editor = {Erika Ábrahám and Sergiy Bogomolov},
publisher = {[Open Publishing Association]},
pages = {1 Online-Ressource : Illustrationen},
type = {Preprint},
year = {2017},
doi = {10.4204/EPTCS.247},
url = { https://arxiv.org/abs/1704.02421},
}×
[issue]
. Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, 1 Online-Ressource : Illustrationen, [Open Publishing Association], 2017. https://arxiv.org/abs/1704.02421
DOI [bibtex]
@conference{OSGQPRFLSOMT2017,
title = {On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories},
author = {Francesco Leofante and Erika Ábrahám and Tim Dieter Niemüller and Gerhard Lakemeyer and Armando Tacchella},
publisher = {IEEE},
pages = {403-410},
type = {Conference Paper},
year = {2017},
doi = {10.1109/IRI.2017.67},
url = { https://publications.rwth-aachen.de/record/713493},
}×
[issue]
Francesco Leofante, Erika Ábrahám, Tim Dieter Niemüller, Gerhard Lakemeyer, Armando Tacchella. On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories, 2017 IEEE International Conference on Information Reuse and Integration (IRI) (IRI 2017), 403-410, IEEE, 2017.
DOI [bibtex]
@conference{SSATTTS2017,
title = {SMT Solving for Arithmetic Theories: Theory and Tool Support},
author = {Erika Ábrahám and Gereon Kremer},
publisher = {IEEE},
pages = {1-8},
type = {Conference Paper},
year = {2017},
doi = {10.1109/SYNASC.2017.00009},
url = { https://publications.rwth-aachen.de/record/780487},
}×
[issue]
Erika Ábrahám, Gereon Kremer. SMT Solving for Arithmetic Theories: Theory and Tool Support, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), 1-8, IEEE, 2017.
DOI [bibtex]
@conference{AHPH2017,
title = {Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro},
author = {Jannik Hüls and Stefan Schupp and Anne Remke and Erika Ábrahám},
publisher = {ACM},
booktitle = {ICPS: ACM international conference proceeding series},
pages = {178–185},
type = {Conference Paper},
year = {2017},
doi = {10.1145/3150928.3150938},
url = { https://publications.rwth-aachen.de/record/814253},
}×
[issue]
Jannik Hüls, Stefan Schupp, Anne Remke, Erika Ábrahám. Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro, 11th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS 2017), ICPS: ACM international conference proceeding series, 178–185, ACM, 2017.
fulltext PDF [bibtex]
@conference{P2017,
title = {Preface},
author = {Erika Ábrahám and Sergiy Bogomolov},
publisher = {[Open Publishing Association]},
booktitle = {EPTCS},
volume = {247},
type = {Conference Paper},
year = {2017},
url = { https://publications.rwth-aachen.de/record/720626},
}×
[issue]
Erika Ábrahám, Sergiy Bogomolov. Preface, 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), Volume 247 of EPTCS, [Open Publishing Association], 2017.
DOI fulltext PDF [bibtex]
@article{CAERASDS2017,
title = {Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071)},
author = {Erika Ábrahám and Hadas Kress-Gazit and Lorenzo Natale},
editor = {Armando Tacchella},
publisher = {Schloss Dagstuhl},
journal = {Dagstuhl Reports},
volume = {7(2)},
pages = {pages 48-63},
type = {Journal Article},
year = {2017},
doi = {10.4230/DagRep.7.2.48},
url = { https://publications.rwth-aachen.de/record/713498},
}×
[issue]
Erika Ábrahám, Hadas Kress-Gazit, Lorenzo Natale. Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071), Dagstuhl Reports 7 (2), pages 48-63, Schloss Dagstuhl, 2017.
fulltext PDF [bibtex]
@proceedings{PIWSNMRA2017,
title = {Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis},
author = {},
editor = {Erika Ábrahám and Sergiy Bogomolov},
publisher = {[Open Publishing Association]},
booktitle = {EPTCS},
volume = {247},
pages = {1 Online-Ressource : Illustrationen},
type = {Proceeding Article},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713497},
}×
[issue]
. Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, Volume 247 of EPTCS, 1 Online-Ressource : Illustrationen, [Open Publishing Association], 2017.
2016
DOI fulltext PDF [bibtex]
@conference{AGBBAIASMNIA2016,
title = {A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic},
author = {Gereon Kremer and Florian Corzilius and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {9890},
pages = {315-335},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-45641-6_21},
url = { https://publications.rwth-aachen.de/record/670551},
}×
[issue]
Gereon Kremer, Florian Corzilius, Erika Ábrahám. A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic, International Workshop on Computer Algebra in Scientific Computing (CASC16), Volume 9890 of LNCS, 315-335, Springer, 2016.
DOI [bibtex]
@article{LL2016,
title = {Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis},
author = {Mohamed Amin Ben Sassi and Sriram Sankaranarayanan and Xin Chen and Erika Ábrahám},
publisher = {Univ. Press},
journal = {IMA journal of mathematical control and information},
volume = {33(3)},
pages = {pages 723-756},
type = {Journal Article},
year = {2016},
doi = {10.1093/imamci/dnv003},
url = { https://publications.rwth-aachen.de/record/571421},
}×
[issue]
Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, Erika Ábrahám. Linear relaxations of polynomial positivity for polynomial Lyapunov function synthesis, IMA journal of mathematical control and information 33 (3), pages 723-756, Univ. Press, 2016.
DOI [bibtex]
@article{TCP2016,
title = {Two CEGAR-based approaches for the safety verification of PLC-controlled plants},
author = {Johanna Nellen and Kai Driessen and Martin Neuhäußer and Erika Ábrahám and Benedikt Wolters},
publisher = {Springer},
journal = {Information systems frontiers},
volume = {18(5)},
pages = {pages 927-952},
type = {Journal Article},
year = {2016},
doi = {10.1007/s10796-016-9671-9},
url = { https://publications.rwth-aachen.de/record/670652},
}×
[issue]
Johanna Nellen, Kai Driessen, Martin Neuhäußer, Erika Ábrahám, Benedikt Wolters. Two CEGAR-based approaches for the safety verification of PLC-controlled plants, Information systems frontiers 18 (5), pages 927-952, Springer, 2016.
DOI [bibtex]
@article{S2016,
title = {Some recent advances in automated analysis},
author = {Erika Ábrahám and Klaus Havelund},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {18(2)},
pages = {pages 121-128},
type = {Journal Article},
year = {2016},
doi = {10.1007/s10009-015-0403-0},
url = { https://publications.rwth-aachen.de/record/679253},
}×
[issue]
Erika Ábrahám, Klaus Havelund. Some recent advances in automated analysis, International journal on software tools for technology transfer 18 (2), pages 121-128, Springer, 2016.
DOI [bibtex]
@conference{SSCMSC2016,
title = {SC2: Satisfiability Checking Meets Symbolic Computation},
author = {Erika Ábrahám and John Abbott and Bernd Becker and Anna M. Bigatti and Martin Brain and Bruno Buchberger and Alessandro Cimatti and James H. Davenport and Matthew England and Pascal Fontaine and Stephen Forrest and Alberto Griggio and Daniel Kroening and Werner M. Seiler and Thomas Sturm},
publisher = {Springer},
booktitle = {LNCS},
volume = {9791},
pages = {28-43},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-42547-4_3},
url = { https://publications.rwth-aachen.de/record/681150},
}×
[issue]
Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. SC2: Satisfiability Checking Meets Symbolic Computation, 9th International Conference on Intelligent Computer Mathematics (CICM 2016), Volume 9791 of LNCS, 28-43, Springer, 2016.
DOI [bibtex]
@conference{ZOFDOUSCT2016,
title = {Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies},
author = {Erika Ábrahám and Florian Corzilius and Einar Broch Johnsen and Gereon Kremer and Jacopo Mauro},
publisher = {Springer},
booktitle = {LNCS},
volume = {9984},
pages = {229-245},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-47677-3_15},
url = { https://publications.rwth-aachen.de/record/681504},
}×
[issue]
Erika Ábrahám, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro. Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies, International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016), Volume 9984 of LNCS, 229-245, Springer, 2016.
DOI [bibtex]
@conference{CSRMASSUHR2016,
title = {Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots},
author = {Francesco Leofante and Simone Vuotto and Erika Ábrahám and Armando Tacchella and Nils Jansen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9952},
pages = {496-514},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-47166-2_34},
url = { https://publications.rwth-aachen.de/record/682004},
}×
[issue]
Francesco Leofante, Simone Vuotto, Erika Ábrahám, Armando Tacchella, Nils Jansen. Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), Volume 9952 of LNCS, 496-514, Springer, 2016.
DOI [bibtex]
@book{TFB2016,
title = {Theory and practice of formal methods: essays dedicated to Frank de Boer on the occasion of his 60th birthday},
author = {},
editor = {Erika Ábrahám and Marcello Bonsangue and Einar Broch Johnsen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9660},
pages = {XII, 427 Seiten : Illustrationen},
type = {Book},
year = {2016},
doi = {10.1007/978-3-319-30734-3},
url = { https://publications.rwth-aachen.de/record/683000},
}×
[issue]
Erika Ábrahám, Marcello Bonsangue, Einar Broch Johnsen. Theory and practice of formal methods: essays dedicated to Frank de Boer on the occasion of his 60th birthday, Volume 9660 of LNCS, XII, 427 Seiten : Illustrationen, Springer, 2016.
[bibtex]
@conference{HFLOEA2016,
title = {Heliostat Field Layout Optimization with Evolutionary Algorithms},
author = {Pascal Richter and David Laukamp and Levin Gerdes and Martin Frank and Erika Ábrahám},
publisher = {[Cool Press Ltd]},
booktitle = {EPiC Series in Computing},
volume = {41},
pages = {240-252},
type = {Conference Paper},
year = {2016},
url = { https://publications.rwth-aachen.de/record/683003},
}×
[issue]
Pascal Richter, David Laukamp, Levin Gerdes, Martin Frank, Erika Ábrahám. Heliostat Field Layout Optimization with Evolutionary Algorithms, 2nd GlobalConference on Artifcial Intelligence (GCAI 2016), Volume 41 of EPiC Series in Computing, 240-252, [Cool Press Ltd], 2016.
DOI [bibtex]
@conference{SCTA2016,
title = {Satisfiability Checking: Theory and Applications},
author = {Erika Ábrahám and Gereon Kremer},
publisher = {Springer},
booktitle = {LNCS},
volume = {9763},
pages = {9-23},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-41591-8_2},
url = { https://publications.rwth-aachen.de/record/683011},
}×
[issue]
Erika Ábrahám, Gereon Kremer. Satisfiability Checking: Theory and Applications, Software Engineering and Formal Methods : 14th International Conference (SEFM 2016), Volume 9763 of LNCS, 9-23, Springer, 2016.
DOI [bibtex]
@book{PWSNMRAS2016,
title = {Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR)},
author = {},
editor = {Erika Ábrahám and Sergiy Bogomolov},
publisher = {IEEE},
type = {Book},
year = {2016},
doi = {10.1109/SNR.2016.7479374},
url = { https://publications.rwth-aachen.de/record/683014},
}×
[issue]
Erika Ábrahám, Sergiy Bogomolov. Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), IEEE, 2016.
DOI [bibtex]
@book{I2016,
title = {Integrated formal methods},
author = {},
editor = {Erika Ábrahám and Marieke Huisman},
publisher = {Springer},
booktitle = {LNCS},
volume = {9681},
pages = {XIV, 538 Seiten : Illustrationen, Diagramme},
type = {Book},
year = {2016},
doi = {10.1007/978-3-319-33693-0},
url = { https://publications.rwth-aachen.de/record/683017},
}×
[issue]
Erika Ábrahám, Marieke Huisman. Integrated formal methods, Volume 9681 of LNCS, XIV, 538 Seiten : Illustrationen, Diagramme, Springer, 2016.
DOI fulltext PDF [bibtex]
@conference{P2016,
title = {Parameter synthesis for probabilistic systems},
author = {Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Albert-Ludwigs-Universität},
pages = {72-74},
type = {Conference Paper},
year = {2016},
doi = {10.6094/UNIFR/10639},
url = { https://publications.rwth-aachen.de/record/683021},
}×
[issue]
Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), 72-74, Albert-Ludwigs-Universität, 2016.
DOI fulltext PDF [bibtex]
@article{SCSCRDS2016,
title = {Symbolic Computation and Satisfiability Checking: Report of Dagstuhl Seminar 15471},
author = {Erika Ábrahám and Pascal Fontaine and Thomas Sturm and Dongming Wang},
publisher = {Schloss Dagstuhl},
journal = {Dagstuhl reports},
volume = {5(11)},
pages = {pages 71-89},
type = {Journal Article},
year = {2016},
doi = {10.4230/DagRep.5.11.71},
url = { https://publications.rwth-aachen.de/record/683051},
}×
[issue]
Erika Ábrahám, Pascal Fontaine, Thomas Sturm, Dongming Wang. Symbolic Computation and Satisfiability Checking: Report of Dagstuhl Seminar 15471, Dagstuhl reports 5 (11), pages 71-89, Schloss Dagstuhl, 2016.
DOI [bibtex]
@conference{SCTSC2016,
title = {Symbolic Computation Techniques in Satisfiability Checking},
author = {Erika Ábrahám},
publisher = {IEEE},
pages = {3-10},
type = {Conference Paper},
year = {2016},
doi = {10.1109/SYNASC.2016.014},
url = { https://publications.rwth-aachen.de/record/696073},
}×
[issue]
Erika Ábrahám. Symbolic Computation Techniques in Satisfiability Checking, 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 3-10, IEEE, 2016.
arXiv:1607.06945 [bibtex]
@unpublished{S2016,
title = {Satisfiability checking and symbolic computation},
author = {Erika Ábrahám and P. Fontaine and S. Forrest and A. Griggio and D. Kroening and W. M. Seiler and T. Sturm and J. Abbott and B. Becker and A. M. Bigatti and M. Brain and B. Buchberger and A. Cimatti and J. H. Davenport and M. England},
pages = {3 Seiten : Illustrationen},
type = {Preprint},
year = {2016},
url = { https://arxiv.org/abs/1607.06945},
}×
[issue]
Erika Ábrahám, P. Fontaine, S. Forrest, A. Griggio, D. Kroening, W. M. Seiler, T. Sturm, J. Abbott, B. Becker, A. M. Bigatti, M. Brain, B. Buchberger, A. Cimatti, J. H. Davenport, M. England. Satisfiability checking and symbolic computation, 3 Seiten : Illustrationen, 2016. https://arxiv.org/abs/1607.06945
fulltext PDF [bibtex]
@phdthesis{A2016,
title = {Analysis and synthesis of hybrid systems in engineering applications},
author = {Johanna Nellen},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (xxvi, 168 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2016},
url = { https://publications.rwth-aachen.de/record/680323},
}×
[issue]
Johanna Nellen. Analysis and synthesis of hybrid systems in engineering applications, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (xxvi, 168 Seiten) : Illustrationen, Diagramme, 2016.
DOI fulltext PDF [bibtex]
@phdthesis{IS2016,
title = {Integrating virtual substitution into strategic SMT solving},
author = {Florian Corzilius},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (IX, 186 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2016},
doi = {10.18154/RWTH-2017-03775},
url = { https://publications.rwth-aachen.de/record/688379},
}×
[issue]
Florian Corzilius. Integrating virtual substitution into strategic SMT solving, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (IX, 186 Seiten) : Illustrationen, Diagramme, 2016.
2015
fulltext PDF [bibtex]
@phdthesis{RTM2015,
title = {Reachability analysis of non-linear hybrid systems using Taylor Models},
author = {Xin Chen},
publisher = {Publikationsserver der RWTH Aachen University},
booktitle = {Aachener Informatik Berichte},
volume = {2015, 09},
institution = {RWTH Aachen University},
pages = {166 S. : graph. Darst.},
type = {PhD Thesis},
year = {2015},
url = { https://publications.rwth-aachen.de/record/465295},
}×
[issue]
Xin Chen. Reachability analysis of non-linear hybrid systems using Taylor Models, PhD Thesis, RWTH Aachen University, Volume 2015, 09 of Aachener Informatik Berichte, 166 S. : graph. Darst., Publikationsserver der RWTH Aachen University, 2015.
fulltext PDF [bibtex]
@phdthesis{C2015,
title = {Counterexamples in probabilistic verification},
author = {Nils Jansen},
publisher = {Publikationsserver der RWTH Aachen University},
institution = {Aachen, Techn. Hochsch.},
pages = {XI, 224 S.S. . graph. Darst.},
type = {PhD Thesis},
year = {2015},
url = { https://publications.rwth-aachen.de/record/479827},
}×
[issue]
Nils Jansen. Counterexamples in probabilistic verification, PhD Thesis, Aachen, Techn. Hochsch., XI, 224 S.S. . graph. Darst., Publikationsserver der RWTH Aachen University, 2015.
DOI [bibtex]
@inbook{ACTRAPCPUHA2015,
title = {A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata},
author = {Johanna Nellen and Erika Ábrahám and Benedikt Wolters},
publisher = {Springer},
booktitle = {Advances in Intelligent Systems and Computing},
volume = {346},
pages = {55-78},
type = {Book Chapter},
year = {2015},
doi = {10.1007/978-3-319-16577-6_3},
url = { https://publications.rwth-aachen.de/record/561931},
}×
[issue]
Johanna Nellen, Erika Ábrahám, Benedikt Wolters. A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants Using Hybrid Automata, Volume 346 of Advances in Intelligent Systems and Computing, 55-78, Springer, 2015.
DOI [bibtex]
@inbook{CER2015,
title = {Counterexamples for Expected Rewards},
author = {Tim Quatmann and Nils Jansen and Hans Christian Dehnert and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {9109},
pages = {435-452},
type = {Book Chapter},
year = {2015},
doi = {10.1007/978-3-319-19249-9_27},
url = { https://publications.rwth-aachen.de/record/541095},
}×
[issue]
Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards, Volume 9109 of LNCS, 435-452, Springer, 2015.
DOI [bibtex]
@inbook{ABSHSRA2015,
title = {A Benchmark Suite for Hybrid Systems Reachability Analysis},
author = {Xin Chen and Stefan Schupp and Ibtissem Ben Makhlouf and Erika Ábrahám and Goran Frehse and Stefan Kowalewski},
publisher = {Springer},
booktitle = {LNCS},
volume = {9058},
pages = {408-414},
type = {Book Chapter},
year = {2015},
doi = {10.1007/978-3-319-17524-9_29},
url = { https://publications.rwth-aachen.de/record/541100},
}×
[issue]
Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse, Stefan Kowalewski. A Benchmark Suite for Hybrid Systems Reachability Analysis, Volume 9058 of LNCS, 408-414, Springer, 2015.
DOI [bibtex]
@conference{BBSCSC2015,
title = {Building Bridges between Symbolic Computation and Satisfiability Checking},
author = {Erika Ábrahám},
publisher = {ACM Press},
pages = {6 S.},
type = {Conference Paper},
year = {2015},
doi = {10.1145/2755996.2756636},
url = { https://publications.rwth-aachen.de/record/561679},
}×
[issue]
Erika Ábrahám. Building Bridges between Symbolic Computation and Satisfiability Checking, 14th International Symposium on Symbolic and Algebraic Computation (ISSAC'15), 6 S., ACM Press, 2015.
DOI [bibtex]
@conference{SROSCTSPSS2015,
title = {SMT-RAT: an Open Source C++ Toolbox for Strategic and Parallel SMT Solving},
author = {Florian Corzilius and Gereon Kremer and Sebastian Junges and Stefan Schupp and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {9340},
pages = {360-368},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-24318-4_26},
url = { https://publications.rwth-aachen.de/record/561680},
}×
[issue]
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám. SMT-RAT: an Open Source C++ Toolbox for Strategic and Parallel SMT Solving, International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Volume 9340 of LNCS, 360-368, Springer, 2015.
DOI [bibtex]
@conference{AGAERSM2015,
title = {A Greedy Approach for the Efficient Repair of Stochastic Models},
author = {Shashank Pathak and Erika Ábrahám and Nils Jansen and Armando Tacchella and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9058},
pages = {295-309},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-17524-9_21},
url = { https://publications.rwth-aachen.de/record/561930},
}×
[issue]
Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen. A Greedy Approach for the Efficient Repair of Stochastic Models, 7th NASA Formal Methods Symposium (NFM'15), Volume 9058 of LNCS, 295-309, Springer, 2015.
DOI fulltext PDF [bibtex]
@article{HCPA2015,
title = {High-level Counterexamples for Probabilistic Automata},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen},
publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig},
journal = {Logical methods in computer science},
volume = {11(1)},
pages = {pages 15},
type = {Journal Article},
year = {2015},
doi = {10.2168/LMCS-11(1:15)2015},
url = { https://publications.rwth-aachen.de/record/540624},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen. High-level Counterexamples for Probabilistic Automata, Logical methods in computer science 11 (1), pages 15, Department of Theoretical Computer Science, Technical University of Braunschweig, 2015.
DOI [bibtex]
@conference{PAPPST2015,
title = {PROPhESY: A PRObabilistic ParamEter SYnthesis Tool},
author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {9206},
pages = {214-231},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-21690-4_13},
url = { https://publications.rwth-aachen.de/record/564236},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, 214-231, Springer, 2015.
[bibtex]
@conference{FMEPHS2015,
title = {Flow* 1.2: More Effective to Play with Hybrid Systems},
author = {Xin Chen and Sriram Sankaranarayanan and Erika Ábrahám},
publisher = {EasyChair},
booktitle = {EPiC Series in Computer Science},
volume = {34},
pages = {152-159},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/565595},
}×
[issue]
Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám. Flow* 1.2: More Effective to Play with Hybrid Systems, 1st and 2nd Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH'15), Volume 34 of EPiC Series in Computer Science, 152-159, EasyChair, 2015.
fulltext PDF [bibtex]
@conference{AGACSEMPP2015,
title = {A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs},
author = {Johanna Nellen and Benedikt Wolters and Lukas Stephan Michael Netz and Sascha Geulen and Erika Ábrahám},
publisher = {EasyChair},
booktitle = {EPiC series in computing},
volume = {36},
pages = {196-214},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/565596},
}×
[issue]
Johanna Nellen, Benedikt Wolters, Lukas Stephan Michael Netz, Sascha Geulen, Erika Ábrahám, Martina Joševski, Dirk Abel. A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs, 1st Global Conference on Artificial Intelligence (GCAI'15), Volume 36 of EPiC series in computing, 196-214, EasyChair, 2015.
arXiv:1503.06974 [bibtex]
@unpublished{CRPHAE2015,
title = {Challenges and Recommendations for Preparing HPC Applications for Exascale},
author = {Erika Ábrahám and Costas Bekas and Ivona Brandic and Samir Genaim and Einar Broch Johnsen and Ivan Kondov and Sabri Pllana and Achim Streit},
pages = {6 Seiten},
type = {Preprint},
year = {2015},
url = { https://arxiv.org/abs/1503.06974},
}×
[issue]
Erika Ábrahám, Costas Bekas, Ivona Brandic, Samir Genaim, Einar Broch Johnsen, Ivan Kondov, Sabri Pllana, Achim Streit. Challenges and Recommendations for Preparing HPC Applications for Exascale, 6 Seiten, 2015. https://arxiv.org/abs/1503.06974
[bibtex]
@conference{OLKH2015,
title = {Online Lernen als Kontrollstrategie in Hybridfahrzeugen},
author = {Sascha Geulen and Martina Joševski and Johanna Nellen and Janosch Fuchs and Lukas Stephan Michael Netz and Benedikt Wolters and Erika Ábrahám and Walter Unger and Dirk Abel},
publisher = {VDI-Verl.},
booktitle = {VDI-Berichte},
volume = {2233},
pages = {101-112},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/571422},
}×
[issue]
Sascha Geulen, Martina Joševski, Johanna Nellen, Janosch Fuchs, Lukas Stephan Michael Netz, Benedikt Wolters, Erika Ábrahám, Walter Unger, Dirk Abel. Online Lernen als Kontrollstrategie in Hybridfahrzeugen, 7th VDI/VDE Fachtagung AUTOREG: Auf dem Weg zum automatisierten Fahren (AUTOREG'15), Volume 2233 of VDI-Berichte, 101-112, VDI-Verl., 2015.
DOI [bibtex]
@conference{PHAECR2015,
title = {Preparing HPC Applications for Exascale: Challenges and Recommendations},
author = {Erika Ábrahám and Costas Bekas and Ivona Brandic and Samir Genaim and Einar Broch Johnsen and Ivan Kondov and Sabri Pllana and Achim Streit},
publisher = {IEEE},
pages = {401-406},
type = {Conference Paper},
year = {2015},
doi = {10.1109/NBiS.2015.61},
url = { https://publications.rwth-aachen.de/record/571423},
}×
[issue]
Erika Ábrahám, Costas Bekas, Ivona Brandic, Samir Genaim, Einar Broch Johnsen, Ivan Kondov, Sabri Pllana, Achim Streit. Preparing HPC Applications for Exascale: Challenges and Recommendations, 18th International Conference on Network-Based Information Systems (NBiS 2015), 401-406, IEEE, 2015.
DOI [bibtex]
@conference{LCSHEV2015,
title = {Learning-based Control Strategies for Hybrid Electric Vehicles},
author = {Sascha Geulen and Martina Josevski and Johanna Nellen and Janosch Fuchs and Lukas Stephan Michael Netz and Benedikt Wolters and Dirk Abel and Erika Ábrahám and Walter Unger},
publisher = {IEEE},
pages = {1722-1728},
type = {Conference Paper},
year = {2015},
doi = {10.1109/CCA.2015.7320858},
url = { https://publications.rwth-aachen.de/record/667226},
}×
[issue]
Sascha Geulen, Martina Josevski, Johanna Nellen, Janosch Fuchs, Lukas Stephan Michael Netz, Benedikt Wolters, Dirk Abel, Erika Ábrahám, Walter Unger. Learning-based Control Strategies for Hybrid Electric Vehicles, 2015 IEEE Conference on Control Applications (CCA), 1722-1728, IEEE, 2015.
DOI [bibtex]
@conference{CCVHS2015,
title = {Current Challenges in the Verification of Hybrid Systems},
author = {Stefan Schupp and Erika Ábrahám and Xin Chen and Ibtissem Ben Makhlouf and Goran Frehse and Sriram Sankaranarayanan and Stefan Kowalewski},
publisher = {Springer},
booktitle = {LNCS},
volume = {9361},
pages = {8-24},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-25141-7_2},
url = { https://publications.rwth-aachen.de/record/564375},
}×
[issue]
Stefan Schupp, Erika Ábrahám, Xin Chen, Ibtissem Ben Makhlouf, Goran Frehse, Sriram Sankaranarayanan, Stefan Kowalewski. Current Challenges in the Verification of Hybrid Systems, 5th Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy 2015), Volume 9361 of LNCS, 8-24, Springer, 2015.
2014
DOI [bibtex]
@article{M2014,
title = {Minimal counterexamples for linear-time probabilistic verification},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Elsevier},
journal = {Theoretical computer science},
volume = {549},
pages = {pages 61-100},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.tcs.2014.06.020},
url = { https://publications.rwth-aachen.de/record/447343},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal counterexamples for linear-time probabilistic verification, Theoretical computer science 549, pages 61-100, Elsevier, 2014.
DOI [bibtex]
@inbook{CGDTMMAIS2014,
title = {Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey},
author = {Erika Ábrahám and Bernd Becker and Hans Christian Dehnert and Nils Jansen and Joost-Pieter Katoen and Ralf Wimmer},
publisher = {Springer},
booktitle = {LNCS},
volume = {8483},
pages = {65-121},
type = {Book Chapter},
year = {2014},
doi = {10.1007/978-3-319-07317-0_3},
url = { https://publications.rwth-aachen.de/record/443312},
}×
[issue]
Erika Ábrahám, Bernd Becker, Hans Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer. Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey, Volume 8483 of LNCS, 65-121, Springer, 2014.
[bibtex]
@conference{MMCSV2014,
title = {Maybe or Maybe not: Contributions to Stochastic Verification},
author = {Ralf Wimmer and Erika Ábrahám},
publisher = {Monsenstein und Vannerdat},
pages = {119-127},
type = {Conference Paper},
year = {2014},
url = { https://publications.rwth-aachen.de/record/443585},
}×
[issue]
Ralf Wimmer, Erika Ábrahám. Maybe or Maybe not: Contributions to Stochastic Verification, Aspekte der Technischen Informatik, 119-127, Monsenstein und Vannerdat, 2014.
[bibtex]
@conference{UFNCS2014,
title = {Under-approximate Flowpipes for Non-linear Continuous Systems},
author = {Xin Chen and Sriram Sankaranarayanan and Erika Ábrahám},
publisher = {IEEE},
booktitle = {ACM Other conferences},
pages = {59-66},
type = {Conference Paper},
year = {2014},
url = { https://publications.rwth-aachen.de/record/444150},
}×
[issue]
Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám. Under-approximate Flowpipes for Non-linear Continuous Systems, 2014 formal methods in computer-aided design (FMCAD 2014), ACM Other conferences, 59-66, IEEE, 2014.
DOI [bibtex]
@article{SCTCMCTKSRTRT2014,
title = {Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories},
author = {Daniela Lepri and Erika Ábrahám and Peter Csaba Ölveczky},
publisher = {Elsevier},
journal = {Science of computer programming},
volume = {99},
pages = {pages 128-192},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.scico.2014.06.006},
url = { https://publications.rwth-aachen.de/record/445441},
}×
[issue]
Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky. Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories, Science of computer programming 99, pages 128-192, Elsevier, 2014.
DOI [bibtex]
@article{SM2014,
title = {Symbolic counterexample generation for large discrete-time Markov chains},
author = {Nils Jansen and Ralf Wimmer and Erika Ábrahám and Barna Zajzon and Joost-Pieter Katoen and Bernd Becker and Johann Schuster},
publisher = {Elsevier},
journal = {Science of computer programming},
volume = {91(Part A)},
pages = {pages 90-114},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.scico.2014.02.001},
url = { https://publications.rwth-aachen.de/record/445537},
}×
[issue]
Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster. Symbolic counterexample generation for large discrete-time Markov chains, Science of computer programming 91 (Part A), pages 90-114, Elsevier, 2014.
DOI [bibtex]
@article{FHMWSWC2014,
title = {Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?},
author = {Muhammad Fadlisyah and Peter Csaba Ölveczky and Erika Ábrahám},
publisher = {Elsevier},
journal = {Science of computer programming},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.scico.2014.06.010},
url = { https://publications.rwth-aachen.de/record/445943},
}×
[issue]
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám. Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?, Science of computer programming, Elsevier, 2014.
[bibtex]
@conference{M2014,
title = {Multi-objective optimization of solar tower power plants},
author = {Pascal Richter and Martin Frank and Erika Ábrahám},
publisher = {Springer},
booktitle = {Mathematics in industry},
type = {Conference Paper},
year = {2014},
url = { https://publications.rwth-aachen.de/record/444449},
}×
[issue]
Pascal Richter, Martin Frank, Erika Ábrahám. Multi-objective optimization of solar tower power plants, Mathematics in industry, Springer, 2014.
DOI [bibtex]
@inbook{FDPM2014,
title = {Fast Debugging of PRISM Models},
author = {Hans Christian Dehnert and Nils Jansen and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {8837},
pages = {146-162},
type = {Book Chapter},
year = {2014},
doi = {10.1007/978-3-319-11936-6_11},
url = { https://publications.rwth-aachen.de/record/460136},
}×
[issue]
Hans Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen. Fast Debugging of PRISM Models, Volume 8837 of LNCS, 146-162, Springer, 2014.
DOI [bibtex]
@book{F2014,
title = {Formal techniques for distributed objects, components, and systems},
author = {},
editor = {Erika Ábrahám and Catuscia Palamidessi},
publisher = {Springer},
booktitle = {LNCS},
volume = {8461},
pages = {XII, 299 S.},
type = {Book},
year = {2014},
doi = {10.1007/978-3-662-43613-4},
url = { https://publications.rwth-aachen.de/record/561681},
}×
[issue]
Erika Ábrahám, Catuscia Palamidessi. Formal techniques for distributed objects, components, and systems, Volume 8461 of LNCS, XII, 299 S., Springer, 2014.
DOI [bibtex]
@conference{ACARAPCP2014,
title = {A CEGAR Approach for the Reachability Analysis of PLC-controlled Chemical Plants},
author = {Johanna Nellen and Erika Ábrahám},
publisher = {IEEE},
pages = {500-507},
type = {Conference Paper},
year = {2014},
doi = {10.1109/IRI.2014.7051930},
url = { https://publications.rwth-aachen.de/record/561928},
}×
[issue]
Johanna Nellen, Erika Ábrahám. A CEGAR Approach for the Reachability Analysis of PLC-controlled Chemical Plants, 2014 IEEE International Conference on Information Reuse and Integration (IRI'14), 500-507, IEEE, 2014.
DOI [bibtex]
@article{OIBI2014,
title = {Observable Interface Behaviour and Inheritance},
author = {Erika Ábrahám and Thi Mai Thuong Tran and Martin Steffen},
publisher = {Cambridge Univ. Press},
journal = {Mathematical structures in computer science},
volume = {26(Special Issue 03)},
pages = {pages 561-605},
type = {Journal Article},
year = {2014},
doi = {10.1017/S0960129514000255},
url = { https://publications.rwth-aachen.de/record/561682},
}×
[issue]
Erika Ábrahám, Thi Mai Thuong Tran, Martin Steffen. Observable Interface Behaviour and Inheritance, Mathematical structures in computer science 26 (Special Issue 03), pages 561-605, Cambridge Univ. Press, 2014.
DOI [bibtex]
@conference{CGHA2014,
title = {Counterexample Generation for Hybrid Automata},
author = {Johanna Nellen and Erika Ábrahám and Xin Chen and Pieter Collins},
publisher = {Springer},
booktitle = {Communications in Computer and Information Science},
volume = {419},
pages = {88-106},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-05416-2_7},
url = { https://publications.rwth-aachen.de/record/561929},
}×
[issue]
Johanna Nellen, Erika Ábrahám, Xin Chen, Pieter Collins. Counterexample Generation for Hybrid Automata, Second International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'13), Volume 419 of Communications in Computer and Information Science, 88-106, Springer, 2014.
DOI fulltext PDF [bibtex]
@article{RTHMCI2014,
title = {Randomized Timed and Hybrid Models for Critical Infrastructures},
author = {},
editor = {Erika Ábrahám and Alberto Avritzer and Anne Remke and William H. Sanders},
publisher = {Schloss Dagstuhl},
journal = {Dagstuhl Reports},
volume = {4(1)},
pages = {pages 37-82},
type = {Journal Article},
year = {2014},
doi = {10.4230/DagRep.4.1.36},
url = { https://publications.rwth-aachen.de/record/564382},
}×
[issue]
. Randomized Timed and Hybrid Models for Critical Infrastructures, Dagstuhl Reports 4 (1), pages 37-82, Schloss Dagstuhl, 2014.
DOI [bibtex]
@book{TACAS2014,
title = {Tools and Algorithms for the Construction and Analysis of Systems},
author = {},
editor = {Erika Ábrahám and Klaus Havelund},
publisher = {Springer},
booktitle = {LNCS},
volume = {8413},
pages = {XVIII, 652 S. : graph. Darst.},
type = {Book},
year = {2014},
doi = {10.1007/978-3-642-54862-8},
url = { https://publications.rwth-aachen.de/record/564383},
}×
[issue]
Erika Ábrahám, Klaus Havelund. Tools and Algorithms for the Construction and Analysis of Systems, Volume 8413 of LNCS, XVIII, 652 S. : graph. Darst., Springer, 2014.
DOI [bibtex]
@conference{APPV2014,
title = {Accelerating Parametric Probabilistic Verification},
author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {8657},
pages = {404-420},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-10696-0_31},
url = { https://publications.rwth-aachen.de/record/540007},
}×
[issue]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 11th International Conference on Quantitative Evaluation of Systems (QEST 2014), Volume 8657 of LNCS, 404-420, Springer, 2014.
2013
DOI [bibtex]
@inbook{FAANLHS2013,
title = {Flow*: An Analyzer for Non-Linear Hybrid Systems},
author = {Xin Chen and Erika Ábrahám and Sriram Sankaranarayanan},
publisher = {Springer},
booktitle = {LNCS},
volume = {8044},
pages = {258-263},
type = {Book Chapter},
year = {2013},
doi = {10.1007/978-3-642-39799-8_18},
url = { https://publications.rwth-aachen.de/record/225803},
}×
[issue]
Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan. Flow*: An Analyzer for Non-Linear Hybrid Systems, Volume 8044 of LNCS, 258-263, Springer, 2013.
arXiv:1305.5055 [bibtex]
@unpublished{HCPA2013,
title = {High-level Counterexamples for Probabilistic Automata},
author = {Ralf Wimmer and Nils Jansen and Andreas Vorpahl and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Cornell University},
type = {Preprint},
year = {2013},
url = { https://arxiv.org/abs/1305.5055},
}×
[issue]
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata, Cornell University, 2013. https://arxiv.org/abs/1305.5055
DOI [bibtex]
@inbook{ASICPCAD2013,
title = {A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition},
author = {Ulrich Loup and Karsten Scheibler and Florian Corzilius and Erika Ábrahám and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {7898},
pages = {193-207},
type = {Book Chapter},
year = {2013},
doi = {10.1007/978-3-642-38574-2_13},
url = { https://publications.rwth-aachen.de/record/207654},
}×
[issue]
Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition, Volume 7898 of LNCS, 193-207, Springer, 2013.
fulltext PDF [bibtex]
@conference{EFCAC2013,
title = {Empirical Flowpipe Constructions for Analog Circuits},
author = {Yan Zhang and Xin Chen and Sriram Sankaranarayanan and Erika Ábrahám},
type = {Conference Paper},
year = {2013},
url = { https://publications.rwth-aachen.de/record/209164},
}×
[issue]
Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Erika Ábrahám. Empirical Flowpipe Constructions for Analog Circuits, 2013.
DOI [bibtex]
@inbook{ATCMCRTM2013,
title = {A Timed CTL Model Checker for Real-Time Maude},
author = {Daniela Lepri and Erika Ábrahám and Peter Csaba Ölveczky},
publisher = {Springer},
booktitle = {LNCS},
volume = {8089},
pages = {334-339},
type = {Book Chapter},
year = {2013},
doi = {10.1007/978-3-642-40206-7_27},
url = { https://publications.rwth-aachen.de/record/225701},
}×
[issue]
Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky. A Timed CTL Model Checker for Real-Time Maude, Volume 8089 of LNCS, 334-339, Springer, 2013.
DOI [bibtex]
@inbook{HCPA2013,
title = {High-level Counterexamples for Probabilistic Automata},
author = {Ralf Wimmer and Nils Jansen and Andreas Vorpahl and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {8054},
pages = {39-54},
type = {Book Chapter},
year = {2013},
doi = {10.1007/978-3-642-40196-1_4},
url = { https://publications.rwth-aachen.de/record/226401},
}×
[issue]
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata, Volume 8054 of LNCS, 39-54, Springer, 2013.
[bibtex]
@conference{SBMCBRC2013,
title = {Stochastic Bounded Model Checking: Bounded Rewards and Compositionality},
author = {Bettina Braitling and Ralf Wimmer and Bernd Becker and Erika Ábrahám},
publisher = {Univ., ITMZ},
pages = {243-254},
type = {Conference Paper},
year = {2013},
url = { https://publications.rwth-aachen.de/record/226121},
}×
[issue]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám. Stochastic Bounded Model Checking: Bounded Rewards and Compositionality, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2013), 243-254, Univ., ITMZ, 2013.
DOI [bibtex]
@inbook{LFSHR2013,
title = {Lyapunov Function Synthesis using Handelman Representations},
author = {Sriram Sankaranarayanan and Xin Chen and Erika Ábrahám},
publisher = {Elsevier},
booktitle = {Nonlinear Control Systems},
volume = {9,1},
pages = {576-581},
type = {Book Chapter},
year = {2013},
doi = {10.3182/20130904-3-FR-2041.00198},
url = { https://publications.rwth-aachen.de/record/226223},
}×
[issue]
Sriram Sankaranarayanan, Xin Chen, Erika Ábrahám. Lyapunov Function Synthesis using Handelman Representations, Volume 9,1 of Nonlinear Control Systems, 576-581, Elsevier, 2013.
DOI [bibtex]
@inbook{OGBCSMTSRN2013,
title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers},
author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {8080},
pages = {186-198},
type = {Book Chapter},
year = {2013},
doi = {10.1007/978-3-642-40663-8_18},
url = { https://publications.rwth-aachen.de/record/226897},
}×
[issue]
Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 8080 of LNCS, 186-198, Springer, 2013.
fulltext PDF [bibtex]
@techreport{OGBCSMTSRN2013,
title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers},
author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám},
publisher = {Shaker [u.a.]},
booktitle = {Aachener Informatik-Berichte : AIB},
volume = {2013,08},
pages = {3-21},
type = {Tech Report},
year = {2013},
url = { https://publications.rwth-aachen.de/record/228582},
}×
[issue]
Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 2013,08 of Aachener Informatik-Berichte : AIB, 3-21, Shaker [u.a.], 2013.
arXiv:1312.3979 [bibtex]
@unpublished{APPV2013,
title = {Accelerating Parametric Probabilistic Verification},
author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
pages = {21 Seiten},
type = {Preprint},
year = {2013},
url = { https://arxiv.org/abs/1312.3979},
}×
[issue]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 21 Seiten, 2013. https://arxiv.org/abs/1312.3979
DOI [bibtex]
@conference{FSMCSMICEPVAC2013,
title = {From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits},
author = {Yan Zhang and Xin Chen and Sriram Sankaranarayanan and Fabio Somenzi and Erika Ábrahám},
publisher = {IEEE},
pages = {662-669},
type = {Conference Paper},
year = {2013},
doi = {10.1109/ICCAD.2013.6691186},
url = { https://publications.rwth-aachen.de/record/444173},
}×
[issue]
Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Fabio Somenzi, Erika Ábrahám. From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits, 2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2013), 662-669, IEEE, 2013.
2012
DOI [bibtex]
@conference{MCSDTMM2012,
title = {Minimal Critical Subsystems for Discrete-Time Markov Models},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Bernd Becker and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {7214},
pages = {299-314},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-28756-5_21},
url = { https://publications.rwth-aachen.de/record/128454},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen. Minimal Critical Subsystems for Discrete-Time Markov Models, Tools and algorithms for the construction and analysis of systems (TACAS 2012), Volume 7214 of LNCS, 299-314, Springer, 2012.
fulltext PDF [bibtex]
@techreport{MCRRPMDP2012,
title = {Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
booktitle = {Reports of SFB/TR 14 AVACS},
volume = {88},
type = {Tech Report},
year = {2012},
url = { https://publications.rwth-aachen.de/record/197366},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes, Volume 88 of Reports of SFB/TR 14 AVACS, 2012.
[bibtex]
@conference{MCSCRDP2012,
title = {Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Kovač},
booktitle = {Schriftenreihe Forschungsergebnisse zur Informatik},
volume = {68},
pages = {169-180},
type = {Conference Paper},
year = {2012},
url = { https://publications.rwth-aachen.de/record/198077},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2012), Volume 68 of Schriftenreihe Forschungsergebnisse zur Informatik, 169-180, Kovač, 2012.
DOI [bibtex]
@conference{SLIVHFMAEHEHBHM2012,
title = {Some Like It Very Hot: Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude},
author = {Muhammad Fadlisyah and Peter Csaba Ölveczky and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {7571},
pages = {139-161},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-34005-5_8},
url = { https://publications.rwth-aachen.de/record/207049},
}×
[issue]
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám. Some Like It Very Hot: Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude, Rewriting logic and its applications (WRLA 2012), Volume 7571 of LNCS, 139-161, Springer, 2012.
DOI [bibtex]
@conference{CDARSHS2012,
title = {Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems},
author = {Xin Chen and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {6927},
pages = {535-542},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-27549-4_69},
url = { https://publications.rwth-aachen.de/record/207001},
}×
[issue]
Xin Chen, Erika Ábrahám. Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems, Computer aided systems theory - EUROCAST 2011, Volume 6927 of LNCS, 535-542, Springer, 2012.
arXiv:1206.0603v1 [bibtex]
@techreport{TCTCMCDMC2012,
title = {The COMICS Tool: Computing Minimal Counterexamples for Discrete-time Markov Chains},
author = {Nils Jansen and Erika Ábrahám and Maik Scheffler and Matthias Volk and Andreas Vorpahl and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker},
publisher = {Cornell Univ.},
type = {Tech Report},
year = {2012},
url = { https://arxiv.org/abs/1206.0603v1},
}×
[issue]
Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool: Computing Minimal Counterexamples for Discrete-time Markov Chains, Cornell Univ., 2012. https://arxiv.org/abs/1206.0603v1
fulltext PDF [bibtex]
@conference{HSFC2012,
title = {Hybrid Sequential Function Charts},
author = {Johanna Nellen and Erika Ábrahám},
publisher = {Kovač},
booktitle = {Schriftenreihe Forschungsergebnisse zur Informatik},
volume = {68},
pages = {109-120},
type = {Conference Paper},
year = {2012},
url = { https://publications.rwth-aachen.de/record/207085},
}×
[issue]
Johanna Nellen, Erika Ábrahám. Hybrid Sequential Function Charts, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2012), Volume 68 of Schriftenreihe Forschungsergebnisse zur Informatik, 109-120, Kovač, 2012.
DOI [bibtex]
@conference{TMFCNHS2012,
title = {Taylor Model Flowpipe Construction for Non-linear Hybrid Systems},
author = {Xin Chen and Erika Ábrahám and Sriram Sankaranarayanan},
publisher = {IEEE Computer Soc.},
booktitle = {Real-Time Systems Symposium-Proceedings},
volume = {2012},
pages = {183-192},
type = {Conference Paper},
year = {2012},
doi = {10.1109/RTSS.2012.70},
url = { https://publications.rwth-aachen.de/record/207611},
}×
[issue]
Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems, Proceedings of the 33rd IEEE Real-Time Systems Symposium (RTSS'12), Volume 2012 of Real-Time Systems Symposium-Proceedings, 183-192, IEEE Computer Soc., 2012.
DOI [bibtex]
@conference{SCGDMC2012,
title = {Symbolic Counterexample Generation for Discrete-time Markov Chains},
author = {Nils Jansen and Erika Ábrahám and Barna Zajzon and Ralf Wimmer and Johann Schuster and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {Springer eBook collection : Computer science},
pages = {134-151},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-35861-6},
url = { https://publications.rwth-aachen.de/record/207613},
}×
[issue]
Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker. Symbolic Counterexample Generation for Discrete-time Markov Chains, Formal aspects of component software (FACS 2012), Springer eBook collection : Computer science, 134-151, Springer, 2012.
[bibtex]
@conference{TMOFGI2012,
title = {Taylor Model Over-approximations for Flowpipe: Guard Intersections},
author = {Xin Chen and Erika Ábrahám and Sriram Sankaranarayanan},
type = {Conference Paper},
year = {2012},
url = { https://publications.rwth-aachen.de/record/207669},
}×
[issue]
Xin Chen, Erika Ábrahám, Sriram Sankaranarayanan. Taylor Model Over-approximations for Flowpipe: Guard Intersections, 5th International Workshop on Numerical Software Verification (NSV'12), 2012.
DOI [bibtex]
@conference{TCTCMCD2012,
title = {The COMICS Tool: Computing Minimal Counterexamples for DTMCs},
author = {Nils Jansen and Erika Ábrahám and Matthias Volk and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {7561},
pages = {349-353},
type = {Conference Paper},
year = {2012},
doi = {10.1007%2F978-3-642-33386-6_27},
url = { https://publications.rwth-aachen.de/record/207901},
}×
[issue]
Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool: Computing Minimal Counterexamples for DTMCs, Automated technology for verification and analysis (ATVA 2012), Volume 7561 of LNCS, 349-353, Springer, 2012.
DOI [bibtex]
@conference{TCMCRTM2012,
title = {Timed CTL Model Checking in Real-Time Maude},
author = {Daniela Lepri and Erika Ábrahám and Peter Csaba Ölveczky},
publisher = {Springer},
booktitle = {LNCS},
volume = {7571},
pages = {182-200},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-34005-5_10},
url = { https://publications.rwth-aachen.de/record/208147},
}×
[issue]
Daniela Lepri, Erika Ábrahám, Peter Csaba Ölveczky. Timed CTL Model Checking in Real-Time Maude, Rewriting logic and its applications (WRLA 2012), Volume 7571 of LNCS, 182-200, Springer, 2012.
DOI [bibtex]
@conference{SRASCNRAT2012,
title = {SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox},
author = {Florian Corzilius and Ulrich Loup and Sebastian Junges and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {7317},
pages = {442-448},
type = {Conference Paper},
year = {2012},
doi = {10.1007%2F978-3-642-31612-8_35},
url = { https://publications.rwth-aachen.de/record/207332},
}×
[issue]
Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika Ábrahám. SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox, Theory and applications of satisfiability testing, Volume 7317 of LNCS, 442-448, Springer, 2012.
2011
DOI [bibtex]
@conference{F2011,
title = {Formal modeling and analysis of hybrid systems in rewriting logic using higher-order numerical methods and discrete-event detection},
author = {Muhammad Fadlisyah and P. C. Olveczky and Erika Ábrahám},
pages = {1-8},
type = {Conference Paper},
year = {2011},
doi = {10.1109/CSICSSE.2011.5963989},
url = { https://publications.rwth-aachen.de/record/127526},
}×
[issue]
Muhammad Fadlisyah, P. C. Olveczky, Erika Ábrahám. Formal modeling and analysis of hybrid systems in rewriting logic using higher-order numerical methods and discrete-event detection, 1-8, 2011.
DOI [bibtex]
@conference{IRSCSEFRA2011,
title = {I-RiSC: an SMT-Compliant Solver for the Existential Fragment of Real Algebra},
author = {Ulrich Loup and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {6742},
pages = {230-246},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-21493-6_15},
url = { https://publications.rwth-aachen.de/record/100365},
}×
[issue]
Ulrich Loup, Erika Ábrahám. I-RiSC: an SMT-Compliant Solver for the Existential Fragment of Real Algebra, Algebraic informatics (CAI 2011), Volume 6742 of LNCS, 230-246, Springer, 2011.
DOI [bibtex]
@conference{VSSS2011,
title = {Virtual Substitution for SMT-Solving},
author = {Florian Corzilius and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {6914},
pages = {360-371},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-22953-4_31},
url = { https://publications.rwth-aachen.de/record/116784},
}×
[issue]
Florian Corzilius, Erika Ábrahám. Virtual Substitution for SMT-Solving, Fundamentals of computation theory (FCT 2011), Volume 6914 of LNCS, 360-371, Springer, 2011.
DOI [bibtex]
@conference{GACLRAC2011,
title = {GiNaCRA: A C++ Library for Real Algebraic Computations},
author = {Ulrich Loup and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {6617},
pages = {512-517},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-20398-5_41},
url = { https://publications.rwth-aachen.de/record/124551},
}×
[issue]
Ulrich Loup, Erika Ábrahám. GiNaCRA: A C++ Library for Real Algebraic Computations, NASA formal methods (NFM 2011), Volume 6617 of LNCS, 512-517, Springer, 2011.
DOI [bibtex]
@conference{OCSTPPNN2011,
title = {Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks},
author = {Pascal Richter and Erika Ábrahám and Gabriel Morin},
publisher = {Springer},
booktitle = {LNCS},
volume = {6593},
pages = {190-199},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-20282-7_20},
url = { https://publications.rwth-aachen.de/record/125206},
}×
[issue]
Pascal Richter, Erika Ábrahám, Gabriel Morin. Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks, Adaptive and natural computing algorithms (ICANNGA 2011), Volume 6593 of LNCS, 190-199, Springer, 2011.
DOI [bibtex]
@conference{H2011,
title = {Hierarchical counterexamples for discrete-time markov chains},
author = {Nils Jansen and Erika Ábrahám and Jens Katelaan and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {6996},
pages = {443-452},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-24372-1_33},
url = { https://publications.rwth-aachen.de/record/128557},
}×
[issue]
Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical counterexamples for discrete-time markov chains, Automated technolgoy for verification and analysis (ATVA 2011), Volume 6996 of LNCS, 443-452, Springer, 2011.
DOI [bibtex]
@conference{E2011,
title = {Efficient bounded reachability computation for rectangular automata},
author = {Xin Chen and Erika Ábrahám and Goran Frehse},
publisher = {Springer},
booktitle = {LNCS},
volume = {6945},
pages = {139-152},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-24288-5_13},
url = { https://publications.rwth-aachen.de/record/127806},
}×
[issue]
Xin Chen, Erika Ábrahám, Goran Frehse. Efficient bounded reachability computation for rectangular automata, Reachability problems (RP 2011), Volume 6945 of LNCS, 139-152, Springer, 2011.
DOI [bibtex]
@conference{CGMCUSBBMC2011,
title = {Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking},
author = {Bettina Braitling and Ralf Wimmer and Bernd Becker and Nils Jansen and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {6722},
pages = {75-89},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-21461-5_5},
url = { https://publications.rwth-aachen.de/record/127839},
}×
[issue]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám. Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking, Formal techniques for distributed systems (FORTE 2011), Volume 6722 of LNCS, 75-89, Springer, 2011.
DOI [bibtex]
@conference{OOFMAIHSHM2011,
title = {Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude},
author = {Muhammad Fadlisyah and Peter Csaba Ölveczky and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {7041},
pages = {415-430},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-24690-6_29},
url = { https://publications.rwth-aachen.de/record/128861},
}×
[issue]
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Ábrahám. Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude, Software engineering and formal methods (SEFM 2011), Volume 7041 of LNCS, 415-430, Springer, 2011.
DOI [bibtex]
@article{PSSBMC2011,
title = {Parallel SAT Solving in Bounded Model Checking},
author = {Erika Ábrahám and Tobias Schubert and Bernd Becker and Martin Fränzle and Christian Herde},
publisher = {Oxford Univ. Pr.},
journal = {Journal of logic and computation},
volume = {21(1)},
pages = {pages 5-21},
type = {Journal Article},
year = {2011},
doi = {10.1093/logcom/exp002},
url = { https://publications.rwth-aachen.de/record/170103},
}×
[issue]
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde. Parallel SAT Solving in Bounded Model Checking, Journal of logic and computation 21 (1), pages 5-21, Oxford Univ. Pr., 2011.
[bibtex]
@masterthesis{WLPD2011,
title = {Webbasierte konstruktivistische Lernumgebung für PHP und Datenbanken},
author = {Till Königshofen},
institution = {Rheinisch-Westfälische Technische Hochschule Aachen},
pages = {159 S. : graph. Darst.},
type = {Diploma Thesis},
year = {2011},
url = { https://publications.rwth-aachen.de/record/230036},
}×
[issue]
Till Königshofen. Webbasierte konstruktivistische Lernumgebung für PHP und Datenbanken, Diploma Thesis, Rheinisch-Westfälische Technische Hochschule Aachen, 159 S. : graph. Darst., 2011.
[bibtex]
@inbook{SCGMC2011,
title = {SMT-based Counterexample Generation for Markov Chains},
author = {Bettina Braitling and Ralf Wimmer and Bernd Becker and Nils Jansen and Erika Ábrahám},
publisher = {OFFIS},
pages = {19-28},
type = {Book Chapter},
year = {2011},
url = { https://publications.rwth-aachen.de/record/564234},
}×
[issue]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám. SMT-based Counterexample Generation for Markov Chains, 19-28, OFFIS, 2011.
2010
[bibtex]
@techreport{SBCDIE2010,
title = {Synthesis of Behavioral Controllers for DES: Increasing Efficiency},
author = {Kai Bollue and Michaela Slaats and Erika Ábrahám and Wolfgang Thomas and Dirk Abel},
publisher = {IFAC},
pages = {30-37},
type = {Tech Report},
year = {2010},
url = { https://publications.rwth-aachen.de/record/118416},
}×
[issue]
Kai Bollue, Michaela Slaats, Erika Ábrahám, Wolfgang Thomas, Dirk Abel. Synthesis of Behavioral Controllers for DES: Increasing Efficiency, 30-37, IFAC, 2010.
DOI [bibtex]
@conference{DMCSR2010,
title = {DTMC Model Checking by SCC Reduction},
author = {Erika Ábrahám and Nils Jansen and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker},
publisher = {IEEE Computer Society},
pages = {37-46},
type = {Conference Paper},
year = {2010},
doi = {10.1109/QEST.2010.13},
url = { https://publications.rwth-aachen.de/record/119427},
}×
[issue]
Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. DTMC Model Checking by SCC Reduction, Proceedings / Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010), 37-46, IEEE Computer Society, 2010.
[bibtex]
@conference{EDSPSS2010,
title = {Exploiting Different Strategies for the Parallelization of an SMT Solver},
author = {Natalia Kalinnik and Erika Ábrahám and Tobias Schubert and Ralf Wimmer and Bernd Becker},
publisher = {Fraunhofer Verl.},
pages = {97-106},
type = {Conference Paper},
year = {2010},
url = { https://publications.rwth-aachen.de/record/119428},
}×
[issue]
Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker. Exploiting Different Strategies for the Parallelization of an SMT Solver, 13. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 97-106, Fraunhofer Verl., 2010.
fulltext PDF [bibtex]
@conference{PZI2010,
title = {Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik},
author = {Erika Ábrahám and Philipp Brauner and Nils Jansen and Thiemo Leonhardt and Ulrich Loup and Ulrik Schroeder},
publisher = {Ges. für Informatik},
booktitle = {GI-Edition lecture notes in informatics : P, Proceedings},
volume = {169},
pages = {239-251},
type = {Conference Paper},
year = {2010},
url = { https://publications.rwth-aachen.de/record/119457},
}×
[issue]
Erika Ábrahám, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Ulrik Schroeder. Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik, DeLFI 2010, Volume 169 of GI-Edition lecture notes in informatics : P, Proceedings, 239-251, Ges. für Informatik, 2010.
fulltext PDF [bibtex]
@conference{SSASHS2010,
title = {SMT-Solving in the Analysis and Synthesis of Hybrid Systems},
author = {Erika Ábrahám and Ulrich Loup and Florian Corzilius and Thomas Sturm},
publisher = {Schloss Dagstuhl, Leibniz-Zentrum für Informatik},
booktitle = {Dagstuhl Seminar Proceedings},
volume = {10271},
pages = {9 S.},
type = {Conference Paper},
year = {2010},
url = { https://publications.rwth-aachen.de/record/119458},
}×
[issue]
Erika Ábrahám, Ulrich Loup, Florian Corzilius, Thomas Sturm. SMT-Solving in the Analysis and Synthesis of Hybrid Systems, Verification over discrete-continuous boundaries, Volume 10271 of Dagstuhl Seminar Proceedings, 9 S., Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2010.
DOI [bibtex]
@conference{ARLBTMTS2010,
title = {A Rewriting-Logic-Based Technique for Modeling Thermal Systems},
author = {Muhammad Fadlisyah and Erika Ábrahám and Daniela Lepri and Peter Csaba Ölveczky},
publisher = {NICTA},
booktitle = {EPTCS},
volume = {36},
pages = {82-100},
type = {Conference Paper},
year = {2010},
doi = {10.4204/EPTCS.36.5},
url = { https://publications.rwth-aachen.de/record/119462},
}×
[issue]
Muhammad Fadlisyah, Erika Ábrahám, Daniela Lepri, Peter Csaba Ölveczky. A Rewriting-Logic-Based Technique for Modeling Thermal Systems, Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), Volume 36 of EPTCS, 82-100, NICTA, 2010.
DOI [bibtex]
@conference{MCCMLPOORTMS2010,
title = {Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications},
author = {Daniela Lepri and Peter Csaba Ölveczky and Erika Ábrahám},
publisher = {NICTA},
booktitle = {EPTCS},
volume = {36},
pages = {117-136},
type = {Conference Paper},
year = {2010},
doi = {10.4204/EPTCS.36.7},
url = { https://publications.rwth-aachen.de/record/119463},
}×
[issue]
Daniela Lepri, Peter Csaba Ölveczky, Erika Ábrahám. Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications, Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), Volume 36 of EPTCS, 117-136, NICTA, 2010.
DOI [bibtex]
@article{TS2010,
title = {The Scalasca performance toolset architecture},
author = {Markus Geimer and Felix Gerd Eugen Wolf and Brian J. N. Wylie and Erika Ábrahám and Daniel Becker and Bernd Mohr},
publisher = {Wiley},
journal = {Concurrency and computation},
volume = {22.2010(6 : Special issue)},
pages = {pages 702-719},
type = {Journal Article},
year = {2010},
doi = {10.1002/cpe.1556},
url = { https://publications.rwth-aachen.de/record/137155},
}×
[issue]
Markus Geimer, Felix Gerd Eugen Wolf, Brian J. N. Wylie, Erika Ábrahám, Daniel Becker, Bernd Mohr. The Scalasca performance toolset architecture, Concurrency and computation 22.2010 (6 : Special issue), pages 702-719, Wiley, 2010.
DOI [bibtex]
@article{ASSNMRLBFAIHS2010,
title = {Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems},
author = {Muhammad Fadlisyah and Erika Ábrahám and Peter Csaba Ölveczky},
publisher = {Elsevier Science},
journal = {Electronic notes in theoretical computer science},
volume = {274},
pages = {pages 17-32},
type = {Journal Article},
year = {2010},
doi = {10.1016/j.entcs.2011.07.004},
url = { https://publications.rwth-aachen.de/record/170101},
}×
[issue]
Muhammad Fadlisyah, Erika Ábrahám, Peter Csaba Ölveczky. Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems, Electronic notes in theoretical computer science 274, pages 17-32, Elsevier Science, 2010.
2009
DOI [bibtex]
@article{B2009,
title = {Behavioral interface description of an object-oriented language with futures and promises},
author = {Erika Ábrahám and Immo Grabe and Andreas Grüner and Martin Steffen},
publisher = {North-Holland},
journal = {The journal of logic and algebraic programming},
volume = {78(7)},
pages = {pages 491-518},
type = {Journal Article},
year = {2009},
doi = {10.1016/j.jlap.2009.01.001},
url = { https://publications.rwth-aachen.de/record/170076},
}×
[issue]
Erika Ábrahám, Immo Grabe, Andreas Grüner, Martin Steffen. Behavioral interface description of an object-oriented language with futures and promises, The journal of logic and algebraic programming 78 (7), pages 491-518, North-Holland, 2009.
[bibtex]
@conference{SSFOTR2009,
title = {SMT-Solving for the First-Order Theory of the Reals},
author = {Erika Ábrahám and Ulrich Loup},
publisher = {Schloss Dagstuhl, Leibniz-Zentrum für Informatik},
booktitle = {Dagstuhl Seminar Proceedings},
volume = {09461},
pages = {7 S.},
type = {Conference Paper},
year = {2009},
url = { https://publications.rwth-aachen.de/record/119465},
}×
[issue]
Erika Ábrahám, Ulrich Loup. SMT-Solving for the First-Order Theory of the Reals, Algorithms and Applications for Next Generation SAT Solvers, Volume 09461 of Dagstuhl Seminar Proceedings, 7 S., Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2009.
[bibtex]
@conference{PAPICS2009,
title = {Picoso - A Parallel Interval Constraint Solver},
author = {Natalia Kalinnik and Tobias Schubert and Erika Ábrahám and Ralf Wimmer and Bernd Becker},
publisher = {CSREA Press},
pages = {473-479},
type = {Conference Paper},
year = {2009},
url = { https://publications.rwth-aachen.de/record/119431},
}×
[issue]
Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker. Picoso - A Parallel Interval Constraint Solver, Proceedings of the 2009 International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2009, 473-479, CSREA Press, 2009.
2008
DOI [bibtex]
@article{AIBOOLM2008,
title = {Abstract Interface Behavior of Object-Oriented Languages with Monitors},
author = {Erika Ábrahám and Andreas Grüner and Martin Steffen},
publisher = {Springer},
journal = {Theory of computing systems},
volume = {43(3/4)},
pages = {pages 322-361},
type = {Journal Article},
year = {2008},
doi = {10.1007/s00224-007-9047-0},
url = { https://publications.rwth-aachen.de/record/170105},
}×
[issue]
Erika Ábrahám, Andreas Grüner, Martin Steffen. Abstract Interface Behavior of Object-Oriented Languages with Monitors, Theory of computing systems 43 (3/4), pages 322-361, Springer, 2008.
fulltext PDF [bibtex]
@article{ADPSMJE2008,
title = {A Deductive Proof System for Multithreaded Java with Exceptions},
author = {Erika Ábrahám and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen},
publisher = {IOS Press},
journal = {Fundamenta informaticae},
volume = {82(4)},
pages = {pages 391-463},
type = {Journal Article},
year = {2008},
url = { https://publications.rwth-aachen.de/record/131126},
}×
[issue]
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. A Deductive Proof System for Multithreaded Java with Exceptions, Fundamenta informaticae 82 (4), pages 391-463, IOS Press, 2008.
DOI [bibtex]
@article{H2008,
title = {Heap-abstraction for an object-oriented calculus with thread classes},
author = {Erika Ábrahám and Andreas Grüner and Martin Steffen},
publisher = {Springer},
journal = {Software and systems modeling},
volume = {7(2)},
pages = {pages 177-208},
type = {Journal Article},
year = {2008},
doi = {10.1007/s10270-007-0065-9},
url = { https://publications.rwth-aachen.de/record/131123},
}×
[issue]
Erika Ábrahám, Andreas Grüner, Martin Steffen. Heap-abstraction for an object-oriented calculus with thread classes, Software and systems modeling 7 (2), pages 177-208, Springer, 2008.
DOI [bibtex]
@conference{US2008,
title = {Usage of the SCALASCA toolset for scalable performance analysis of large-scale parallel applications},
author = {Felix Gerd Eugen Wolf and Brian J. N. Wylie and Erika Ábrahám and Daniel Becker and Wolfgang Frings and Karl Fürlinger and Markus Geimer and Marc-André Hermanns and Bernd Mohr and Shirley Moore and Matthias Pfeifer and Zoltán Péter Szebenyi},
publisher = {Springer},
pages = {157-167},
type = {Conference Paper},
year = {2008},
doi = {10.1007/978-3-540-68564-7_10},
url = { https://publications.rwth-aachen.de/record/98531},
}×
[issue]
Felix Gerd Eugen Wolf, Brian J. N. Wylie, Erika Ábrahám, Daniel Becker, Wolfgang Frings, Karl Fürlinger, Markus Geimer, Marc-André Hermanns, Bernd Mohr, Shirley Moore, Matthias Pfeifer, Zoltán Péter Szebenyi. Usage of the SCALASCA toolset for scalable performance analysis of large-scale parallel applications, Tools for high performance computing, 157-167, Springer, 2008.
2007
DOI [bibtex]
@conference{OVSSLBMCLHA2007,
title = {On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata},
author = {Marc Herbstritt and Bernd Becker and Erika Ábrahám and Christian Herde},
publisher = {IEEE Service Center},
pages = {391-396},
type = {Conference Paper},
year = {2007},
doi = {10.1109/DDECS.2007.4295318},
url = { https://publications.rwth-aachen.de/record/119470},
}×
[issue]
Marc Herbstritt, Bernd Becker, Erika Ábrahám, Christian Herde. On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata, 2007 IEEE design and diagnostics of electronic circuits and systems, 391-396, IEEE Service Center, 2007.
DOI [bibtex]
@inbook{PS2007,
title = {Parallel SAT solving in bounded model checking},
author = {Erika Ábrahám and Tobias Schubert and Bernd Becker and Martin Fränzle and Christian Herde},
publisher = {Springer},
booktitle = {LNCS},
volume = {4346},
pages = {301-315},
type = {Book Chapter},
year = {2007},
doi = {10.1007/978-3-540-70952-7_21},
url = { https://publications.rwth-aachen.de/record/88690},
}×
[issue]
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde. Parallel SAT solving in bounded model checking, Volume 4346 of LNCS, 301-315, Springer, 2007.
2006
DOI [bibtex]
@article{B2006,
title = {Bounded model checking with parametric data structures},
author = {Erika Ábrahám and Marc Herbstritt and Bernd Becker and Martin Steffen},
publisher = {Elsevier},
journal = {Electronic notes in theoretical computer science},
volume = {174(3)},
pages = {pages 3-16},
type = {Journal Article},
year = {2006},
doi = {10.1016/j.entcs.2006.12.019},
url = { https://publications.rwth-aachen.de/record/157630},
}×
[issue]
Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen. Bounded model checking with parametric data structures, Electronic notes in theoretical computer science 174 (3), pages 3-16, Elsevier, 2006.
[bibtex]
@conference{M2006,
title = {Memory-aware bounded model checking for linear hybrid systems},
author = {Erika Ábrahám and Marc Herbstritt and Bernd Becker and Martin Steffen},
publisher = {Fraunhofer-Institut für Integrierte Schaltungen, Außenstelle Entwurfsautomatisierung},
pages = {153-162},
type = {Conference Paper},
year = {2006},
url = { https://publications.rwth-aachen.de/record/116300},
}×
[issue]
Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen. Memory-aware bounded model checking for linear hybrid systems, Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 153-162, Fraunhofer-Institut für Integrierte Schaltungen, Außenstelle Entwurfsautomatisierung, 2006.
DOI [bibtex]
@conference{D2006,
title = {Dynamic heap-abstraction for open, object-oriented systems with thread classes},
author = {Erika Ábrahám and Andreas Grüner and Martin Steffen},
publisher = {Springer},
booktitle = {LNCS},
volume = {3988},
pages = {1-10},
type = {Conference Paper},
year = {2006},
doi = {10.1007/11780342_1},
url = { https://publications.rwth-aachen.de/record/113855},
}×
[issue]
Erika Ábrahám, Andreas Grüner, Martin Steffen. Dynamic heap-abstraction for open, object-oriented systems with thread classes, Logical approaches to computational barriers, Volume 3988 of LNCS, 1-10, Springer, 2006.
DOI [bibtex]
@conference{A2006,
title = {Abstract interface behavior of object-oriented languages with monitors},
author = {Erika Ábrahám and Andreas Grüner and Martin Steffen},
publisher = {Springer},
booktitle = {LNCS},
volume = {4037},
pages = {218-232},
type = {Conference Paper},
year = {2006},
doi = {10.1007/11768869},
url = { https://publications.rwth-aachen.de/record/111866},
}×
[issue]
Erika Ábrahám, Andreas Grüner, Martin Steffen. Abstract interface behavior of object-oriented languages with monitors, Formal methods for open object-based distributed systems, Volume 4037 of LNCS, 218-232, Springer, 2006.
2005
DOI [bibtex]
@article{AABPSMJ2005,
title = {An Assertion-Based Proof System for Multithreaded Java},
author = {Erika Ábrahám and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen},
publisher = {Elsevier},
journal = {Theoretical computer science},
volume = {331(2/3)},
pages = {pages 251-290},
type = {Journal Article},
year = {2005},
doi = {10.1016/j.tcs.2004.09.019},
url = { https://publications.rwth-aachen.de/record/170083},
}×
[issue]
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. An Assertion-Based Proof System for Multithreaded Java, Theoretical computer science 331 (2/3), pages 251-290, Elsevier, 2005.
[bibtex]
@conference{DHAOOOSTC2005,
title = {Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes},
author = {Erika Ábrahám and Andreas Grüner and Martin Steffen},
publisher = {Queen Mary, University of London, Department of Computer Science},
booktitle = {Research report / Queen Mary, University of London, Department of Computer Science},
volume = {RR-05-04},
pages = {47-61},
type = {Conference Paper},
year = {2005},
url = { https://publications.rwth-aachen.de/record/119469},
}×
[issue]
Erika Ábrahám, Andreas Grüner, Martin Steffen. Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes, COSMICAH 2005, Volume RR-05-04 of Research report / Queen Mary, University of London, Department of Computer Science, 47-61, Queen Mary, University of London, Department of Computer Science, 2005.
DOI [bibtex]
@conference{OBMCLHS2005,
title = {Optimizing Bounded Model Checking for Linear Hybrid Systems},
author = {Erika Ábrahám and Bernd Becker and Felix Klaedtke and Martin Steffen},
publisher = {Springer},
booktitle = {LNCS},
volume = {3385},
pages = {396-412},
type = {Conference Paper},
year = {2005},
doi = {10.1007/978-3-540-30579-8_26},
url = { https://publications.rwth-aachen.de/record/119443},
}×
[issue]
Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen. Optimizing Bounded Model Checking for Linear Hybrid Systems, Verification, model checking, and abstract interpretation (VMCAI 2005), Volume 3385 of LNCS, 396-412, Springer, 2005.
DOI [bibtex]
@conference{AFATSUC2005,
title = {A Fully Abstract Trace Semantics for UML Components},
author = {Frank S. de Boer and Marcello Bonsangue and Martin Steffen and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {3657 : Tutorial},
pages = {49-69},
type = {Conference Paper},
year = {2005},
doi = {10.1007/11561163_3},
url = { https://publications.rwth-aachen.de/record/119440},
}×
[issue]
Frank S. de Boer, Marcello Bonsangue, Martin Steffen, Erika Ábrahám. A Fully Abstract Trace Semantics for UML Components, Formal methods for components and objects (FMCO 2004), Volume 3657 : Tutorial of LNCS, 49-69, Springer, 2005.
DOI [bibtex]
@conference{OCRSCC2005,
title = {Observability, Connectivity, and Replay in a Sequential Calculus of Classes},
author = {Erika Ábrahám and Frank S. de Boer and Marcello Bonsangue and Andreas Grüner and Martin Steffen},
publisher = {Springer},
booktitle = {LNCS},
volume = {3657 : Tutorial},
pages = {296-316},
type = {Conference Paper},
year = {2005},
doi = {10.1007/11561163},
url = { https://publications.rwth-aachen.de/record/119439},
}×
[issue]
Erika Ábrahám, Frank S. de Boer, Marcello Bonsangue, Andreas Grüner, Martin Steffen. Observability, Connectivity, and Replay in a Sequential Calculus of Classes, Formal methods for components and objects (FMCO 2004), Volume 3657 : Tutorial of LNCS, 296-316, Springer, 2005.
DOI [bibtex]
@conference{IPOEMJ2005,
title = {Inductive Proof Outlines for Exceptions in Multithreaded Java},
author = {Erika Ábrahám and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen},
publisher = {Elsevier},
booktitle = {Electronic notes in theoretical computer science},
volume = {159},
pages = {281-297},
type = {Conference Paper},
year = {2005},
doi = {10.1016/j.entcs.2005.12.072},
url = { https://publications.rwth-aachen.de/record/119437},
}×
[issue]
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Inductive Proof Outlines for Exceptions in Multithreaded Java, Proceedings of the First IPM International Workshop on Foundations of Software Engineering (FSEN 2005), Volume 159 of Electronic notes in theoretical computer science, 281-297, Elsevier, 2005.
DOI [bibtex]
@conference{OCFACCC2005,
title = {Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes},
author = {Erika Ábrahám and Marcello Bonsangue and Frank S. de Boer and Martin Steffen},
publisher = {Springer},
booktitle = {LNCS},
volume = {3407},
pages = {37-51},
type = {Conference Paper},
year = {2005},
doi = {10.1007/b107116},
url = { https://publications.rwth-aachen.de/record/119436},
}×
[issue]
Erika Ábrahám, Marcello Bonsangue, Frank S. de Boer, Martin Steffen. Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes, Theoretical aspects of computing - ICTAC 2004, Volume 3407 of LNCS, 37-51, Springer, 2005.