@masterthesis{PS2024,
title = {Proving termination of probabilistic recursive programs via SMT-solving},
author = {Leo Mommers},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02602},
url = { https://publications.rwth-aachen.de/record/980858},
}×

@conference{SSYMT2024,
title = {SMT: Something You Must Try},
author = {Erika Ábrahám and Jószef Kovács and Anne Remke},
publisher = {Springer},
booktitle = {LNCS},
volume = {14300},
pages = {3-18},
type = {Conference Paper},
year = {2024},
doi = {10.1007/978-3-031-47705-8_1},
url = { https://publications.rwth-aachen.de/record/976267},
}×

@article{L2024,
title = {Levelwise construction of a single cylindrical algebraic cell},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Philippe Specht and Christopher W. Brown and James H. Davenport and Matthew England},
publisher = {Elsevier},
journal = {Journal of symbolic computation},
volume = {123},
pages = {pages 102288},
type = {Journal Article},
year = {2024},
doi = {10.1016/j.jsc.2023.102288},
url = { https://publications.rwth-aachen.de/record/975125},
}×

@article{O2023,
title = {On the applicability of hybrid systems safety verification tools from the automotive perspective},
author = {Stefan Schupp and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow and Zeng Qiu},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {26(1)},
pages = {pages 49-78},
type = {Journal Article},
year = {2023},
doi = {10.1007/s10009-023-00707-0},
url = { https://publications.rwth-aachen.de/record/962039},
}×

@conference{ENNVLFPLAF2023,
title = {Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions},
author = {László Antal and Hana Masara and Erika Ábrahám},
publisher = {NICTA},
booktitle = {EPTCS},
volume = {395},
pages = {[30]-68},
type = {Conference Paper},
year = {2023},
doi = {10.4204/EPTCS.395.4},
url = { https://publications.rwth-aachen.de/record/980068},
}×

@conference{TAC2023,
title = {Theoretical Aspects of Computing},
author = {Erika Ábrahám and Clemens Dubslaff and Silvia Lizeth Tapia Tarifa},
publisher = {Springer},
booktitle = {LNCS},
volume = {14446},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-47963-2},
url = { https://publications.rwth-aachen.de/record/976283},
}×

@unpublished{ENNVLFPLAF2023,
title = {Extending Neural Network Verification to a Larger Family of Piece-wise Linear Activation Functions},
author = {László Antal and Hana Masara and Erika Ábrahám},
pages = {30-68},
type = {Preprint},
year = {2023},
url = { https://arxiv.org/abs/2311.10780},
}×

@masterthesis{G2023,
title = {Generate elaborative feedback for novices’ programming exercises based on interaction data},
author = {Johanna Tolzmann},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen, Diagramme},
type = {Master Thesis},
year = {2023},
doi = {10.18154/RWTH-2023-10933},
url = { https://publications.rwth-aachen.de/record/973679},
}×

@conference{FANMSLRAP2023,
title = {FMplex: A Novel Method for Solving Linear Real Arithmetic Problems},
author = {Jasper Kurt Ferdinand Nalbach and Valentin Maxim Promies and Erika Ábrahám and Paul Kobialka},
publisher = {Open Publishing Association},
booktitle = {EPTCS},
volume = {390},
type = {Conference Paper},
year = {2023},
doi = {10.4204/EPTCS.390.2},
url = { https://publications.rwth-aachen.de/record/972368},
}×

@article{IRACPSE2023,
title = {Integrated Rigorous Analysis in Cyber-Physical Systems Engineering},
author = {Erika Ábrahám and Stefan Hallerstede and John Hatcliff and Danielle Stewart and Noah Abou El Wafa},
publisher = {Schloss Dagstuhl},
journal = {Dagstuhl Reports},
volume = {13(1)},
pages = {pages 155-183},
type = {Journal Article},
year = {2023},
doi = {10.4230/DagRep.13.1.155},
url = { https://publications.rwth-aachen.de/record/969886},
}×

@conference{CTAISHA2023,
title = {Comparing Two Approaches to Include Stochasticity in Hybrid Automata},
author = {Lisa Willemsen and Anne Remke and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-43835-6_17},
url = { https://publications.rwth-aachen.de/record/969885},
}×

@proceedings{FSEICFTIMRSP2023,
title = {Fundamentals of Software Engineering: 10th International Conference, FSEN 2023, Tehran, Iran, May 4-5, 2023, Revised Selected Papers},
author = {},
editor = {Hossein Hojjat and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {14155},
type = {Proceeding Article},
year = {2023},
doi = {10.1007/978-3-031-42441-0},
url = { https://publications.rwth-aachen.de/record/969884},
}×

@unpublished{FANMSLRAP2023,
title = {FMplex: A Novel Method for Solving Linear Real Arithmetic Problems},
author = {Jasper Kurt Ferdinand Nalbach and Valentin Maxim Promies and Erika Ábrahám and Paul Kobialka},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2309.03138},
url = { https://arxiv.org/abs/2309.03138},
}×

@conference{IAPH2023,
title = {Introducing Asynchronicity to Probabilistic Hyperproperties},
author = {Lina Gerlach and Oyendrila Dobe and Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour},
publisher = {Springer},
booktitle = {LNCS},
volume = {14287},
pages = {47-64},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-43835-6_4},
url = { https://publications.rwth-aachen.de/record/969695},
}×

@unpublished{CTAISHA2023,
title = {Comparing Two Approaches to Include Stochasticity in Hybrid Automata},
author = {Lisa Willemsen and Anne Remke and Erika Ábrahám},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2307.08052},
url = { https://arxiv.org/abs/2307.08052},
}×

@unpublished{IAPH2023,
title = {Introducing Asynchronicity to Probabilistic Hyperproperties},
author = {Lina Gerlach and Oyendrila Dobe and Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2307.05282},
url = { https://arxiv.org/abs/2307.05282},
}×

@unpublished{MRPRARC2023,
title = {Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks},
author = {Joanna Delicaris and Stefan Schupp and Erika Ábrahám and Anne Remke},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2304.14996},
url = { https://arxiv.org/abs/2304.14996},
}×

@proceedings{SSSCSC2023,
title = {SC-Square 2023: Satisfiability Checking and Symbolic Computation 2023},
author = {},
editor = {Erika Ábrahám and Thomas Sturm},
publisher = {CEUR-WS.org},
booktitle = {CEUR Workshop Proceedings},
volume = {3455},
type = {Proceeding Article},
year = {2023},
url = { https://publications.rwth-aachen.de/record/964115},
}×

@conference{MRPRARC2023,
title = {Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks},
author = {Joanna Delicaris and Stefan Schupp and Erika Ábrahám and Anne Remke},
publisher = {Springer},
booktitle = {LNCS},
volume = {13931},
pages = {164-182},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-35257-7_10},
url = { https://publications.rwth-aachen.de/record/964104},
}×

@unpublished{ESCCAC2023,
title = {Exploiting Strict Constraints in the Cylindrical Algebraic Covering},
author = {Philipp Bär and Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Christopher W. Brown},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2306.16757},
url = { https://arxiv.org/abs/2306.16757},
}×

@conference{ESCCAC2023,
title = {Exploiting Strict Constraints in the Cylindrical Algebraic Covering},
author = {Philipp Bär and Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Christopher Brown},
booktitle = {CEUR workshop proceedings},
volume = {3429},
pages = {13 Seiten},
type = {Conference Paper},
year = {2023},
url = { https://publications.rwth-aachen.de/record/961989},
}×

@inbook{SSSS2023,
title = {Subtropical Satisfiability for SMT Solving},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {13903},
pages = {430-446},
type = {Book Chapter},
year = {2023},
doi = {10.1007/978-3-031-33170-1_26},
url = { https://publications.rwth-aachen.de/record/960581},
}×

@conference{AEGSC2023,
title = {Automated Exercise Generation for Satisfiability Checking},
author = {Erika Ábrahám and Jasper Kurt Ferdinand Nalbach and Valentin Maxim Promies},
publisher = {Springer},
booktitle = {LNCS},
volume = {13962},
pages = {1-16},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-27534-0_1},
url = { https://publications.rwth-aachen.de/record/957774},
}×

@masterthesis{E2023,
title = {Exploiting strict constraints in the computation of cylindrical algebraic coverings},
author = {Philipp Bär},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen, Diagramme},
type = {Bachelor Thesis},
year = {2023},
doi = {10.18154/RWTH-2023-04217},
url = { https://publications.rwth-aachen.de/record/956500},
}×

@conference{ACAMAUVBLSTM2023,
title = {A Collision Avoidance Method for Autonomous Underwater Vehicles Based on Long Short-Term Memories},
author = {László Antal and Martin Aubard and Erika Ábrahám and Ana Madureira and Luís Madureira and Maria Costa and José Pinto and Renato Campos},
publisher = {Springer},
booktitle = {Lecture Notes in Networks and Systems},
volume = {649},
pages = {448-457},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-27499-2_42},
url = { https://publications.rwth-aachen.de/record/955843},
}×

@unpublished{L2023,
title = {Levelwise construction of a single cylindrical algebraic cell},
author = {Jasper Kurt Ferdinand Nalbach and Erika Ábrahám and Philippe Specht and Christopher W. Brown and James H. Davenport and Matthew England},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2212.09309},
url = { https://arxiv.org/abs/2212.09309},
}×

@misc{VSSLG2023,
title = {Verfahren und System zur Steuerung von Lasten in einem Gebäude},
author = {Jonas Blum and Stefan Hardt and Pascal Richter and Erika Ábrahám and Ahmed Abida and Simon Klemp},
pages = {17 Seiten : Illustrationen},
type = {Patent},
year = {2023},
url = { https://publications.rwth-aachen.de/record/953391},
}×

@article{MM2022,
title = {Model checking hyperproperties for Markov decision processes},
author = {Oyendrila Dobe and Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {289(Part B)},
pages = {pages 104978},
type = {Journal Article},
year = {2022},
doi = {10.1016/j.ic.2022.104978},
url = { https://publications.rwth-aachen.de/record/861552},
}×

@phdthesis{O2022,
title = {Optimisation and analysis of railway timetables under consideration of uncertainties},
author = {Rebecca Haehn},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2022},
doi = {10.18154/RWTH-2022-10063},
url = { https://publications.rwth-aachen.de/record/855177},
}×

@proceedings{Q2022,
title = {Quantitative evaluation of systems},
author = {},
editor = {Erika Ábrahám and Marco Paolieri},
publisher = {Springer},
booktitle = {LNCS},
volume = {13479},
pages = {XVII, 399 Seiten : Illustrationen},
type = {Proceeding Article},
year = {2022},
doi = {10.1007/978-3-031-16336-4},
url = { https://publications.rwth-aachen.de/record/854216},
}×

@article{NPSCSC2022,
title = {New Perspectives in Symbolic Computation and Satisfiability Checking},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Alberto Griggio},
publisher = {Schloss Dagstuhl},
journal = {Dagstuhl reports},
volume = {12(2)},
pages = {pages 67-86},
type = {Journal Article},
year = {2022},
doi = {10.4230/DagRep.12.2.67},
url = { https://publications.rwth-aachen.de/record/854210},
}×

@conference{EARC2022,
title = {Experiments with Automated Reasoning in the Class},
author = {Isabela Dramnesc and Erika Ábrahám and Tudor Jebelean and Gábor Kusper and Sorin Stratulat},
publisher = {Springer},
booktitle = {Lecture Notes in Artificial Intelligence},
volume = {13467},
pages = {287-304},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-16681-5_20},
url = { https://publications.rwth-aachen.de/record/854208},
}×

@article{RH2022,
title = {Recent developments in theory and tool support for hybrid systems verification with HyPro},
author = {Stefan Schupp and Erika Ábrahám and Tristan Ebert},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {289(Part A)},
pages = {pages 104945},
type = {Journal Article},
year = {2022},
doi = {10.1016/j.ic.2022.104945},
url = { https://publications.rwth-aachen.de/record/850718},
}×

@unpublished{RSHSMV2022,
title = {Robot Swarms as Hybrid Systems: Modelling and Verification},
author = {Stefan Schupp and Francesco Leofante and Leander Behr and Erika Ábrahám and Armando Tacchella},
type = {Preprint},
year = {2022},
doi = {10.48550/arXiv.2207.06758},
url = { https://arxiv.org/abs/2207.06758},
}×

@conference{ATSSRT2022,
title = {Acceleration Techniques for Symbolic Simulation of Railway Timetables},
author = {Rebecca Haehn and Erika Ábrahám and Niklas Kotowski},
publisher = {Springer},
booktitle = {LNCS},
volume = {13294},
pages = {46-62},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-05814-1_4},
url = { https://publications.rwth-aachen.de/record/850270},
}×

@conference{PHR2022,
title = {Probabilistic Hyperproperties with Rewards},
author = {Oyendrila Dobe and Lukas Wilke and Erika Ábrahám and Borzoo Bonakdarpour and Ezio Bartocci},
publisher = {Springer},
booktitle = {LNCS},
volume = {13260},
pages = {656-673},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-06773-0_35},
url = { https://publications.rwth-aachen.de/record/850269},
}×

@conference{HMCPD2022,
title = {HyperPCTL Model Checking by Probabilistic Decomposition},
author = {Eshita Zaman and Gianfranco Ciardo and Erika Ábrahám and Borzoo Bonakdarpour},
publisher = {Springer},
booktitle = {LNCS},
volume = {13274, Formal methods},
pages = {209-226},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-07727-2_12},
url = { https://publications.rwth-aachen.de/record/850268},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{C2021,
title = {Controller verification meets controller code: a case study},
author = {Felix Freiberger and Stefan Schupp and Holger Hermanns and Erika Ábrahám},
publisher = {Association for Computing Machinery},
booktitle = {ACM conferences},
pages = {98-103},
type = {Conference Paper},
year = {2021},
doi = {10.1145/3487212.3487337},
url = { https://publications.rwth-aachen.de/record/841835},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@masterthesis{AS2020,
title = {A novel adaption of the Simplex algorithm for linear real arithmetic},
author = {Jasper Kurt Ferdinand Nalbach},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Master Thesis},
year = {2020},
doi = {10.18154/RWTH-2021-04303},
url = { https://publications.rwth-aachen.de/record/818122},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{HATLPH2018,
title = {HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties},
author = {Erika Ábrahám and Borzoo Bonakdarpour},
publisher = {Springer},
booktitle = {LNCS},
volume = {11024, Theoretical Computer Science and General Issues},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-99154-2_2},
url = { https://publications.rwth-aachen.de/record/753085},
}×

@conference{TPOAAPL2018,
title = {Task Planning with OMT: An Application to Production Logistics},
author = {Francesco Leofante and Erika Ábrahám and Armando Tacchella},
publisher = {Springer},
booktitle = {LNCS},
volume = {11023, Programming and Software Engineering},
pages = {316-325},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-98938-9_18},
url = { https://publications.rwth-aachen.de/record/753083},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{TCTEMSPO2017,
title = {Towards CLIPS-based Task Execution and Monitoring with SMT-based Planning and Optimization},
author = {Tim Dieter Niemüller and Gerhard Lakemeyer and Francesco Leofante and Erika Ábrahám},
type = {Conference Paper},
year = {2017},
url = { https://publications.rwth-aachen.de/record/809638},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@article{CAERASDS2017,
title = {Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071)},
author = {Armando Tacchella},
editor = {Erika Ábrahám and Hadas Kress-Gazit and Lorenzo Natale},
publisher = {Schloss Dagstuhl},
journal = {Dagstuhl Reports},
volume = {7(2)},
pages = {pages 48-63},
type = {Journal Article},
year = {2017},
doi = {10.4230/DagRep.7.2.48},
url = { https://publications.rwth-aachen.de/record/713498},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{P2016,
title = {Parameter synthesis for probabilistic systems},
author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Albert-Ludwigs-Universität},
pages = {72-74},
type = {Conference Paper},
year = {2016},
doi = {10.6094/UNIFR/10639},
url = { https://publications.rwth-aachen.de/record/683021},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{M2016,
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 = {2016},
url = { https://publications.rwth-aachen.de/record/444449},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{ABSHSRA2015,
title = {A Benchmark Suite for Hybrid Systems Reachability Analysis},
author = {Xin Chen and Stefan Schupp and Ibtissem Ben Makhlouf and Erika Ábrahám and Goran Frehse and Stefan Kowalewski},
publisher = {Springer},
booktitle = {LNCS},
volume = {9058},
pages = {408-414},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-17524-9_29},
url = { https://publications.rwth-aachen.de/record/541100},
}×

@conference{CER2015,
title = {Counterexamples for Expected Rewards},
author = {Tim Quatmann and Nils Jansen and Hans Christian Dehnert and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {9109},
pages = {435-452},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-19249-9_27},
url = { https://publications.rwth-aachen.de/record/541095},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{FDPM2014,
title = {Fast Debugging of PRISM Models},
author = {Hans Christian Dehnert and Nils Jansen and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {8837},
pages = {146-162},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-11936-6_11},
url = { https://publications.rwth-aachen.de/record/460136},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{CGDTMMAIS2014,
title = {Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey},
author = {Erika Ábrahám and Bernd Becker and Hans Christian Dehnert and Nils Jansen and Joost-Pieter Katoen and Ralf Wimmer},
publisher = {Springer},
booktitle = {LNCS},
volume = {8483},
pages = {65-121},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-07317-0_3},
url = { https://publications.rwth-aachen.de/record/443312},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{OGBCSMTSRN2013,
title = {On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers},
author = {Sebastian Junges and Ulrich Loup and Florian Corzilius and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {8080},
pages = {186-198},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-40663-8_18},
url = { https://publications.rwth-aachen.de/record/226897},
}×

@conference{HCPA2013,
title = {High-level Counterexamples for Probabilistic Automata},
author = {Ralf Wimmer and Nils Jansen and Andreas Vorpahl and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {8054},
pages = {39-54},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-40196-1_4},
url = { https://publications.rwth-aachen.de/record/226401},
}×

@conference{LFSHR2013,
title = {Lyapunov Function Synthesis using Handelman Representations},
author = {Sriram Sankaranarayanan and Xin Chen and Erika Ábrahám},
publisher = {Elsevier},
booktitle = {Nonlinear Control Systems},
volume = {9,1},
pages = {576-581},
type = {Conference Paper},
year = {2013},
doi = {10.3182/20130904-3-FR-2041.00198},
url = { https://publications.rwth-aachen.de/record/226223},
}×

@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},
}×

@conference{FAANLHS2013,
title = {Flow*: An Analyzer for Non-Linear Hybrid Systems},
author = {Xin Chen and Erika Ábrahám and Sriram Sankaranarayanan},
publisher = {Springer},
booktitle = {LNCS},
volume = {8044},
pages = {258-263},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-39799-8_18},
url = { https://publications.rwth-aachen.de/record/225803},
}×

@conference{ATCMCRTM2013,
title = {A Timed CTL Model Checker for Real-Time Maude},
author = {Daniela Lepri and Erika Ábrahám and Peter Csaba Ölveczky},
publisher = {Springer},
booktitle = {LNCS},
volume = {8089},
pages = {334-339},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-40206-7_27},
url = { https://publications.rwth-aachen.de/record/225701},
}×

@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},
}×

@conference{ASICPCAD2013,
title = {A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition},
author = {Ulrich Loup and Karsten Scheibler and Florian Corzilius and Erika Ábrahám and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {7898},
pages = {193-207},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-38574-2_13},
url = { https://publications.rwth-aachen.de/record/207654},
}×

@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},
}×

@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},
}×

@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/978-3-642-33386-6_27},
url = { https://publications.rwth-aachen.de/record/207901},
}×

@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},
}×

@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},
}×

@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},
}×

@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/978-3-642-31612-8_35},
url = { https://publications.rwth-aachen.de/record/207332},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{SCGMC2011,
title = {SMT-based Counterexample Generation for Markov Chains},
author = {Bettina Braitling and Ralf Wimmer and Bernd Becker and Nils Jansen and Erika Ábrahám},
publisher = {OFFIS},
pages = {19-28},
type = {Conference Paper},
year = {2011},
url = { https://publications.rwth-aachen.de/record/564234},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×