Software and Computational Systems Lab

Publications of Gidon Ernst

1. Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo. 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 = {Gidon Ernst and Sean Sedwards and Zhenya Zhang and Ichiro 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}, }
2. Gidon Ernst. A Complete Approach to Loop Verification with Invariants and Summaries. arXiv preprint arXiv:2010.05812, 2020.
   BibTeX Entry

   @article{ernst:loops2020, author = {Gidon Ernst}, title = {A Complete Approach to Loop Verification with Invariants and Summaries}, journal = {arXiv preprint arXiv:2010.05812}, year = {2020}, }
3. Yuyan Bao, Gary Leavens, and Gidon Ernst. 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 = {Yuyan Bao and Gary Leavens and Gidon 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. Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, and Ichiro 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. Nominated for best paper PDF
   BibTeX Entry

   @article{ernst:emsoft2018, author = {Zhenya Zhang and Gidon Ernst and Sean Sedwards and Paolo Arcaini and Ichiro 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 = {Nominated for best paper}, }
5. Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller, and Wolfgang Reif. 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 = {Gerhard Schellhorn and Gidon Ernst and Jörg Pfähler and Stefan Bodenmüller and Wolfgang 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. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, and Wolfgang Reif. 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 = {Gidon Ernst and Jörg Pfähler and Gerhard Schellhorn and Wolfgang 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. Gidon Ernst, Gerhard Schellhorn, and Wolfgang Reif. 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 = {Gidon Ernst and Gerhard Schellhorn and Wolfgang 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. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg, and Wolfgang Reif. KIV-Overview and VerifyThis competition. Software Tools for Technology Transfer (STTT), 17(6):677-694, 2015. Springer.
   BibTeX Entry

   @article{ernst:sttt2015, author = {Gidon Ernst and Jörg Pfähler and Gerhard Schellhorn and Dominik Haneberg and Wolfgang 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. Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, and Wolfgang Reif. 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 = {Bogdan Tofan and Gerhard Schellhorn and Gidon Ernst and Jörg Pfähler and Wolfgang 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. Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Jörg Pfähler, and Wolfgang Reif. 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 = {Gerhard Schellhorn and Bogdan Tofan and Gidon Ernst and Jörg Pfähler and Wolfgang 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. Gidon Ernst and Axel Habermaier. Garantiert fehlerfrei!. Mechatroniknews, Februar 2013. Cluster Mechatronik & Automation e.V..
    BibTeX Entry

    @article{ernst:mechatronik2013, author = {Gidon Ernst and Axel Habermaier}, title = {Garantiert fehlerfrei!}, journal = {Mechatroniknews}, year = {2013}, publisher = {Cluster Mechatronik \& Automation e.V.}, month = {Februar}, }

12. Dongge Liu, Van-Thuan Pham, Gidon Ernst, Toby Murray, and Benjamin 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. To appear.
    BibTeX Entry

    @inproceedings{ernst:saner2022, author = {Dongge Liu and Van-Thuan Pham and Gidon Ernst and Toby Murray and Benjamin 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}, note = {To appear.}, }
13. Gidon Ernst. Loop Verification with Invariants and Summaries. In Proc. of Verification, Model-Checking, and Abstract Interpretation (VMCAI), LNCS, 2022. Springer.
    BibTeX Entry

    @inproceedings{ernst:vmcai2022, author = {Gidon Ernst}, title = {Loop Verification with Invariants and Summaries}, booktitle = {Proc. of Verification, Model-Checking, and Abstract Interpretation (VMCAI)}, volume = {13182}, year = {2022}, series = {LNCS}, publisher = {Springer}, }
14. Gidon Ernst, Johannes Blau, and Toby Murray. Deductive Verification via the Debug Adapter Protocol. In Proc. of Formal Integrated Development Environment (F-IDE), 2021.
    BibTeX Entry

    @inproceedings{ernst:fide2021, author = {Gidon Ernst and Johannes Blau and Toby Murray}, title = {Deductive Verification via the Debug Adapter Protocol}, booktitle = {Proc. of Formal Integrated Development Environment (F-IDE)}, year = {2021}, }
15. Grigory Fedyukovich and Gidon Ernst. Bridging Arrays and ADTs in Recursive Proofs. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, pages 24-42, 2021. Springer.
    BibTeX Entry

    @inproceedings{ernst:tacas2021, author = {Grigory Fedyukovich and Gidon Ernst}, title = {Bridging Arrays and {ADTs} in Recursive Proofs}, booktitle = {Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {12652}, pages = {24--42}, year = {2021}, series = {LNCS}, publisher = {Springer}, }
16. Gidon Ernst and others. ARCH-COMP 2021 category report: Falsification with Validation of Results. In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC, pages 133-152, 2021. EasyChair.
    BibTeX Entry

    @inproceedings{ernst:arch2021, author = {Gidon Ernst and others}, title = {{ARCH-COMP} 2021 category report: Falsification with Validation of Results}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {80}, pages = {133--152}, year = {2021}, series = {EPiC}, publisher = {EasyChair}, }
17. Dongge Liu, Gidon Ernst, Toby Murray, and Ben Rubinstein. Legion: Best-First Concolic Testing. In Proc. of Automated Software Engineering (ASE), pages 54-65, 2020. IEEE. PDF
    BibTeX Entry

    @inproceedings{ernst:ase2020, author = {Dongge Liu and Gidon Ernst and Toby Murray and Ben 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}, }
18. Dongge Liu, Gidon Ernst, Toby Murray, and Benjamin Rubinstein. 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 = {Dongge Liu and Gidon Ernst and Toby Murray and Benjamin Rubinstein}, title = {Legion: Best-First Concolic Testing (Competition Contribution).}, booktitle = {Proc. of Fundamental Approaches to Software Engineering (FASE)}, pages = {545--549}, year = {2020}, }
19. Gidon Ernst and Lukas Rieger. 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 = {Gidon Ernst and Lukas 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.}, }
20. Gidon Ernst, Toby Murray, and Mukesh Tiwari. 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 = {Gidon Ernst and Toby Murray and Mukesh 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.}, }
21. Gidon Ernst and others. ARCH-COMP 2020 category report: Falsification. In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC, pages 140-152, 2020. EasyChair.
    BibTeX Entry

    @inproceedings{ernst:arch2020, author = {Gidon Ernst and others}, title = {{ARCH-COMP} 2020 category report: Falsification}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {74}, pages = {140--152}, year = {2020}, series = {EPiC}, publisher = {EasyChair}, }
22. Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo. 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 = {Gidon Ernst and Sean Sedwards and Zhenya Zhang and Ichiro 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}, }
23. Gidon Ernst and Toby Murray. 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 = {Gidon Ernst and Toby 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}, }
24. Gidon Ernst, Paolo Arcaini, Alexandre Donze, Georgios Fainekos, Logan Mathesen, Gulia Pedrielli, Shakiba Yaghoubi, Yoriyuki Yamagata, and Zhenya 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 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{ernst:arch2019, author = {Gidon Ernst and Paolo Arcaini and Alexandre Donze and Georgios Fainekos and Logan Mathesen and Gulia Pedrielli and Shakiba Yaghoubi and Yoriyuki Yamagata and Zhenya 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}, }
25. Gidon Ernst, Marieke Huisman, Wojciech Mostowski, and Matthias 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. PDF
    BibTeX Entry

    @inproceedings{ernst:toolympics2019, author = {Gidon Ernst and Marieke Huisman and Wojciech Mostowski and Matthias 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}, }
26. Abdullah Issa, Toby Murray, and Gidon 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. Work in Progress Report. PDF
    BibTeX Entry

    @inproceedings{ernst:ozchi2018, author = {Abdullah Issa and Toby Murray and Gidon 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.}, }
27. Adel Dokhanchi, Shakiba Yaghoubi, Bardh Hoxha, Georgios Fainekos, Gidon Ernst, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo, and Sean 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. PDF
    BibTeX Entry

    @inproceedings{ernst:arch2018, author = {Adel Dokhanchi and Shakiba Yaghoubi and Bardh Hoxha and Georgios Fainekos and Gidon Ernst and Zhenya Zhang and Paolo Arcaini and Ichiro Hasuo and Sean 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}, }
28. Zhenya Zhang, Gidon Ernst, Ichiro Hasuo, and Sean Sedwards. 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 = {Zhenya Zhang and Gidon Ernst and Ichiro Hasuo and Sean 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}, }
29. Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, and Wolfgang Reif. 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örg Pfähler and Gidon Ernst and Stefan Bodenmüller and Gerhard Schellhorn and Wolfgang 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}, }
30. Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, and Wolfgang 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. PDF
    BibTeX Entry

    @inproceedings{ernst:abz2016, author = {Gerhard Schellhorn and Gidon Ernst and Jörg Pfähler and Wolfgang 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}, }
31. Yuyan Bao, Gary Leavens, and Gidon Ernst. 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 = {Yuyan Bao and Gary Leavens and Gidon Ernst}, title = {{Conditional effects in fine-grained region logic}}, booktitle = {Proc. of Formal Techniques for Java-like Programs (FTfJP)}, year = {2015}, publisher = {ACM}, }
32. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, and Wolfgang 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. PDF
    BibTeX Entry

    @inproceedings{ernst:vstte2015, author = {Gidon Ernst and Jörg Pfähler and Gerhard Schellhorn and Wolfgang 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}, }
33. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, and Wolfgang Reif. 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 = {Gidon Ernst and Jörg Pfähler and Gerhard Schellhorn and Wolfgang 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}, }
34. Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, and Wolfgang 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. Invited Paper PDF
    BibTeX Entry

    @inproceedings{ernst:abz2014-overview, author = {Gerhard Schellhorn and Gidon Ernst and Jörg Pfähler and Dominik Haneberg and Wolfgang 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}, }
35. Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, and Wolfgang Reif. 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örg Pfähler and Gidon Ernst and Gerhard Schellhorn and Dominik Haneberg and Wolfgang 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}, }
36. Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, and Wolfgang Reif. 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 = {Gidon Ernst and Gerhard Schellhorn and Dominik Haneberg and Jörg Pfähler and Wolfgang 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}, }
37. Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, and Wolfgang Reif. 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 = {Gidon Ernst and Gerhard Schellhorn and Dominik Haneberg and Jörg Pfähler and Wolfgang 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}, }
38. Gidon Ernst, Gerhard Schellhorn, and Wolfgang 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. PDF
    BibTeX Entry

    @inproceedings{ernst:sefm2011, author = {Gidon Ernst and Gerhard Schellhorn and Wolfgang 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}, }
39. Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, Radu Grigore, Marieke Huisman, Vladimir Klebanov, Claude Marché, Rosemary Monahan, Wojciech Mostowski, Nadia Polikarpova, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, and Mattias Ulbrich. 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 = {Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and Jean{-}Christophe Filli{\^{a}}tre and Radu Grigore and Marieke Huisman and Vladimir Klebanov and Claude March{\'{e}} and Rosemary Monahan and Wojciech Mostowski and Nadia Polikarpova and Christoph Scheben and Gerhard Schellhorn and Bogdan Tofan and Julian Tschannen and Mattias 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}, }
40. Maximilian Junker, Dominik Haneberg, Gerhard Schellhorn, Wolfgang Reif, and Gidon 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.
    BibTeX Entry

    @inproceedings{ernst:gi2011, author = {Maximilian Junker and Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif and Gidon 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}, }
41. Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, and Wolfgang Reif. 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 = {Gerhard Schellhorn and Bogdan Tofan and Gidon Ernst and Wolfgang 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}, }
42. Faisal Aslam, Luminous Fennell, Christian Schindelhauer, Peter Thiemann, Gidon Ernst, Elmar Haussmann, Stefan Rührup, and and Zastash 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.
    BibTeX Entry

    @inproceedings{ernst:dcoss2010, author = {Faisal Aslam and Luminous Fennell and Christian Schindelhauer and Peter Thiemann and Gidon Ernst and Elmar Haussmann and Stefan Rührup and and Zastash 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}, }
43. Faisal Aslam, Christian Schindelhauer, Gidon Ernst, David Spyra, Jan Meyer, and Mohannad Zalloom. 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 = {Faisal Aslam and Christian Schindelhauer and Gidon Ernst and David Spyra and Jan Meyer and Mohannad 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}, }

44. Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, and Gidon Ernst. VerifyThis 2018: A Program Verification Competition. Technical report hal-01981937, Université Paris-Saclay, 2018. PDF Supplement
    BibTeX Entry

    @techreport{ernst:verifythis2018, author = {Marieke Huisman and Rosemary Monahan and Peter Müller and Andrei Paskevich and Gidon 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}, }
45. Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, and Wolfgang Reif. 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örg Pfähler and Gidon Ernst and Gerhard Schellhorn and Dominik Haneberg and Wolfgang 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}, }
46. Yuyan Bao, Gary Leavens, and Gidon Ernst. 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 = {Yuyan Bao and Gary Leavens and Gidon 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}, }

47. Gidon Ernst, Ichiro Hasuo, Zhenya Zhang, and Sean Sedwards. 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 = {Gidon Ernst and Ichiro Hasuo and Zhenya Zhang and Sean 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.}, }
48. Gidon Ernst. A Verified POSIX-Compliant Flash File System-Modular Verification Technology & Crash Tolerance. PhD Thesis, Augsburg University, 2016. PDF Supplement
    BibTeX Entry

    @misc{ernst:phd2016, author = {Gidon 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}, }