Falsification of Hybrid Systems Using Adaptive Probabilistic Search.

Publications of G. Ernst

Articles in journal or book chapters

  1. 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}, }
  2. 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 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}, }
  3. 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}, }
  4. 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}, }
  5. 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}, }
  6. 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}, }
  7. 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}, }
  8. G. Schellhorn, B. Tofan, G. Ernst, J. Pf"ahler, 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}, }
  9. 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. 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), 2019. Springer. Link to this entry To appear. 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)}, year = {2019}, publisher = {Springer}, pdf = {https://arxiv.org/abs/1812.04159}, note = {To appear.}, }
  2. 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}, }
  3. 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}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2019-ARCH.Category_Report_Falsification.pdf}, }
  4. 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}, }
  5. 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.}, }
  6. 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}, }
  7. G. Ernst, I. Hasuo, Z. Zhang, and S. Sedwards. Time-staging Enhancement of Hybrid System Falsification. In Proc. of Symbolic and Numerical Methods for Reachability Analysis (SNR), EPTCS, 2018. Link to this entry PDF
    BibTeX Entry
    @inproceedings{ernst:snr2018, author = {G. Ernst and I. Hasuo and Z. Zhang and S. Sedwards}, title = {{Time-staging Enhancement of Hybrid System Falsification}}, booktitle = {Proc. of Symbolic and Numerical Methods for Reachability Analysis (SNR)}, year = {2018}, series = {EPTCS}, pdf = {https://www.sosy-lab.org/research/pub/2018-SNR.Time-staging_Enhancement_of_Hybrid_System_Falsification.pdf}, }
  8. 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}, }
  9. 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}, }
  10. 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}, }
  11. 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}, }
  12. 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}, }
  13. 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}, }
  14. 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}, }
  15. 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}, }
  16. 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}, }
  17. 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}, }
  18. 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}, }
  19. 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}, }
  20. 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}, }
  21. 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}, }
  22. 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}, }
  23. 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. A Verified POSIX-Compliant Flash File System-Modular Verification Technology & Crash Tolerance. PhD Thesis, Augsburg University, Institute for Software and Systems Engineering, 2016. Link to this entry 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, Institute for Software and Systems Engineering}, }

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 Aug 02 01:43:42 2021