Publications of Gidon Ernst
Books and proceedings
-
Proc. of the SpecifyThis Track at ISoLa 2024.
LNCS,
2024.
Springer.
BibTeX Entry
@proceedings{ernst:isola2024, title = {Proc. of the SpecifyThis Track at ISoLa 2024}, editor = {Gidon Ernst and Paula Herber and Marieke Huisman and Mattias Ulbrich}, volume = {15221}, year = {2024}, series = {LNCS}, publisher = {{Springer}}, } -
Proc. of Formal Techniques for Java-like Programs (FTfJP@ECOOP).
2019.
ACM.
doi:10.1145/3340672
Publisher's Version
PDF
Supplement
BibTeX Entry
@proceedings{ernst:ftfjp2019, title = {Proc. of Formal Techniques for Java-like Programs (FTfJP@ECOOP)}, editor = {Toby Murray and Gidon Ernst}, year = {2019}, publisher = {{ACM}}, isbn = {978-1-4503-6864-3}, doi = {10.1145/3340672}, url = {https://doi.org/10.1145/3340672}, }
Articles in journal or book chapters
-
Quick Theory Exploration for Algebraic Data Types via Program Transformations.
2024.
BibTeX Entry
@article{ernst:lemmacalc2024, author = {Gidon Ernst and Grigory Fedyukovich and Robin Sögtrop}, title = {Quick Theory Exploration for Algebraic Data Types via Program Transformations}, year = {2024}, } -
Falsification of Hybrid Systems using Adaptive Probabilistic Search.
Transact. on Modeling and Comp. Simulations (TOMACS), 31(3):1-22,
2021.
ACM.
BibTeX Entry
@article{ernst:tomacs2021, author = {G. Ernst and S. Sedwards and Z. Zhang and I. Hasuo}, title = {Falsification of Hybrid Systems using Adaptive Probabilistic Search}, journal = {Transact. on Modeling and Comp. Simulations (TOMACS)}, volume = {31}, number = {3}, pages = {1--22}, year = {2021}, publisher = {ACM}, } -
Unifying separation logic and region logic to allow interoperability.
Formal Aspects of Computing, 30(3--4):381-441,
2018.
Springer.
BibTeX Entry
@article{ernst:bao2018, author = {Y. Bao and G. T. Leavens and G. Ernst}, title = {Unifying separation logic and region logic to allow interoperability}, journal = {Formal Aspects of Computing}, volume = {30}, number = {3--4}, pages = {381--441}, year = {2018}, publisher = {Springer}, } -
Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search.
Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 37(11):2894-2905,
2018.
IEEE.
Presented at the International Conference on Embedded Software (EMSOFT) 2018, Nominated for best paper
PDF
BibTeX Entry
@article{ernst:emsoft2018, author = {Z. Zhang and G. Ernst and S. Sedwards and P. Arcaini and I. Hasuo}, title = {{Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search}}, journal = {Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)}, volume = {37}, number = {11}, pages = {2894--2905}, year = {2018}, publisher = {IEEE}, pdf = {https://www.sosy-lab.org/research/pub/2018-TCAD.Two-Layered_Falsification_of_Hybrid_Systems_guided_by_Monte_Carlo_Tree_Search.pdf}, note = {Presented at the International Conference on Embedded Software (EMSOFT)~2018, \bf Nominated for best paper}, } -
Symbolic execution for a clash-free subset of ASMs.
Science of Computer Programming (SCP), 158:21-40,
2018.
Elsevier.
PDF
BibTeX Entry
@article{ernst:scp2017, author = {G. Schellhorn and G. Ernst and J. Pf{\"a}hler and S. Bodenm{\"u}ller and W. Reif}, title = {{Symbolic execution for a clash-free subset of ASMs}}, journal = {Science of Computer Programming (SCP)}, volume = {158}, pages = {21--40}, year = {2018}, publisher = {Elsevier}, pdf = {https://www.sosy-lab.org/research/pub/2017-SCP.Symbolic_Execution_for_a_Clash-Free_Subset_of_ASMs.pdf}, } -
Modular, crash-safe refinement for ASMs with submachines.
Science of Computer Programming (SCP), 131:3-21,
2016.
Elsevier.
PDF
BibTeX Entry
@article{ernst:scp2016, author = {G. Ernst and J. Pf{\"a}hler and G. Schellhorn and W. Reif}, title = {{Modular, crash-safe refinement for ASMs with submachines}}, journal = {Science of Computer Programming (SCP)}, volume = {131}, pages = {3--21}, year = {2016}, publisher = {Elsevier}, pdf = {https://www.sosy-lab.org/research/pub/2016-SCP.Modular_Crash-Safe_Refinement_for_ASMs_with_Submachines.pdf}, } -
Verification of B+ trees by integration of shape analysis and interactive theorem proving.
Software & Systems Modeling (SoSyM), 14(1):27-44,
2015.
Springer.
BibTeX Entry
@article{ernst:sosym2015, author = {G. Ernst and G. Schellhorn and W. Reif}, title = {{Verification of B+ trees by integration of shape analysis and interactive theorem proving}}, journal = {Software \& Systems Modeling (SoSyM)}, volume = {14}, number = {1}, pages = {27--44}, year = {2015}, publisher = {Springer}, } -
KIV-Overview and VerifyThis competition.
Software Tools for Technology Transfer (STTT), 17(6):677-694,
2015.
Springer.
BibTeX Entry
@article{ernst:sttt2015, author = {G. Ernst and J. Pf{\"a}hler and G. Schellhorn and D. Haneberg and W. Reif}, title = {{KIV---Overview and VerifyThis competition}}, journal = {Software Tools for Technology Transfer (STTT)}, volume = {17}, number = {6}, pages = {677--694}, year = {2015}, publisher = {Springer}, } -
Compositional verification of a lock-free stack with RGITL.
Electronic Communications of the Automated Verification of Critical Systems (EASST), 66,
2014.
BibTeX Entry
@article{ernst:east2014, author = {B. Tofan and G. Schellhorn and G. Ernst and J. Pf{\"a}hler and W. Reif}, title = {{Compositional verification of a lock-free stack with RGITL}}, journal = {Electronic Communications of the Automated Verification of Critical Systems (EASST)}, volume = {66}, year = {2014}, } -
RGITL: A temporal logic framework for compositional reasoning about interleaved programs.
Annals of Mathematics and Artificial Intelligence (AMAI), 71:1-44,
2014.
Springer.
BibTeX Entry
@article{ernst:amai2014, author = {G. Schellhorn and B. Tofan and G. Ernst and J. Pf{\"a}hler and W. Reif}, title = {{RGITL: A temporal logic framework for compositional reasoning about interleaved programs}}, journal = {Annals of Mathematics and Artificial Intelligence (AMAI)}, volume = {71}, pages = {1--44}, year = {2014}, publisher = {Springer}, issue = {1--3}, } -
Garantiert fehlerfrei!.
Mechatroniknews,
Februar
2013.
Cluster Mechatronik & Automation e.V..
BibTeX Entry
@article{ernst:mechatronik2013, author = {G. Ernst and A. Habermaier}, title = {Garantiert fehlerfrei!}, journal = {Mechatroniknews}, year = {2013}, publisher = {Cluster Mechatronik \& Automation e.V.}, month = {Februar}, }
Articles in conference or workshop proceedings
-
Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals.
In Proc. of Hybrid Systems: Computation and Control,
2025.
(To appear)
BibTeX Entry
@inproceedings{ernst:hscc2025, author = {Jiří Fejlek and Gidon Ernst}, title = {Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals}, booktitle = {Proc. of Hybrid Systems: Computation and Control}, year = {2025}, note = {(To appear)}, } -
Towards Automatic Structured Inference of Module Abstractions.
In Festschrift for Prof. Wolfgang Reif,
2025.
(To appear)
BibTeX Entry
@inproceedings{ernst:reif65, author = {Gidon Ernst and Marian Lingsch-Rosenfeld}, title = {Towards Automatic Structured Inference of Module Abstractions}, booktitle = {Festschrift for Prof. Wolfgang Reif}, year = {2025}, note = {(To appear)}, } -
The VerifyThis Collaborative Long-term Challenge Series.
In Proc. of ETAPS 2023 TOOLympics,
LNCS,
2024.
BibTeX Entry
@inproceedings{ernst:vt-ltc2023, author = {W.~Ahrendt and G.~Ernst and P.~Herber and M.~Huisman and R.~Monti and M.~Ulbrich and A.~Weigl}, title = {The VerifyThis Collaborative Long-term Challenge Series}, booktitle = {Proc. of ETAPS 2023 TOOLympics}, volume = {14550}, year = {2024}, series = {LNCS}, } -
The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems.
In Proc. of ETAPS 2023 TOOLympics,
LNCS,
2024.
BibTeX Entry
@inproceedings{ernst:arch-overview2023, author = {A.~Abate and M.~Althoff and L.~Bu and G.~Ernst and G.~Frehse and L.~Geretti and T.~Johnson and C.~Menghi and S.~Mitsch and S.~Schupp and S.~Soudjani}, title = {The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems}, booktitle = {Proc. of ETAPS 2023 TOOLympics}, volume = {14550}, year = {2024}, series = {LNCS}, } -
Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification.
In Proc. of the SpecifyThis Track at ISoLa 2024,
LNCS,
2024.
Springer.
BibTeX Entry
@inproceedings{ernst:specifythis2024, author = {Gidon Ernst and Wolfram Pfeifer and Mattias Ulbrich}, title = {{Contract-LIB}: A Proposal for a Common Interchange Format for Software System Specification}, booktitle = {Proc. of the SpecifyThis Track at ISoLa 2024}, volume = {15221}, year = {2024}, series = {LNCS}, publisher = {{Springer}}, } -
Verify This: Memcached—A Practical Long-term Challenge for the Integration of Formal Methods (Short Paper).
In Proc. of Integrated Formal Methods (iFM),
LNCS,
pages 82-89,
2023.
Springer.
BibTeX Entry
@inproceedings{ernst:ifm2023, author = {G.~Ernst and A.~Weigl}, title = {Verify This: Memcached—A Practical Long-term Challenge for the Integration of Formal Methods (Short Paper)}, booktitle = {Proc. of Integrated Formal Methods (iFM)}, volume = {14300}, pages = {82--89}, year = {2023}, series = {LNCS}, publisher = {Springer}, } -
Assume but Verify: Deductive Verification of Leaked Information
in Concurrent Applications.
In Proc. of Computer and Communications Security (CCS),
pages 1746-1760,
2023.
ACM.
BibTeX Entry
@inproceedings{ernst:ccs2023, author = {T.~Murray and M.~Tiwari and G.~Ernst and D.~Naumann}, title = {Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications}, booktitle = {Proc. of Computer and Communications Security (CCS)}, pages = {1746--1760}, year = {2023}, publisher = {ACM}, } -
Compositional Vulnerability Detection with Insecurity Separation Logic.
In Proc. of International Conference on Formal Engineering Methods (ICFEM),
LNCS,
pages 65-82,
2023.
Springer.
BibTeX Entry
@inproceedings{ernst:icfem2023, author = {T.~Murray and P.~Yang and G.~Ernst}, title = {Compositional Vulnerability Detection with Insecurity Separation Logic}, booktitle = {Proc. of International Conference on Formal Engineering Methods (ICFEM)}, volume = {14308}, pages = {65--82}, year = {2023}, series = {LNCS}, publisher = {Springer}, } -
Korn: Horn clause based Verification of C programs (Competition Contribution).
In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
LNCS 13994,
2023.
Springer.
BibTeX Entry
@inproceedings{ernst:korn2023, author = {G.~Ernst}, title = {\textsc{Korn}: {Horn} clause based Verification of {C} programs (Competition Contribution)}, booktitle = {Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, pages = {}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {}, } -
Assume but Verify: Deductive Verification of
Leaked Information in Concurrent Applications.
In Proc. of Computer and Communications Security (CCS),
2023.
To Appear.
BibTeX Entry
@inproceedings{ernst:2023assumeverify, author = {Toby Murray and Mukesh Tiwari and Gidon Ernst and David A. Naumann}, title = {Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications}, booktitle = {Proc. of Computer and Communications Security (CCS)}, year = {2023}, note = {To Appear.}, } -
State selection algorithms and their impact on the performance of stateful network protocol fuzzing.
In Proc. of Software Analysis, Evolution and Reengineering (SANER),
2022.
IEEE.
BibTeX Entry
@inproceedings{ernst:saner2022, author = {D. Liu and V.-T. Pham and G. Ernst and T. Murray and B.I.P. Rubinstein}, title = {State selection algorithms and their impact on the performance of stateful network protocol fuzzing}, booktitle = {Proc. of Software Analysis, Evolution and Reengineering (SANER)}, year = {2022}, publisher = {IEEE}, } -
Legion: Best-First Concolic Testing.
In Proc. of Automated Software Engineering (ASE),
pages 54-65,
2020.
IEEE.
PDF
BibTeX Entry
@inproceedings{ernst:ase2020, author = {D. Liu and G. Ernst and T. Murray and B. Rubinstein}, title = {Legion: Best-First Concolic Testing}, booktitle = {Proc. of Automated Software Engineering (ASE)}, pages = {54--65}, year = {2020}, publisher = {IEEE}, pdf = {https://arxiv.org/abs/2002.06311}, } -
Legion: Best-First Concolic Testing (Competition Contribution)..
In Proc. of Fundamental Approaches to Software Engineering (FASE),
pages 545-549,
2020.
BibTeX Entry
@inproceedings{ernst:testcomp2020, author = {D. Liu and G. Ernst and T. Murray and B.I.P. Rubinstein}, title = {Legion: Best-First Concolic Testing (Competition Contribution).}, booktitle = {Proc. of Fundamental Approaches to Software Engineering (FASE)}, pages = {545--549}, year = {2020}, } -
Information Flow Testing of a PGP Keyserver.
In Proc. of the VerifyThis Long-term Challenge 2020,
pages 11-13,
2020.
KIT Library.
Technical Report.
BibTeX Entry
@inproceedings{ernst:vtltc2020-iftesting, author = {G. Ernst and L. Rieger}, title = {{Information Flow Testing of a PGP Keyserver}}, booktitle = {{Proc. of the VerifyThis Long-term Challenge 2020}}, pages = {11--13}, year = {2020}, publisher = {KIT Library}, note = {Technical Report.}, } -
Verifying the Security of a PGP Keyserver.
In Proc. of the VerifyThis Long-term Challenge 2020,
pages 14-16,
2020.
KIT Library.
Technical Report.
BibTeX Entry
@inproceedings{ernst:vtltc2020-ifverify, author = {G. Ernst and T. Murray and M. Tiwari}, title = {{Verifying the Security of a PGP Keyserver}}, booktitle = {{Proc. of the VerifyThis Long-term Challenge 2020}}, pages = {14--16}, year = {2020}, publisher = {KIT Library}, note = {Technical Report.}, } -
Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input.
In Proc. of Quantitative Evaluation of Systems (QEST),
LNCS,
pages 165-181,
2019.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:qest2019, author = {G. Ernst and S. Sedwards and Z. Zhang and I. Hasuo}, title = {Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input}, booktitle = {Proc. of Quantitative Evaluation of Systems (QEST)}, volume = {11785}, pages = {165--181}, year = {2019}, series = {LNCS}, publisher = {Springer}, pdf = {https://arxiv.org/abs/1812.04159}, } -
SecCSL: Security Concurrent Separation Logic.
In Proc. of Computer Aided Verification (CAV),
LNCS,
pages 208-230,
2019.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:cav2019, author = {G. Ernst and T. Murray}, title = {{SecCSL: Security Concurrent Separation Logic}}, booktitle = {Proc. of Computer Aided Verification (CAV)}, volume = {11562}, pages = {208--230}, year = {2019}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2019-CAV.SecCSL_Security_Concurrent_Separation_Logic.pdf}, } -
ARCH-COMP19 Category Report: Results on the Falsification Benchmarks.
In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH),
EPiC,
pages 129-140,
2019.
EasyChair.
doi:10.29007/68dk
Publisher's Version
PDF
BibTeX Entry
@inproceedings{ernst:arch2019, author = {G. Ernst and P. Arcaini and A. Donze and G. Fainekos and L. Mathesen and G. Pedrielli and S. Yaghoubi and Y. Yamagata and Z. Zhang}, title = {{ARCH-COMP19 Category Report: Results on the Falsification Benchmarks}}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {61}, pages = {129--140}, year = {2019}, series = {EPiC}, publisher = {EasyChair}, doi = {10.29007/68dk}, pdf = {https://www.sosy-lab.org/research/pub/2019-ARCH.Category_Report_Falsification.pdf}, } -
VerifyThis - Verification Competition with a Human Factor.
In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
LNCS,
2019.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:toolympics2019, author = {G. Ernst and M. Huisman and W. Mostowski and M. Ulbrich}, title = {{VerifyThis -- Verification Competition with a Human Factor}}, booktitle = {Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {11429}, year = {2019}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2019-TACAS.VerifyThis-Verification_Competition_with_a_Human_Factor.pdf}, } -
In Search of Perfect Users: Towards Understanding the Usability of Converged Multi-Level Secure User Interfaces.
In Proc. of Computer Human Interaction Australia (OzCHI),
pages 572-576,
2018.
ACM.
Work in Progress Report.
PDF
BibTeX Entry
@inproceedings{ernst:ozchi2018, author = {A. Issa and T. Murray and G. Ernst}, title = {{In Search of Perfect Users: Towards Understanding the Usability of Converged Multi-Level Secure User Interfaces}}, booktitle = {Proc. of Computer Human Interaction Australia (OzCHI)}, pages = {572--576}, year = {2018}, publisher = {ACM}, pdf = {https://www.sosy-lab.org/research/pub/2018-OzCHI.In_Search_of_Perfect_Users.pdf}, note = {Work in Progress Report.}, } -
ARCH-COMP18 Category Report: Results on the Falsification Benchmarks.
In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH),
EPiC,
pages 104-109,
2018.
EasyChair.
PDF
BibTeX Entry
@inproceedings{ernst:arch2018, author = {A. Dokhanchi and S. Yaghoubi and B. Hoxha and G. Fainekos and G. Ernst and Z. Zhang and P. Arcaini and I. Hasuo and S. Sedwards}, title = {{ARCH-COMP18 Category Report: Results on the Falsification Benchmarks}}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {54}, pages = {104--109}, year = {2018}, series = {EPiC}, publisher = {EasyChair}, pdf = {https://www.sosy-lab.org/research/pub/2018-ARCH.Results_on_the_Falsification_Benchmarks.pdf}, } -
Time-staging Enhancement of Hybrid System Falsification (Abstract).
In Proc. of Monitoring and Testing of Cyber-Physical Systems (MT-CPS),
2018.
IEEE.
BibTeX Entry
@inproceedings{ernst:mt-cps2018, author = {Z. Zhang and G. Ernst and I. Hasuo and S. Sedwards}, title = {{Time-staging Enhancement of Hybrid System Falsification (Abstract)}}, booktitle = {Proc. of Monitoring and Testing of Cyber-Physical Systems (MT-CPS)}, year = {2018}, publisher = {IEEE}, } -
Modular verification of order-preserving writeback caches.
In Proc. of Integrated Formal Methods (iFM),
LNCS,
pages 375-390,
2017.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:ifm2017, author = {J. Pf{\"a}hler and G. Ernst and S. Bodenm{\"u}ller and G. Schellhorn and W. Reif}, title = {Modular verification of order-preserving writeback caches}, booktitle = {Proc. of Integrated Formal Methods (iFM)}, volume = {10510}, pages = {375--390}, year = {2017}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2017-iFM.Modular_Verification_of_Order-Preserving_Write-Back_Caches.pdf}, } -
A relational encoding for a clash-free subset of ASMs.
In Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ),
LNCS,
pages 237-243,
2016.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:abz2016, author = {G. Schellhorn and G. Ernst and J. Pf{\"a}hler and W. Reif}, title = {{A relational encoding for a clash-free subset of ASMs}}, booktitle = {Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ)}, volume = {9675}, pages = {237--243}, year = {2016}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2016-ABZ.A_Relational_Encoding_for_a_Clash-Free_Subset_of_ASMs.pdf}, } -
Conditional effects in fine-grained region logic.
In Proc. of Formal Techniques for Java-like Programs (FTfJP),
2015.
ACM.
BibTeX Entry
@inproceedings{ernst:ftfjp2015, author = {Y. Bao and G. T. Leavens and G. Ernst}, title = {{Conditional effects in fine-grained region logic}}, booktitle = {Proc. of Formal Techniques for Java-like Programs (FTfJP)}, year = {2015}, publisher = {ACM}, } -
Inside a verified Flash file system: transactions & garbage collection.
In Proc. of Verified Software: Theories, Tools, Experiments (VSTTE),
LNCS,
pages 73-93,
2015.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:vstte2015, author = {G. Ernst and J. Pf{\"a}hler and G. Schellhorn and W. Reif}, title = {{Inside a verified Flash file system: transactions \& garbage collection}}, booktitle = {Proc. of Verified Software: Theories, Tools, Experiments (VSTTE)}, volume = {9593}, pages = {73--93}, year = {2015}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2015-VSTTE.Inside_a_Verified_Flash_File_System.pdf}, } -
Modular refinement for submachines of ASMs.
In Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ),
LNCS,
pages 188-203,
2014.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:abz2014, author = {G. Ernst and J. Pf{\"a}hler and G. Schellhorn and W. Reif}, title = {{Modular refinement for submachines of ASMs}}, booktitle = {Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ)}, volume = {8477}, pages = {188--203}, year = {2014}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2014-ABZ.Modular_Refinement_for_Submachines_of_ASMs.pdf}, } -
Development of a verified Flash file system.
In Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ),
LNCS,
pages 9-24,
2014.
Springer.
Invited Paper
PDF
BibTeX Entry
@inproceedings{ernst:abz2014-overview, author = {G. Schellhorn and G. Ernst and J. Pf{\"a}hler and D. Haneberg and W. Reif}, title = {{Development of a verified Flash file system}}, booktitle = {Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ)}, volume = {8477}, pages = {9--24}, year = {2014}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2014-ABZ.Development_of_a_Verified_Flash_File_System.pdf}, note = {Invited Paper}, } -
Formal specification of an erase block management layer for Flash memory.
In Haifa Verification Conference (HVC),
LNCS,
pages 214-229,
2013.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:hvc2013, author = {J. Pf{\"a}hler and G. Ernst and G. Schellhorn and D. Haneberg and W. Reif}, title = {{Formal specification of an erase block management layer for Flash memory}}, booktitle = {Haifa Verification Conference (HVC)}, volume = {8244}, pages = {214--229}, year = {2013}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2013-HVC_Formal_Specification_of_an_Erase_Block_management_Layer_for_Flash_Memory.pdf}, } -
Verification of a Virtual Filesystem Switch.
In Proc. of Verified Software: Theories, Tools, Experiments (VSTTE),
LNCS,
pages 242-261,
2013.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:vstte2013, author = {G. Ernst and G. Schellhorn and D. Haneberg and J. Pf{\"a}hler and W. Reif}, title = {{Verification of a Virtual Filesystem Switch}}, booktitle = {Proc. of Verified Software: Theories, Tools, Experiments (VSTTE)}, volume = {8164}, pages = {242--261}, year = {2013}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2013-VSTTE.Verification_of_a_Virtual_Filesystem_Switch.pdf}, } -
A formal model of a Virtual Filesystem Switch.
In Proc. of Software and Systems Modeling (SSV),
EPTCS,
pages 33-45,
2012.
PDF
BibTeX Entry
@inproceedings{ernst:ssv2012, author = {G. Ernst and G. Schellhorn and D. Haneberg and J. Pf{\"a}hler and W. Reif}, title = {{A formal model of a Virtual Filesystem Switch}}, booktitle = {Proc. of Software and Systems Modeling (SSV)}, volume = {102}, pages = {33--45}, year = {2012}, series = {EPTCS}, pdf = {https://www.sosy-lab.org/research/pub/2012-SSV.A_Formal_Model_of_a_Virtual_Filesysem_Switch.pdf}, } -
Verification of B+ trees: an experiment combining shape analysis and interactive theorem proving.
In Proc. of Software Engineering and Formal Methods (SEFM),
LNCS,
pages 188-203,
2011.
Springer.
PDF
BibTeX Entry
@inproceedings{ernst:sefm2011, author = {G. Ernst and G. Schellhorn and W. Reif}, title = {{Verification of B+ trees: an experiment combining shape analysis and interactive theorem proving}}, booktitle = {Proc. of Software Engineering and Formal Methods (SEFM)}, volume = {7041}, pages = {188--203}, year = {2011}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2011-SEFM.Verification_of_B+_trees.pdf}, } -
The COST IC0701 verification competition 2011.
In Proc. of Formal Verification of Object-Oriented Software (FoVeOOS),
LNCS,
pages 3-21,
2011.
Springer.
BibTeX Entry
@inproceedings{ernst:foveoos2011, author = {T. Bormer and M. Brockschmidt and D. Distefano and G. Ernst and J.-C. Filli{\^a}tre and R. Grigore and M. Huisman and V. Klebanov and C. March{\'e} and R. Monahan and W. Mostowski and N. Polikarpova and C. Scheben and G. Schellhorn and B. Tofan and J. Tschannen and M. Ulbrich}, title = {{The COST IC0701 verification competition 2011}}, booktitle = {Proc. of Formal Verification of Object-Oriented Software (FoVeOOS)}, volume = {7421}, pages = {3--21}, year = {2011}, series = {LNCS}, publisher = {Springer}, } -
Simulating a Flash File System with CoreASM and Eclipse.
In Proc. of Dependable Software for Critical Infrastructures (DSCI),
GI Lecture Notes in Informatics,
2011.
Gesellschaft für Informatik.
BibTeX Entry
@inproceedings{ernst:gi2011, author = {M. Junker and D. Haneberg and G. Schellhorn and W. Reif and G. Ernst}, title = {{Simulating a Flash File System with CoreASM and Eclipse}}, booktitle = {Proc. of Dependable Software for Critical Infrastructures (DSCI)}, volume = {192}, year = {2011}, series = {GI Lecture Notes in Informatics}, publisher = {Gesellschaft für Informatik}, } -
Interleaved programs and rely-guarantee reasoning with ITL.
In Proc. of Temporal Representation and Reasoning (TIME),
pages 99-106,
2011.
IEEE.
PDF
BibTeX Entry
@inproceedings{ernst:time2011, author = {G. Schellhorn and B. Tofan and G. Ernst and W. Reif}, title = {{Interleaved programs and rely-guarantee reasoning with ITL}}, booktitle = {Proc. of Temporal Representation and Reasoning (TIME)}, pages = {99--106}, year = {2011}, publisher = {IEEE}, pdf = {https://www.sosy-lab.org/research/pub/2011-TIME.Interleaved_Program_Rely-Guarantee-Reasoning-with-ITL.pdf}, } -
Optimized Java binary and virtual machine for tiny motes.
In Proc. of Distributed Computing in Sensor Systems (DCOSS),
LNCS,
pages 15-30,
2010.
Springer.
BibTeX Entry
@inproceedings{ernst:dcoss2010, author = {F. Aslam and L. Fennell and C. Schindelhauer and P. Thiemann and G. Ernst and E. Haussmann and S. R{\"u}hrup and Z. A. Uzmi}, title = {{Optimized Java binary and virtual machine for tiny motes}}, booktitle = {Proc. of Distributed Computing in Sensor Systems (DCOSS)}, volume = {6131}, pages = {15--30}, year = {2010}, series = {LNCS}, publisher = {Springer}, } -
Introducing TakaTuka: a Java Virtual Machine for motes.
In Proc. of the Embedded Network Sensor Systems (SENSYS),
pages 399-400,
2008.
ACM.
Poster Abstract
BibTeX Entry
@inproceedings{ernst:sensys2008, author = {F. Aslam and C. Schindelhauer and G. Ernst and D. Spyra and J. Meyer and M. Zalloom}, title = {{Introducing TakaTuka: a Java Virtual Machine for motes}}, booktitle = {Proc. of the Embedded Network Sensor Systems (SENSYS)}, pages = {399--400}, year = {2008}, publisher = {ACM}, note = {Poster Abstract}, }
Internal reports
-
VerifyThis 2018: A Program Verification Competition.
Technical report hal-01981937, Université Paris-Saclay,
2018.
PDF
Supplement
BibTeX Entry
@techreport{ernst:verifythis2018, author = {M. Huisman and R. Monahan and P. M{\"u}ller and A. Paskevich and G. Ernst}, title = {{VerifyThis 2018: A Program Verification Competition}}, number = {hal-01981937}, year = {2018}, url = {https://hal.inria.fr/hal-01981937}, pdf = {https://www.sosy-lab.org/research/pub/2018-HAL.VerifyThis_2018.pdf}, institution = {Universit{\'e} Paris-Saclay}, } -
Crash-safe refinement for a verified Flash file system.
Technical report 2014-02, University of Augsburg,
2014.
PDF
BibTeX Entry
@techreport{ernst:tr2014-02, author = {J. Pf{\"a}hler and G. Ernst and G. Schellhorn and D. Haneberg and W. Reif}, title = {{Crash-safe refinement for a verified Flash file system}}, number = {2014-02}, year = {2014}, pdf = {https://www.sosy-lab.org/research/pub/2014-TR.Crash-Safe_Refinement_for_a_Verified_Flash_File_System.pdf}, institution = {University of Augsburg}, type = {Technical Report}, } -
Translating separation logic into dynamic frames using fine-grained region logic.
Technical report CS-TR-13-02a, University of Central Florida,
2014.
BibTeX Entry
@techreport{ernst:bao2014, author = {Y. Bao and G. T. Leavens and G. Ernst}, title = {{Translating separation logic into dynamic frames using fine-grained region logic}}, number = {CS-TR-13-02a}, year = {2014}, institution = {University of Central Florida}, type = {Technical Report}, }
Theses and projects (PhD, MSc, BSc, Project)
-
Time-staging Enhancement of Hybrid System Falsification.
2018.
Presented at: Symbolic and Numerical Methods for Reachability Analysis (SNR). To appear in Proc. of SNR 2021.
PDF
BibTeX Entry
@misc{ernst:snr2018, author = {G. Ernst and I. Hasuo and Z. Zhang and S. Sedwards}, title = {{Time-staging Enhancement of Hybrid System Falsification}}, year = {2018}, pdf = {https://www.sosy-lab.org/research/pub/2018-SNR.Time-staging_Enhancement_of_Hybrid_System_Falsification.pdf}, note = {Presented at: Symbolic and Numerical Methods for Reachability Analysis (SNR). To appear in Proc. of SNR 2021.}, } -
A Verified POSIX-Compliant Flash File System-Modular Verification Technology & Crash Tolerance.
PhD Thesis, Augsburg University,
2016.
Summa cum laude
PDF
Supplement
BibTeX Entry
@misc{ernst:phd2016, author = {G. Ernst}, title = {A Verified {POSIX}-Compliant Flash File System---Modular Verification Technology \& Crash Tolerance}, year = {2016}, url = {https://isse.de/flashix}, pdf = {https://opus.bibliothek.uni-augsburg.de/opus4/files/3887/thesis_ernst.pdf}, howpublished = {PhD Thesis, Augsburg University}, note = {\textbf{Summa cum laude}}, }
Disclaimer:
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.