Prof. Dr. Ernst-Rüdiger Olderog

Contact

  • E-Mail:

Prof. Dr. Ernst-Rüdiger Olderog

Curriculum Vitae

1974-1979 study of informatics, mathematics and logics at the University of Kiel
1979 diploma degree in informatics
1981 Ph.D. in computer science
1981-1983 Programming Research Group at Oxford University
1984-1989 Various research visits in Amsterdam, Edinburgh, Yorktown Heights, and Saarbrücken
1989 Habilitation for computer science
1989-1994 Associate professor of computer science at the University of Oldenburg
since 1994 Full professor of computer science at the University of Oldenburg
1994-1999 Leibniz Award of the German Research Council (DFG)
1995-2005

Chairman of IFIP Working Group 2.2 on Formal Description of Programming Concepts
2000-2014 Managing Editor Acta Informatica
2012 Member of Academia Europaea
since 2012 Director of DFG Research Training Group SCARE
2017-2019

Dean of Faculty II

Books

  • [book] bibtex | Go to document Go to document
    K. R. Apt, F. S. de Boer, and E. -R. Olderog, Verification of Sequential and Concurrent Programs, 3rd Edition, Springer-Verlag, 2009.
    @book{ABO09-Book3,
      author = { K. R. Apt and F. S. de Boer and E.-R. Olderog },
      title = {Verification of Sequential and Concurrent Programs, 3rd Edition},
      series = {Texts in Computer Science},
      publisher = {Springer-Verlag},
      year = {2009},
      note = {502 pp, ISBN 978-1-84882-744-8},
      url = {http://www.springer.com/computer/theoretical+computer+science/book/978-1-84882-744-8} }
  • [book] bibtex | Go to document Go to document
    E. -R. Olderog and H. Dierks, Real-Time Systems --- Formal Specification and Automatic Verification -- Errata: see below, Cambridge University Press, 2008.
    @book{OD08,
      author = {E.-R. Olderog and H. Dierks},
      title = {Real-Time Systems --- Formal Specification and Automatic Verification -- Errata: see below},
      publisher = {Cambridge University Press},
      year = 2008, note = {ISBN 978-0-521-88333-7. For more information see: \url{http://csd.informatik.uni-oldenburg.de/rt-book/}{http://csd.informatik.uni-oldenburg.de/rt-book/}},
      url = {http://www.cambridge.org/de/academic/subjects/computer-science/distributed-networked-and-mobile-computing/real-time-systems-formal-specification-and-automatic-verification} }
  • [book] bibtex
    K. -R. Apt and E. -R. Olderog, Verification of Sequential and Concurrent Programs., 2nd ed., springer, 1997.
    @book{ero97-verification,
      author = {K.-R. Apt and E.-R. Olderog},
      title = {Verification of Sequential and Concurrent Programs.},
      edition = {2nd},
      publisher = springer, year = 1997, note = {ISBN 0-387-94896-1. \url{http://www.springer-ny.com/catalog/np/mar97np/DATA/0-387-94896-1.html} {This book in the Springer catalogue}. \url{ http://csd.informatik.uni-oldenburg.de/pub/Papers/ero97-verification-a.ps.gz} {More Information}. } }
  • [book] bibtex
    K. R. Apt and E. -R. Olderog, Programmverifikation, springer, 1994.
    @book{ero94,
      author = {K. R. Apt and E.-R. Olderog},
      title = {Programmverifikation},
      publisher = springer, note = {{\url{http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/Errata.ps} {Errata-Liste}} bzw. {\url{http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/Errata\_long.ps} {Errata-Liste mit Tippfehlern}}},
      year = 1994 }
  • [book] bibtex | Go to document Go to document
    E. -R. Olderog, Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship, Cambridge University Press, 1991.
    @book{Old05-nets,
      author = {E.-R. Olderog},
      title = {Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship},
      publisher = {Cambridge University Press},
      year = 1991, pages = {267},
      note = {Paperback Edition 2005},
      url = {http://www.cambridge.org/de/academic/subjects/computer-science/programming-languages-and-applied-logic/nets-terms-and-formulas-three-views-concurrent-processes-and-their-relationship} }

Errata

Errata for the book Real-Time Systems --- Formal Specification and Automatic Verification: Errata-Real-Time_Systems.pdf

Publications

  • [article] bibtex | Go to document Go to document
    B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E. Olderog, "AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)," CoRR, vol. abs/2005.07130, 2020.
    @article{DBLP:journals/corr/abs-2005-07130,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {AdamMC: {A} Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)},
      journal = {CoRR},
      volume = {abs/2005.07130},
      year = {2020},
      url = {https://arxiv.org/abs/2005.07130},
      archiveprefix = {arXiv},
      eprint = {2005.07130},
      timestamp = {Fri, 22 May 2020 16:21:28 +0200},
      biburl = {https://dblp.org/rec/journals/corr/abs-2005-07130.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [article] bibtex | Go to document Go to document
    B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E. Olderog, "Model Checking Branching Properties on Petri Nets with Transits (Full Version)," CoRR, vol. abs/2007.07235, 2020.
    @article{DBLP:journals/corr/abs-2007-07235,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {Model Checking Branching Properties on Petri Nets with Transits (Full Version)},
      journal = {CoRR},
      volume = {abs/2007.07235},
      year = {2020},
      url = {https://arxiv.org/abs/2007.07235},
      archiveprefix = {arXiv},
      eprint = {2007.07235},
      timestamp = {Tue, 21 Jul 2020 12:53:33 +0200},
      biburl = {https://dblp.org/rec/journals/corr/abs-2007-07235.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Go to document Go to document
    B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E. Olderog, "Model Checking Branching Properties on Petri Nets with Transits," in Proc. Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, 2020, pp. 394-410.
    @inproceedings{DBLP:conf/atva/FinkbeinerGHO20,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {Model Checking Branching Properties on Petri Nets with Transits},
      booktitle = {Automated Technology for Verification and Analysis - 18th International Symposium, {ATVA} 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings},
      pages = {394--410},
      year = {2020},
      optcrossref = {DBLP:conf/atva/2020},
      url = {https://doi.org/10.1007/978-3-030-59152-6\_22},
      doi = {10.1007/978-3-030-59152-6\_22},
      timestamp = {Tue, 13 Oct 2020 16:57:38 +0200},
      biburl = {https://dblp.org/rec/conf/atva/FinkbeinerGHO20.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Go to document Go to document
    B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E. Olderog, "AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL," in Proc. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, 2020, pp. 64-76.
    @inproceedings{DBLP:conf/cav/FinkbeinerGHO20,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {AdamMC: {A} Model Checker for Petri Nets with Transits against Flow-LTL},
      booktitle = {Computer Aided Verification - 32nd International Conference, {CAV} 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}},
      pages = {64--76},
      year = {2020},
      optcrossref = {DBLP:conf/cav/2020-2},
      url = {https://doi.org/10.1007/978-3-030-53291-8\_5},
      doi = {10.1007/978-3-030-53291-8\_5},
      timestamp = {Fri, 17 Jul 2020 12:05:42 +0200},
      biburl = {https://dblp.org/rec/conf/cav/FinkbeinerGHO20.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [article] bibtex | Go to document Go to document
    M. Gieseking, E. Olderog, and N. Würdemann, "Solving high-level Petri games," Acta Inf., vol. 57, iss. 3-5, pp. 591-626, 2020.
    @article{DBLP:journals/acta/GiesekingOW20,
      author = {Manuel Gieseking and Ernst-R{\"{u}}diger Olderog and Nick W{\"{u}}rdemann},
      title = {Solving high-level Petri games},
      journal = {Acta Inf.},
      volume = {57},
      number = {3-5},
      pages = {591--626},
      year = {2020},
      url = {https://doi.org/10.1007/s00236-020-00368-5},
      doi = {10.1007/s00236-020-00368-5},
      timestamp = {Fri, 22 May 2020 21:54:01 +0200},
      biburl = {https://dblp.org/rec/journals/acta/GiesekingOW20.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [article] bibtex | Go to document Go to document
    M. Gieseking and E. Olderog, "High-Level Representation of Benchmark Families for Petri Games," CoRR, vol. abs/1904.05621, 2019.
    @article{DBLP:journals/corr/abs-1904-05621,
      author = {Manuel Gieseking and Ernst-R{\"{u}}diger Olderog},
      title = {High-Level Representation of Benchmark Families for Petri Games},
      journal = {CoRR},
      volume = {abs/1904.05621},
      year = {2019},
      url = {http://arxiv.org/abs/1904.05621},
      archiveprefix = {arXiv},
      eprint = {1904.05621},
      timestamp = {Thu, 25 Apr 2019 13:55:01 +0200},
      biburl = {https://dblp.org/rec/bib/journals/corr/abs-1904-05621},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [article] bibtex | Go to document Go to document
    B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E. Olderog, "Model Checking Data Flows in Concurrent Network Updates (Full Version)," CoRR, vol. abs/1907.11061, 2019.
    @article{DBLP:journals/corr/abs-1907-11061,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {Model Checking Data Flows in Concurrent Network Updates (Full Version)},
      journal = {CoRR},
      volume = {abs/1907.11061},
      year = {2019},
      url = {http://arxiv.org/abs/1907.11061},
      archiveprefix = {arXiv},
      eprint = {1907.11061},
      timestamp = {Thu, 01 Aug 2019 08:59:33 +0200},
      biburl = {https://dblp.org/rec/journals/corr/abs-1907-11061.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Go to document Go to document
    B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E. Olderog, "Model Checking Data Flows in Concurrent Network Updates," in Proc. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, 2019, pp. 515-533.
    @inproceedings{DBLP:conf/atva/FinkbeinerGHO19,
      author = {Bernd Finkbeiner and Manuel Gieseking and Jesko Hecking-Harbusch and Ernst-R{\"{u}}diger Olderog},
      title = {Model Checking Data Flows in Concurrent Network Updates},
      booktitle = {Automated Technology for Verification and Analysis - 17th International Symposium, {ATVA} 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings},
      pages = {515--533},
      year = {2019},
      optcrossref = {DBLP:conf/atva/2019},
      url = {http://www.uni-oldenburg.de/fileadmin/user\_upload/f2inform-csd/FinGieHecOld19.pdf},
      opturl = {https://doi.org/10.1007/978-3-030-31784-3\_30},
      doi = {10.1007/978-3-030-31784-3\_30},
      timestamp = {Tue, 22 Oct 2019 15:35:01 +0200},
      biburl = {https://dblp.org/rec/bib/conf/atva/FinkbeinerGHO19},
      bibsource = {dblp computer science bibliography, https://dblp.org} }
  • [inproceedings] bibtex | Go to document Go to document
    E. -R. Olderog, "Space for Traffic Manoeuvres -- An Overview," in Proc. Symposium on Real-Time and Hybrid Systems, 2018, pp. 211-230.
    @inproceedings{Olderog18,
      author = {E.-R. Olderog},
      title = {Space for Traffic Manoeuvres -- An Overview},
      editor = {Cliff Jones and Ji Wang and Naijun Zhan},
      booktitle = {Symposium on Real-Time and Hybrid Systems},
      pages = {211--230},
      series = {LNCS},
      volume = {11180},
      publisher = {Springer},
      year = {2018},
      url = {https://doi.org/10.1007/978-3-030-01461-2_11} }
  • [article] bibtex | Go to document Go to document
    B. Finkbeiner and E. -R. Olderog, "Petri Games: Synthesis of Distributed Systems with Causal Memory," Information and Computation, vol. 253, Part 2, pp. 181-203, 2017.
    @article{FinkbeinerOlderog16, title = {Petri Games: Synthesis of Distributed Systems with Causal Memory},
      author = {B. Finkbeiner and E.-R. Olderog},
      journal = {Information and Computation},
      volume = {253, Part 2 },
      year = {2017},
      pages = {181--203},
      url = {https://www.uni-oldenburg.de/fileadmin/user_upload/f2inform-csd/pub/mainPG-IC.pdf},
      abstract = {We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete.} }
  • [article] bibtex | Go to document Go to document
    G. v. Bochmann, M. Hilscher, S. Linker, and E. -R. Olderog, "Synthesizing and Verifying Controllers for Multi-lane Traffic Maneuvers," Formal Aspects of Computing, vol. 29, iss. 4, pp. 583-600, 2017.
    @article{BHLO17,
      author = {G. v. Bochmann and M. Hilscher and S. Linker and E.-R. Olderog},
      title = {Synthesizing and Verifying Controllers for Multi-lane Traffic Maneuvers},
      journal = {Formal Aspects of Computing},
      volume = {29},
      number = {4},
      year = {2017},
      pages = {583--600},
      doi = {10.1007/s00165-017-0424-4},
      url = {https://www.uni-oldenburg.de/fileadmin/user_upload/informatik/ag/csd/pub/faoc-synthesis.pdf} }
  • [incollection] bibtex | Go to document Go to document
    E. -R. Olderog, A.P.Ravn, and R. Wisniewski, "Linking Discrete and Dynamic Models: Applied to Traffic Manoevres," in Provably Correct Systems, Hinchey, M. G., Bowen, J. P., and Olderog, E. -R., Eds., Springer, 2017, pp. 95-120.
    @incollection{ORW17,
      author = {E.-R. Olderog and A.P.Ravn and R. Wisniewski},
      title = {Linking Discrete and Dynamic Models: Applied to Traffic Manoevres},
      editor = {M.G. Hinchey and J.P. Bowen and E.-R. Olderog},
      booktitle = {Provably Correct Systems},
      note = {NASA Monographs in Systems and Software Engineering},
      publisher = {Springer},
      year = {2017},
      pages = {95-120},
      url = {https://www.uni-oldenburg.de/fileadmin/user_upload/informatik/ag/csd/pub/main-ORW.pdf} }
  • [inproceedings] bibtex | Go to document Go to document
    E. -R. Olderog and M. Schwammberger, "Formalising a Hazard Warning Communication Protocol with Timed Automata," in Proc. Models, Algorithms, Logics and Tools, 2017, pp. 640-660.
    @inproceedings{OlderogSchwammberger17,
      author = {E.-R. Olderog and M. Schwammberger},
      title = {Formalising a Hazard Warning Communication Protocol with Timed Automata},
      editor = {Luca Aceto and Giorgio Bacci and Giovanni Bacci and Anna Ing{\'{o}}lfsd{\'{o}}ttir and Axel Legay and Radu Mardare},
      booktitle = {Models, Algorithms, Logics and Tools},
      pages = {640--660},
      series = {LNCS},
      volume = {10460},
      publisher = {Springer},
      year = {2017},
      url = {https://doi.org/10.1007/978-3-319-63121-9_32} }
  • [inproceedings] bibtex | Go to document Go to document
    B. Finkbeiner, M. Gieseking, J. Hecking-Harbusch, and E. Olderog, "Symbolic vs. Bounded Synthesis for Petri Games," in Proc. Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017, 2017, pp. 23-43.
    @inproceedings{DBLP:journals/corr/abs-1711-10637,
      author = {Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-R\"udiger},
      year = {2017},
      title = {Symbolic vs. Bounded Synthesis for Petri Games},
      editor = {Fisman, Dana and Jacobs, Swen},
      booktitle = {Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017},
      series = {Electronic Proceedings in Theoretical Computer Science {(EPTCS)}},
      volume = {260},
      publisher = {Open Publishing Association},
      pages = {23--43},
      doi = {10.4204/EPTCS.260.5},
      url = {https://arxiv.org/abs/1711.10637} }
  • [inproceedings] bibtex | Go to document Go to document
    B. Engelmann and E. Olderog, "A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs," in Proc. Proc. Theory and Practice of Formal Methods, 2016, pp. 173-193.
    @inproceedings{EngelmannOlderog2015,
      author = {Bj\"orn Engelmann and Ernst-R\"udiger Olderog},
      title = {{A} {S}ound and {C}omplete {H}oare {L}ogic for {D}ynamically-{T}yped, {O}bject-{O}riented {P}rograms},
      booktitle = {Proc. Theory and Practice of Formal Methods},
      year = {2016},
      editor = {Erika {\' A}brah{\' a}m and Marcello Bonsangue and Einar Broch Johnsen},
      volume = {9660},
      series = {LNCS},
      publisher = {Springer},
      pages = {173--193},
      url = {http://link.springer.com/chapter/10.1007%2F978-3-319-30734-3_13},
      optaddress = {Eindhoven, The Netherlands} }
  • [article] bibtex | Go to document Go to document
    E. -R. Olderog and M. Swaminathan, "Structural Transformations for Data-Enriched Real-Time Systems," Formal Asp. Comput., vol. 27, pp. 727-750, 2015.
    @article{OlderogSwaminathan14,
      author = {E.-R Olderog and M. Swaminathan},
      title = {Structural Transformations for Data-Enriched Real-Time Systems},
      journal = {Formal Asp. Comput.},
      volume = {27},
      pages = {727--750},
      year = {2015},
      url = {http://dx.doi.org/10.1007/s00165-014-0306-y} }
  • [misc] bibtex | Go to document Go to document
    B. Engelmann, E. -R. Olderog, and N. Flick, Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic, 2015.
    @misc{EOF2015,
      author = {Bj{\"o}rn Engelmann and E.-R Olderog and Nils-Erik Flick},
      title = {Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic},
      month = {January},
      year = {2015},
      howpublished = {arXiv:1501.02699v1 [cs.PL]},
      abstract = {Dynamically typed object-oriented languages enable programmers to write elegant, reusable and extensible programs. However, with the current methodology for program verification, the absence of static type information creates significant overhead. Our proposal is two-fold: First, we propose a layer of abstraction hiding the complexity of dynamic typing when provided with sufficient type information. Since this essentially creates the illusion of verifying a statically-typed program, the effort required is equivalent to the statically-typed case. Second, we show how the required type information can be efficiently derived for all type-safe programs by integrating a type inference algorithm into Hoare logic, yielding a semi-automatic procedure allowing the user to focus on those typing problems really requiring his attention. While applying type inference to dynamically typed programs is a well-established method by now, our approach complements conventional soft typing systems by offering formal proof as a third option besides modifying the program (static typing) and accepting the presence of runtime type errors (dynamic typing).},
      url = {http://arxiv.org/abs/1501.02699} }
  • [inproceedings] bibtex | Go to document Go to document
    E. -R. Olderog, A. P. Ravn, and R. Wisniewski, "Linking Spatial and Dynamic Models for Traffic Maneuvers," in Proc. 54th IEEE Conf. on Decision and Control (CDC), Osaka, Japan, 2015, pp. 6809-6816.
    @inproceedings{ORW2015,
      author = {E.-R. Olderog and A.P. Ravn and R. Wisniewski},
      title = {Linking Spatial and Dynamic Models for Traffic Maneuvers},
      booktitle = {54th IEEE Conf. on Decision and Control (CDC), Osaka, Japan },
      year = {2015},
      pages = {6809-6816},
      month = {Dec},
      publisher = {IEEE},
      url = {https://www.uni-oldenburg.de/fileadmin/user_upload/f2inform-csd/pub/root-ORW15.pdf},
      doi = {10.1109/CDC.2015.7403292},
      subproject = {H3},
      conference-short = {CDC},
      conference-long = {IEEE Conference on Decision and Control},
      abstract = {For traffic maneuvers of multiple vehicles on highways we build an abstract spatial and a concrete dynamic model. In the spatial model we show the safety (collision freedom) of lane-change maneuvers. By linking the spatial and dynamic model via suitable refinements of the spatial atoms to distance measures, the safety carries over to the concrete mode} }
  • [inproceedings] bibtex
    G. v. Bochmann, M. Hilscher, S. Linker, and E. Olderog, "Synthesizing Controllers for Multi-Lane Traffic Maneuvers," in Proc. International Symposium on Dependable Software Engineering (SETTA), 2015, pp. 71-86.
    @inproceedings{avacs-h3-dec-15, title = {Synthesizing Controllers for Multi-Lane Traffic Maneuvers},
      author = {Gregor v. Bochmann AND Martin Hilscher AND Sven Linker AND Ernst-Rüdiger Olderog},
      editor = {Xuandong Li AND Zhiming Liu AND Wang Yi},
      booktitle = {International Symposium on Dependable Software Engineering (SETTA)},
      year = {2015},
      month = {Nov.},
      pages = {71-86},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      volume = 9409, abstract = {The dynamic behavior of a car can be modeled as a hybrid system involving continuous state changes and discrete state transitions. However, we show that the control of safe (collision free) lane change maneuvers in multi-lane traffic on highways can be described by finite state machines extended with continuousvariables coming from the environment. We use standard theory for controller synthesis to derive the dynamic behavior of a lane-change controller. Thereby, we contrast the setting of interleaving semantics and synchronous concurrent semantics. We also consider the possibility of exchanging knowledge between neighboring cars in order to come up with the right decisions.},
      conference-long = {International Symposium on Dependable Software Engineering},
      conference-short = {SETTA} }
  • [inproceedings] bibtex | Go to document Go to document
    B. Finkbeiner, M. Gieseking, and E. Olderog, "Adam: Causality-Based Synthesis of Distributed Systems," in Proc. Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, 2015, pp. 433-439.
    @inproceedings{fingieold15, title = {Adam: Causality-Based Synthesis of Distributed Systems},
      author = {Bernd Finkbeiner and Manuel Gieseking and Ernst-R{\"{u}}diger Olderog},
      booktitle = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {I}},
      year = {2015},
      editor = {Daniel Kroening and Corina S. Pasareanu},
      pages = {433--439},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      volume = {9206},
      abstract = {We present ADAM, a tool for the automatic synthesis of distributed systems with multiple concurrent processes. For each process, an individual controller is synthesized that acts on locally available information obtained through synchronization with the environment and with other system processes. ADAM is based on Petri games, an extension of Petri nets where each token is a player in a multiplayer game. ADAM implements the first symbolic game solving algorithm for Petri games. We report on experience from several case studies with up to 38 system processes.},
      conference-long = {International Conference on Computer Aided Verification},
      conference-short = {CAV},
      url = {http://www.uni-oldenburg.de/fileadmin/user\_upload/f2inform-csd/fingieold15.pdf} }
  • [inproceedings] bibtex | Go to document Go to document
    B. Finkbeiner and E. -R. Olderog, "Petri Games: Synthesis of Distributed Systems with Causal Memory," in Proc. Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 10-12, 2014., 2014, pp. 217-230.
    @inproceedings{FinOld14,
      author = {Bernd Finkbeiner and E.-R Olderog},
      title = {Petri Games: Synthesis of Distributed Systems with Causal Memory},
      editor = {Adriano Peron and Carla Piazza},
      booktitle = {Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 10-12, 2014.},
      series = {{EPTCS}},
      year = {2014},
      volume = {161},
      pages = {217--230},
      url = {http://arxiv.org/abs/1406.1069v2} }
  • [inproceedings] bibtex
    M. Hilscher, S. Linker, and E. -R. Olderog, "Proving Safety of Traffic Manoeuvres on Country Roads," in Proc. Theories of Programming and Formal Methods, 2013, pp. 196-212.
    @inproceedings{HLO13,
      author = {M. Hilscher and S. Linker and E.-R. Olderog},
      editor = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
      title = {Proving Safety of Traffic Manoeuvres on Country Roads},
      booktitle = {Theories of Programming and Formal Methods},
      publisher = {Springer},
      series = {LNCS},
      volume = {8051},
      year = {2013},
      pages = {196--212} }
  • [inproceedings] bibtex | Go to document Go to document
    E. -R. Olderog and M. Swaminathan, "Structural Transformations for Data-Enriched Real-Time Systems," in Proc. Integrated Formal Methods (iFM), 2013, pp. 378-393.
    @inproceedings{OlderogSwaminathan13,
      author = {E.-R. Olderog and Mani Swaminathan},
      title = {Structural Transformations for Data-Enriched Real-Time Systems},
      editor = {Einar Broch Johnsen and Luigia Petre},
      booktitle = {Integrated Formal Methods (iFM)},
      volume = {7940},
      series = {Lecture Notes in Computer Science},
      pages = {378-393},
      publisher = {Springer-Verlag},
      year = {2013},
      url = {http://dx.doi.org/10.1007/978-3-642-38613-8_26} }
  • [article] bibtex
    K. R. Apt, F. S. de Boer, E. -R. Olderog, and S. de Gouw, "Verification of object-oriented programs: A transformational approach," J Computer System Sciences, vol. 78, pp. 823-852, 2012.
    @article{ABOG12,
      author = {K. R. Apt and F. S. de Boer and E.-R. Olderog and S. de Gouw},
      title = {Verification of object-oriented programs: A transformational approach},
      journal = {J Computer System Sciences},
      volume = {78},
      number = {},
      pages = {823--852},
      year = {2012},
      optnote = {DOI information: 10.1016/j.jcss.2011.08.002} }
  • [article] bibtex
    E. -R. Olderog and R. Wilhelm, "Turing und die Verifikation," Informatik-Spektrum, vol. 35, iss. 4, pp. 271-279, 2012.
    @article{OW12,
      author = {E.-R. Olderog and R. Wilhelm},
      title = {Turing und die {Verifikation}},
      journal = {Informatik-Spektrum},
      volume = {35},
      number = {4},
      pages = {271--279},
      year = {2012},
      optnote = {Themenheft: Turing} }
  • [article] bibtex | Go to document Go to document
    M. Swaminathan, J. -P. Katoen, and E. -R. Olderog, "Layered Reasoning for randomized distributed algorithms," Formal Asp. Comput., vol. 24, iss. 4-6, pp. 477-496, 2012.
    @article{SwaminathanKatoenOlderog12,
      author = {M. Swaminathan and J.-P. Katoen and E.-R. Olderog},
      title = {Layered Reasoning for randomized distributed algorithms},
      journal = {Formal Asp. Comput.},
      volume = {24},
      number = {4-6},
      year = {2012},
      pages = {477-496},
      url = {http://dx.doi.org/10.1007/s00165-012-0231-x} }
  • [inproceedings] bibtex
    E. -R. Olderog, "Automatic Verification of Real-Time Systems with Rich Data -- An Overview," in Proc. Theory and Applications of Models of Computation (TAMC), 2012, pp. 84-93.
    @inproceedings{Old12,
      author = {E.-R. Olderog},
      title = {Automatic Verification of Real-Time Systems with Rich Data -- An Overview},
      booktitle = {Theory and Applications of Models of Computation (TAMC)},
      editor = {Manindra Agrawal and S. Barry Cooper and Angsheng Li},
      series = {LNCS},
      volume = {7287},
      pages = {84--93},
      publisher = {Springer},
      year = {2012} }
  • [article] bibtex | Go to document Go to document
    J. Faber, S. Linker, E. Olderog, and J. Quesel, "Syspect - Modelling, Specifying, and Verifying Real-Time Systems with Rich Data," International Journal of Software and Informatics, vol. 5, iss. 1-2, pp. 117-137, 2011.
    @article{FLO+2011,
      author = {Johannes Faber and Sven Linker and Ernst-R{\"u}diger Olderog and Jan-David Quesel},
      title = {Syspect - Modelling, Specifying, and Verifying Real-Time Systems with Rich Data},
      journal = {International Journal of Software and Informatics},
      year = {2011},
      volume = {5},
      number = {1-2},
      part = {1},
      pages = {117--137},
      note = {ISSN 1673-7288.},
      url = {http://www.ijsi.org/IJSI/ch/reader/create_pdf.aspx?file_no=i78&flag=1&journal_id=ijsi},
      abstract = {We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect. },
      publists = {syspect} }
  • [inproceedings] bibtex | Go to document Go to document
    M. Hilscher, S. Linker, E. -R. Olderog, and A. P. Ravn, "An Abstract Model for Proving Safety of Multi-Lane Traffic Manoeuvres," in Proc. Int'l Conf.\ on Formal Engineering Methods (ICFEM), 2011, pp. 404-419.
    @inproceedings{avacs-h3-dec-11,
      author = {M. Hilscher AND S. Linker AND E.-R. Olderog AND A.P. Ravn},
      title = {An Abstract Model for Proving Safety of Multi-Lane Traffic Manoeuvres},
      booktitle = {Int'l Conf.\ on Formal Engineering Methods (ICFEM)},
      year = {2011},
      editor = {Shengchao Qin AND Zongyan Qiu},
      volume = {6991},
      series = {Lecture Notes in Computer Science},
      pages = {404--419},
      month = {Oct.},
      publisher = {Springer-Verlag},
      note = {The original publication is available at \url{http://www.springerlink.com/content/y4721k1525v23520}{www.springerlink.com}.},
      subproject = {H3},
      pdf = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hlor2011-icfem.pdf},
      url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hlor2011-icfem.pdf},
      abstract = { We present an approach to prove safety (collision freedom) of multi-lane motorway trac with lane-change manoeuvres. This is ultimately a hybrid veri cation problem due to the continuous dynamics of the cars. We abstract from the dynamics by introducing a new spatial interval logic based on the view of each car. To guarantee safety, we present two variants of a lane-change controller, one with perfect knowledge of the safety envelopes of neighbouring cars and one which takes only the size of the neighbouring cars into account. Based on these controllers we provide a local safety proof for unboundedly many cars by showing that at any moment the reserved space of each car is disjoint from the reserved space of any other car. } }
  • [inproceedings] bibtex
    J. Hoenicke, E. -R. Olderog, and A. Podelski, "Fairness for Dynamic Control," in Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2010, pp. 251-265.
    @inproceedings{HOP10,
      author = {J. Hoenicke and E.-R. Olderog and A. Podelski},
      title = {Fairness for Dynamic Control},
      editor = {J. Esparza and R. Majumdar },
      booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS) },
      series = {Lecture Notes in Computer Science},
      volume = {6015},
      publisher = {Springer-Verlag},
      pages = {251--265},
      year = {2010} }
  • [inproceedings] bibtex
    E. -R. Olderog and A. Podelski, "Explicit Fair Scheduling for Dynamic Control," in Proc. Concurrency, Compositionality, and Correctness, 2010, pp. 96-117.
    @inproceedings{OlPo10,
      author = {E.-R. Olderog and A. Podelski},
      editor = {D. Dams and U. Hannemann and M. Steffen},
      title = { Explicit Fair Scheduling for Dynamic Control },
      booktitle = {Concurrency, Compositionality, and Correctness },
      series = {Lecture Notes in Computer Science},
      volume = {5930 },
      publisher = {Springer-Verlag },
      pages = {96--117 },
      year = {2010} }
  • [inproceedings] bibtex | Go to document Go to document
    J. Hoenicke, R. Meyer, and E. -R. Olderog, "Kleene, Rabin, and Scott Are Available," in Proc. CONCUR 2010 - Concurrency Theory (CONCUR), 2010, pp. 462-477.
    @inproceedings{HMO10,
      author = {J. Hoenicke and R. Meyer and E.-R. Olderog},
      title = {Kleene, Rabin, and Scott Are Available},
      editor = {Paul Gastin and Fran\c{c}ois Laroussinie},
      booktitle = {CONCUR 2010 - Concurrency Theory (CONCUR)},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      volume = {6269},
      pages = {462-477},
      year = {2010},
      url = {http://dx.doi.org/10.1007/978-3-642-15375-4_32} }
  • [inproceedings] bibtex | Go to document Go to document
    E. -R. Olderog and M. Swaminathan, "Layered Composition for Timed Automata," in Proc. Formal Modeling and Analysis of Timed Systems (FORMATS), 2010, pp. 228-242.
    @inproceedings{OS10,
      author = {E.-R. Olderog and M. Swaminathan},
      title = {Layered Composition for Timed Automata},
      editor = {K. Chatterjee and T. A Henzinger},
      booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS) },
      series = {Lecture Notes in Computer Science},
      volume = {6246},
      publisher = {Springer-Verlag},
      pages = {228-242},
      year = {2010},
      url = {http://dx.doi.org/10.1007/978-3-642-15297-9_18} }
  • [inproceedings] bibtex
    E. -R. Olderog and R. Meyer, "Automata-theoretic verification based on counterexample specification," in Proc. Informatik als Dialog zwischen Theorie und Anwendung, 2009, pp. 217-225.
    @inproceedings{ero-rm-09,
      author = {E.-R. Olderog and R. Meyer},
      title = {Automata-theoretic verification based on counterexample specification},
      editor = {V. Diekert and K. Weicker and N. Weicker},
      booktitle = {Informatik als Dialog zwischen Theorie und Anwendung},
      year = {2009},
      pages = {217--225},
      publisher = {Vieweg-Teubner},
      publists = {rmeyer} }
  • [inproceedings] bibtex
    K. R. Apt, F. S. de Boer, and E. -R. Olderog, "Modular Verification of Recursive Programs," in Proc. Languages: From Formal to Natural, 2009, pp. 1-21.
    @inproceedings{ABO09,
      author = { K.R. Apt and F.S. de Boer and E.-R. Olderog },
      editor = { O. Grumberg and M. Kaminski and S. Katz and S. Wintner },
      title = { Modular Verification of Recursive Programs },
      booktitle = { Languages: From Formal to Natural },
      series = { Lecture Notes in Computer Science},
      volume = { 5333 },
      publisher = { Springer-Verlag },
      editor = { },
      pages = { 1--21 },
      year = { 2009 } }
  • [article] bibtex
    M. Möller, E. -R. Olderog, H. Rasch, and H. Wehrheim, "Integrating a Formal Method into a Software Engineering Process with UML and Java," Formal Apsects of Computing, vol. 20, pp. 161-204, 2008.
    @article{MORW08,
      author = {M. M{\"o}ller and E.-R. Olderog and H. Rasch and H. Wehrheim},
      title = {Integrating a Formal Method into a Software Engineering Process with {UML} and {Java}},
      journal = {Formal Apsects of Computing},
      year = {2008},
      volume = {20},
      pages = {161--204},
      abstract = {We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed {\em reactive systems}. To this end, we propose a specific UML {\em profile} for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for {\em verifying} properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating {\em contracts} for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by \CSPjassda{},
      an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts.},
      publists = {syspect} }
  • [inproceedings] bibtex | Go to document Go to document
    E. -R. Olderog, "Automatic Verification of Combined Specifications," in Proc. Proc. of the 1st Internat. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2007), Macau, 2008, pp. 3-16.
    @inproceedings{Old08,
      author = {E.-R. Olderog},
      title = {Automatic Verification of Combined Specifications},
      booktitle = {Proc. of the 1st Internat. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2007), Macau},
      year = {2008},
      editor = {G. Pu and V. Stolz},
      series = {ENTCS},
      journal = {Electr. Notes Theor. Comput. Sci.},
      issn = {1571-0661},
      volume = {207},
      number = {},
      month = {April},
      pages = {3--16},
      ee = {http://dx.doi.org/10.1016/j.entcs.2008.03.082},
      url = {},
      keywords = {Real-time systems, complex data, CSP, Object-Z, Duration Calculus, model checking, abstraction refinement, UML profile, tool support},
      abstract = { This paper gives an overview of results of the project ``Beyond Timed Automata'' carried out in the Collaborative Research Center AVACS (Automatic Verification and Analysis of Complex Systems) of the Universities of Oldenburg, Freiburg, and Saarbr\"ucken. We discuss how properties of high-level specifications of real-time systems combining the dimensions of process behaviour, data, and time can be automatically verified, exploiting recent advances in semantics, constraint-based model checking, and decision procedures for complex data. As specification language we consider CS-OZ-DC, which integrates concepts from Communicating Sequential Processes (CSP), Object-Z (OZ), and Duration Calculus (DC). Our approach to automatic verification of CSP-OZ-DC rests on a compositional semantics of this languages in terms of Phase-Event-Automata. These can be translated into Transition Constraint Systems which serve as an input language of an abstract refinement model checker called ARMC which can handle constraints covering both real-time and infinite data. This is demonstrated by a case study concerning emergency messages in the European Train Control System (ETCS). For CSP-OZ-DC we also discuss a UML profile and tool support. } }
  • [article] bibtex
    B. Becker, A. Podelski, W. Damm, M. Fränzle, E. -R. Olderog, and R. Wilhelm, "SFB/TR 14 AVACS -- Automatic Verification and Analysis of Complex Systems," it -- Information Technology, vol. 49, iss. 2, pp. 118-126, 2007.
    @article{AVACS07,
      author = {B. Becker and A. Podelski and W. Damm and M. Fr{\"a}nzle and E.-R. Olderog and R. Wilhelm},
      title = {{SFB/TR 14 AVACS -- Automatic Verification and Analysis of Complex Systems}},
      journal = {it -- Information Technology},
      publisher = {Oldenbourg},
      year = {2007},
      number = {2},
      volume = {49},
      pages = {118--126},
      note = {See also \url{http://www.avacs.org}{http://www.avacs.org}} }
  • [inproceedings] bibtex
    D. Basin, E. -R. Olderog, and P. E. Sevinç, "Specifying and analyzing security automata using CSP-OZ," in Proc. Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007), 2007, pp. 70-81.
    @inproceedings{BSO07,
      author = {D. Basin and E.-R. Olderog and P.E. Sevin\c{c}},
      title = {Specifying and analyzing security automata using {CSP-OZ}},
      booktitle = {Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007)},
      pages = {70--81},
      year = 2007, month = {March},
      publisher = {ACM Press},
      location = {Singapore},
      abstract = { Security automata are a variant of B\"uchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification language combining Communicating Sequential Processes (CSP) and Object-Z (OZ), to specify security automata, formalize their combination with target systems, and analyze the security of the resulting system specifications. We provide theoretical results relating CSP-OZ specifications and security automata and show how refinement can be used to reason about specifications of security automata and their combination with target systems. Through a case study, we provide evidence for the practical usefulness of this approach. This includes the ability to specify concisely complex operations and complex control, support for structured specifications, refinement, and transformational design, as well as automated, tool-supported analysis. } }
  • [inproceedings] bibtex
    W. Damm, A. Mikschl, J. Oehlerking, E. Olderog, J. Pang, A. Platzer, M. Segelken, and B. Wirtz, "Automating Verification of Cooperation, Control, and Design in Traffic Applications.," in Proc. Formal Methods and Hybrid Real-Time Systems, 2007, pp. 115-169.
    @inproceedings{DammMOOPPSW07,
      author = {Werner Damm and Alfred Mikschl and Jens Oehlerking and Ernst-R{\"u}diger Olderog and Jun Pang and Andr{\'e} Platzer and Marc Segelken and Boris Wirtz},
      title = {Automating Verification of Cooperation, Control, and Design in Traffic Applications.},
      year = {2007},
      pages = {115--169},
      editor = {Cliff Jones and Zhiming Liu and Jim Woodcock},
      booktitle = {Formal Methods and Hybrid Real-Time Systems},
      publisher = {Springer-Verlag},
      series = {LNCS},
      volume = {4700},
      doi = {10.1007/978-3-540-75221-9_6},
      issn = {},
      keywords = {},
      abstract = { We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.},
      note = {\url{http://dx.doi.org/10.1007/978-3-540-75221-9_6}{(c) Springer-Verlag}} }
  • [inproceedings] bibtex
    E. -R. Olderog and B. Steffen, "Formale Semantik und Programmverifikation," in Proc. Informatik-Handbuch, 4. Auflage, 2006, pp. 145-166.
    @inproceedings{erobs06,
      author = {E.-R. Olderog and B. Steffen},
      title = {{F}ormale {S}emantik und {P}rogrammverifikation},
      booktitle = {Informatik-Handbuch, 4. Auflage},
      editor = {P. Rechenberg and G. Pomberger},
      year = 2006, publisher = {Hanser Verlag},
      pages = {145--166} }
  • [article] bibtex
    W. Damm, H. Hungar, and E. -R. Olderog, "Verification of cooperating traffic agents," International Journal of Control, vol. 79, iss. 5, pp. 395-421, 2006.
    @article{DHO06,
      author = {W. Damm and H. Hungar and E.-R. Olderog},
      title = {Verification of cooperating traffic agents},
      journal = {International Journal of Control},
      year = {2006},
      optkey = {},
      volume = {79},
      number = {5},
      month = {May},
      pages = {395--421},
      abstract = { This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented verification methodology is equally applicable for avionics applications (such as TCAS, the Traffic Alert and Collision Avoidance System), train applications (such as ETCS, the European Train Control System), or automotive applications (such as platooning). We present a verification rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind ``a collision will never occur'', and whose premises can either be established by off-line analysis of the worst-case behavior of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. A companion paper will show how such local proof obligations can be discharged automatically. } }
  • [inproceedings] bibtex
    P. E. Sevinç, D. Basin, and E. -R. Olderog, "Controlling Access to Documents: A Formal Access Control Model," in Proc. ETRICS 2006, 2006, pp. 352-367.
    @inproceedings{SBO06,
      author = {P. E. Sevin\c{c} and D. Basin and E.-R. Olderog},
      booktitle = {ETRICS 2006},
      editor = {G\"unter M\"uller},
      month = {June},
      pages = {352--367},
      publisher = {Springer-Verlag},
      series = {LNCS},
      title = {Controlling Access to Documents: A Formal Access Control Model},
      volume = 3995, year = 2006, abstract = { Current access-control systems for documents suffer from one or more of the following limitations: they are coarse-grained, limited to XML documents, ot unable to maintain control over copies of documents once they are released by the system. We present a formal model of a system that overcomes all of these restrictions. It is very fine-grained, supporst a general class of documents, and provides a foundation for usage control. } }
  • [article] bibtex
    E. -R. Olderog and H. Wehrheim, "Specification and (property) inheritance in CSP-OZ," Science of Computer Programming, vol. 55, pp. 227-257, 2005.
    @article{OW05,
      author = {E.-R. Olderog and H. Wehrheim},
      title = {{Specification and (property) inheritance in CSP-OZ}},
      journal = {Science of Computer Programming},
      year = {2005},
      volume = {55},
      pages = {227--257},
      abstract = { CSP-OZ [Fis97, Fis00] is a combination of Communicating Sequential Processes (CSP) and Object-Z (OZ). It enables the specification of systems having both a state-based and a behaviour-oriented view using the object-oriented concepts of classes, instantiation and inheritance. CSP-OZ has a process semantics in the failure divergence model of CSP. In this paper we explain CSP-OZ and investigate the notion of inheritance. Furthermore, we study the issue of property inheritance among classes. We prove in a uniform way that behavioural subtyping relations between classes introduced in [Weh02] guarantee the inheritance of safety and ``liveness'' properties. \emph{Key words}: CSP, Object-Z, failures divergence semantics, inheritance, safety and ``liveness'' properties, model-checking, FDR \begin{thebibliography} \bibitem{Fis97} C.~Fischer. \newblock {CSP-OZ}: A combination of {Object-Z} and {CSP}. \newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open Object-Based Distributed Systems (FMOODS'97)},
      volume~2, pages 423--438. Chapman \& Hall, 1997. \bibitem{Fis00} C.~Fischer. \newblock {\em Combination and Implementation of Processes and Data: From {CSP-OZ} to {Java}}. \newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000. \bibitem{Weh02} H.~Wehrheim. \newblock Behavioural subtyping in object-oriented specification formalisms. \newblock University of Oldenburg, Habilitation Thesis, 2002. \end{thebibliography} } }
  • [inproceedings] bibtex
    W. Damm, H. Hungar, and E. -R. Olderog, "On the Verification of Cooperating Traffic Agents," in Proc. FMCO 2003: Formal Methods for Components and Objects, 2004, pp. 77-110.
    @inproceedings{DaHuOl04,
      author = {W. Damm and H. Hungar and E.-R. Olderog},
      title = {On the Verification of Cooperating Traffic Agents},
      booktitle = {FMCO 2003: Formal Methods for Components and Objects},
      year = {2004},
      editor = {F.S. de Boer and M.M. Bonsangue and S. Graf and W.-P. de Roever},
      volume = {3188},
      pages = {77--110},
      series = {LNCS},
      abstract = { This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented veri cation methodology is equally applicable for avionics applications (such as TCAS), train applications (such as ETCS), or automotive applications (such as platooning). We present a veri cation rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind ``a collision will never occur'', and whose premises can either be established by o -line analysis of the worst-case behavior of the involved tra c agents, or by purely local proofs, involving only a single tra c agent. In a companion paper we will show, how such local proof obligations can be discharged automatically. } }
  • [inproceedings] bibtex | Go to document Go to document
    M. Möller, E. -R. Olderog, H. Rasch, and H. Wehrheim, "Linking CSP-OZ with UML and Java: A Case Study," in Proc. Integrated Formal Methods, 2004, pp. 267-286.
    @inproceedings{MORW04,
      author = {M. M\"oller and E.-R. Olderog and H. Rasch and H. Wehrheim},
      title = {{Linking CSP-OZ with UML and Java: A Case Study}},
      editor = {E. Boiten and J. Derrick and G. Smith},
      booktitle = {Integrated Formal Methods},
      series = {Lecture Notes in Computer Science},
      number = {2999},
      publisher = springer, issn = {0302-9743},
      pages = {267--286},
      year = {2004},
      month = {March},
      abstract = { We describe how CSP-OZ, an integrated formal method combining the process algebra CSP with the specification language Object-Z, can be linked to standard software engineering languages, viz.\ UML and Java. Our aim is to generate a significant part of the CSP-OZ specification from an initially developed UML model using a UML profile for CSP-OZ, and afterwards transform the formal specification into assertions written in the Java Modelling Language JML complemented by CSP$_{jassda}$. The intermediate CSP-OZ specification serves to verify correctness of the UML model, and the assertions control at runtime the adherence of a Java implementation to these formal requirements. We explain this approach using the case study of a ``holonic manufacturing system'' in which coordination of transportation and processing is distributed among stores, machine tools and agents without central control. },
      url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/morw04.pdf},
      publists = {moeller formoos} }
  • [inproceedings] bibtex
    E. -R. Olderog and H. Wehrheim, "Specification and Inheritance in CSP-OZ," in Proc. Formal Methods for Components and Objects, 2003, pp. 361-379.
    @inproceedings{OlWe02,
      author = {E.-R. Olderog and H. Wehrheim},
      title = {{Specification and Inheritance in CSP-OZ}},
      editor = {F. de Boer and M. Bosangue and S. Graf and W.-P. de Roever},
      booktitle = {Formal Methods for Components and Objects},
      volume = {2852},
      series = {LNCS},
      pages = {361--379},
      publisher = {Springer},
      year = {2003},
      abstract = { CSP-OZ [Fis97,Fis00] is a combination of Communicating Sequential Processes (CSP) and Object-Z (OZ). It enables the specification of systems having both a state-based and a behaviour-oriented view using the object-oriented concepts of classes, instantiation and inheritance. CSP-OZ has a process semantics in the failures divergence model of CSP. In this paper we explain CSP-OZ and investigate the notion of inheritance. Behavioural subtyping relations between classes introduced in [Weh02] guarantee the inheritance of safety and ``liveness'' properties. \begin{thebibliography} \bibitem{Fis97} C.~Fischer. \newblock {CSP-OZ}: A combination of {Object-Z} and {CSP}. \newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open Object-Based Distributed Systems (FMOODS'97)},
      volume~2, pages 423--438. Chapman \& Hall, 1997. \bibitem{Fis00} C.~Fischer. \newblock {\em Combination and Implementation of Processes and Data: From {CSP-OZ} to {Java}}. \newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000. \bibitem{Weh02} H.~Wehrheim. \newblock Behavioural subtyping in object-oriented specification formalisms. \newblock University of Oldenburg, Habilitation Thesis, 2002. \end{thebibliography} } }
  • [article] bibtex
    E. -R. Olderog and H. Dierks, "Moby/RT: A Tool for Specification and Verification of Real-Time Systems," Journal of Universal Computer Science, vol. 9, pp. 88-105, 2003.
    @article{OD03,
      author = {E.-R. Olderog and H. Dierks},
      title = {{Moby/RT: A Tool for Specification and Verification of Real-Time Systems}},
      journal = {Journal of Universal Computer Science},
      year = {2003},
      optkey = {},
      volume = {9},
      optnumber = {},
      pages = {88--105},
      optmonth = {},
      optnote = {},
      abstract = { The tool Moby/RT supports the design of real-time systems at the levels of requirements, design specifications and programs. Requirements are expressed by constraint diagrams [Kle00], design specifications by PLC-Automata [Die00], and programs by Structured Text, a programming language dedicated for programmable logic controllers (PLCs), or by programs for LEGO Mindstorm robots. In this paper we outline the theoretical background of Moby-RT by discussing its semantic basis and its use for automatic verification by utilising the model-checker UPPAAL. \begin{thebibliography} \bibitem{Kle00} Kleuker, C. (2000). \newblock {\em {Constraint Diagrams}}. \newblock PhD thesis, University of Oldenburg. \bibitem[Dierks, 2000]{Die00} Dierks, H. (2000). \newblock {PLC-Automata: A New Class of Implementable Real-Time Automata}. \newblock {\em TCS},
      253(1):61--93. \end{thebibliography} } }
  • [article] bibtex
    H. Dierks and E. -R. Olderog, "Temporale Spezifikationslogiken," at-Automatisierungstechnik, vol. 51, iss. 2, p. a1-a4, 2003.
    @article{DO03,
      author = {H. Dierks and E.-R. Olderog},
      title = {{Temporale Spezifikationslogiken}},
      journal = {at-Automatisierungstechnik},
      year = {2003},
      optkey = {},
      volume = {51},
      number = {2},
      optmonth = {},
      pages = {A1--A4},
      optnote = {},
      optannote = {},
      abstract = { Logiken sind in der Informatik ein weitverbreitetes Mittel zur Spezifikation. Dazu werden Logiken verschiedener Auspr{\"a}gung benutzt, z.B. temporale Logiken f{\"u}r reaktive Systeme, zu denen die Systeme der Automatisierungstechnik z{\"a}hlen. Dieser Beitrag enth{\"a}lt eine Einf{\"u}hrung in die wichtigsten temporalen Logiken und Literaturverweise. \textbf{English}\\ Logics are often used in computer science as specification languages. There is a rich variety of logics to choose from depending on the problem. Systems in automation technology are typically reactive systems for which temporal logics are adequate. We introduce the most important temporal logics and give reference for further reading. } }
  • [article] bibtex
    J. Hoenicke and E. -R. Olderog, "CSP-OZ-DC: A Combination of Specification Techniques for Processes, Data and Time," Nordic Journal of Computing, vol. 9, iss. 4, pp. 301-334, 2002.
    @article{HO02b,
      author = {J. Hoenicke and E.-R. Olderog},
      title = {{CSP-OZ-DC}: A Combination of Specification Techniques for Processes, Data and Time},
      journal = {Nordic Journal of Computing},
      year = {2002},
      volume = {9},
      number = {4},
      pages = {301--334},
      note = {appeared March 2003},
      abstract = { CSP-OZ-DC is a new combination of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. This combination is illustrated by specifying the train controller of a case study on radio controlled railway crossings. The technical contribution of the paper is a smooth integration of the underlying semantic models and its use for verifying timing properties of CSP-OZ-DC specifications. This is done by combining the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for timed automata with a new tool \emph{f2u} that transforms FDR transition systems and certain patterns of Duration Calculus formulae into timed automata. This approach is illustrated by the example of a vending machine. \begin{thebibliography} \bibitem{BLL97} J.~Bengtsson, K.G. Larsen, F.~Larsson, P.~Pettersson, and Wang Yi. \newblock Uppaal -- a tool suite for automatic verification of real-time systems. \newblock In R.~Alur, T.A. Henzinger, and E.D. Sonntag, editors, {\em Hybrid Systems III -- Verification and Control},
      volume 1066 of {\em LNCS},
      pages 232--243. Springer, 1997. \bibitem{Hoa85} C.A.R. Hoare. \newblock {\em Communicating Sequential Processes}. \newblock Prentice Hall, 1985. \bibitem{Ros94} A.W. Roscoe. \newblock Model-checking {CSP}. \newblock In A.W. Roscoe, editor, {\em A Classical Mind --- Essays in Honour of C.A.R.Hoare},
      pages 353--378. Prentice-Hall, 1994. \bibitem{Smi00} G.~Smith. \newblock {\em The Object-Z Specification Language}. \newblock Kluwer Academic Publisher, 2000. \bibitem{ZHR91} C.~Zhou, C.A.R. Hoare, and A.P. Ravn. \newblock A calculus of durations. \newblock {\em Information Processing Letters},
      40(5):269--276, 1991. \end{thebibliography} } }
  • [inproceedings] bibtex | Go to document Go to document
    J. Hoenicke and E. -R. Olderog, "Combining Specification Techniques for Processes Data and Time," in Proc. Integrated Formal Methods, 2002, pp. 245-266.
    @inproceedings{ho02,
      author = {J. Hoenicke and E.-R. Olderog},
      title = {{Combining Specification Techniques for Processes Data and Time}},
      editor = {M. Butler and L. Petre and K. Sere},
      booktitle = {Integrated Formal Methods},
      series = {Lecture Notes in Computer Science},
      volume = {2335},
      publisher = springer, url = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/ho02-ifm.pdf},
      year = {2002},
      month = {May},
      pages = {245--266},
      abstract = { We present a new combination CSP-OZ-DC of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. The emphasis is on a smooth integration of the underlying semantic models and its use for verifying properties of CSP-OZ-DC specifications by a combined application of the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for Timed Automata. This approach is applied to part of a case study on radio controlled railway crossings. } }
  • [inproceedings] bibtex
    M. Broy and E. -R. Olderog, "Trace-Oriented Models of Concurrency," in Proc. Handbook of Process Algebra, 2001, pp. 101-195.
    @inproceedings{bo01,
      author = {M. Broy and E.-R. Olderog},
      title = {{Trace-Oriented Models of Concurrency}},
      booktitle = {Handbook of Process Algebra},
      optcrossref = {},
      optkey = {},
      pages = {101-195},
      year = {2001},
      editor = {J.A. Bergstra and A. Ponse and S.A. Scott},
      optvolume = {},
      optnumber = {},
      optseries = {},
      optaddress = {},
      optmonth = {},
      optorganization = {},
      publisher = {Elsevier Science B.V.},
      optnote = {},
      abstract = { This chapter provides an in-depth presentation of trace-oriented models of concurrent processes. We begin by introducing and investigating finite traces as a simple abstraction of the transition behaviour of automata. Using finite traces safety properties of processes can be modelled. Later infinite traces or {\it streams} together with stream processing functions are studied. Using infinite traces more advanced phenomena like fairness and liveness properties can be modelled. We discuss and relate operational, denotational, algebraic and logical approaches to trace-oriented models and explain methods for the specification and verification of process behaviour based on these models. } }
  • [inproceedings] bibtex | Go to document Go to document
    C. Fischer, E. -R. Olderog, and H. Wehrheim, "A CSP view on UML-RT structure diagrams," in Proc. Fundamental Approaches to Software Engineering, 2001, pp. 91-108.
    @inproceedings{fow01,
      author = {C. Fischer and E.-R. Olderog and H. Wehrheim},
      title = {{A CSP view on UML-RT structure diagrams}},
      booktitle = {{Fundamental Approaches to Software Engineering}},
      optcrossref = {},
      optkey = {},
      pages = {91-108},
      year = {2001},
      editor = {H. Husmann},
      volume = {2029},
      optnumber = {},
      series = lncs, optaddress = {},
      optmonth = {},
      optorganization = {},
      publisher = springer, optnote = {},
      optannote = {},
      abstract = { UML-RT is an extension of UML for modelling embedded reactive and real-time software systems. Its particular focus lies on system descriptions on the architectural level, defining the overall system structure. In this paper we propose to use UML-RT structure diagrams together with the formal method CSP-OZ combining CSP and Object-Z. While CSP-OZ is used for specifying the system components themselves (by CSP-OZ classes), UML-RT diagrams provide the architecture description. Thus the usual architecture specification in terms of the CSP operators parallel composition, renaming and hiding is replaced by a graphical description. To preserve the formal semantics of CSP-OZ specifications, we develop a translation from UML-RT structure diagrams to CSP. Besides achieving a more easily accessible, graphical architecture modelling for CSP-OZ, we thus also give a semantics to UML-RT structure diagrams. },
      publists = {formoos},
      url = {http://csd.informatik.uni-oldenburg.de/~wehrheim/fase01.ps} }
  • [inproceedings] bibtex | Go to document Go to document
    E. -R. Olderog and A. P. Ravn, "Documenting Design Refinement," in Proc. Proc. of the Third Workshop on Formal Methods in Software Practice, 2000, pp. 89-100.
    @inproceedings{or00,
      author = {E.-R. Olderog and A.P. Ravn},
      title = {Documenting Design Refinement},
      editor = {M.P.E. Heimdahl},
      booktitle = {Proc. of the Third Workshop on Formal Methods in Software Practice},
      pages = {89--100},
      publisher = {ACM},
      year = {2000},
      abstract = { We show how UML class diagrams can be used to document design by refinement in the early design stages. This is illustrated by an example from the area of embedded real-time and hybrid systems. A precise semantics is given for the UML class diagrams by translation to the Z schema calculus. },
      url = {http://csd.Informatik.Uni-Oldenburg.DE/pub/Papers/or00.ps} }
  • [article] bibtex
    E.-R.Olderog, "Sichere Bahnsteuerungen," Log IN, iss. 1, pp. 64-65, 1999.
    @article{ero99-login,
      author = {E.-R.Olderog},
      title = {Sichere {B}ahnsteuerungen},
      journal = {Log {IN}},
      pages = {64--65},
      number = {1},
      year = {1999} }
  • [article] bibtex | Go to document Go to document
    M. Schenke and E. -R. Olderog, "Transformational design of real-time systems -- Part 1: from requirements to program specifications.," Acta Informatica 36, pp. 1-65, 1999.
    @article{msero99,
      author = {Michael Schenke and E.-R. Olderog},
      title = {Transformational design of real-time systems -- Part 1: from requirements to program specifications.},
      journal = {Acta Informatica 36},
      pages = {1-65},
      year = {1999},
      url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/msero97_1.ps.gz} }
  • [inproceedings] bibtex
    E. -R. Olderog, "Correct Real-Time Software for Programmable Logic Controllers," in Proc. Correct System Design - Recent Insights and Advances, 1999, pp. 342-362.
    @inproceedings{ero99,
      author = {E.-R. Olderog},
      title = {{Correct Real-Time Software for Programmable Logic Controllers}},
      booktitle = {{Correct System Design - Recent Insights and Advances}},
      series = {Lecture Notes in Computer Science},
      volume = {1710},
      publisher = {Springer},
      year = {1999},
      pages = {342--362} }
  • [inproceedings] bibtex
    E. -R. Olderog, "Entwicklung korrekter zeitkritischer Systeme," in Proc. Formale Beschreibungstechniken für verteilte Systeme, 1999, pp. 7-16.
    @inproceedings{ero99-gi/itg,
      author = {E.-R. Olderog},
      title = {Entwicklung korrekter zeitkritischer {Systeme}},
      booktitle = {{Formale} {Beschreibungstechniken} f\"ur verteilte {Systeme}},
      editor = {K. Spies and B. Sch\"atz },
      series = {GI/ITG Fachgespr\"ach},
      volume = {9},
      publisher = {Utz Verlag},
      year = {1999},
      pages = {7--16} }
  • [inproceedings] bibtex
    B. Krieg-Brückner, J. Peleska, E. -R. Olderog, and A. Baer, "The UniForM Workbench, a Universal Development Environment for Formal Methods," in Proc. FM'99 -- Formal Methods, 1999, pp. 1186-1205.
    @inproceedings{uniform99,
      author = {B. Krieg-Br\"uckner and J. Peleska and E.-R. Olderog and A. Baer},
      title = {{The UniForM Workbench, a Universal Development Environment for Formal Methods}},
      editor = {J.M. Wing and J. Woodcock and J. Davies},
      booktitle = {{FM'99 -- Formal Methods}},
      series = {Lecture Notes in Computer Science},
      volume = {1709},
      publisher = {Springer},
      year = {1999},
      pages = {1186--1205} }
  • [inproceedings] bibtex
    E. -R. Olderog, "Formal Methods in Real-Time Systems," in Proc. Proceedings of the 10th EuroMicro Workshop on Real Time Systems, 1998, pp. 254-263.
    @inproceedings{ero98:formalmethodrealtimesystem,
      author = {E.-R. Olderog},
      title = {Formal Methods in Real-Time Systems},
      booktitle = {Proceedings of the 10th EuroMicro Workshop on Real Time Systems},
      year = 1998, organization = {IEEE Computer Society},
      month = {June},
      pages = {254--263} }
  • [inproceedings] bibtex
    V. Grabowski, C. Dietz, and E. -R. Olderog, "Semantics for Timed Message Sequence Charts via Constraint Diagrams," in Proc. Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC, 1998, pp. 251-260.
    @inproceedings{erocd98,
      author = {V. Grabowski and C. Dietz and E.-R. Olderog},
      title = {{Semantics for Timed Message Sequence Charts via Constraint Diagrams}},
      booktitle = {Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC},
      editor = {Y. Lahav and A. Wolisz and J. Fischer and E. Holz},
      series = {Informatik-Bericht Nr. 104},
      year = {1998},
      pages = {251-260},
      publisher = {Humbold-Universitaet zu Berlin/Germany} }
  • [inproceedings] bibtex
    E. -R. Olderog and H. Dierks, "Decomposing Real-Time Specifications," in Proc. Compositionality: The Significant Difference, 1998, pp. 465-489.
    @inproceedings{erohd98,
      author = {E.-R. Olderog and H. Dierks},
      title = {{Decomposing Real-Time Specifications}},
      booktitle = {{Compositionality: The Significant Difference}},
      optcrossref = {},
      optkey = {},
      editor = {H. Langmaack and A. Pnueli and W.P. de Roever},
      volume = {1536},
      optnumber = {},
      series = lncs, year = {1998},
      optorganization = {},
      publisher = springer, optaddress = {},
      optmonth = {},
      pages = {465--489},
      optannote = {},
      note = {{\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/erohd97.ps.gz} {An abstract is available on-line}}} }
  • [article] bibtex
    C. Fischer, S. Kleuker, and E. -R. Olderog, "Beweisbar korrekte Telekommunikationssysteme," Informationstechnik und Technische Informatik, vol. 3, pp. 22-28, 1997.
    @article{cfskero97,
      author = {C. Fischer and S. Kleuker and E.-R. Olderog},
      title = {{B}eweisbar korrekte {T}elekommunikationssysteme},
      journal = {Informationstechnik und Technische Informatik},
      year = 1997, volume = 3, pages = {22--28},
      note = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/cfskero97-a.ps.gz} {An extended abstract is available on-line}},
      publists = {s-kleuker} }
  • [incollection] bibtex
    E. -R. Olderog, A. P. Ravn, and J. U. Skakkebæk, "Refining System Requirements to Program Specifications," in Formal Methods for Real-Time Computing, Heitmeyer, C. and Mandrioli, D., Eds., Wiley, 1996, vol. 5, pp. 107-134.
    @incollection{ero96,
      author = {E.-R. Olderog and A. P. Ravn and J. U. Skakkeb{\ae}k},
      title = {Refining System Requirements to Program Specifications},
      editor = {C. Heitmeyer and D. Mandrioli},
      booktitle = {Formal Methods for Real-Time Computing},
      chapter = 5, pages = {107--134},
      publisher = {Wiley},
      series = {Trends in Software},
      volume = 5, year = 1996, note = {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/ero96.ps.gz} {An abstract is available on-line}} }
  • [inproceedings] bibtex | Go to document Go to document
    E. -R. Olderog and M. Schenke, "Design of Real-Time Systems: The Interface between Duration Calculus and Program Specifications," in Proc. Structures in Concurrency Theory, 1995, pp. 32-54.
    @inproceedings{eroms95,
      author = {E.-R. Olderog and M. Schenke},
      title = {Design of Real-Time Systems: The Interface between Duration Calculus and Program Specifications},
      editor = {J. Desel},
      booktitle = {Structures in Concurrency Theory},
      publisher = springer, series = wics, year = 1995, pages = {32--54},
      url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/eroms95.ps.gz} }
  • [inproceedings] bibtex
    J. He, C. A. R. Hoare, M. Fränzle, M. Müller-Olm, E. -R. Olderog, M. Schenke, M. R. Hansen, A. P. Ravn, and H. Rischel, "Provably Correct Systems," in Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94), 1994, pp. 288-335.
    @inproceedings{eroms94-ftrtft,
      author = {Jifeng He and C. A. R. Hoare and M. Fr\"anzle and M. M\"uller-Olm and E.-R. Olderog and M. Schenke and M. R. Hansen and A. P. Ravn and H. Rischel},
      title = {Provably Correct Systems},
      editor = {H. Langmaack and W. P. {de Roever} and J. Vytopil},
      booktitle = {Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94)},
      series = lncs, publisher = springer, year = 1994, volume = 863, pages = {288--335} }
  • [inproceedings] bibtex
    J. P. Bowen, M. Fränzle, E. -R. Olderog, and A. P. Ravn, "Developing Correct Systems," in Proc. Proceedings of the 5th EUROMICRO Workshop on Real-Time Systems (Oulu, Finland), 1993, pp. 176-189.
    @inproceedings{ero93,
      author = {J. P. Bowen and M. Fr\"anzle and E.-R. Olderog and A. P. Ravn},
      title = {Developing Correct Systems},
      booktitle = {Proceedings of the 5th EUROMICRO Workshop on Real-Time Systems (Oulu, Finland)},
      pages = {176--189},
      publisher = {IEEE Computer Society Press},
      year = 1993 }
  • [techreport] bibtex | Go to document Go to document
    M. R. Hansen, E. -R. Olderog, M. Schenke, M. Fränzle, B. von Karger, M. Müller-Olm, and H. Rischel, "A Duration Calculus Semantics for Real-Time Reactive Systems," uniol-fb10, ProCoS II document [OLD MRH 1/1], 1993.
    @techreport{eroms93,
      author = {M. R. Hansen and E.-R. Olderog and M. Schenke and M. Fr\"anzle and B. {von Karger} and M. M\"uller-Olm and H. Rischel},
      title = {A {Duration Calculus} Semantics for Real-Time Reactive Systems},
      type = {ProCoS II document},
      number = {[OLD MRH 1/1]},
      institution = uniol-fb10, month = sep, year = 1993, url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/eroms93.ps.gz} }
  • [inproceedings] bibtex
    E. -R. Olderog and S. Rössig, "A Case Study in Transformational Design of Concurrent Systems," in Proc. Theory and Practice of Software Development (TAPSOFT'93), 1993, pp. 90-104.
    @inproceedings{erosr93,
      author = {E.-R. Olderog and S. R\"ossig},
      title = {A Case Study in Transformational Design of Concurrent Systems},
      editor = {M.-C. Gaudel and J.-P. Jouannaud},
      booktitle = {Theory and Practice of Software Development (TAPSOFT'93)},
      series = lncs, volume = 668, publisher = springer, year = 1993, pages = {90--104} }
  • [incollection] bibtex
    E. -R. Olderog, "Systematic derivation of communicating programs," in Programming and Mathematical Method, Broy, M., Ed., springer, 1992, pp. 369-407.
    @incollection{ero92,
      author = {E.-R. Olderog},
      title = {Systematic derivation of communicating programs},
      booktitle = {Programming and Mathematical Method},
      publisher = springer, year = 1992, editor = {M. Broy},
      pages = {369--407} }
  • [inproceedings] bibtex
    E. -R. Olderog, "Interfaces between Languages for Communicating Systems," in Proc. Automata, Languages and Programming. Proceedings of the 19th ICALP 1992, 1992, pp. 641-655.
    @inproceedings{ero92-icalp,
      author = {E.-R. Olderog},
      title = {Interfaces between Languages for Communicating Systems},
      editor = {W. Kuich},
      booktitle = {Automata, Languages and Programming. Proceedings of the 19th ICALP 1992},
      series = lncs, volume = 623, publisher = springer, year = 1992, pages = {641--655},
      note = {Invited paper} }
  • [article] bibtex
    E. -R. Olderog, "Correctness of Concurrent Processes," tcs, vol. 80, pp. 263-288, 1991.
    @article{ero91-correctness,
      author = {E.-R. Olderog},
      title = {Correctness of Concurrent Processes},
      journal = tcs, year = 1991, volume = 80, pages = {263--288} }
  • [incollection] bibtex
    K. R. Apt and E. -R. Olderog, "Introduction to Program Verification," in Formal Description of Programming Concepts, Neuhold, E. J. and Paul, M., Eds., springer, 1991, pp. 363-429.
    @incollection{ero91-intro,
      author = {K. R. Apt and E.-R. Olderog},
      title = {Introduction to Program Verification},
      booktitle = {Formal Description of Programming Concepts},
      series = {IFIP State-of-the-Art Reports},
      publisher = springer, year = 1991, editor = {E. J. Neuhold and M. Paul},
      pages = {363--429} }
  • [inproceedings] bibtex
    E. -R. Olderog and K. R. Apt, "Using transformations to verify parallel programs," in Proc. Algebraic Methods II: Theory, Tools and Applications, 1991, pp. 55-81.
    @inproceedings{ero91-algebraic,
      author = {E.-R. Olderog and K. R. Apt},
      title = {Using transformations to verify parallel programs},
      booktitle = {Algebraic Methods II: Theory, Tools and Applications},
      editor = {J. A. Bergstra and L. M. G. Feijs},
      volume = 490, series = lncs, year = 1991, publisher = springer, pages = {55--81} }
  • [inproceedings] bibtex
    E. -R. Olderog, "Towards a Design Calculus for Communicating Programs," in Proc. Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR'91) (Amsterdam, The Netherlands), 1991, pp. 61-77.
    @inproceedings{ero91-concur,
      author = {E.-R. Olderog},
      title = {Towards a Design Calculus for Communicating Programs},
      booktitle = {Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR'91) (Amsterdam, The Netherlands)},
      editor = {J. C. M. Baeten and J. F. Groote},
      volume = 527, series = lncs, year = 1991, publisher = springer, pages = {61--77} }
  • [article] bibtex
    C. J. -J. Meyer and E. -R. Olderog, "Hiding in Stream Semantics of Uniform Concurrency," acta, vol. 27, pp. 381-397, 1990.
    @article{ero90-acta,
      author = {J.-J. Ch. Meyer and E.-R. Olderog},
      title = {Hiding in Stream Semantics of Uniform Concurrency},
      journal = acta, year = 1990, volume = 27, pages = {381--397} }
  • [incollection] bibtex
    K. R. Apt, F. S. de Boer, and E. -R. Olderog, "Proving termination of parallel programs," in Beauty is our Business --- A Birthday Salute to Edsger W. Dijkstra, Feijen, W. H. J., van Gasteren, A. J. M., Gries, D., and Misra, J., Eds., springer, 1990.
    @incollection{ero90-dijkstra,
      author = {K. R. Apt and F. S. {de Boer} and E.-R. Olderog},
      title = {Proving termination of parallel programs},
      booktitle = {Beauty is our Business --- A Birthday Salute to Edsger W. Dijkstra},
      publisher = springer, year = 1990, editor = {W. H. J. Feijen and A. J. M. {van Gasteren} and D. Gries and J. Misra} }
  • [incollection] bibtex
    E. -R. Olderog, "From trace specifications to process terms," in Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, de Bakker, J. W., de Roever, W. -P., and Rozenberg, G., Eds., springer, 1990, vol. 430, pp. 592-621.
    @incollection{ero90,
      author = {E.-R. Olderog},
      title = {From trace specifications to process terms},
      booktitle = {Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness},
      publisher = springer, year = 1990, editor = {J. W. {de Bakker} and W.-P. {de Roever} and G. Rozenberg},
      volume = 430, series = lncs, pages = {592--621} }
  • [article] bibtex
    B. D., C. A. R. \. Hoare, J. P. Bowen, He Jifeng, H. Langmaack, E. -R. Olderog, U. H. Martin, V. Stavridou, F. Nielson, H. R. Nielson, H. Barringer, D. Edwards, H. H. Lø., A. P. Ravn, and H. S. Rischel, "A ProCoS Project Description," Bulletin of the European Association for Theoretical Computer Science (EATCS), vol. 39, pp. 60-73, 1989.
    @article{ero89, title = {A {ProCoS} Project Description},
      author = {D. Bj\o{}rner and C. A. R.\ Hoare and J. P. Bowen and {He Jifeng} and H. Langmaack and E.-R. Olderog and U. H. Martin and V. Stavridou and F. Nielson and H. R. Nielson and H. Barringer and D. Edwards and H. H. L\o{}vengreen and A. P. Ravn and H. S. Rischel},
      journal = {Bulletin of the European Association for Theoretical Computer Science (EATCS)},
      volume = 39, pages = {60--73},
      month = {October},
      year = 1989 }
  • [article] bibtex
    J. W. de Bakker, C. J. -J. Meyer, E. -R. Olderog, and J. I. Zucker, "Transition Systems, Metric Spaces and Ready Sets in the Semantics of Uniform Concurrency," jcss, vol. 36, pp. 158-224, 1988.
    @article{ero88-jcss,
      author = {J. W. {de Bakker} and J.-J. Ch. Meyer and E.-R. Olderog and J. I. Zucker},
      title = {Transition Systems, Metric Spaces and Ready Sets in the Semantics of Uniform Concurrency},
      journal = jcss, year = 1988, volume = 36, pages = {158--224} }
  • [article] bibtex
    J. A. Bergstra, J. W. Klop, and E. -R. Olderog, "Readies and Failures in the Algebra of Communicating Processes," siam, vol. 17, pp. 1134-1177, 1988.
    @article{ero88-siam,
      author = {J. A. Bergstra and J. W. Klop and E.-R. Olderog},
      title = {Readies and Failures in the Algebra of Communicating Processes},
      journal = siam, year = 1988, volume = 17, pages = {1134--1177} }
  • [article] bibtex
    E. -R. Olderog and K. R. Apt, "Fairness in Parallel Programs: the Transformational Approach," acmtoplas, vol. 10, pp. 420-455, 1988.
    @article{ero88-toplas,
      author = {E.-R. Olderog and K. R. Apt},
      title = {Fairness in Parallel Programs: the Transformational Approach},
      journal = acmtoplas, year = 1988, volume = 10, pages = {420--455} }
  • [article] bibtex
    J. W. de Bakker, C. J. -J. Meyer, and E. -R. Olderog, "Infinite Streams and Finite Observations in the Semantics of Uniform Concurrence," tcs, vol. 49, pp. 87-112, 1987.
    @article{ero87,
      author = {J. W. de Bakker and J.-J. Ch. Meyer and E.-R. Olderog},
      title = {Infinite Streams and Finite Observations in the Semantics of Uniform Concurrence},
      journal = tcs, year = 1987, volume = 49, pages = {87--112} }
  • [inproceedings] bibtex
    J. A. Bergstra, J. W. Klop, and E. -R. Olderog, "Failures without Chaos: a Process Semantics for Fair Abstraction," in Proc. Formal Description of Programming Concepts -- III, Amsterdam, 1987, pp. 77-101.
    @inproceedings{bko87,
      author = {J.A. Bergstra and J.W. Klop and E.-R. Olderog},
      title = {Failures without Chaos: a Process Semantics for Fair Abstraction},
      booktitle = {Formal Description of Programming Concepts -- III},
      editor = {M. Wirsing},
      series = {Lecture Notes in Computer Science},
      year = {1987},
      publisher = {North-Holland},
      address = {Amsterdam},
      pages = {77--101} }
  • [article] bibtex
    E. -R. Olderog and C. A. R. Hoare, "Specification-oriented Semantics for Communicating Processes," acta, vol. 23, pp. 9-66, 1986.
    @article{ero86,
      author = {E.-R. Olderog and C. A. R. Hoare},
      title = {Specification-oriented Semantics for Communicating Processes},
      journal = acta, year = 1986, volume = 23, pages = {9--66} }
  • [inproceedings] bibtex
    J. W. de Bakker, C. J. -J. Meyer, E. -R. Olderog, and J. I. Zucker, "Transition systems, infinitary languages and the semantics of uniform concurrency," in Proc. Proc.~17th ACM Symp.~on Theory of Computing, 1985, pp. 252-262.
    @inproceedings{bmoz85,
      author = {J.W. de Bakker and J.-J. Ch. Meyer and E.-R. Olderog and J.I. Zucker},
      title = {Transition systems, infinitary languages and the semantics of uniform concurrency},
      booktitle = {Proc.~17th ACM Symp.~on Theory of Computing},
      year = {1985},
      publisher = {ACM Press},
      pages = {252--262},
      note = {Providence, R.I.} }
  • [article] bibtex
    E. -R. Olderog, "Correctness of Programs with Pascal-like Procedures without Global Variables," Theoretical Computer Science, vol. 30, pp. 49-90, 1984.
    @article{ol84,
      author = {E.-R. Olderog},
      title = {Correctness of Programs with {P}ascal-like Procedures without Global Variables},
      journal = {Theoretical Computer Science},
      year = {1984},
      volume = {30},
      pages = {49--90} }
  • [inproceedings] bibtex
    E. -R. Olderog, "Hoare's logic for programs with procedures---what has been achieved?," in Proc. Proc. Logics of Programs, 1984, pp. 383-395.
    @inproceedings{ol84-overview,
      author = {E.-R. Olderog},
      title = {Hoare's logic for programs with procedures---what has been achieved?},
      booktitle = {Proc. Logics of Programs},
      editor = {E.M. Clarke and D. Kozen},
      volume = {164},
      series = {Lecture Notes in Computer Science},
      year = {1984},
      publisher = {Springer},
      pages = {383--395} }
  • [article] bibtex
    K. R. Apt and E. -R. Olderog, "Proof Rules and Transformations Dealing with Fairness," Science of Computer Programming, vol. 3, pp. 65-100, 1983.
    @article{ao83,
      author = {K.R. Apt and E.-R. Olderog},
      title = {Proof Rules and Transformations Dealing with Fairness},
      journal = {Science of Computer Programming},
      year = {1983},
      volume = {3},
      pages = {65--100} }
  • [article] bibtex
    E. -R. Olderog, "On the Notion of Expressiveness and the Rule of Adaptation," Theoretical Computer Science, vol. 24, pp. 337-347, 1983.
    @article{ol83,
      author = {E.-R. Olderog},
      title = {On the Notion of Expressiveness and the Rule of Adaptation},
      journal = {Theoretical Computer Science},
      year = {1983},
      volume = {24},
      pages = {337--347} }
  • [inproceedings] bibtex
    E. -R. Olderog, "A Characterization of Hoare's logic for programs with Pascal-like procedures," in Proc. Proc.~15th ACM Symp.~on Theory of Computing, 1983, pp. 320-329.
    @inproceedings{ol83-phd,
      author = {E.-R. Olderog},
      title = {A Characterization of {H}oare's logic for programs with {P}ascal-like procedures},
      booktitle = {Proc.~15th ACM Symp.~on Theory of Computing},
      year = {1983},
      publisher = {ACM Press},
      month = {April},
      pages = {320--329},
      note = {Boston, Mass.} }
  • [article] bibtex
    E. -R. Olderog, "Sound and Complete Hoare-like Calculi based on Copy Rules," Acta Informatica, vol. 16, pp. 161-197, 1981.
    @article{ol81-msc,
      author = {E.-R. Olderog},
      title = {Sound and Complete {H}oare-like Calculi based on Copy Rules},
      journal = {Acta Informatica},
      year = {1981},
      volume = {16},
      pages = {161--197} }
  • [inproceedings] bibtex
    H. Langmaack and E. -R. Olderog, "Present-day Hoare-like systems for programming languages with procedures: power, limits and most likely extensions," in Proc. Automata, Languages and Programming (Proc.~7th ICALP), 1980, pp. 363-373.
    @inproceedings{lo80-l4,
      author = {H. Langmaack and E.-R. Olderog},
      title = {Present-day {H}oare-like systems for programming languages with procedures: power, limits and most likely extensions},
      booktitle = {Automata, Languages and Programming (Proc.~7th ICALP)},
      editor = {J.W. de Bakker and J. van Leeuwen},
      volume = {85},
      series = {Lecture Notes in Computer Science},
      year = {1980},
      publisher = {Springer},
      pages = {363--373} }
(Changed: 2020-05-25)