|
2025
|
|
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
|
|
2024
|
|
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
|
|
2023
|
|
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
|
|
2022
|
|
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
|
|
2021
|
|
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
|
|
2020
|
|
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
|
|
2019
|
|
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
|
|
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. 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
|
|
2017
|
|
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
|
|
2016
|
|
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
|
|
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. 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
|
|
2014
|
|
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
|
|
2013
|
|
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
|
|
2012
|
|
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
|
|
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
|
|
2011
|
|
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
|
|
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
|
|
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
|
|
2010
|
|
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
|
|
2009
|
|
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
|
|
2008
|
|
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
|
|
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
|
|
2007
|
|
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
|
|
2006
|
|
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
|
|
2005
|
|
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), 伟德国际_伟德国际1946$娱乐app游戏 Paris 12 - Val de Marne, Créteil, France, Marech 2005.
BibTeX | RIS
|
|
2004
|
|
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
|
|
2003
|
|
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
|
|
2002
|
|
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
|
|
2001
|
|
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
|
|
2000
|
|
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. |
