Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif. 2025. Verification of forward simulations with thread-local, step-local proof obligations. Science of Computer Programming 241, 103227. DOI: 10.1016/j.scico.2024.103227
PDF | BibTeX | RIS | DOI

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

Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif. 2023. Refinement and separation: modular verification of wandering trees. Lecture Notes in Computer Science 14300, 214-234. 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. Lecture Notes in Computer Science 13800, 129-147. 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. Lecture Notes in Computer Science 14010, 70-87. DOI: 10.1007/978-3-031-33163-3_6
PDF | BibTeX | RIS | DOI

Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich and Wolfgang Reif. 2022. Software & system verification with KIV. Lecture Notes in Computer Science 13360, 408-436. 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. Formal Aspects of Computing 34, 1, 2. 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. In Bartek Klin, Sławomir Lasota, Anca Muscholl (Eds.). 33rd International Conference on Concurrency Theory (CONCUR 2022), September 12-16, 2022, Warsaw, Poland. Schloss Dagstuhl, Leibniz-Zentrum für Informatik, Dagstuhl, 31:1-31:23 DOI: 10.4230/LIPIcs.CONCUR.2022.31
PDF | BibTeX | RIS | DOI

Stefan Bodenmüller, Gerhard Schellhorn, Martin Bitterlich and Wolfgang Reif. 2021. Flashix: modular verification of a concurrent and crash-safe flash file system. Lecture Notes in Computer Science 12750, 239-265. 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. Formal Aspects of Computing 33, 4-5, 547-573. DOI: 10.1007/s00165-021-00541-8
PDF | BibTeX | RIS | DOI

Gerhard Schellhorn, Stefan Bodenmüller, Jörg Pfähler and Wolfgang Reif. 2020. Adding concurrency to a sequential refinement tower. Lecture Notes in Computer Science 12071, 6-23. 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. Lecture Notes in Computer Science 12136, 39-58. 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. Lecture Notes in Computer Science 12546, 218-236. DOI: 10.1007/978-3-030-63461-2_12
PDF | BibTeX | RIS | DOI

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

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. Lecture Notes in Computer Science 10886, 105-120. 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. Science of Computer Programming 158, 21-40. DOI: 10.1016/j.scico.2017.08.014
PDF | BibTeX | RIS | DOI

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin and Heike Wehrheim. 2017. Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects of Computing 30, 5, 597-625. 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. Lecture Notes in Computer Science 10510, 375-390. DOI: 10.1007/978-3-319-66845-1_25
PDF | BibTeX | RIS | DOI

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler and Wolfgang Reif. 2016. A relational encoding for a clash-free subset of ASMs. Lecture Notes in Computer Science 9675, 237-243. 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. Lecture Notes in Computer Science 9593, 73-93. 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. Science of Computer Programming 131, 3-21. DOI: 10.1016/j.scico.2016.04.009
BibTeX | RIS | DOI

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. In Bernhard Thalheim, Klaus-Dieter Schewe, Andreas Prinz and Bruno Buchberger (Ed.). Correct Software in Web Applications and Web Services. Springer, Berlin [u.a.] (Texts & Monographs in Symbolic Computation (TEXTSMONOGR)), 45-81. 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. International Journal on Software Tools for Technology Transfer 17, 6, 677-694. 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. Software & Systems Modeling 14, 1, 27-44. 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. Lecture Notes in Computer Science 9109, 161-177. DOI: 10.1007/978-3-319-19249-9_11
BibTeX | RIS | DOI

Bogdan Tofan, Gerhard Schellhorn and Wolfgang Reif. 2014. A compositional proof method for linearizability applied to a wait-free multiset. Lecture Notes in Computer Science 8739, 357-372. 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. ACM Transactions on Computational Logic 15, 4, 31. 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. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2014-02. .
PDF | BibTeX | RIS

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg and Wolfgang Reif. 2014. Development of a verified flash file system. Lecture Notes in Computer Science 8477, 9-24. 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. Lecture Notes in Computer Science 8477, 188-203. 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. Lecture Notes in Computer Science 8442, 200-214. 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. Annals of Mathematics and Artificial Intelligence 71, 1-3, 131-174. 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. Science of Computer Programming 96, 3, 297-314. 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. Lecture Notes in Computer Science 8164, 242-261. DOI: 10.1007/978-3-642-54108-7_13
BibTeX | RIS | DOI

Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler and Wolfgang Reif. 2013. Compositional verification of a lock-free stack with RGITL. Electronic Communications of the EASST 66, . 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. Lecture Notes in Computer Science 8244, 214-229. DOI: 10.1007/978-3-319-03077-7_15
BibTeX | RIS | DOI

Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler and Wolfgang Reif. 2012. A formal model of a virtual filesystem switch. Electronic Proceedings in Theoretical Computer Science 102, 33-45. DOI: 10.4204/eptcs.102.5
BibTeX | RIS | DOI

Gerhard Schellhorn, Heike Wehrheim and John Derrick. 2012. How to prove algorithms linearisable. Lecture Notes in Computer Science 7358, 243-259. 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. Electronic Communications of the EASST 53, . 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. Lecture Notes in Computer Science 7421, 3-21. 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. In Francesco Flammini (Ed.). Railway Safety, Reliability, and Security: Technologies and Systems Engineering. IGI Global, Hershey, NY, 65-115.
BibTeX | RIS

Gerhard Schellhorn. 2011. Completeness of fair ASM refinement. Science of Computer Programming 76, 9, 756-773. 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. Lecture Notes in Computer Science 6916, 239-255. 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. In Carlo Combi, Martin Leucker and Frank Wolter (Ed.). 2011 Eighteenth International Symposium on Temporal Representation and Reasoning, 12-14 Sept. 2011, Lubeck, Germany. IEEE, Piscataway, NJ, 99-106. 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. In Bernhard Beckert, Ferruccio Damiani, Dilian Gurov (Eds.). Formal Verification of Object-Oriented Software: Papers presented at the 2nd International Conference, October 5-7, 2011, Turin, Italy. Karlsruhe Institute of Technology, Faculty of Informatics, Karlsruhe, 342-359
PDF | BibTeX | RIS | URL

John Derrick, Gerhard Schellhorn and Heike Wehrheim. 2011. Mechanically verified proof obligations for linearizability. ACM Transactions on Programming Languages and Systems 33, 1, 4. 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. International Journal of Software and Informatics 5, 1-2, 159-184.
BibTeX | RIS | URL

Simon Bäumler, Gerhard Schellhorn, Bogdan Tofan and Wolfgang Reif. 2011. Proving linearizability with temporal logic. Formal Aspects of Computing 23, 1, 91-112. 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). Science of Computer Programming 76, 9, 737-738. 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. In Hans-Ulrich Heiß, Peter Pepper, Holger Schlingloff and Jörg Schneider (Ed.). INFORMATIK 2011 – Informatik schafft Communities, Berlin, Deutschland, 4.-7. Oktober 2011. Gesellschaft für Informatik e.V., Bonn (GI-Edition : lecture notes in informatics : GI-Edition / Proceedings ; P-192), 355.
BibTeX | RIS | URL

Gidon Ernst, Gerhard Schellhorn and Wolfgang Reif. 2011. Verification of B+ trees: an experiment combining shape analysis and interactive theorem proving. Lecture Notes in Computer Science 7041, 188-203. 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. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2011-08. Universität Augsburg, Augsburg.
PDF | BibTeX | RIS

John Derrick, Gerhard Schellhorn and Heike Wehrheim. 2011. Verifying linearisability with potential linearisation points. Lecture Notes in Computer Science 6664, 323-337. DOI: 10.1007/978-3-642-21437-0_25
BibTeX | RIS | DOI

Andriy Dunets, Gerhard Schellhorn and Wolfgang Reif. 2010. Automated flaw detection in algebraic specifications. Journal of Automated Reasoning 45, 4, 359-395. 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. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2010-07. Universität Augsburg, Augsburg.
PDF | BibTeX | RIS

Simon Bäumler, Michael Balser, Florian Nafz, Wolfgang Reif and Gerhard Schellhorn. 2010. Interactive verification of concurrent systems using symbolic execution. AI Communications 23, 2-3, 285-307. 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. Lecture Notes in Computer Science 6120, 377-396. DOI: 10.1007/978-3-642-13321-3_21
BibTeX | RIS | DOI

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius and Wolfgang Reif. 2009. A systematic verification approach for Mondex electronic purses using ASMs. Lecture Notes in Computer Science 5115, 93-110. 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. Lecture Notes in Computer Science 5850, 190-206. 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. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2009-20. Universität Augsburg, Augsburg.
PDF | BibTeX | RIS

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

Gerhard Schellhorn. 2008. ASM refinement preserving invariants. Journal of Universal Computer Science 14, 12, 1929-1948. 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. Lecture Notes in Computer Science 5311, 141-155. 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. Lecture Notes in Computer Science 4966, 99-115. 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. In Piotr Rudnicki, Geoff Sutcliffe, Boris Konev, Renate Schmidt and Stephan Schulz (Ed.). The Combined KEAPPA - IWIL Workshops Proceedings: Proceedings of the LPAR 2008 Workshops Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, held at The 15th International Conference on Logic for Programming, Artificial Intelligence and ReasoningNovember 23-27, 2008, Doha, Qatar. CEUR-WS, 92-102.
BibTeX | RIS | URL

Richard Banach and Gerhard Schellhorn. 2008. On the refinement of atomic actions. Electronic Notes in Theoretical Computer Science 201, 3-30. 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. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2008-19. Universität Augsburg, Augsburg.
PDF | BibTeX | RIS

Frank Ortmeier, Alwin Hoffmann, Ulrich Huggenberger, Wolfgang Reif, Dominik Haneberg, Gerhard Schellhorn and Christian Tarragona. 2008. Simulations-basierte Programmierung von Industrierobotern. In Internationales Forum Mechatronik 2008, Stuttgart, Deutschland, 22-23.09.2008.
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. Lecture Notes in Computer Science 5014, 165-180. 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. Formal Aspects of Computing 20, 1, 41-59. DOI: 10.1007/s00165-007-0057-0
BibTeX | RIS | DOI

Nina Moebius, Dominik Haneberg, Wolfgang Reif and Gerhard Schellhorn. 2007. A modeling framework for the development of Provably Secure E-Commerce applications. In Sergiu Dascalu, Petre Dini, Sandro Morasca, Tadashi Ohta and Andre Oboler (Ed.). International Conference on Software Engineering Advances (ICSEA 2007), 25-31 Aug. 2007, Cap Esterel, France. IEEE, Piscataway, NJ, 8. 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. Lecture Notes in Computer Science 4591, 313-332. DOI: 10.1007/978-3-540-73210-5_17
BibTeX | RIS | DOI

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius and Wolfgang Reif. 2006. A systematic verification approach for Mondex electronic purses using ASMs. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2006-27. Universität Augsburg, Augsburg.
PDF | BibTeX | RIS

Frank Ortmeier and Gerhard Schellhorn. 2006. Formal fault tree analysis: practical experiences. In Stephan Merz (Ed.). AVoCS' 06: sixth International Workshop on Automated Verification or Critical Systems, September 18-19, 2006, Nancy, France. Institut National Polytechnique de Lorraine, Vandoeuvre-lès-Nancy
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. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2006-31. .
PDF | BibTeX | RIS

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg and Wolfgang Reif. 2006. The Mondex challenge: machine checked proofs for an electronic purse. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2006-02. .
PDF | BibTeX | RIS

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg and Wolfgang Reif. 2006. The mondex challenge: machine checked proofs for an electronic purse. Lecture Notes in Computer Science 4085, 16-31. 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. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2006-32. .
PDF | BibTeX | RIS

Dominik Haneberg, Holger Grandy, Wolfgang Reif and Gerhard Schellhorn. 2006. Verifying smart card applications: an ASM approach. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2006-08. .
PDF | BibTeX | RIS

Gerhard Schellhorn. 2005. ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theoretical Computer Science 336, 2-3, 403-435. DOI: 10.1016/j.tcs.2004.11.013
BibTeX | RIS | DOI

Frank Ortmeier, Wolfgang Reif and Gerhard Schellhorn. 2005. Deductive Cause-Consequence Analysis (DCCA). IFAC Proceedings Volumes 38, 1, 62-67. 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). Lecture Notes in Computer Science 3463, 210-224. 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. In Public transport 2020 - making the connection: people, environment, business; 56th UITP world congress, Rome, 5 - 9 June 2005; proceedings of the User Interfaces for Theorem Provers Workshop (UITP 2005). UITP, Brussels
BibTeX | RIS

Dominik Haneberg, H. Grandy, Wolfgang Reif and Gerhard Schellhorn. 2005. Verifying security protocols: an ASM approach. In D. Beauquier, E. Börger, A. Slissenko (Eds.). Proceedings of the 12th International Workshop on Abstract State Machines (ASM 2005), University Paris 12 - Val de Marne, Créteil, France, Marech 2005.
BibTeX | RIS

Frank Ortmeier, Andreas Thums, Gerhard Schellhorn and Wolfgang Reif. 2004. Combining formal methods and safety analysis - the ForMoSA approach. Lecture Notes in Computer Science 3147, 474-493. 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. In René Jacquart (Ed.). Building the information society: IFIP 18th World Computer Congress; Topical sessions 22-27 August 2004, Toulouse, France. Kluwer Academic Publishers, New York [u.a.] (IFIP ; 156), 637-642.
BibTeX | RIS

Andreas Thums, Gerhard Schellhorn, Frank Ortmeier and Wolfgang Reif. 2004. Interactive verification of statecharts. Lecture Notes in Computer Science 3147, 355-373. 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". Lecture Notes in Computer Science 3147, 419-422. 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. In E. Schnieder and G. Tarnai (Ed.). Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2004), Braunschweig, Germany, December 2-3, 2004. Technische Uni Braunschweig, Inst. für Regelungs- und Automatisierungstechnik, Braunschweig
BibTeX | RIS

Andreas Thums and Gerhard Schellhorn. 2003. Formal safety analysis in transportation control. In Eckehard Schnieder (Ed.). International Workshop on Software Specification of Safety Relevant Transportation Control Tasks : 23 - 24 April 2002, Braunschweig. VDI-Verlag, Düsseldorf (Verein Deutscher Ingenieure: Fortschrittberichte VDI / Reihe 12 / Verkehrstechnik, Fahrzeugtechnik ; 535)
BibTeX | RIS

Rudolf Berghammer, Dominik Haneberg, Wolfgang Reif and Gerhard Schellhorn. 2003. J.UCS Special Issue on Tools for System Design and Verification. Journal of Universal Computer Science 9, 2, 86-87.
PDF | BibTeX | RIS | URL

Andreas Thums and Gerhard Schellhorn. 2003. Model checking FTA. Lecture Notes in Computer Science 2805, 739-757. 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. Reliability Engineering & System Safety 81, 3, 259-268. DOI: 10.1016/S0951-8320(03)00090-5
BibTeX | RIS | DOI

Gerhard Schellhorn, Andreas Thums and Wolfgang Reif. 2002. Formal fault tree semantics. In Proceedings of The Sixth World Conference on Integrated Design & Process Technology: June 23 - 27, 2003, Pasadena, California (IDPT-2002). Society for Design and Process Science, Dallas, TX
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. Lecture Notes in Computer Science 2434, 296-308. 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. Journal of Computer Security 10, 4, 339-367. 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. Journal of Logic and Computation 12, 4, 549-560. DOI: 10.1093/logcom/12.4.549
BibTeX | RIS | DOI

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

Wolfgang Reif, Gerhard Schellhorn and Andreas Thums. 2001. Integration formaler Spezifikation und Sicherheitsanalyse. Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg 2001-06. Universität Augsburg, Augsburg.
PDF | BibTeX | RIS

Gerhard Schellhorn. 2001. Verification of ASM refinements using generalized forward simulation. J.UCS - Journal of Universal Computer Science 7, 11, 952-979. DOI: 10.3217/jucs-007-11-0952
BibTeX | RIS | DOI | URL

Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn and Tobias Vollmer. 2000. Do you trust your model checker?. In Warren A. Hunt Jr. and Steven D. Johnson (Ed.). Formal methods in computer-aided design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1–3, 2000. Springer, Berlin [u.a.] (Lecture Notes in Computer Science ; 1954), 199-216. 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. Lecture Notes in Computer Science 1783, 363-366. 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. VDI-Zeitschrift: Fortschritt-Berichte VDI, Reihe 12 2000, 12.
BibTeX | RIS

Wolfgang Reif, Gerhard Schellhorn and Andreas Thums. 2000. Safety analysis of a radio-based crossing control system using formal methods. IFAC Proceedings Volumes 33, 9, 261-266. 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. Lecture Notes in Computer Science 1895, 17-36. DOI: 10.1007/10722599_2
BibTeX | RIS | DOI

Michael Balser, C. Duelli, Wolfgang Reif and Gerhard Schellhorn. 2000. Verifying concurrent systems with symbolic execution. In AiML-ICTL 2000: Advances in Modal Logic - International Conference on Temporal Logic 2000, October 4-7, 2000, University of Leipzig, Germany.
BibTeX | RIS

Michael Balser, Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1999. KIV 3.0 for provably correct systems. In Dieter Hutter, Werner Stephan, Paolo Traverso and Markus Ullmann (Ed.). Applied Formal Methods — FM-Trends 98: International Workshop on Current Trends in Applied Formal Methods Boppard, Germany, October 7–9, 1998. Springer, Berlin [u.a.] (Lecture Notes in Computer Science ; 1641), 330-337. 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. In Dieter Hutter, Werner Stephan, Paolo Traverso and Markus Ullmann (Ed.). Applied Formal Methods — FM-Trends 98: International Workshop on Current Trends in Applied Formal Methods Boppard, Germany, October 7–9, 1998. Springer, Berlin [u.a.] (Lecture Notes in Computer Science ; 1641), 351-358. DOI: 10.1007/3-540-48257-1_26
BibTeX | RIS | DOI

Gerhard Schellhorn. 1999. Verification of abstract state machines. Fachbereich Informatik, Universität Ulm, Ulm.
PDF | BibTeX | RIS

Gerhard Schellhorn. 1999. Verifikation abstrakter Zustandsmaschinen. Fachbereich Informatik, Universität Ulm, Ulm.
PDF | BibTeX | RIS

Wolfgang Ahrendt, Bernhard Beckert, R. Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn and Peter H. Schmitt. 1998. Integrating automated and interactive theorem proving. In Wolfgang Bibel and Peter H. Schmitt (Ed.). Automated Deduction — A Basis for Applications: Volume II: Systems and Implementation Techniques. Springer, Dordrecht (Applied Logic Series ; 9), 97-116. 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. Fachbereich Informatik, Universität Ulm, Ulm (Ulmer Informatik-Berichte ; 98-12).
BibTeX | RIS | URL | URL

Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel and M. Balser. 1998. Structured specifications and interactive proofs with KIV. In Wolfgang Bibel and Peter H. Schmitt (Ed.). Automated deduction - a basis for applications: Volume II - systems and implementation techniques. Springer, Dordrecht (Applied Logic Series ; 9), 13-39. 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. In Wolfgang Bibel and P. H. Schmitt (Ed.). Automated deduction - a basis for applications: volume 3 - applications. Kluwer, Dordrecht
BibTeX | RIS

Wolfgang Reif and Gerhard Schellhorn. 1998. Theorem proving in large theories. In Wolfgang Bibel and Peter H. Schmitt (Ed.). Automated deduction — a basis for applications: Volume II - systems and implementation techniques. Springer, Dordrecht (Applied Logic Series ; 9), 225-241. 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. Ulmer Informatik Berichte 98-13.
BibTeX | RIS

Gerhard Schellhorn and Wolfgang Reif. 1997. Proving properties of finite enumerations: a problem set for automated theorem provers. Ulmer Informatik-Berichte 97-12.
BibTeX | RIS

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1997. Proving system correctness with KIV. In Michel Bidoit and Max Dauchet (Ed.). TAPSOFT '97: Theory and Practice of Software Development; 7th International Joint Conference CAAP/FASE Lille, France, April 14–18, 1997. Springer, Berlin [u.a.] (Lecture Notes in Computer Science ; 1214), 859-862. DOI: 10.1007/bfb0030647
BibTeX | RIS | DOI

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1997. Proving system correctness with KIV 3.0. Lecture Notes in Computer Science 1249, 69-72. 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. J.UCS - Journal of Universal Computer Science 3, 4, 377-413. DOI: 10.3217/jucs-003-04-0377
BibTeX | RIS | DOI | URL

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1996. KIV 3.0: concepts and applications. Universität Ulm, Ulm.
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. (Technischer Bericht / A / Fachbereich Informatik, Universität des Saarlandes). DOI: 10.22028/D291-25803
BibTeX | RIS | DOI

Gerhard Schellhorn and W. Ahrendt. 1996. Verification of a prolog compiler - first steps with KIV. Universität Ulm, Ulm (Ulmer Informatik-Berichte ; 96-05).
BibTeX | RIS | URL

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. In Manfred Broy and Stefan Jähnichen (Ed.). KORSO: methods, languages, and tools for the construction of correct software: final report. Springer, Berlin [u.a.] (Lecture Notes in Computer Science ; 1009), 25-57. DOI: 10.1007/bfb0015454
BibTeX | RIS | DOI

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1995. Interactive correctness proofs for software modules using KIV. In COMPASS '95: Proceedings of the Tenth Annual Conference on Computer Assurance Systems Integrity, Software Safety and Process Security, 25-29 June 1995, Gaithersburg, MD, USA, USA. IEEE, Piscataway, NJ, 151-162. 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. Lecture Notes in Computer Science 891, 229-245. DOI: 10.1007/3-540-58867-1_57
BibTeX | RIS | DOI

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1995. Tactics in KIV. Journal on Information Processing and Cybernetics 1994, 30.
BibTeX | RIS

Thomas Fuchß, Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1995. Three selected case studies in verification. In Manfred Broy and Stefan Jähnichen (Ed.). KORSO - methods, languages, and tools for the construction of correct software: Final Report. Springer, Berlin [u.a.] (Lecture Notes in Computer Science ; 1009), 369-387. DOI: 10.1007/bfb0015472
BibTeX | RIS | DOI

Gerhard Schellhorn. 1994. Specification and verification of distributed technical systems with central control. Fakultät für Informatik, Universität Karlsruhe, Karlsruhe (Technical Report, Fakultät für Informatik, Universität Karlsruhe ; 1994,3). DOI: 10.5445/IR/294
BibTeX | RIS | DOI | URL

Wolfgang Reif, Gerhard Schellhorn and Kurt Stenzel. 1994. Tactics in KIV. In KI-94, 18th German Annual Conference on Artificial Intelligence, September 18 - 23 1994, Saarbrücken, Germany.
BibTeX | RIS