- Suche

- Kontakt

publications

    2013

  • Verification of a Virtual Filesystem Switch
    Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, and Wolfgang Reif
    In Proc. of Fifth Working Conference on Verified Software: Theories, Tools and Experiments (to appear)
    abstract; Verification of a Virtual Filesystem Switch (475 KB);
     

    • 2012

  • A Formal Model of a Virtual Filesystem Switch
    Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
    In Proc. of Systems Software Verification, pp 33-45, EPTCS Vol. 102
    abstract; A Formal Model of a Virtual Filesystem Switch (233 KB);
     
  • The COST IC0701 Verification Competition 2011
    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
    In Proc. of Formal Verification of Object-Oriented Software (FoVeOOS), pp 3-21, Springer (LNCS)

     

    • 2011

  • Verification of B+ Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving
    Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
    In Proc. of Software Engineering and Formal Methods (SEFM), pp 188-203, Springer (LNCS)
    abstract; Verification of B+ Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (530 KB);
     
  • Simulating a Flash File System with CoreASM and Eclipse
    Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif and Gidon Ernst
    GI Lecture Notes in Informatics 192: Informatik 2011, Gesellschaft für Informatik
    abstract;
     
  • The COST IC0701 Verification Competition 2011
    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, Mattias Ulbrich
    In Proc. of Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Springer, LNCS
    abstract; Springer Link;
     
  • Interleaved Programs and Rely-Guarantee Reasoning with ITL
    G. Schellhorn, B.Tofan, G. Ernst, and W. Reif
    In Proc. of International Symposium on Temporal Representation and Reasoning in AI (TIME), IEEE (CPS), P4508, pp. 99 - 106
    abstract;