Dr. Gerhard Schellhorn

Senior Researcher
Institute for Software & Systems Engineering
Phone: +49 821 598 2124
Email:
Room: 3016 (N)
Address: Universitätsstraße 6a, 86159 Augsburg

Research

Research topics:

  • Logic Calculi, Algebraic Specification, Program Logics, Abstract State Machines
  • Modular specification of concurrent systems with temporal logic and IO-Automata
  • Interactive Verification, Proof Automation
  • Refinement: Data Refinement, ASM Refinement, Linearizability, Opacity

I am involved in the following research areas and projects:

VeriCAS (finished): Verification of lock-free algorithms

 

Courses

 

  • Software Engineering
  • Compiler Construction
  • Introduction to Robotics
  • Formal Methods in Software Engineering

 

 

Publications

2024 | 2023 | 2022 | 2021 | 2020 | 2019 | 2018 | 2017 | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 | 1995 | 1994

2024

Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn and Heike Wehrheim. 2024. A fully verified persistency library. DOI: 10.1007/978-3-031-50521-8_2
PDF | BibTeX | RIS | DOI

2023

Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif. 2023. Refinement and separation: modular verification of wandering trees. DOI: 10.1007/978-3-031-47705-8_12
PDF | BibTeX | RIS | DOI

Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich and Wolfgang Reif. 2023. Separating separation logic – modular verification of red-black trees. DOI: 10.1007/978-3-031-25803-9_8
PDF | BibTeX | RIS | DOI

Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif. 2023. Thread-local, step-local proof obligations for refinement of state-based concurrent systems. DOI: 10.1007/978-3-031-33163-3_6
PDF | BibTeX | RIS | DOI

2022

Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich and Wolfgang Reif. 2022. Software & system verification with KIV. DOI: 10.1007/978-3-031-08166-8_20
PDF | BibTeX | RIS | DOI

Stefan Bodenmüller, Gerhard Schellhorn and Wolfgang Reif. 2022. Verification of crashsafe caching in a virtual file system switch. DOI: 10.1145/3523737
PDF | BibTeX | RIS | DOI

Brijesh Dongol, Gerhard Schellhorn and Heike Wehrheim. 2022. Weak progressive forward simulation is necessary and sufficient for strong observational refinement. DOI: 10.4230/LIPIcs.CONCUR.2022.31
PDF | BibTeX | RIS | DOI

2021

Stefan Bodenmüller, Gerhard Schellhorn, Martin Bitterlich and Wolfgang Reif. 2021. Flashix: modular verification of a concurrent and crash-safe flash file system. DOI: 10.1007/978-3-030-76020-5_14
PDF | BibTeX | RIS | DOI

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn and Heike Wehrheim. 2021. Verifying correctness of persistent concurrent data structures: a sound and complete method. DOI: 10.1007/s00165-021-00541-8
PDF | BibTeX | RIS | DOI

2020

Gerhard Schellhorn, Stefan Bodenmüller, Jörg Pfähler and Wolfgang Reif. 2020. Adding concurrency to a sequential refinement tower. DOI: 10.1007/978-3-030-48077-6_2
PDF | BibTeX | RIS | DOI

Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn and Heike Wehrheim. 2020. Defining and verifying durable opacity: correctness for persistent software transactional memory. DOI: 10.1007/978-3-030-50086-3_3
BibTeX | RIS | DOI

Stefan Bodenmüller, Gerhard Schellhorn and Wolfgang Reif. 2020. Modular integration of crashsafe caching into a verified virtual file system switch. DOI: 10.1007/978-3-030-63461-2_12
PDF | BibTeX | RIS | DOI

2019

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn and Heike Wehrheim. 2019. Verifying correctness of persistent concurrent data structures. DOI: 10.1007/978-3-030-30942-8_12
BibTeX | RIS | DOI

2018

Gerhard Schellhorn, Monika Wedel, Oleg Travkin, Jürgen König and Heike Wehrheim. 2018. FastLane is opaque – a case study in mechanized proofs of opacity. DOI: 10.1007/978-3-319-92970-5_7
BibTeX | RIS | DOI

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller and Wolfgang Reif. 2018. Symbolic execution for a clash-free subset of ASMs. DOI: 10.1016/j.scico.2017.08.014
PDF | BibTeX | RIS | DOI

2017

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin and Heike Wehrheim. 2017. Mechanized proofs of opacity: a comparison of two techniques. DOI: 10.1007/s00165-017-0433-3
PDF | BibTeX | RIS | DOI

Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn and Wolfgang Reif. 2017. Modular verification of order-preserving write-back caches. DOI: 10.1007/978-3-319-66845-1_25
PDF | BibTeX | RIS | DOI

2016

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler and Wolfgang Reif. 2016. A relational encoding for a clash-free subset of ASMs. DOI: 10.1007/978-3-319-33600-8_15
BibTeX | RIS | DOI

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn and Wolfgang Reif. 2016. Inside a verified flash file system: transactions and garbage collection. DOI: 10.1007/978-3-319-29613-5_5
BibTeX | RIS | DOI

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn and Wolfgang Reif. 2016. Modular, crash-safe refinement for ASMs with submachines. DOI: 10.1016/j.scico.2016.04.009
BibTeX | RIS | DOI

2015

Marian Borek, Kuzman Katkalov, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 2015. Integrating a model-driven approach and formal verification for the development of secure service applications. DOI: 10.1007/978-3-319-17112-8_3
BibTeX | RIS | DOI

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg and Wolfgang Reif. 2015. KIV: overview and VerifyThis competition. DOI: 10.1007/s10009-014-0308-3
BibTeX | RIS | DOI

Gidon Ernst, Gerhard Schellhorn and Wolfgang Reif. 2015. Verification of B+ trees by integration of shape analysis and interactive theorem proving. DOI: 10.1007/s10270-013-0320-1
BibTeX | RIS | DOI

John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin and Heike Wehrheim. 2015. Verifying opacity of a transactional Mutex lock. DOI: 10.1007/978-3-319-19249-9_11
BibTeX | RIS | DOI

2014

Bogdan Tofan, Gerhard Schellhorn and Wolfgang Reif. 2014. A compositional proof method for linearizability applied to a wait-free multiset. DOI: 10.1007/978-3-319-10181-1_22
BibTeX | RIS | DOI

Gerhard Schellhorn, John Derrick and Heike Wehrheim. 2014. A sound and complete proof technique for linearizability of concurrent data structures. DOI: 10.1145/2629496
BibTeX | RIS | DOI

Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg and Wolfgang Reif. 2014. Crash-safe refinement for a verified flash file system.
PDF | BibTeX | RIS

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg and Wolfgang Reif. 2014. Development of a verified flash file system. DOI: 10.1007/978-3-662-43652-3_2
BibTeX | RIS | DOI

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn and Wolfgang Reif. 2014. Modular refinement for submachines of ASMs. DOI: 10.1007/978-3-662-43652-3_16
BibTeX | RIS | DOI

John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin and Heike Wehrheim. 2014. Quiescent consistency: defining and verifying relaxed linearizability. DOI: 10.1007/978-3-319-06410-9_15
BibTeX | RIS | DOI

Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Jörg Pfähler and Wolfgang Reif. 2014. RGITL: a temporal logic framework for compositional reasoning about interleaved programs. DOI: 10.1007/s10472-013-9389-z
BibTeX | RIS | DOI

Bogdan Tofan, Oleg Travkin, Gerhard Schellhorn and Heike Wehrheim. 2014. Two approaches for proving linearizability of multiset. DOI: 10.1016/j.scico.2014.04.001
BibTeX | RIS | DOI

Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler and Wolfgang Reif. 2014. Verification of a virtual filesystem switch. DOI: 10.1007/978-3-642-54108-7_13
BibTeX | RIS | DOI

2013

Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler and Wolfgang Reif. 2013. Compositional verification of a lock-free stack with RGITL. DOI: 10.14279/tuj.eceasst.66.885
PDF | BibTeX | RIS | DOI

Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg and Wolfgang Reif. 2013. Formal specification of an erase block management layer for flash memory. DOI: 10.1007/978-3-319-03077-7_15
BibTeX | RIS | DOI

2012

Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler and Wolfgang Reif. 2012. A formal model of a virtual filesystem switch. DOI: 10.4204/eptcs.102.5
BibTeX | RIS | DOI

Gerhard Schellhorn, Heike Wehrheim and John Derrick. 2012. How to prove algorithms linearisable. DOI: 10.1007/978-3-642-31424-7_21
BibTeX | RIS | DOI

Oleg Travkin, Heike Wehrheim and Gerhard Schellhorn. 2012. Proving linearizability of multiset with local proof obligations. DOI: 10.14279/tuj.eceasst.53.795
PDF | BibTeX | RIS | DOI | URL

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. 2012. The COST IC0701 verification competition 2011. DOI: 10.1007/978-3-642-31762-0_2
BibTeX | RIS | DOI

Alex Habermaier, Matthias Güdemann, Frank Ortmeier, Wolfgang Reif and Gerhard Schellhorn. 2012. The ForMoSA approach to qualitative and quantitative model-based safety analysis.
BibTeX | RIS

2011

Gerhard Schellhorn. 2011. Completeness of fair ASM refinement. DOI: 10.1016/j.scico.2009.10.004
BibTeX | RIS | DOI

Bogdan Tofan, Gerhard Schellhorn and Wolfgang Reif. 2011. Formal verification of a lock-free stack with hazard pointers. DOI: 10.1007/978-3-642-23283-1_16
BibTeX | RIS | DOI

Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst and Wolfgang Reif. 2011. Interleaved programs and rely-guarantee reasoning with ITL. DOI: 10.1109/time.2011.12
BibTeX | RIS | DOI

Bogdan Tofan, Gerhard Schellhorn and Wolfgang Reif. 2011. Local rely-guarantee conditions for linearizability and lock-freedom.
PDF | BibTeX | RIS | URL

John Derrick, Gerhard Schellhorn and Heike Wehrheim. 2011. Mechanically verified proof obligations for linearizability. DOI: 10.1145/1889997.1890001
BibTeX | RIS | DOI

Wolfgang Reif, Dominik Haneberg, Nina Moebius, Gerhard Schellhorn and Kurt Stenzel. 2011. Mondex: engineering a provable secure electronic purse.
BibTeX | RIS | URL

Simon Bäumler, Gerhard Schellhorn, Bogdan Tofan and Wolfgang Reif. 2011. Proving linearizability with temporal logic. DOI: 10.1007/s00165-009-0130-y
BibTeX | RIS | DOI

Eerke A. Boiten, John Derrick and Gerhard Schellhorn. 2011. Selected papers of the Refinement Workshop Turku (2008). DOI: 10.1016/j.scico.2011.03.003
BibTeX | RIS | DOI

Maximilian Junker, Dominik Haneberg, Gerhard Schellhorn, Wolfgang Reif and Gidon Ernst. 2011. Simulating a flash file system with CoreASM and Eclipse.
BibTeX | RIS | URL

Gidon Ernst, Gerhard Schellhorn and Wolfgang Reif. 2011. Verification of B+ trees: an experiment combining shape analysis and interactive theorem proving. DOI: 10.1007/978-3-642-24690-6_14
BibTeX | RIS | DOI

Bogdan Tofan, Gerhard Schellhorn and Wolfgang Reif. 2011. Verifying a stack with hazard pointers in temporal logic.
PDF | BibTeX | RIS

John Derrick, Gerhard Schellhorn and Heike Wehrheim. 2011. Verifying linearisability with potential linearisation points. DOI: 10.1007/978-3-642-21437-0_25
BibTeX | RIS | DOI

2010

Andriy Dunets, Gerhard Schellhorn and Wolfgang Reif. 2010. Automated flaw detection in algebraic specifications. DOI: 10.1007/s10817-010-9166-1
BibTeX | RIS | DOI

Bogdan Tofan, Gerhard Schellhorn, Simon Bäumler and Wolfgang Reif. 2010. Embedding rely-guarantee reasoning in temporal logic.
PDF | BibTeX | RIS

Simon Bäumler, Michael Balser, Florian Nafz, Wolfgang Reif and Gerhard Schellhorn. 2010. Interactive verification of concurrent systems using symbolic execution. DOI: 10.3233/AIC-2010-0458
BibTeX | RIS | DOI

Bogdan Tofan, Simon Bäumler, Gerhard Schellhorn and Wolfgang Reif. 2010. Temporal logic verification of lock-freedom. DOI: 10.1007/978-3-642-13321-3_21
BibTeX | RIS | DOI

2009

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius and Wolfgang Reif. 2009. A systematic verification approach for Mondex electronic purses using ASMs. DOI: 10.1007/978-3-642-11447-2_7
BibTeX | RIS | DOI

Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg and Wolfgang Reif. 2009. Abstract specification of the UBIFS file system for flash memory. DOI: 10.1007/978-3-642-05089-3_13
PDF | BibTeX | RIS | DOI

Bogdan Tofan, Simon Bäumler, Gerhard Schellhorn and Wolfgang Reif. 2009. Verifying linearizability and lock-freedom with temporal logic.
PDF | BibTeX | RIS

2008

Gerhard Schellhorn and Richard Banach. 2008. A concept-driven construction of the Mondex protocol using three refinements. DOI: 10.1007/978-3-540-87603-8_6
BibTeX | RIS | DOI

Gerhard Schellhorn. 2008. ASM refinement preserving invariants. DOI: 10.3217/jucs-014-12-1929
PDF | BibTeX | RIS | DOI

Andriy Dunets, Gerhard Schellhorn and Wolfgang Reif. 2008. Automating algebraic specifications of non-freely generated data types. DOI: 10.1007/978-3-540-88387-6_12
BibTeX | RIS | DOI

Andriy Dunets, Gerhard Schellhorn and Wolfgang Reif. 2008. Bounded relational analysis of free data types. DOI: 10.1007/978-3-540-79124-9_8
BibTeX | RIS | DOI

Simon Bäumler, Michael Balser, Wolfgang Reif and Gerhard Schellhorn. 2008. Interactive verification of concurrent systems using symbolic execution.
BibTeX | RIS | URL

Richard Banach and Gerhard Schellhorn. 2008. On the refinement of atomic actions. DOI: 10.1016/j.entcs.2008.02.013
PDF | BibTeX | RIS | DOI

Simon Bäumler, Michael Balser, Wolfgang Reif and Gerhard Schellhorn. 2008. Proving linearizability with temporal logic.
PDF | BibTeX | RIS

Frank Ortmeier, Alwin Hoffmann, Ulrich Huggenberger, Wolfgang Reif, Dominik Haneberg, Gerhard Schellhorn and Christian Tarragona. 2008. Simulations-basierte Programmierung von Industrierobotern.
PDF | BibTeX | RIS | URL

Holger Grandy, Markus Bischof, Kurt Stenzel, Gerhard Schellhorn and Wolfgang Reif. 2008. Verification of Mondex electronic purses with KIV: from a security protocol to verified code. DOI: 10.1007/978-3-540-68237-0_13
BibTeX | RIS | DOI

Dominik Haneberg, Gerhard Schellhorn, Holger Grandy and Wolfgang Reif. 2008. Verification of Mondex electronic purses with KIV: from transactions to a security protocol. DOI: 10.1007/s00165-007-0057-0
BibTeX | RIS | DOI

2007

Nina Moebius, Dominik Haneberg, Wolfgang Reif and Gerhard Schellhorn. 2007. A modeling framework for the development of Provably Secure E-Commerce applications. DOI: 10.1109/icsea.2007.7
BibTeX | RIS | DOI

Dominik Haneberg, Holger Grandy, Wolfgang Reif and Gerhard Schellhorn. 2007. Verifying smart card applications: an ASM approach. DOI: 10.1007/978-3-540-73210-5_17
BibTeX | RIS | DOI

2006

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius and Wolfgang Reif. 2006. A systematic verification approach for Mondex electronic purses using ASMs.
PDF | BibTeX | RIS

Frank Ortmeier and Gerhard Schellhorn. 2006. Formal fault tree analysis: practical experiences.
BibTeX | RIS

Holger Grandy, Nina Moebius, Markus Bischof, Dominik Haneberg, Gerhard Schellhorn, Kurt Stenzel and Wolfgang Reif. 2006. The Mondex case study: from specifications to code.
PDF | BibTeX | RIS

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg and Wolfgang Reif. 2006. The Mondex challenge: machine checked proofs for an electronic purse.
PDF | BibTeX | RIS

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg and Wolfgang Reif. 2006. The mondex challenge: machine checked proofs for an electronic purse. DOI: 10.1007/11813040_2
BibTeX | RIS | DOI

Dominik Haneberg, Gerhard Schellhorn, Holger Grandy and Wolfgang Reif. 2006. Verification of Mondex electronic purses with KIV: from transactions to a security protocol.
PDF | BibTeX | RIS

Dominik Haneberg, Holger Grandy, Wolfgang Reif and Gerhard Schellhorn. 2006. Verifying smart card applications: an ASM approach.
PDF | BibTeX | RIS

2005

Gerhard Schellhorn. 2005. ASM refinement and generalizations of forward simulation in data refinement: a comparison. DOI: 10.1016/j.tcs.2004.11.013
BibTeX | RIS | DOI

Frank Ortmeier, Wolfgang Reif and Gerhard Schellhorn. 2005. Deductive Cause-Consequence Analysis (DCCA). DOI: 10.3182/20050703-6-CZ-1902.01435
BibTeX | RIS | DOI

Frank Ortmeier, Wolfgang Reif and Gerhard Schellhorn. 2005. Formal safety analysis of a radio-based railroad crossing using Deductive Cause-Consequence Analysis (DCCA). DOI: 10.1007/11408901_15
BibTeX | RIS | DOI

Dominik Haneberg, Simon Bäumler, Michael Balser, Holger Grandy, Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn, Jonathan Schmitt and Kurt Stenzel. 2005. The user interface of the KIV verification system: a system description.
BibTeX | RIS

Dominik Haneberg, H. Grandy, Wolfgang Reif and Gerhard Schellhorn. 2005. Verifying security protocols: an ASM approach.
BibTeX | RIS

2004

Frank Ortmeier, Andreas Thums, Gerhard Schellhorn and Wolfgang Reif. 2004. Combining formal methods and safety analysis - the ForMoSA approach. DOI: 10.1007/978-3-540-27863-4_26
BibTeX | RIS | DOI

Wolfgang Reif, Frank Ortmeier, Andreas Thums and Gerhard Schellhorn. 2004. Integrated formal methods for safety analysis of train systems.
BibTeX | RIS

Andreas Thums, Gerhard Schellhorn, Frank Ortmeier and Wolfgang Reif. 2004. Interactive verification of statecharts. DOI: 10.1007/978-3-540-27863-4_20
BibTeX | RIS | DOI

Frank Ortmeier, Wolfgang Reif and Gerhard Schellhorn. 2004. Introduction to subject area "Verification". DOI: 10.1007/978-3-540-27863-4_23
BibTeX | RIS | DOI

Frank Ortmeier, Gerhard Schellhorn and Wolfgang Reif. 2004. Safety optimization of a radio-based railroad crossing.
BibTeX | RIS

2003

Andreas Thums and Gerhard Schellhorn. 2003. Formal safety analysis in transportation control.
BibTeX | RIS

Rudolf Berghammer, Dominik Haneberg, Wolfgang Reif and Gerhard Schellhorn. 2003. J.UCS Special Issue on Tools for System Design and Verification.
PDF | BibTeX | RIS | URL

Andreas Thums and Gerhard Schellhorn. 2003. Model checking FTA. DOI: 10.1007/978-3-540-45236-2_40
BibTeX | RIS | DOI

Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering and Helmut Trappschuh. 2003. Safety analysis of the height control system for the Elbtunnel. DOI: 10.1016/S0951-8320(03)00090-5
BibTeX | RIS | DOI

2002

Gerhard Schellhorn, Andreas Thums and Wolfgang Reif. 2002. Formal fault tree semantics.
BibTeX | RIS

Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering and Helmut Trappschuh. 2002. Safety analysis of the height control system for the Elbtunnel. DOI: 10.1007/3-540-45732-1_29
BibTeX | RIS | DOI

Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul Karger, Vernon Austel and David Toll. 2002. Verified formal security models for multiapplicative smart cards. DOI: 10.3233/JCS-2002-10403
BibTeX | RIS | DOI

Michael Balser, Christoph Duelli, Wolfgang Reif and Gerhard Schellhorn. 2002. Verifying concurrent systems with symbolic execution. DOI: 10.1093/logcom/12.4.549
BibTeX | RIS | DOI

2001

Wolfgang Reif, Gerhard Schellhorn and Andreas Thums. 2001. Flaw detection in formal specifications. DOI: 10.1007/3-540-45744-5_52
BibTeX | RIS | DOI

Wolfgang Reif, Gerhard Schellhorn and Andreas Thums. 2001. Integration formaler Spezifikation und Sicherheitsanalyse.
PDF | BibTeX | RIS

Gerhard Schellhorn. 2001. Verification of ASM refinements using generalized forward simulation. DOI: 10.3217/jucs-007-11-0952
BibTeX | RIS | DOI | URL

2000

Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn and Tobias Vollmer. 2000. Do you trust your model checker?. DOI: 10.1007/3-540-40922-x_12
BibTeX | RIS | DOI

Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel and Andreas Thums. 2000. Formal system development with KIV. DOI: 10.1007/3-540-46428-X_25
BibTeX | RIS | DOI

Wolfgang Reif, Gerhard Schellhorn and Andreas Thums. 2000. Formale Sicherheitsanalyse einer funkbasierten Bahnübergangssteuerung.
BibTeX | RIS

Wolfgang Reif, Gerhard Schellhorn and Andreas Thums. 2000. Safety analysis of a radio-based crossing control system using formal methods. DOI: 10.1016/s1474-6670(17)38156-9
BibTeX | RIS | DOI

Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul Karger, Vernon Austel and David Toll. 2000. Verification of a formal security model for multiapplicative smart cards. DOI: 10.1007/10722599_2
BibTeX | RIS | DOI

Michael Balser, C. Duelli, Wolfgang Reif and Gerhard Schellhorn. 2000. Verifying concurrent systems with symbolic execution.
BibTeX | RIS

1999

Michael Balser, Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1999. KIV 3.0 for provably correct systems. DOI: 10.1007/3-540-48257-1_23
BibTeX | RIS | DOI

Dieter Hutter, Heiko Mantel, Georg Rock, Werner Stephan, Andreas Wolpers, Michael Balser, Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1999. VSE: controlling the complexity in formal software developments. DOI: 10.1007/3-540-48257-1_26
BibTeX | RIS | DOI

Gerhard Schellhorn. 1999. Verification of abstract state machines.
PDF | BibTeX | RIS

Gerhard Schellhorn. 1999. Verifikation abstrakter Zustandsmaschinen.
PDF | BibTeX | RIS

1998

Wolfgang Ahrendt, Bernhard Beckert, R. Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn and Peter H. Schmitt. 1998. Integrating automated and interactive theorem proving. DOI: 10.1007/978-94-017-0435-9_4
BibTeX | RIS | DOI

Gerhard Schellhorn. 1998. Proving properties of directed graphs: a problem set for automated theorem provers.
BibTeX | RIS | URL | URL

Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel and M. Balser. 1998. Structured specifications and interactive proofs with KIV. DOI: 10.1007/978-94-017-0435-9_1
BibTeX | RIS | DOI

Gerhard Schellhorn and W. Ahrendt. 1998. The WAM case study: verifying compiler correctness for prolog with KIV.
BibTeX | RIS

Wolfgang Reif and Gerhard Schellhorn. 1998. Theorem proving in large theories. DOI: 10.1007/978-94-017-0437-3_9
BibTeX | RIS | DOI

Gerhard Schellhorn and Wolfgang Reif. 1998. Theorems from compiler verification: a problem set for automated theorem provers.
BibTeX | RIS

1997

Gerhard Schellhorn and Wolfgang Reif. 1997. Proving properties of finite enumerations: a problem set for automated theorem provers.
BibTeX | RIS

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1997. Proving system correctness with KIV. DOI: 10.1007/bfb0030647
BibTeX | RIS | DOI

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1997. Proving system correctness with KIV 3.0. DOI: 10.1007/3-540-63104-6_10
BibTeX | RIS | DOI

Gerhard Schellhorn and W. Ahrendt. 1997. Reasoning about abstract state machines: the WAM case study. DOI: 10.3217/jucs-003-04-0377
BibTeX | RIS | DOI | URL

1996

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1996. KIV 3.0: concepts and applications.
BibTeX | RIS

Andreas Ramses Heckler, Rudolf Hettler, Heinrich Hussmann, Jacques Loeckx, Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1996. LEX: a case study in development and validation of formal specifications. DOI: 10.22028/D291-25803
BibTeX | RIS | DOI

Gerhard Schellhorn and W. Ahrendt. 1996. Verification of a prolog compiler - first steps with KIV.
BibTeX | RIS | URL

1995

Peter Pepper, Martin Wirsing, Ralph Betschko, Manfred Broy, Sabine Dick, Klaus Didrich, Joachim Faulhaber, Wolfgang Grieskamp, Heinrich Hußmann, Michael Mehlich, Wolfgang Reif, Martin Beyer, Stefan Gastinger, Maritta Heisel, Friedrich von Henke, Liu Junbo, Bernd Krieg-Brückner, Thomas Santen, Gerhard Schellhorn, Oscar Slotosch, Kurt Stenzel, Martin Strecker, Nikolas Vlachantonis and Burkhart Wolff. 1995. A method for the development of correct software. DOI: 10.1007/bfb0015454
BibTeX | RIS | DOI

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1995. Interactive correctness proofs for software modules using KIV. DOI: 10.1109/cmpass.1995.521894
BibTeX | RIS | DOI

Gerhard Schellhorn and Axel Burandt. 1995. KIV: specification and verification of distributed technical systems with central control. DOI: 10.1007/3-540-58867-1_57
BibTeX | RIS | DOI

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1995. Tactics in KIV.
BibTeX | RIS

Thomas Fuchß, Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1995. Three selected case studies in verification. DOI: 10.1007/bfb0015472
BibTeX | RIS | DOI

1994

Gerhard Schellhorn. 1994. Specification and verification of distributed technical systems with central control. DOI: 10.5445/IR/294
BibTeX | RIS | DOI | URL

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1994. Tactics in KIV.
BibTeX | RIS

Institute for Software & Systems Engineering

The Institute for Software & Systems Engineering (ISSE), directed by Prof. Dr. Wolfgang Reif, is a scientific institution within the Faculty of Applied Computer Science of the University of Augsburg. In research, the institute supports both fundamental and application-oriented research in all areas of software and systems engineering. In teaching, the institute facilitates the further development of the faculty's and university's relevant course offerings.

Search