Suche

Publications


    2017

  • Modular Verification of Order-Preserving Write-Back Caches
    Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
    iFM 2017 (accepted)
    abstract; ifm2017-preprint (0 KB);

     
  • Symbolic Execution for a Clash-Free Subset of ASMs
    Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
    SCP 2017 (accepted)
    abstract; scp2017-preprint (419 KB);

     
  • 2016

  • Modular, Crash-Safe Refinement for ASMs with Submachines
    Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
    Science of Computer Programming, Elsevier
    abstract; scico2016-preprint (0 KB);

     
  • A Relational Encoding for a Clash-Free Subset of ASMs
    Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
    Proc. of 5th International Conference ABZ 2016, Springer
    abstract; A Relational Encoding for a Clash-Free Subset of ASMs (312 KB);

     
  • Inside a Verified Flash File System: Transactions & Garbage Collection
    Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
    Proc. of 7th Working Conference on Verified Software: Theories, Tools and Experiments, Springer
    abstract; Inside a Verified Flash File System: Transactions & Garbage Collection (432 KB);

     
  • 2015

  • Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications
    Marian Borek, Kuzman Katkalov, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel
    Correct Software in Web Applications and Web Services, 2015, Texts & Monographs in Symbolic Computation 0943-853X, pp 45-81, Springer
    abstract;

     
  • Verifying Opacity of a Transactional Mutex Lock
    J. Derrick and B. Dongol and G. Schellhorn and O. Travkin and H. Wehrheim
    Proceeding of FM 2015, LNCS 9109, pp. 161-177, Springer
    abstract; Springer Link;

     
  • 2014

  • A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset
    B. Tofan, G. Schellhorn, W. Reif
    In Proc. of Integrated Formal Methods (iFM), vol. 8739 LNCS, pp.357-372 , Springer
    abstract;

     
  • A Sound and Complete Method for Linearizability of Concurrent Data Structures
    G. Schellhorn, J.Derrick, and H. Wehrheim
    Journal of Transactions on Computational Logic, ACM New York, Vol. 15 Issue 4, November 2014, Article No. 31
    abstract;

     
  • Modular Refinement for Submachines of ASMs
    Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
    Proc. of 4th International Conference ABZ 2014, Springer
    abstract; Modular Refinement for Submachines of ASMs (421 KB);

     
  • Development of a Verified Flash File System
    Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif
    Proc. of 4th International Conference ABZ 2014, Springer
    abstract; Development of a Verified Flash File System (446 KB); Presentation (invited Talk) (2892 KB);

     
  • KIV: overview and VerifyThis competition
    Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
    International Journal on Software Tools for Technology Transfer (STTT), Springer
    abstract;

     
  • Two Approaches for Proving Linearizability of Multiset
    B. Tofan, O. Travkin, G. Schellhorn, H. Wehrheim
    Science of Computer Programming Journal, vol. 96, Part 3, pp. 297–314, Elsevier
    abstract;

     
  • Quiescent Consistency: Defining and Verifying Relaxed Linearizability
    J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, H. Wehrheim
    In Proc. of Formal Methods (FM), Springer, LNCS, vol. 8442, pp. 200 - 214
    abstract;

     
  • Crash-Safe Refinement for a Verified Flash File System
    Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg and Wolfgang Reif
    Reports / Technische Berichte - Herausgeber: Fakultät für Angewandte Informatik der Universität Augsburg, OPUS, Report 2014-02
    abstract;

     
  • 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, Springer
    abstract; Verification of a Virtual Filesystem Switch (363 KB);

     
  • RGITL: A Temporal Logic Framework for Compositional Reasoning about Interleaved Programs
    G. Schellhorn, B. Tofan, G. Ernst, J. Pfähler, and W. Reif
    Annals of Mathematics and Artificial Intelligence (AMAI) Journal, vol. 71, issue 1-3, pp. 131-174, Springer
    abstract;

     
  • 2013

  • Formal Specification of an Erase Block Management Layer for Flash Memory
    Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, and Wolfgang Reif
    In Proc. of 9th International Haifa Verification Conference, Springer
    abstract; Formal Specification of an Erase Block Management Layer for Flash Memory (362 KB);

     
  • Compositional Verification of a Lock-Free Stack with RGITL
    B. Tofan, G. Schellhorn, G. Ernst, J. Pfähler, and W. Reif
    ECEASST Journal, vol. 66
    abstract;

     
  • Verification of B+ trees by integration of shape analysis and interactive theorem proving
    Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
    Software & Systems Modeling, Springer
    abstract; Verification of B+ trees by integration of shape analysis and interactive theorem proving (441 KB);

     
  • 2012

  • A Formal Model of a Virtual Filesystem Switch
    Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, 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);

     
  • Proving linearizability of multiset with local proof obligations
    O. Travkin, H. Wehrheim, G. Schellhorn
    In Proc. of Automated Verification of Critical Systems (AVoCS) , ECEASST, Vol. 53, ISSN 1863-2122, 2012
    abstract;

     
  • How to prove algorithms linearizable
    G. Schellhorn, J.Derrick, and H. Wehrheim
    In Proc. of Computer Aided Verification (CAV), Springer, LNCS, vol 7358, pp. 243-259, 2012
    abstract;

     
  • The ForMoSA Approach to Qualitative and Quantitative Model-Based Safety Analysis
    Axel Habermaier, Matthias Güdemann, Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn
    Railway Safety, Reliability, and Security: Technologies and Systems Engineering, IGI Global, 2012
    abstract; Book Website;

     
  • 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)
    abstract;

     
  • 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;

     
  • Formal Verification of a Lock-Free Stack with Hazard Pointers
    B. Tofan, G. Schellhorn, and W. Reif
    In Proc. of International Colloquium on Theoretical Aspects of Computing (ICTAC), Springer, LNCS, vol. 6916, pp. 239 - 255
    abstract; Formal Verification of a Lock-Free Stack with Hazard Pointers (195 KB);

     
  • 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; Interleaved Programs and Rely-Guarantee Reasoning with ITL (285 KB);

     
  • Local Rely-Guarantee Conditions for Linearizability and Lock-Freedom
    B.Tofan, G. Schellhorn, and W. Reif
    In Pre-Proceedings of Conference on Formal Verification of Object Oriented Software (FoVeOOS), Karlsruhe Reports in Informatics, vol. 26, pp. 342 - 359
    abstract; Local Rely-Guarantee Conditions for Linearizability and Lock-Freedom (218 KB);

     
  • Mondex: Engineering a Provable Secure Electronic Purse
    Dominik Haneberg, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
    International Journal of Software and Informatics, 5(1):159-184, 2011. http://www.ijsi.org
    abstract;

     
  • Verifying linearisability with potential linearisation points
    J. Derrick, G. Schellhorn, and H. Wehrheim
    In Proc. of Formal Methods (FM), Springer, LNCS, vol. 6664, pp. 323 - 337
    abstract;

     
  • Mechanically verified proof obligations for linearizability
    J. Derrick, G. Schellhorn, and H. Wehrheim
    Journal ACM Transactions on Programming Languages and Systems (TOPLAS) , ACM New York, Volume 33 Issue 1, Article No. 4, January 2011
    abstract;

     
  • Proving Linearizability with Temporal Logic
    S. Bäumler, G. Schellhorn, B. Tofan and W. Reif
    Journal of Formal Aspects of Computing (FAC), Springer, 23(1), pp. 91 - 112
    abstract;

     
  • 2010

  • Temporal Logic Verification of Lock-Freedom
    B. Tofan, S. Bäumler, G. Schellhorn, and W. Reif
    In Proc. of Mathematics of Program Construction (MPC), Springer, LNCS, vol. 6120, pp. 377 - 396
    abstract; Temporal Logic Verification of Lock-Freedom (211 KB);

     
  • Interactive verification of concurrent systems using symbolic execution
    S. Bäumler, M. Balser, F. Nafz, W. Reif and G. Schellhorn
    European Journal on Artificial Intelligence (AI Communications), Vol. 23, Number 2-3 / 2010, p. 285-307, DOI 10.3233/AIC-2010-0458, IOS Press
    abstract;

     
  • Automated Flaw Detection in Algebraic Specifications
    A. Dunets, G. Schellhorn, W. Reif
    Journal of Automated Reasoning (2010), JARS-D-08-00041R3, Springer
    abstract;

     
  • 2009

  • Abstract Specification of the UBIFS File System for Flash Memory
    Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
    Proceedings of FM 2009: Formal Methods, pages 190-206, Springer Berlin / Heidelberg
    abstract; http://link.springer.com/chapter/10.1007/978-3-642-05089-3_13;

     
  • 2008

  • Proving linearizability with Temporal Logic
    S. Bäumler, G. Schellhorn, M. Balser, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg, December 2008
    abstract; techreport (0 KB);

     
  • Interactive Verification of Concurrent Systems using Symbolic Execution
    Simon Bäumler, Michael Balser, Wolfgang Reif, Gerhard Schellhorn
    LPAR 2008 Workshop: The 7th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings, Vol. 418
    abstract; Paper (0 KB);

     
  • Automating Algebraic Specifications of Non-freely Generated Data Types
    Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
    Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA 2008), Springer LNCS 5311
    abstract; download PDF version (715 KB); Springerlink;

     
  • A Systematic Verification Approach for Mondex Electronic Purses using ASMs
    G. Schellhorn, H. Grandy, D. Haneberg, N. Moebius, W. Reif
    Rigorous Methods for Software Construction and Analysis - Papers Dedicated to Egon Börger on the Occasion of His 60th Birthday. Jean-Raymond Abrial, Uwe Glässer (Editors), LNCS 5115, Springer
    abstract; http://link.springer.com/chapter/10.1007/978-3-642-11447-2_7;

     
  • Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code
    H. Grandy, M. Bischof, K. Stenzel, G. Schellhorn, W. Reif
    FM 2008, 15th International Symposium on Formal Methods, Springer LNCS 5018
    abstract; SpringerLink;

     
  • Bounded Relational Analysis of Free Data Types
    Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
    Proceedings of the International Conference on Tests and Proofs (TAP 2008), Springer LNCS 4966
    abstract; download PDF version (614 KB); Talk (1105 KB); SpringerLink;

     
  • Verification of Mondex electronic purses with KIV: from transactions to a security protocol
    D. Haneberg, G. Schellhorn, H. Grandy, W. Reif
    Formal Aspects of Computing (2008) 20:41-59, Springer
    abstract; http://link.springer.com/article/10.1007%2Fs00165-007-0057-0;

     
  • 2007

  • A Modeling Framework for the Development of Provably Secure E-Commerce Applications
    Nina Moebius, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn
    Proceedings of the International Conference on Software Engineering Advances 2007, IEEE Computer Society Press **** Best Paper Award ****
    abstract; http://dx.doi.org/10.1109/ICSEA.2007.7;

     
  • Verifying Smart Card Applications: An ASM Approach.
    D. Haneberg, H. Grandy, W. Reif, G. Schellhorn
    Proceedings of the conference on integrated Formal Methods 2007 (iFM 2007), Springer LNCS 4591, Springer
    abstract; http://link.springer.com/chapter/10.1007/978-3-540-73210-5_17;

     
  • A Systematic Verification Approach for Mondex Electronic Purses using ASMs
    Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius, Wolfgang Reif
    Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Springer, LNCS
    abstract;

     
  • Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol
    Dominik Haneberg, Gerhard Schellhorn, Holger Grandy, Wolfgang Reif
    Formal Aspects of Computing, 2007
    abstract; SpringerLink;

     
  • 2006

  • Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol
    D. Haneberg, G. Schellhorn, H. Grandy, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg, December 2006
    abstract; Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol (284 KB);

     
  • The Mondex Case Study: From Specifications to Code
    H. Grandy, N. Moebius, M. Bischof, D. Haneberg, G. Schellhorn, K. Stenzel, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg, December 2006
    abstract; The Mondex Case Study: From Specifications to Code (445 KB);

     
  • A Systematic Verification Approach for Mondex Electronic Purses using ASMs
    G. Schellhorn, H. Grandy, D. Haneberg, N. Moebius, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg
    abstract; A Systematic Verification Approach for Mondex Electronic Purses using ASMs (279 KB);

     
  • The Mondex Challenge: Machine Checked Proofs for an Electronic Purse
    Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif
    Proceedings of FM 2006: Formal Methods 14th International Symposium on Formal Methods Hamilton, Canada, August 21-27, 2006, Springer LNCS 4085, Springer
    abstract; http://link.springer.com/chapter/10.1007/11813040_2;

     
  • The User Interface of the KIV Verification System - A System Description
    Dominik Haneberg, Simon Bäumler, Michael Balser, Holger Grandy, Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn, Jonathan Schmitt, Kurt Stenzel
    ENTCS special issue (to appear), Elsevier
    abstract;

     
  • The Mondex Challenge: Machine Checked Proofs for an Electronic Purse
    G. Schellhorn, H. Grandy, D. Haneberg, W. Reif
    Technical Report, Institute of Computer Science, University of Augsburg
    abstract; The Mondex Challenge: Machine Checked Proofs for an Electronic Purse (0 KB);

     
  • Formal Fault Tree Analysis - Practical Experiences
    Frank Ortmeier, Gerhard Schellhorn
    In proceedings of AVOCS 2006, Elsevier

     
  • 2005

  • ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison
    G. Schellhorn
    Theoretical Computer Science, Vol. 336, No. 2-3, pp. 403-436
    abstract; download pdf draft (266 KB); download postscript draft (514 KB);

     
  • The User Interface of the KIV Verification System - A System Description
    Dominik Haneberg, Simon Bäumler, Michael Balser, Holger Grandy, Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn, Jonathan Schmitt, Kurt Stenzel
    Proceedings of the User Interfaces for Theorem Provers Workshop (UITP 2005)
    download pdf version (810 KB);

     
  • Verifying Security Protocols: An ASM Approach.
    Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn
    Proceedings of the 12th International Workshop on Abstract State Machines (ASM 2005)
    download pdf version (193 KB);

     
  • Formal Safety Analysis of a Radio-Based Railroad Crossing Using Deductive Cause-Consequence Analysis (DCCA)
    F. Ortmeier, W. Reif, and G. Schellhorn
    Proceedings 5th European Dependable Computing Conference, Hungary, April 20-22, 2005, LNCS 3463, Springer
    download pdf version (150 KB); download postscript version (417 KB);

     
  • Deductive Cause-Consequence Analysis (DCCA)
    F. Ortmeier, W. Reif, and G. Schellhorn
    Proceedings of the 16th IFAC World Congress Elsevier Jun-2006 ISBN: 978-0-08-045108-4 and 0-08-045108-X
    download pdf version (104 KB); download postscript version (112 KB);

     
  • 2004

  • Combining Formal Methods and Safety Analysis - the ForMoSA Approach
    F. Ortmeier, A. Thums, G. Schellhorn, and W. Reif
    H. Ehrig, Integration of Software Specification Techniques for Applications in Engineering. LNCS 3147, Springer
    download pdf version (233 KB);

     
  • Safety Optimization of a Radio-Based Railroad Crossing
    Frank Ortmeier, Gerhard Schellhorn, Wolfgang Reif
    E. Schnieder, and G. Tarnai, editors: FORMS/FORMAT 2004. Formal Methods for Automation and Safety in Railway and Automotive Systems, Proceedings of Symposium FORMS/FORMAT 2004, Braunschweig, Germany, 2nd and 3rd December 2004. ISBN 3-9803363-8-7.
    download pdf version (152 KB);

     
  • Interactive Verification of Statecharts
    A. Thums, G. Schellhorn, F. Ortmeier, and W. Reif
    H. Ehrig, Integration of Software Specification Techniques for Applications in Engineering. LNCS 3147, Springer
    download pdf version (393 KB); download postscript version (120 KB);

     
  • Introduction to Subject Area "Verification"
    F. Ortmeier, W. Reif, and G. Schellhorn
    IH. Ehrig, Integration of Software Specification Techniques for Applications in Engineering. LNCS 3147, Springer
    download pdf version (56 KB); download postscript version (77 KB);

     
  • Integrated Formal Methods for Safety Analysis of Train Systems
    W. Reif, F. Ortmeier, A. Thums, G. Schellhorn
    Proceedings of the 18th IFIP World Computer Congress, TC Building the Information Society. Kluwer 2004, ISBN 1-4020-8156-1
    download pdf version (71 KB); download postscript version (33 KB);

     
  • 2003

  • Safety Analysis of the Height Control System for the Elbtunnel
    Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering and Helmut Trappschuh.
    Journal of Reliability Engineering and System Safety, 81(3), Elsevier
    download pdf version (174 KB); download postscript version (191 KB);

     
  • Model Checking FTA
    A. Thums and G. Schellhorn
    K. Araki and S. Gnesi and D. Mandrioli, FME Formal Methods, Pages 739-757, LNCS 2805, Springer
    download pdf version (245 KB); download postscript version (1378 KB);

     
  • 2002

  • Verified Formal Security Models for Multiapplicative Smart Cards
    G. Schellhorn, W. Reif, A. Schairer, P. Karger, V. Austel, D. Toll
    Journal for Computer Security, vol. 10, no. 4, p. 339 - 367, 2002
    abstract; download pdf version (228 KB); download ps version (263 KB);

     
  • Formal Fault Tree Semantics
    G. Schellhorn, A. Thums, and W. Reif
    Proceedings of The Sixth World Conference on Integrated Design & Process Technology
    download pdf version (99 KB); download postscript version (71 KB);

     
  • Safety Analysis of the Height Control System for the Elbtunnel
    Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering and Helmut Trappschuh
    Proceedings SAFECOMP 2002, Springer Berlin Heidelberg 2002
    download pdf version (178 KB); download postscript version (190 KB); LNCS 2434;

     
  • Verifying Concurrent Systems with Symbolic Execution
    M. Balser, C. Duelli, W. Reif, and G. Schellhorn
    Journal of Logic and Computation 12
    download pdf version (135 KB); download postscript version (195 KB);

     
  • Formal Safety Analysis in Transportation Control
    Andreas Thums, Gerhard Schellhorn
    Proceedings of the Workshop on Software specification for safety relevant transportation control tasks
    download pdf version (102 KB); download postscript version (61 KB);

     
  • 2001

  • Integration formaler Spezifikation und Sicherheitsanalyse
    Wolfgang Reif, Gerhard Schellhorn, Andreas Thums
    Technical report 2001-6, Institut für Informatik, Universität Augsburg
    abstract; download pdf version (300 KB); download postscript version (260 KB);

     
  • Verification of ASM Refinements Using Generalized Forward Simulation
    G. Schellhorn
    download pdf version (206 KB); download postscript version (186 KB); available via the J.UCS home page (in volume 7, issue 11);

     
  • Flaw Detection in Formal Specifications
    W. Reif, G. Schellhorn, and A. Thums
    Proceedings of IJCAR 2001 - Automated Reasoning, Springer Berlin Heidelberg 2001
    download postscript version (194 KB); LNAI 2083;

     
  • 2000

  • Verifying Concurrent Systems with Symbolic Execution
    M. Balser, C. Duelli, W. Reif, G. Schellhorn
    accepted for ICTL 2000

     
  • Verification of a Formal Security Model for Multiapplicative Smart Cards
    G. Schellhorn, W. Reif, A. Schairer, P. Karger, V. Austel, D.Toll
    Proc. of the 6th European Symposium on Research in Computer Security (ESORICS), Springer LNCS 1895
    download pdf version (176 KB); download postscript version (152 KB);

     
  • Formale Sicherheitsanalyse einer funkbasierten Bahnübergangssteuerung
    W. Reif, G. Schellhorn, and A. Thums
    Fortschritt-Berichte VDI, Reihe 12Forms 2000 -- Formale Techniken für die Eisenbahnsicherung

     
  • Do You Trust Your Model Checker?
    W. Reif, J. Ruf, G. Schellhorn, T. Vollmer
    Warren A. Hunt, Jr. and Steven D. Johnson, editor, FMCAD 2000: Formal methods in Comuter Aided Design, Springer LNCS 1954
    download pdf version (247 KB); download postscript version (83 KB);

     
  • Formal System Development with KIV
    M. Balser, W. Reif, G. Schellhorn, K. Stenzel, and A. Thums
    T. Maibaum, editor, Fundamental Approaches to Software Engineering, Springer LNCS 1783
    download pdf version (86 KB); download postscript version (35 KB);

     
  • Safety Analysis of a Radio-Based Crossing Control System Using Formal Methods
    W. Reif, G. Schellhorn, and A. Thums
    download postscript version (71 KB);

     
  • 1999

  • KIV 3.0 for Provably Correct Systems
    M. Balser, W. Reif, G. Schellhorn, and K. Stenzel
    Current Trends in Applied Formal Methods, Springer LNCS 1641
    download postscript version (102 KB);

     
  • VSE: Controlling the Complexity in Formal Software Developments
    D. Hutter, H. Mantel, G. Rock, W. Stephan, A. Wolpers, M. Balser, W. Reif, G. Schellhorn, and K. Stenzel
    Current Trends in Applied Formal Methods, Springer LNCS 1641

     
  • Verifikation abstrakter Zustandsmaschinen (Verification of Abstract State Machines)
    G. Schellhorn
    PhD thesis, Universität Ulm, Fakultät für Informatik
    download english pdf version (1133 KB); download english postscript version (438 KB); download german pdf version (1199 KB); download german postscript version (491 KB);

     
  • 1998

  • Theorems from Compiler Verification: A Problem Set for Automated Theorem Provers
    G. Schellhorn and W. Reif
    Ulmer Informatik-Berichte 98-13
    download postscript version (252 KB);

     
  • Integrating Automated and Interactive Theorem Proving
    W. Ahrendt, B. Beckert, R. Hähnle, W. Menzel, W.Reif, G. Schellhorn, and P. Schmitt
    W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications. Volume II: Systems and Implementation Techniques, Chapter 1: Interactive Theorem Proving, Kluwer Academic Publishers
    download postscript version (79 KB);

     
  • Proving Properties of Directed Graphs: A Problem Set for Automated Theorem Provers
    G. Schellhorn
    Ulmer Informatik-Berichte 98-12
    download postscript version (76 KB);

     
  • Theorem Proving in Large Theories
    W. Reif and G. Schellhorn
    W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications. Volume III: Applications, Chapter 2, Kluwer Academic Publishers
    download postscript version (74 KB);

     
  • The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV
    G. Schellhorn and W. Ahrendt
    W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications. Volume III: Applications, Chapter 3: Automated Theorem Proving in Software Engineering, Kluwer Academic Publishers
    download postscript version (139 KB);

     
  • Structured specifications and interactive proofs with KIV
    W. Reif, G. Schellhorn, K. Stenzel, and M. Balser
    W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications, Kluwer Academic Publishers
    download postscript version (158 KB);

     
  • 1997

  • Reasoning about Abstract State Machines: The WAM Case Study
    G. Schellhorn and W. Ahrendt
    Journal of Universal Computer Science (J.UCS), 3(4):377-413
    abstract;

     
  • Proving System Correctness with KIV 3.0
    W. Reif, G. Schellhorn, and K. Stenzel
    14th International Conference on Automated Deduction. Proceedings, Springer LNCS 1249

     
  • Proving Properties of Finite Enumerations: A Problem Set for Automated Theorem Provers
    G. Schellhorn and W. Reif
    Ulmer Informatik-Berichte 97-12
    download postscript version (71 KB);

     
  • Proving System Correctness with KIV
    W. Reif, G. Schellhorn, and K. Stenzel
    M. Bidoit and M. Dauchet, editors, TAPSOFT'97: Theory and Practice of Software Development. Proceedings, Springer LNCS 1214

     
  • 1996

  • LEX: a case study in development and validation of formal specifications
    A. Heckler, R. Hettler, H. Hußmann, J. Loeckx, W. Reif, G. Schellhorn, and K. Stenzel
    Technical Report A/06/96

     
  • Verification of a Prolog Compiler - First Steps with KIV
    G. Schellhorn and W. Ahrendt
    Ulmer Informatik-Berichte 96-05
    download postscript version (449 KB);

     
  • Kiv 3.0: Concepts and applications
    W. Reif, G. Schellhorn, and K. Stenzel
    Technical report
    download postscript version (288 KB);

     
  • 1995

  • Interactive Correctness Proofs for Software Modules Using KIV
    W. Reif, G. Schellhorn, and K. Stenzel
    COMPASS'95 - Tenth Annual Conference on Computer Assurance, Gaithersburg (MD), IEEE press
    abstract; download postscript version (80 KB);

     
  • Tactics in KIV
    W. Reif, G. Schellhorn, and K. Stenzel
    Journal on Information Processing and Cybernetics, 30

     
  • Three Selected Case Studies in Verification
    T. Fuchß, W. Reif, G. Schellhorn, and K. Stenzel
    M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software - Final Report, Springer LNCS 1009
    download postscript version (66 KB);

     
  • 1994

  • Specification and Verification of Distributed Technical Systems with Central Control
    G. Schellhorn and A. Burandt
    C. Lewerentz and T. Lindner, editors, Case Study "Production Cell", A Comparative Study in Formal Software Development. FZI Publication 1/94

     
  • Specification and Verification of Distributed Technical Systems with Central Control
    G. Schellhorn and A. Burandt
    C. Lewerentz and T. Lindner, editors, Formal Development of Reactive Systems, Springer LNCS 891

     
  • Specification and Verification of Distributed Technical Systems with Central Control
    G. Schellhorn
    Technical report

     
  • Tactics in KIV
    W. Reif, G. Schellhorn, and K. Stenzel
    J. Kunze and H. Stoyan, editors, Workshop-Proceedings 18. Deutsche Jahrestagung für Künstliche Intelligenz, KI 94, Gesellschaft für Informatik e. V.