Paper TestCov: Robust Test-Suite Execution and Coverage Measurement accepted for presentation at ASE 2019!

Publications of G. Ernst

(All PublicationsIndex)

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), volume 11562 of LNCS, pages 208--230, 2019.
    Springer.
    [ Article ] [bibtex-entry]

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

  5. 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]

  6. 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]

  7. 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.
    Work in Progress Report. [ Article ] [bibtex-entry]

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

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

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

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

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

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

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

  15. 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]

  16. 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]

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

  18. 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]

  19. 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]

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

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

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

  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.
    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]

Theses (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.
    [ Material ] [ 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: Fri Nov 15 11:21:46 2019


This document was translated from BibTEX by bibtex2html