We are hiring new student research assistants and tutors. Apply now!
4 papers accepted at SPIN 2024!

Publications of Gidon Ernst

Articles in journal or book chapters

  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. Link to this entry
    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. Link to this entry
    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. Link to this entry
    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. Link to this entry 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. Link to this entry 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. Link to this entry 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. Link to this entry
    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. Link to this entry
    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. Link to this entry
    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. Link to this entry
    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.. Link to this entry
    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}, }

Articles in conference or workshop proceedings

  1. 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. Link to this entry 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.}, }
  2. Gidon Ernst. Loop Verification with Invariants and Summaries. In Proc. of Verification, Model-Checking, and Abstract Interpretation (VMCAI), LNCS, 2022. Springer. Link to this entry
    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}, }
  3. Gidon Ernst, Johannes Blau, and Toby Murray. Deductive Verification via the Debug Adapter Protocol. In Proc. of Formal Integrated Development Environment (F-IDE), 2021. Link to this entry
    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}, }
  4. 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. Link to this entry
    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}, }
  5. 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. Link to this entry
    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}, }
  6. 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. Link to this entry 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}, }
  7. 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. Link to this entry
    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}, }
  8. 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. Link to this entry 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.}, }
  9. 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. Link to this entry 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.}, }
  10. 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. Link to this entry
    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}, }
  11. 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. Link to this entry 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}, }
  12. Gidon Ernst and Toby 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 = {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}, }
  13. 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 Link to this entry 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}, }
  14. 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. Link to this entry 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}, }
  15. 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. Link to this entry 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.}, }
  16. 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. Link to this entry 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}, }
  17. 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. Link to this entry
    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}, }
  18. 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. Link to this entry 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}, }
  19. 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. Link to this entry 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}, }
  20. 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. Link to this entry
    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}, }
  21. 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. Link to this entry 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}, }
  22. 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. Link to this entry 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}, }
  23. 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. Link to this entry 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}, }
  24. 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. Link to this entry 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}, }
  25. 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. Link to this entry 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}, }
  26. 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. Link to this entry 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}, }
  27. 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. Link to this entry 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}, }
  28. 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. Link to this entry
    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}, }
  29. 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. Link to this entry
    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}, }
  30. 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. Link to this entry 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}, }
  31. 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. Link to this entry
    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}, }
  32. 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. Link to this entry 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}, }

Internal reports

  1. 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. Link to this entry 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}, }
  2. 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. Link to this entry 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}, }
  3. 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. Link to this entry
    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}, }

Theses and projects (PhD, MSc, BSc, Project)

  1. Gidon Ernst, Ichiro Hasuo, Zhenya Zhang, and Sean 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 = {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.}, }
  2. Gidon Ernst. A Verified POSIX-Compliant Flash File System-Modular Verification Technology & Crash Tolerance. PhD Thesis, Augsburg University, 2016. Link to this entry 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}, }

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: Tue Mar 19 02:04:35 2024 UTC