Publications-New

Split title: 'On Variable Orderings in MCSAT for Non-linear Real Arithmetic : (extended abstract)'
Fixed Title: 'On Variable Orderings in MCSAT for Non-linear Real Arithmetic: (extended abstract)'
Split title: 'Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development'
Fixed Title: 'Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development'
Split title: 'Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)'
Fixed Title: 'Proceedings of the PhD Symposium at iFM'18 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM'18)'
Split title: 'The HyDRA Tool : A Playground for the Development of Hybrid Systems Reachability Analysis Methods'
Fixed Title: 'The HyDRA Tool: A Playground for the Development of Hybrid Systems Reachability Analysis Methods'
Split title: 'Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics'
Fixed Title: 'Symbolic Computation Techniques in SMT Solving: Mathematical Beauty Meets Efficient Heuristics'
Split title: '2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering : GE 2018 : 28 May 2018, Gothenburg, Sweden : proceedings'
Fixed Title: '2018 ACM/IEEE 1st International Workshop on Gender Equality in Software Engineering: GE 2018'
Split title: 'HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties'
Fixed Title: 'HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties'
Split title: 'Task Planning with OMT: An Application to Production Logistics'
Fixed Title: 'Task Planning with OMT: An Application to Production Logistics'
Split title: 'Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations'
Fixed Title: 'Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations'
Split title: 'Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain'
Fixed Title: 'Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain'
Split title: 'Spread the Work : Multi-threaded Safety Analysis for Hybrid Systems'
Fixed Title: 'Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems'
Split title: 'SMT Solving for Arithmetic Theories: Theory and Tool Support'
Fixed Title: 'SMT Solving for Arithmetic Theories: Theory and Tool Support'
Split title: 'Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017'
Fixed Title: 'Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis'
Split title: 'Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis : Uppsala, Sweden, 22nd April 2017'
Fixed Title: 'Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis'
Split title: 'SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces'
Fixed Title: 'SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces'
Split title: 'Bridging two communities to solve real problems : SC2 2016 : First Workshop on Satisfiability Checking and Symbolic Computation : FETOPEN-CSA SC2 Workshop 1 : September 24, 2016 : affiliated with the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016) : Timisoara, Romania'
Fixed Title: 'Bridging two communities to solve real problems: SC2 2016'
Split title: 'HyPro : A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis'
Fixed Title: 'HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis'
Split title: 'Divide and Conquer : Variable Set Separation in Hybrid Systems Reachability Analysis'
Fixed Title: 'Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis'
Split title: 'Symbolic Computation and Satisfiability Checking : Report of Dagstuhl Seminar 15471'
Fixed Title: 'Symbolic Computation and Satisfiability Checking: Report of Dagstuhl Seminar 15471'
Split title: 'Integrated formal methods : 12th international conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016 : proceedings'
Fixed Title: 'Integrated formal methods'
Split title: 'Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR) : April 11, 2016, Vienna, Austria : held as part of CPS Week, April 11-14, 2016, Vienna, Austria'
Fixed Title: 'Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR)'
Split title: 'Satisfiability Checking : Theory and Applications'
Fixed Title: 'Satisfiability Checking: Theory and Applications'
Split title: 'Theory and practice of formal methods : essays dedicated to Frank de Boer on the occasion of his 60th birthday'
Fixed Title: 'Theory and practice of formal methods: essays dedicated to Frank de Boer on the occasion of his 60th birthday'
Split title: 'Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies'
Fixed Title: 'Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies'
Split title: 'SC2 : Satisfiability Checking Meets Symbolic Computation'
Fixed Title: 'SC2: Satisfiability Checking Meets Symbolic Computation'
Split title: 'Preparing HPC Applications for Exascale: Challenges and Recommendations'
Fixed Title: 'Preparing HPC Applications for Exascale: Challenges and Recommendations'
Split title: 'Flow* 1.2: More Effective to Play with Hybrid Systems'
Fixed Title: 'Flow* 1.2: More Effective to Play with Hybrid Systems'
Split title: 'PROPhESY : A PRObabilistic ParamEter SYnthesis Tool'
Fixed Title: 'PROPhESY: A PRObabilistic ParamEter SYnthesis Tool'
Split title: 'SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving'
Fixed Title: 'SMT-RAT: an Open Source C++ Toolbox for Strategic and Parallel SMT Solving'
Split title: 'Tools and Algorithms for the Construction and Analysis of Systems : 20th international conference, TACAS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5 - 13, 2014 ; proceedings'
Fixed Title: 'Tools and Algorithms for the Construction and Analysis of Systems'
Split title: 'Formal techniques for distributed objects, components, and systems : 34th IFIP WG 6.1 international conference, FORTE 2014, held as part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3 - 5, 2014 ; proceedings'
Fixed Title: 'Formal techniques for distributed objects, components, and systems'
Split title: 'Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?'
Fixed Title: 'Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 Sauna World Championships?'
Split title: 'Maybe or Maybe not : Contributions to Stochastic Verification'
Fixed Title: 'Maybe or Maybe not: Contributions to Stochastic Verification'
Split title: 'Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey'
Fixed Title: 'Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey'
Split title: 'From Statistical Model Checking to Statistical Model Inference : Characterizing the Effect of Process Variations in Analog Circuits'
Fixed Title: 'From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits'
Split title: 'Stochastic Bounded Model Checking : Bounded Rewards and Compositionality'
Fixed Title: 'Stochastic Bounded Model Checking: Bounded Rewards and Compositionality'
Split title: 'Flow*: An Analyzer for Non-Linear Hybrid Systems'
Fixed Title: 'Flow*: An Analyzer for Non-Linear Hybrid Systems'
Split title: 'The COMICS Tool : Computing Minimal Counterexamples for DTMCs'
Fixed Title: 'The COMICS Tool: Computing Minimal Counterexamples for DTMCs'
Split title: 'Taylor Model Over-approximations for Flowpipe : Guard Intersections'
Fixed Title: 'Taylor Model Over-approximations for Flowpipe: Guard Intersections'
Split title: 'SMT-RAT : An SMT-Compliant Nonlinear Real Arithmetic Toolbox'
Fixed Title: 'SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox'
Split title: 'Some Like It Very Hot : Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude'
Fixed Title: 'Some Like It Very Hot: Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude'
Split title: 'The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains'
Fixed Title: 'The COMICS Tool: Computing Minimal Counterexamples for Discrete-time Markov Chains'
Split title: 'GiNaCRA: A C++ Library for Real Algebraic Computations'
Fixed Title: 'GiNaCRA: A C++ Library for Real Algebraic Computations'
Split title: 'I-RiSC : an SMT-Compliant Solver for the Existential Fragment of Real Algebra'
Fixed Title: 'I-RiSC: an SMT-Compliant Solver for the Existential Fragment of Real Algebra'
Split title: 'Synthesis of Behavioral Controllers for DES: Increasing Efficiency'
Fixed Title: 'Synthesis of Behavioral Controllers for DES: Increasing Efficiency'
2021
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 = {ACM New York, NY, USA},
type = {Conference Paper},
year = {2021},
doi = {10.1145/3452143.3465538},
url = { https://publications.rwth-aachen.de/record/823081},
}×
[issue]
Jasper Kurt Ferdinand Nalbach, Erika Ábrahám, Gereon Kremer. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities, ISSAC '21: International Symposium on Symbolic and Algebraic Computation (ISSAC '21), ACM New York, NY, USA, 2021.
DOI fulltext PDF [bibtex]
@phdthesis{DB2021,
title = {Determinization and ambiguity of classical and probabilistic Büchi automata},
author = {Anton Pirogov},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2021},
doi = {10.18154/RWTH-2021-02027},
url = { https://publications.rwth-aachen.de/record/813936},
}×
[issue]
Anton Pirogov. Determinization and ambiguity of classical and probabilistic Büchi automata, PhD Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, Diagramme, RWTH Aachen University, 2021.
DOI 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.
2020
DOI fulltext PDF [bibtex]
@masterthesis{AS2020,
title = {A novel adaption of the Simplex algorithm for linear real arithmetic},
author = {Jasper Kurt Ferdinand Nalbach},
institution = {RWTH Aachen University},
pages = {79 Seiten},
type = {Master Thesis},
year = {2020},
doi = {10.18154/RWTH-2021-04303},
url = { https://publications.rwth-aachen.de/record/818122},
}×
[issue]
Jasper Kurt Ferdinand Nalbach, Gereon Kremer. A novel adaption of the Simplex algorithm for linear real arithmetic, Master Thesis, RWTH Aachen University, 79 Seiten, 2020.
[bibtex]
@masterthesis{P2020,
title = {Parameter synthesis in probabilistic timed automata},
author = {Bram Kohlen},
institution = {RWTH Aachen University},
pages = {91 Seiten},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/811856},
}×
[issue]
Bram Kohlen, Jip Josephine Spel. Parameter synthesis in probabilistic timed automata, Master Thesis, RWTH Aachen University, 91 Seiten, 2020.
DOI fulltext PDF [bibtex]
@phdthesis{O2020,
title = {Optimal planning modulo theories},
author = {Francesco Leofante},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (96 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-06076},
url = { https://publications.rwth-aachen.de/record/792387},
}×
[issue]
Francesco Leofante. Optimal planning modulo theories, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (96 Seiten) : Illustrationen, Diagramme, 2020.
DOI fulltext PDF [bibtex]
@phdthesis{C2020,
title = {Cylindrical algebraic decomposition for nonlinear arithmetic problems},
author = {Gereon Kremer},
booktitle = {Aachener Informatik-Berichte},
volume = {2020-04},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme},
type = {PhD Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-05913},
url = { https://publications.rwth-aachen.de/record/792185},
}×
[issue]
Gereon Kremer. Cylindrical algebraic decomposition for nonlinear arithmetic problems, PhD Thesis, RWTH Aachen University, Volume 2020-04 of Aachener Informatik-Berichte, 1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme, 2020.
DOI fulltext PDF [bibtex]
@conference{PSPH2020,
title = {Parameter Synthesis for Probabilistic Hyperproperties},
author = {Erika Ábrahám and Ezio Bartocci and Borzoo Bonakdarpour and Oyendrila Dobe},
booktitle = {EPiC Series in Computing},
volume = {73},
pages = {12-31},
type = {Conference Paper},
year = {2020},
doi = {10.29007/37lf},
url = { https://publications.rwth-aachen.de/record/792181},
}×
[issue]
Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe. Parameter Synthesis for Probabilistic Hyperproperties, The 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2020), Volume 73 of EPiC Series in Computing, 12-31, 2020.
DOI [bibtex]
@conference{FTSRS2020,
title = {Freight Train Scheduling in Railway Systems},
author = {Rebecca Haehn and Erika Ábrahám and Nils Nießen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12040},
pages = {225-241},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-43024-5_14},
url = { https://publications.rwth-aachen.de/record/789633},
}×
[issue]
Rebecca Haehn, Erika Ábrahám, Nils Nießen. Freight Train Scheduling in Railway Systems, 20th International Conference on Measurement, Modelling and Evaluation of Computing Systems (MMB 2020), Volume 12040 of LNCS, 225-241, Springer, 2020.
arXiv:2003.05633 [bibtex]
@unpublished{DCNLRACCDSUCAC2020,
title = {Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
publisher = {Elsevier Science},
pages = {41 Seiten},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2003.05633},
}×
[issue]
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings, 41 Seiten, Elsevier Science, 2020. https://arxiv.org/abs/2003.05633
Show all