The DFG research training group ConVeY started on July 1st.

Publications of G. Ernst

(All PublicationsIndex)

Thesis

  1. G. Ernst.
    A Verified POSIX-Compliant Flash File System---Modular Verification Technology & Crash Tolerance.
    PhD thesis, Augsburg University, 2016.
    [ Article ] [bibtex-entry]

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.
    [bibtex-entry]

  2. 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.
    [ Article ] [bibtex-entry]

  3. 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.
    [ Article ] [bibtex-entry]

  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.
    [ Article ] [bibtex-entry]

  5. 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.
    [bibtex-entry]

  6. 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.
    [bibtex-entry]

  7. Tofan B, 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.
    [bibtex-entry]

  8. G. Schellhorn, B. Tofan, G. Ernst, J. Pfahler, 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.
    [bibtex-entry]

  9. G. Ernst and A. Habermaier.
    Garantiert fehlerfrei!.
    Mechatroniknews, Februar 2013.
    [bibtex-entry]

Articles in conference or workshop proceedings

  1. 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), volume 61 of EPiC, pages 129--140, 2019.
    EasyChair.
    [ Article ] [bibtex-entry]

  2. 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), volume 11429 of LNCS, 2019.
    Springer.
    [ Article ] [bibtex-entry]

  3. G. Ernst and T. Murray.
    SecCSL: Security Concurrent Separation Logic.
    In Proc. of Computer Aided Verification (CAV), 2019.
    Springer.
    To appear. [ Article ] [bibtex-entry]

  4. 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), volume 54 of EPiC, pages 104--109, 2018.
    EasyChair.
    [ Article ] [bibtex-entry]

  5. 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.
    [ Article ] [bibtex-entry]

  6. 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.
    [bibtex-entry]

  7. 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), volume 10510 of LNCS, pages 375--390, 2017.
    Springer.
    [ Article ] [bibtex-entry]

  8. 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), volume 9675 of LNCS, pages 237--243, 2016.
    Springer.
    [ Article ] [bibtex-entry]

  9. 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.
    [bibtex-entry]

  10. 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), volume 9593 of LNCS, pages 73--93, 2015.
    Springer.
    [ Article ] [bibtex-entry]

  11. 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), volume 8477 of LNCS, pages 188--203, 2014.
    Springer.
    [ Article ] [bibtex-entry]

  12. 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), volume 8477 of LNCS, pages 9--24, 2014.
    Springer.
    Invited Paper.
    [ Article ] [bibtex-entry]

  13. 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), volume 8164 of LNCS, pages 242--261, 2013.
    Springer.
    [ Article ] [bibtex-entry]

  14. 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), volume 8244 of LNCS, pages 214--229, 2013.
    Springer.
    [ Article ] [bibtex-entry]

  15. 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), volume 102 of EPTCS, pages 33--45, 2012.
    [ Article ] [bibtex-entry]

  16. 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), volume 7421 of LNCS, pages 3--21, 2011.
    Springer.
    [bibtex-entry]

  17. 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), volume 7041 of LNCS, pages 188--203, 2011.
    Springer.
    [ Article ] [bibtex-entry]

  18. 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), volume 192 of GI Lecture Notes in Informatics, 2011.
    Gesellschaft für Informatik.
    [bibtex-entry]

  19. 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.
    [ Article ] [bibtex-entry]

  20. 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), volume 6131 of LNCS, pages 15--30, 2010.
    Springer.
    [bibtex-entry]

  21. 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.
    Poster Abstract.
    [bibtex-entry]

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.
    [ Material ] [ Article ] [bibtex-entry]

  2. 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.
    [bibtex-entry]

  3. 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.
    [ Article ] [bibtex-entry]

(All PublicationsIndex)



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: Sun Jul 21 05:09:51 2019


This document was translated from BibTEX by bibtex2html