We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
Paper accepted at HSCC 2025

Publications of Gidon Ernst

Books and proceedings
  1. Gidon Ernst, Paula Herber, Marieke Huisman, and Mattias Ulbrich, editors. Proc. of the SpecifyThis Track at ISoLa 2024. LNCS, 2024. Springer. Link to this entry
    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}}, }
  2. Toby Murray and Gidon Ernst, editors. Proc. of Formal Techniques for Java-like Programs (FTfJP@ECOOP). 2019. ACM. doi:10.1145/3340672 Link to this entry 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
  1. Gidon Ernst, Grigory Fedyukovich, and Robin Sögtrop. Quick Theory Exploration for Algebraic Data Types via Program Transformations. 2024. Link to this entry
    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}, }
  2. G. Ernst, S. Sedwards, Z. Zhang, and I. Hasuo. Falsification of Hybrid Systems using Adaptive Probabilistic Search. Transact. on Modeling and Comp. Simulations (TOMACS), 31(3):1-22, 2021. ACM. Link to this entry
    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}, }
  3. Y. Bao, G. T. Leavens, and G. Ernst. Unifying separation logic and region logic to allow interoperability. Formal Aspects of Computing, 30(3--4):381-441, 2018. Springer. Link to this entry
    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}, }
  4. Z. Zhang, G. Ernst, S. Sedwards, P. Arcaini, and I. Hasuo. 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. Link to this entry 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}, }
  5. G. Schellhorn, G. Ernst, J. Pfähler, S. Bodenmüller, and W. Reif. Symbolic execution for a clash-free subset of ASMs. Science of Computer Programming (SCP), 158:21-40, 2018. Elsevier. Link to this entry 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}, }
  6. G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif. Modular, crash-safe refinement for ASMs with submachines. Science of Computer Programming (SCP), 131:3-21, 2016. Elsevier. Link to this entry 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}, }
  7. G. Ernst, G. Schellhorn, and W. Reif. Verification of B+ trees by integration of shape analysis and interactive theorem proving. Software & Systems Modeling (SoSyM), 14(1):27-44, 2015. Springer. Link to this entry
    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}, }
  8. G. Ernst, J. Pfähler, G. Schellhorn, D. Haneberg, and W. Reif. KIV-Overview and VerifyThis competition. Software Tools for Technology Transfer (STTT), 17(6):677-694, 2015. Springer. Link to this entry
    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}, }
  9. B. Tofan, G. Schellhorn, G. Ernst, J. Pfähler, and W. Reif. Compositional verification of a lock-free stack with RGITL. Electronic Communications of the Automated Verification of Critical Systems (EASST), 66, 2014. Link to this entry
    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}, }
  10. G. Schellhorn, B. Tofan, G. Ernst, J. Pfähler, and W. Reif. RGITL: A temporal logic framework for compositional reasoning about interleaved programs. Annals of Mathematics and Artificial Intelligence (AMAI), 71:1-44, 2014. Springer. Link to this entry
    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}, }
  11. G. Ernst and A. Habermaier. Garantiert fehlerfrei!. Mechatroniknews, Februar 2013. Cluster Mechatronik & Automation e.V.. Link to this entry
    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
  1. Jiří Fejlek and Gidon Ernst. Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals. In Proc. of Hybrid Systems: Computation and Control, 2025. Link to this entry (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)}, }
  2. Gidon Ernst and Marian Lingsch-Rosenfeld. Towards Automatic Structured Inference of Module Abstractions. In Festschrift for Prof. Wolfgang Reif, 2025. Link to this entry (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)}, }
  3. W. Ahrendt, G. Ernst, P. Herber, M. Huisman, R. Monti, M. Ulbrich, and A. Weigl. The VerifyThis Collaborative Long-term Challenge Series. In Proc. of ETAPS 2023 TOOLympics, LNCS, 2024. Link to this entry
    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}, }
  4. A. Abate, M. Althoff, L. Bu, G. Ernst, G. Frehse, L. Geretti, T. Johnson, C. Menghi, S. Mitsch, S. Schupp, and S. Soudjani. The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems. In Proc. of ETAPS 2023 TOOLympics, LNCS, 2024. Link to this entry
    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}, }
  5. Gidon Ernst, Wolfram Pfeifer, and Mattias Ulbrich. 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. Link to this entry
    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}}, }
  6. G. Ernst and A. Weigl. 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. Link to this entry
    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}, }
  7. T. Murray, M. Tiwari, G. Ernst, and D. Naumann. Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. In Proc. of Computer and Communications Security (CCS), pages 1746-1760, 2023. ACM. Link to this entry
    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}, }
  8. T. Murray, P. Yang, and G. Ernst. Compositional Vulnerability Detection with Insecurity Separation Logic. In Proc. of International Conference on Formal Engineering Methods (ICFEM), LNCS, pages 65-82, 2023. Springer. Link to this entry
    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}, }
  9. G. Ernst. 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. Link to this entry
    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 = {}, }
  10. Toby Murray, Mukesh Tiwari, Gidon Ernst, and David A. Naumann. Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. In Proc. of Computer and Communications Security (CCS), 2023. Link to this entry 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.}, }
  11. D. Liu, V.-T. Pham, G. Ernst, T. Murray, and B.I.P. Rubinstein. 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. Link to this entry
    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}, }
  12. D. Liu, G. Ernst, T. Murray, and B. Rubinstein. Legion: Best-First Concolic Testing. In Proc. of Automated Software Engineering (ASE), pages 54-65, 2020. IEEE. Link to this entry 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}, }
  13. D. Liu, G. Ernst, T. Murray, and B.I.P. Rubinstein. Legion: Best-First Concolic Testing (Competition Contribution).. In Proc. of Fundamental Approaches to Software Engineering (FASE), pages 545-549, 2020. Link to this entry
    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}, }
  14. G. Ernst and L. Rieger. Information Flow Testing of a PGP Keyserver. In Proc. of the VerifyThis Long-term Challenge 2020, pages 11-13, 2020. KIT Library. Link to this entry 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.}, }
  15. G. Ernst, T. Murray, and M. Tiwari. Verifying the Security of a PGP Keyserver. In Proc. of the VerifyThis Long-term Challenge 2020, pages 14-16, 2020. KIT Library. Link to this entry 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.}, }
  16. G. Ernst, S. Sedwards, Z. Zhang, and I. Hasuo. Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input. In Proc. of Quantitative Evaluation of Systems (QEST), LNCS, pages 165-181, 2019. Springer. Link to this entry 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}, }
  17. G. Ernst and T. Murray. SecCSL: Security Concurrent Separation Logic. In Proc. of Computer Aided Verification (CAV), LNCS, pages 208-230, 2019. Springer. Link to this entry 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}, }
  18. G. Ernst, P. Arcaini, A. Donze, G. Fainekos, L. Mathesen, G. Pedrielli, S. Yaghoubi, Y. Yamagata, and Z. Zhang. 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 Link to this entry 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}, }
  19. G. Ernst, M. Huisman, W. Mostowski, and M. Ulbrich. VerifyThis - Verification Competition with a Human Factor. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, 2019. Springer. Link to this entry 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}, }
  20. A. Issa, T. Murray, and G. Ernst. 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. Link to this entry 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.}, }
  21. A. Dokhanchi, S. Yaghoubi, B. Hoxha, G. Fainekos, G. Ernst, Z. Zhang, P. Arcaini, I. Hasuo, and S. Sedwards. 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. Link to this entry 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}, }
  22. Z. Zhang, G. Ernst, I. Hasuo, and S. Sedwards. Time-staging Enhancement of Hybrid System Falsification (Abstract). In Proc. of Monitoring and Testing of Cyber-Physical Systems (MT-CPS), 2018. IEEE. Link to this entry
    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}, }
  23. J. Pfähler, G. Ernst, S. Bodenmüller, G. Schellhorn, and W. Reif. Modular verification of order-preserving writeback caches. In Proc. of Integrated Formal Methods (iFM), LNCS, pages 375-390, 2017. Springer. Link to this entry 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}, }
  24. G. Schellhorn, G. Ernst, J. Pfähler, and W. Reif. 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. Link to this entry 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}, }
  25. Y. Bao, G. T. Leavens, and G. Ernst. Conditional effects in fine-grained region logic. In Proc. of Formal Techniques for Java-like Programs (FTfJP), 2015. ACM. Link to this entry
    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}, }
  26. G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif. Inside a verified Flash file system: transactions & garbage collection. In Proc. of Verified Software: Theories, Tools, Experiments (VSTTE), LNCS, pages 73-93, 2015. Springer. Link to this entry 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}, }
  27. G. Ernst, J. Pfähler, G. Schellhorn, and W. Reif. Modular refinement for submachines of ASMs. In Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ), LNCS, pages 188-203, 2014. Springer. Link to this entry 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}, }
  28. G. Schellhorn, G. Ernst, J. Pfähler, D. Haneberg, and W. Reif. Development of a verified Flash file system. In Proc. of Alloy, ASM, B, TLA, VDM, and Z (ABZ), LNCS, pages 9-24, 2014. Springer. Link to this entry 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}, }
  29. J. Pfähler, G. Ernst, G. Schellhorn, D. Haneberg, and W. Reif. Formal specification of an erase block management layer for Flash memory. In Haifa Verification Conference (HVC), LNCS, pages 214-229, 2013. Springer. Link to this entry 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}, }
  30. G. Ernst, G. Schellhorn, D. Haneberg, J. Pfähler, and W. Reif. Verification of a Virtual Filesystem Switch. In Proc. of Verified Software: Theories, Tools, Experiments (VSTTE), LNCS, pages 242-261, 2013. Springer. Link to this entry 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}, }
  31. G. Ernst, G. Schellhorn, D. Haneberg, J. Pfähler, and W. Reif. A formal model of a Virtual Filesystem Switch. In Proc. of Software and Systems Modeling (SSV), EPTCS, pages 33-45, 2012. Link to this entry 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}, }
  32. G. Ernst, G. Schellhorn, and W. Reif. 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. Link to this entry 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}, }
  33. T. Bormer, M. Brockschmidt, D. Distefano, G. Ernst, J.-C. Filliâtre, R. Grigore, M. Huisman, V. Klebanov, C. Marché, R. Monahan, W. Mostowski, N. Polikarpova, C. Scheben, G. Schellhorn, B. Tofan, J. Tschannen, and M. Ulbrich. The COST IC0701 verification competition 2011. In Proc. of Formal Verification of Object-Oriented Software (FoVeOOS), LNCS, pages 3-21, 2011. Springer. Link to this entry
    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}, }
  34. M. Junker, D. Haneberg, G. Schellhorn, W. Reif, and G. Ernst. 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. Link to this entry
    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}, }
  35. G. Schellhorn, B. Tofan, G. Ernst, and W. Reif. Interleaved programs and rely-guarantee reasoning with ITL. In Proc. of Temporal Representation and Reasoning (TIME), pages 99-106, 2011. IEEE. Link to this entry 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}, }
  36. F. Aslam, L. Fennell, C. Schindelhauer, P. Thiemann, G. Ernst, E. Haussmann, S. Rührup, and Z. A. Uzmi. Optimized Java binary and virtual machine for tiny motes. In Proc. of Distributed Computing in Sensor Systems (DCOSS), LNCS, pages 15-30, 2010. Springer. Link to this entry
    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}, }
  37. F. Aslam, C. Schindelhauer, G. Ernst, D. Spyra, J. Meyer, and M. Zalloom. Introducing TakaTuka: a Java Virtual Machine for motes. In Proc. of the Embedded Network Sensor Systems (SENSYS), pages 399-400, 2008. ACM. Link to this entry 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
  1. M. Huisman, R. Monahan, P. Müller, A. Paskevich, and G. Ernst. VerifyThis 2018: A Program Verification Competition. Technical report hal-01981937, Université Paris-Saclay, 2018. Link to this entry 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}, }
  2. J. Pfähler, G. Ernst, G. Schellhorn, D. Haneberg, and W. Reif. Crash-safe refinement for a verified Flash file system. Technical report 2014-02, University of Augsburg, 2014. Link to this entry 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}, }
  3. Y. Bao, G. T. Leavens, and G. Ernst. Translating separation logic into dynamic frames using fine-grained region logic. Technical report CS-TR-13-02a, University of Central Florida, 2014. Link to this entry
    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)
  1. G. Ernst, I. Hasuo, Z. Zhang, and S. Sedwards. Time-staging Enhancement of Hybrid System Falsification. 2018. Link to this entry 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.}, }
  2. G. Ernst. A Verified POSIX-Compliant Flash File System-Modular Verification Technology & Crash Tolerance. PhD Thesis, Augsburg University, 2016. Link to this entry 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.

Last modified: Mon Mar 31 21:35:29 2025 UTC