Publications-New

2021
DOI [bibtex]
@conference{OICACSMTS2021,
title = {On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving},
author = {Gereon Kremer and Erika Ábrahám and Matthew England and James H. Davenport},
publisher = {IEEE},
pages = {37-39},
type = {Conference Paper},
year = {2021},
doi = {10.1109/SYNASC54541.2021.00018},
url = { https://publications.rwth-aachen.de/record/846648},
}×
[issue]
Gereon Kremer, Erika Ábrahám, Matthew England, James H. Davenport. On the Implementation of Cylindrical Algebraic Coverings for Satisfiability Modulo Theories Solving, 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 37-39, IEEE, 2021.
arXiv:2108.05320 [bibtex]
@unpublished{PUSTCQFNLRA2021,
title = {Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
pages = {5 Seiten},
type = {Preprint},
year = {2021},
url = { https://arxiv.org/abs/2108.05320},
}×
[issue]
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic, 5 Seiten, 2021. https://arxiv.org/abs/2108.05320
DOI [bibtex]
@conference{C2021,
title = {Controller verification meets controller code: a case study},
author = {Felix Freiberger and Stefan Schupp and Holger Hermanns and Erika Ábrahám},
publisher = {ACM},
pages = {98-103},
type = {Conference Paper},
year = {2021},
doi = {10.1145/3487212.3487337},
url = { https://publications.rwth-aachen.de/record/841835},
}×
[issue]
Felix Freiberger, Stefan Schupp, Holger Hermanns, Erika Ábrahám. Controller verification meets controller code: a case study, 19th International Conference on Formal Methods and Models for System Design (MEMOCODE 21), 98-103, ACM, 2021.
DOI [bibtex]
@inbook{HAMCPH2021,
title = {HyperProb: A Model Checker for Probabilistic Hyperproperties},
author = {Oyendrila Dobe and Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour},
publisher = {Springer},
booktitle = {LNCS},
volume = {13047},
pages = {657-666},
type = {Book Chapter},
year = {2021},
doi = {10.1007/978-3-030-90870-6_35},
url = { https://publications.rwth-aachen.de/record/841833},
}×
[issue]
Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour. HyperProb: A Model Checker for Probabilistic Hyperproperties, Volume 13047 of LNCS, 657-666, Springer, 2021.
DOI [bibtex]
@conference{ACCRCHSLCD2021,
title = {ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics},
author = {Matthias Althoff and Erika Ábrahám and Marcelo Forets and Goran Frehse and Daniel Freire and Christian Schilling and Stefan Schupp and Mark Wetzlinger},
booktitle = {EPiC Series in Computing},
volume = {80},
pages = {1-31},
type = {Conference Paper},
year = {2021},
doi = {10.29007/lhbw},
url = { https://publications.rwth-aachen.de/record/841832},
}×
[issue]
Matthias Althoff, Erika Ábrahám, Marcelo Forets, Goran Frehse, Daniel Freire, Christian Schilling, Stefan Schupp, Mark Wetzlinger. ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics, 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Volume 80 of EPiC Series in Computing, 1-31, 2021.
fulltext PDF [bibtex]
@masterthesis{A2021,
title = {Accelerating symbolic simulation to analyze the effect of delays in train timetables},
author = {Niklas Kotowski},
institution = {RWTH Aachen University},
pages = {70 S.},
type = {Master Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/834267},
}×
[issue]
Niklas Kotowski. Accelerating symbolic simulation to analyze the effect of delays in train timetables, Master Thesis, RWTH Aachen University, 70 S., 2021.
DOI [bibtex]
@conference{SSRTUCSD2021,
title = {Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies},
author = {Rebecca Haehn and Erika Ábrahám and Nils Nießen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12846},
pages = {257-275},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-85172-9_14},
url = { https://publications.rwth-aachen.de/record/825264},
}×
[issue]
Rebecca Haehn, Erika Ábrahám, Nils Nießen. Symbolic Simulation of Railway Timetables Under Consideration of Stochastic Dependencies, 18th International Conference on Quantitative Evaluation of SysTems (QEST 2021), Volume 12846 of LNCS, 257-275, Springer, 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, International Symposium on Symbolic and Algebraic Computation (ISSAC '21), ACM Conferences, 313-320, Association for Computing Machinery, 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.
arXiv:2109.01585 [bibtex]
@unpublished{OM2021,
title = {On the proof complexity of MCSAT},
author = {Gereon Kremer and Erika Ábrahám and Vijay Ganesh},
type = {Preprint},
year = {2021},
url = { https://arxiv.org/abs/2109.01585},
}×
[issue]
Gereon Kremer, Erika Ábrahám, Vijay Ganesh. On the proof complexity of MCSAT, 2021. https://arxiv.org/abs/2109.01585
2020
DOI fulltext PDF [bibtex]
@conference{PSRT2020,
title = {Probabilistic Simulation of a Railway Timetable},
author = {Rebecca Haehn and Erika Ábrahám and Nils Nießen},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
booktitle = {OpenAccess Series in Informatics (OASIcs)},
volume = {85},
pages = {16:1-16:14},
type = {Conference Paper},
year = {2020},
doi = {10.4230/OASICS.ATMOS.2020.16},
url = { https://publications.rwth-aachen.de/record/807139},
}×
[issue]
Rebecca Haehn, Erika Ábrahám, Nils Nießen. Probabilistic Simulation of a Railway Timetable, 20th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2020), Volume 85 of OpenAccess Series in Informatics (OASIcs), 16:1-16:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
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
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.
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 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]
@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.
[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. Parameter synthesis in probabilistic timed automata, Master Thesis, RWTH Aachen University, 91 Seiten, 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. A novel adaption of the Simplex algorithm for linear real arithmetic, Master Thesis, RWTH Aachen University, 79 Seiten, 2020.
DOI [bibtex]
@conference{PHN2020,
title = {Probabilistic Hyperproperties with Nondeterminism},
author = {Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour and Oyendrila Dobe},
publisher = {Springer},
booktitle = {LNCS},
volume = {12302},
pages = {518-534},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-59152-6_29},
url = { https://publications.rwth-aachen.de/record/833949},
}×
[issue]
Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe. Probabilistic Hyperproperties with Nondeterminism, International Symposium on Automated Technology for Verification and Analysis (ATVA 2020), Volume 12302 of LNCS, 518-534, Springer, 2020.
DOI [bibtex]
@conference{ATHPNSFSSHA2020,
title = {A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata},
author = {Carina Pilch and Maurice Krause and Anne Remke and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {12229},
pages = {381-400},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-55754-6_23},
url = { https://publications.rwth-aachen.de/record/833951},
}×
[issue]
Carina Pilch, Maurice Krause, Anne Remke, Erika Ábrahám. A Transformation of Hybrid Petri Nets with Stochastic Firings into a Subclass of Stochastic Hybrid Automata, 12th NASA Formal Methods Symposium (NFM 2020), Volume 12229 of LNCS, 381-400, Springer, 2020.
DOI fulltext PDF [bibtex]
@misc{NOFPCRGEA2020,
title = {New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract)},
author = {Erika Ábrahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {2752},
pages = {178-188},
type = {Invited Abstract},
year = {2020},
doi = {10.18154/RWTH-2021-09565},
url = { https://publications.rwth-aachen.de/record/833961},
}×
[issue]
Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks. New Opportunities for the Formal Proof of Computational Real Geometry? (Extended Abstract), Volume 2752 of CEUR Workshop Proceedings, 178-188, RWTH Aachen, 2020.
arXiv:2004.04034 [bibtex]
@unpublished{NOFPCRG2020,
title = {New Opportunities for the Formal Proof of Computational Real Geometry?},
author = {Erika Ábrahám and James Davenport and Matthew England and Gereon Kremer and Zak Tonks},
pages = {14 Seiten},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2004.04034},
}×
[issue]
Erika Ábrahám, James Davenport, Matthew England, Gereon Kremer, Zak Tonks. New Opportunities for the Formal Proof of Computational Real Geometry?, 14 Seiten, 2020. https://arxiv.org/abs/2004.04034
Show all