Prof. Dr. ErnstRüdiger Olderog
Contact
 EMail: olderog@neh+inform_{oxr6c}atik.un2zeil+olden^{wodfq}burqxvg.dek68jw
Prof. Dr. ErnstRüdiger Olderog
Entwicklung korrekter Systeme
Department of Computing Science (» Postal address)
Lectures
Winter term 2020 / 2021
2.01.401
Grundlagen der Theoretischen Informatik

2.01.401A
Grundlagen der Theoretischen Informatik

2.01.401B
Grundlagen der Theoretischen Informatik

2.01.401C
Grundlagen der Theoretischen Informatik

2.01.401D
Grundlagen der Theoretischen Informatik

2.01.401E
Grundlagen der Theoretischen Informatik

2.01.401F
Grundlagen der Theoretischen Informatik

2.01.454
Kommunizierende und mobile Systeme

2.01.942
Oberseminar Entwicklung korrekter Systeme

Curriculum Vitae
19741979  study of informatics, mathematics and logics at the University of Kiel 

1979  diploma degree in informatics 
1981  Ph.D. in computer science 
19811983  Programming Research Group at Oxford University 
19841989  Various research visits in Amsterdam, Edinburgh, Yorktown Heights, and Saarbrücken 
1989  Habilitation for computer science 
19891994  Associate professor of computer science at the University of Oldenburg 
since 1994  Full professor of computer science at the University of Oldenburg 
19941999  Leibniz Award of the German Research Council (DFG) 
19952005  Chairman of IFIP Working Group 2.2 on Formal Description of Programming Concepts 
20002014  Managing Editor Acta Informatica 
2012  Member of Academia Europaea 
since 2012  Director of DFG Research Training Group SCARE 
20172019  Dean of Faculty II 
Books

[book] bibtex  Go to documentK. R. Apt, F. S. de Boer, and E. R. Olderog, Verification of Sequential and Concurrent Programs, 3rd Edition, SpringerVerlag, 2009.
@book{ABO09Book3,
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 = {SpringerVerlag},
year = {2009},
note = {502 pp, ISBN 9781848827448},
url = {http://www.springer.com/computer/theoretical+computer+science/book/9781848827448} } 
[book] bibtex  Go to documentE. R. Olderog and H. Dierks, RealTime Systems  Formal Specification and Automatic Verification  Errata: see below, Cambridge University Press, 2008.
@book{OD08,
author = {E.R. Olderog and H. Dierks},
title = {RealTime Systems  Formal Specification and Automatic Verification  Errata: see below},
publisher = {Cambridge University Press},
year = 2008, note = {ISBN 9780521883337. For more information see: \url{http://csd.informatik.unioldenburg.de/rtbook/}{http://csd.informatik.unioldenburg.de/rtbook/}},
url = {http://www.cambridge.org/de/academic/subjects/computerscience/distributednetworkedandmobilecomputing/realtimesystemsformalspecificationandautomaticverification} } 
[book] bibtexK. R. Apt and E. R. Olderog, Verification of Sequential and Concurrent Programs., 2nd ed., springer, 1997.
@book{ero97verification,
author = {K.R. Apt and E.R. Olderog},
title = {Verification of Sequential and Concurrent Programs.},
edition = {2nd},
publisher = springer, year = 1997, note = {ISBN 0387948961. \url{http://www.springerny.com/catalog/np/mar97np/DATA/0387948961.html} {This book in the Springer catalogue}. \url{ http://csd.informatik.unioldenburg.de/pub/Papers/ero97verificationa.ps.gz} {More Information}. } } 
[book] bibtexK. 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.UniOldenburg.DE/~skript/pub/Papers/Errata.ps} {ErrataListe}} bzw. {\url{http://csd.Informatik.UniOldenburg.DE/~skript/pub/Papers/Errata\_long.ps} {ErrataListe mit Tippfehlern}}},
year = 1994 } 
[book] bibtex  Go to documentE. R. Olderog, Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship, Cambridge University Press, 1991.
@book{Old05nets,
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/computerscience/programminglanguagesandappliedlogic/netstermsandformulasthreeviewsconcurrentprocessesandtheirrelationship} }
Errata
Errata for the book RealTime Systems  Formal Specification and Automatic Verification: ErrataRealTime_Systems.pdf
Publications

[article] bibtex  Go to documentB. Finkbeiner, M. Gieseking, J. HeckingHarbusch, and E. Olderog, "AdamMC: A Model Checker for Petri Nets with Transits against FlowLTL (Full Version)," CoRR, vol. abs/2005.07130, 2020.
@article{DBLP:journals/corr/abs200507130,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko HeckingHarbusch and ErnstR{\"{u}}diger Olderog},
title = {AdamMC: {A} Model Checker for Petri Nets with Transits against FlowLTL (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/abs200507130.bib},
bibsource = {dblp computer science bibliography, https://dblp.org} } 
[article] bibtex  Go to documentB. Finkbeiner, M. Gieseking, J. HeckingHarbusch, and E. Olderog, "Model Checking Branching Properties on Petri Nets with Transits (Full Version)," CoRR, vol. abs/2007.07235, 2020.
@article{DBLP:journals/corr/abs200707235,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko HeckingHarbusch and ErnstR{\"{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/abs200707235.bib},
bibsource = {dblp computer science bibliography, https://dblp.org} } 
[inproceedings] bibtex  Go to documentB. Finkbeiner, M. Gieseking, J. HeckingHarbusch, 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 1923, 2020, Proceedings, 2020, pp. 394410.
@inproceedings{DBLP:conf/atva/FinkbeinerGHO20,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko HeckingHarbusch and ErnstR{\"{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 1923, 2020, Proceedings},
pages = {394410},
year = {2020},
optcrossref = {DBLP:conf/atva/2020},
url = {https://doi.org/10.1007/9783030591526\_22},
doi = {10.1007/9783030591526\_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 documentB. Finkbeiner, M. Gieseking, J. HeckingHarbusch, and E. Olderog, "AdamMC: A Model Checker for Petri Nets with Transits against FlowLTL," in Proc. Computer Aided Verification  32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 2124, 2020, Proceedings, Part II, 2020, pp. 6476.
@inproceedings{DBLP:conf/cav/FinkbeinerGHO20,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko HeckingHarbusch and ErnstR{\"{u}}diger Olderog},
title = {AdamMC: {A} Model Checker for Petri Nets with Transits against FlowLTL},
booktitle = {Computer Aided Verification  32nd International Conference, {CAV} 2020, Los Angeles, CA, USA, July 2124, 2020, Proceedings, Part {II}},
pages = {6476},
year = {2020},
optcrossref = {DBLP:conf/cav/20202},
url = {https://doi.org/10.1007/9783030532918\_5},
doi = {10.1007/9783030532918\_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 documentM. Gieseking, E. Olderog, and N. Würdemann, "Solving highlevel Petri games," Acta Inf., vol. 57, iss. 35, pp. 591626, 2020.
@article{DBLP:journals/acta/GiesekingOW20,
author = {Manuel Gieseking and ErnstR{\"{u}}diger Olderog and Nick W{\"{u}}rdemann},
title = {Solving highlevel Petri games},
journal = {Acta Inf.},
volume = {57},
number = {35},
pages = {591626},
year = {2020},
url = {https://doi.org/10.1007/s00236020003685},
doi = {10.1007/s00236020003685},
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 documentM. Gieseking and E. Olderog, "HighLevel Representation of Benchmark Families for Petri Games," CoRR, vol. abs/1904.05621, 2019.
@article{DBLP:journals/corr/abs190405621,
author = {Manuel Gieseking and ErnstR{\"{u}}diger Olderog},
title = {HighLevel 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/abs190405621},
bibsource = {dblp computer science bibliography, https://dblp.org} } 
[article] bibtex  Go to documentB. Finkbeiner, M. Gieseking, J. HeckingHarbusch, and E. Olderog, "Model Checking Data Flows in Concurrent Network Updates (Full Version)," CoRR, vol. abs/1907.11061, 2019.
@article{DBLP:journals/corr/abs190711061,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko HeckingHarbusch and ErnstR{\"{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/abs190711061.bib},
bibsource = {dblp computer science bibliography, https://dblp.org} } 
[inproceedings] bibtex  Go to documentB. Finkbeiner, M. Gieseking, J. HeckingHarbusch, 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 2831, 2019, Proceedings, 2019, pp. 515533.
@inproceedings{DBLP:conf/atva/FinkbeinerGHO19,
author = {Bernd Finkbeiner and Manuel Gieseking and Jesko HeckingHarbusch and ErnstR{\"{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 2831, 2019, Proceedings},
pages = {515533},
year = {2019},
optcrossref = {DBLP:conf/atva/2019},
url = {http://www.unioldenburg.de/fileadmin/user\_upload/f2informcsd/FinGieHecOld19.pdf},
opturl = {https://doi.org/10.1007/9783030317843\_30},
doi = {10.1007/9783030317843\_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 documentE. R. Olderog, "Space for Traffic Manoeuvres  An Overview," in Proc. Symposium on RealTime and Hybrid Systems, 2018, pp. 211230.
@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 RealTime and Hybrid Systems},
pages = {211230},
series = {LNCS},
volume = {11180},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/9783030014612_11} } 
[article] bibtex  Go to documentB. Finkbeiner and E. R. Olderog, "Petri Games: Synthesis of Distributed Systems with Causal Memory," Information and Computation, vol. 253, Part 2, pp. 181203, 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 = {181203},
url = {https://www.unioldenburg.de/fileadmin/user_upload/f2informcsd/pub/mainPGIC.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 EXPTIMEcomplete.} } 
[article] bibtex  Go to documentG. v. Bochmann, M. Hilscher, S. Linker, and E. R. Olderog, "Synthesizing and Verifying Controllers for Multilane Traffic Maneuvers," Formal Aspects of Computing, vol. 29, iss. 4, pp. 583600, 2017.
@article{BHLO17,
author = {G. v. Bochmann and M. Hilscher and S. Linker and E.R. Olderog},
title = {Synthesizing and Verifying Controllers for Multilane Traffic Maneuvers},
journal = {Formal Aspects of Computing},
volume = {29},
number = {4},
year = {2017},
pages = {583600},
doi = {10.1007/s0016501704244},
url = {https://www.unioldenburg.de/fileadmin/user_upload/informatik/ag/csd/pub/faocsynthesis.pdf} } 
[incollection] bibtex  Go to documentE. 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. 95120.
@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 = {95120},
url = {https://www.unioldenburg.de/fileadmin/user_upload/informatik/ag/csd/pub/mainORW.pdf} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and M. Schwammberger, "Formalising a Hazard Warning Communication Protocol with Timed Automata," in Proc. Models, Algorithms, Logics and Tools, 2017, pp. 640660.
@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 = {640660},
series = {LNCS},
volume = {10460},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/9783319631219_32} } 
[inproceedings] bibtex  Go to documentB. Finkbeiner, M. Gieseking, J. HeckingHarbusch, 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. 2343.
@inproceedings{DBLP:journals/corr/abs171110637,
author = {Finkbeiner, Bernd and Gieseking, Manuel and HeckingHarbusch, Jesko and Olderog, ErnstR\"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 = {2343},
doi = {10.4204/EPTCS.260.5},
url = {https://arxiv.org/abs/1711.10637} } 
[inproceedings] bibtex  Go to documentB. Engelmann and E. Olderog, "A Sound and Complete Hoare Logic for DynamicallyTyped, ObjectOriented Programs," in Proc. Proc. Theory and Practice of Formal Methods, 2016, pp. 173193.
@inproceedings{EngelmannOlderog2015,
author = {Bj\"orn Engelmann and ErnstR\"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 = {173193},
url = {http://link.springer.com/chapter/10.1007%2F9783319307343_13},
optaddress = {Eindhoven, The Netherlands} } 
[article] bibtex  Go to documentE. R. Olderog and M. Swaminathan, "Structural Transformations for DataEnriched RealTime Systems," Formal Asp. Comput., vol. 27, pp. 727750, 2015.
@article{OlderogSwaminathan14,
author = {E.R Olderog and M. Swaminathan},
title = {Structural Transformations for DataEnriched RealTime Systems},
journal = {Formal Asp. Comput.},
volume = {27},
pages = {727750},
year = {2015},
url = {http://dx.doi.org/10.1007/s001650140306y} } 
[misc] bibtex  Go to documentB. 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 NilsErik 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 objectoriented 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 twofold: 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 staticallytyped program, the effort required is equivalent to the staticallytyped case. Second, we show how the required type information can be efficiently derived for all typesafe programs by integrating a type inference algorithm into Hoare logic, yielding a semiautomatic procedure allowing the user to focus on those typing problems really requiring his attention. While applying type inference to dynamically typed programs is a wellestablished 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 documentE. 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. 68096816.
@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 = {68096816},
month = {Dec},
publisher = {IEEE},
url = {https://www.unioldenburg.de/fileadmin/user_upload/f2informcsd/pub/rootORW15.pdf},
doi = {10.1109/CDC.2015.7403292},
subproject = {H3},
conferenceshort = {CDC},
conferencelong = {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 lanechange 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] bibtexG. v. Bochmann, M. Hilscher, S. Linker, and E. Olderog, "Synthesizing Controllers for MultiLane Traffic Maneuvers," in Proc. International Symposium on Dependable Software Engineering (SETTA), 2015, pp. 7186.
@inproceedings{avacsh3dec15, title = {Synthesizing Controllers for MultiLane Traffic Maneuvers},
author = {Gregor v. Bochmann AND Martin Hilscher AND Sven Linker AND ErnstRüdiger Olderog},
editor = {Xuandong Li AND Zhiming Liu AND Wang Yi},
booktitle = {International Symposium on Dependable Software Engineering (SETTA)},
year = {2015},
month = {Nov.},
pages = {7186},
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 multilane 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 lanechange 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.},
conferencelong = {International Symposium on Dependable Software Engineering},
conferenceshort = {SETTA} } 
[inproceedings] bibtex  Go to documentB. Finkbeiner, M. Gieseking, and E. Olderog, "Adam: CausalityBased Synthesis of Distributed Systems," in Proc. Computer Aided Verification  27th International Conference, CAV 2015, San Francisco, CA, USA, July 1824, 2015, Proceedings, Part I, 2015, pp. 433439.
@inproceedings{fingieold15, title = {Adam: CausalityBased Synthesis of Distributed Systems},
author = {Bernd Finkbeiner and Manuel Gieseking and ErnstR{\"{u}}diger Olderog},
booktitle = {Computer Aided Verification  27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 1824, 2015, Proceedings, Part {I}},
year = {2015},
editor = {Daniel Kroening and Corina S. Pasareanu},
pages = {433439},
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.},
conferencelong = {International Conference on Computer Aided Verification},
conferenceshort = {CAV},
url = {http://www.unioldenburg.de/fileadmin/user\_upload/f2informcsd/fingieold15.pdf} } 
[inproceedings] bibtex  Go to documentB. 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 1012, 2014., 2014, pp. 217230.
@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 1012, 2014.},
series = {{EPTCS}},
year = {2014},
volume = {161},
pages = {217230},
url = {http://arxiv.org/abs/1406.1069v2} } 
[inproceedings] bibtexM. 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. 196212.
@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 = {196212} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and M. Swaminathan, "Structural Transformations for DataEnriched RealTime Systems," in Proc. Integrated Formal Methods (iFM), 2013, pp. 378393.
@inproceedings{OlderogSwaminathan13,
author = {E.R. Olderog and Mani Swaminathan},
title = {Structural Transformations for DataEnriched RealTime Systems},
editor = {Einar Broch Johnsen and Luigia Petre},
booktitle = {Integrated Formal Methods (iFM)},
volume = {7940},
series = {Lecture Notes in Computer Science},
pages = {378393},
publisher = {SpringerVerlag},
year = {2013},
url = {http://dx.doi.org/10.1007/9783642386138_26} } 
[article] bibtexK. R. Apt, F. S. de Boer, E. R. Olderog, and S. de Gouw, "Verification of objectoriented programs: A transformational approach," J Computer System Sciences, vol. 78, pp. 823852, 2012.
@article{ABOG12,
author = {K. R. Apt and F. S. de Boer and E.R. Olderog and S. de Gouw},
title = {Verification of objectoriented programs: A transformational approach},
journal = {J Computer System Sciences},
volume = {78},
number = {},
pages = {823852},
year = {2012},
optnote = {DOI information: 10.1016/j.jcss.2011.08.002} } 
[article] bibtexE. R. Olderog and R. Wilhelm, "Turing und die Verifikation," InformatikSpektrum, vol. 35, iss. 4, pp. 271279, 2012.
@article{OW12,
author = {E.R. Olderog and R. Wilhelm},
title = {Turing und die {Verifikation}},
journal = {InformatikSpektrum},
volume = {35},
number = {4},
pages = {271279},
year = {2012},
optnote = {Themenheft: Turing} } 
[article] bibtex  Go to documentM. Swaminathan, J. P. Katoen, and E. R. Olderog, "Layered Reasoning for randomized distributed algorithms," Formal Asp. Comput., vol. 24, iss. 46, pp. 477496, 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 = {46},
year = {2012},
pages = {477496},
url = {http://dx.doi.org/10.1007/s001650120231x} } 
[inproceedings] bibtexE. R. Olderog, "Automatic Verification of RealTime Systems with Rich Data  An Overview," in Proc. Theory and Applications of Models of Computation (TAMC), 2012, pp. 8493.
@inproceedings{Old12,
author = {E.R. Olderog},
title = {Automatic Verification of RealTime 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 = {8493},
publisher = {Springer},
year = {2012} } 
[article] bibtex  Go to documentJ. Faber, S. Linker, E. Olderog, and J. Quesel, "Syspect  Modelling, Specifying, and Verifying RealTime Systems with Rich Data," International Journal of Software and Informatics, vol. 5, iss. 12, pp. 117137, 2011.
@article{FLO+2011,
author = {Johannes Faber and Sven Linker and ErnstR{\"u}diger Olderog and JanDavid Quesel},
title = {Syspect  Modelling, Specifying, and Verifying RealTime Systems with Rich Data},
journal = {International Journal of Software and Informatics},
year = {2011},
volume = {5},
number = {12},
part = {1},
pages = {117137},
note = {ISSN 16737288.},
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 realtime 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 CSPOZDC of CSP (Communicating Sequential Processes), OZ (ObjectZ) 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 HPILoT (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 documentM. Hilscher, S. Linker, E. R. Olderog, and A. P. Ravn, "An Abstract Model for Proving Safety of MultiLane Traffic Manoeuvres," in Proc. Int'l Conf.\ on Formal Engineering Methods (ICFEM), 2011, pp. 404419.
@inproceedings{avacsh3dec11,
author = {M. Hilscher AND S. Linker AND E.R. Olderog AND A.P. Ravn},
title = {An Abstract Model for Proving Safety of MultiLane 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 = {404419},
month = {Oct.},
publisher = {SpringerVerlag},
note = {The original publication is available at \url{http://www.springerlink.com/content/y4721k1525v23520}{www.springerlink.com}.},
subproject = {H3},
pdf = {http://csd.informatik.unioldenburg.de/pub/Papers/hlor2011icfem.pdf},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hlor2011icfem.pdf},
abstract = { We present an approach to prove safety (collision freedom) of multilane motorway trac with lanechange 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 lanechange 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] bibtexJ. 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. 251265.
@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 = {SpringerVerlag},
pages = {251265},
year = {2010} } 
[inproceedings] bibtexE. R. Olderog and A. Podelski, "Explicit Fair Scheduling for Dynamic Control," in Proc. Concurrency, Compositionality, and Correctness, 2010, pp. 96117.
@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 = {SpringerVerlag },
pages = {96117 },
year = {2010} } 
[inproceedings] bibtex  Go to documentJ. Hoenicke, R. Meyer, and E. R. Olderog, "Kleene, Rabin, and Scott Are Available," in Proc. CONCUR 2010  Concurrency Theory (CONCUR), 2010, pp. 462477.
@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 = {462477},
year = {2010},
url = {http://dx.doi.org/10.1007/9783642153754_32} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and M. Swaminathan, "Layered Composition for Timed Automata," in Proc. Formal Modeling and Analysis of Timed Systems (FORMATS), 2010, pp. 228242.
@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 = {SpringerVerlag},
pages = {228242},
year = {2010},
url = {http://dx.doi.org/10.1007/9783642152979_18} } 
[inproceedings] bibtexE. R. Olderog and R. Meyer, "Automatatheoretic verification based on counterexample specification," in Proc. Informatik als Dialog zwischen Theorie und Anwendung, 2009, pp. 217225.
@inproceedings{erorm09,
author = {E.R. Olderog and R. Meyer},
title = {Automatatheoretic 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 = {217225},
publisher = {ViewegTeubner},
publists = {rmeyer} } 
[inproceedings] bibtexK. R. Apt, F. S. de Boer, and E. R. Olderog, "Modular Verification of Recursive Programs," in Proc. Languages: From Formal to Natural, 2009, pp. 121.
@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 = { SpringerVerlag },
editor = { },
pages = { 121 },
year = { 2009 } } 
[article] bibtexM. 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. 161204, 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 = {161204},
abstract = {We describe how CSPOZ, a formal method combining the process algebra CSP with the specification language ObjectZ, can be integrated into an objectoriented 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 CSPOZ 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 documentE. 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. 316.
@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 = {15710661},
volume = {207},
number = {},
month = {April},
pages = {316},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.03.082},
url = {},
keywords = {Realtime systems, complex data, CSP, ObjectZ, 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 highlevel specifications of realtime systems combining the dimensions of process behaviour, data, and time can be automatically verified, exploiting recent advances in semantics, constraintbased model checking, and decision procedures for complex data. As specification language we consider CSOZDC, which integrates concepts from Communicating Sequential Processes (CSP), ObjectZ (OZ), and Duration Calculus (DC). Our approach to automatic verification of CSPOZDC rests on a compositional semantics of this languages in terms of PhaseEventAutomata. 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 realtime and infinite data. This is demonstrated by a case study concerning emergency messages in the European Train Control System (ETCS). For CSPOZDC we also discuss a UML profile and tool support. } } 
[article] bibtexB. 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. 118126, 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 = {118126},
note = {See also \url{http://www.avacs.org}{http://www.avacs.org}} } 
[inproceedings] bibtexD. Basin, E. R. Olderog, and P. E. Sevinç, "Specifying and analyzing security automata using CSPOZ," in Proc. Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007), 2007, pp. 7081.
@inproceedings{BSO07,
author = {D. Basin and E.R. Olderog and P.E. Sevin\c{c}},
title = {Specifying and analyzing security automata using {CSPOZ}},
booktitle = {Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007)},
pages = {7081},
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 CSPOZ, a specification language combining Communicating Sequential Processes (CSP) and ObjectZ (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 CSPOZ 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, toolsupported analysis. } } 
[inproceedings] bibtexW. 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 RealTime Systems, 2007, pp. 115169.
@inproceedings{DammMOOPPSW07,
author = {Werner Damm and Alfred Mikschl and Jens Oehlerking and ErnstR{\"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 = {115169},
editor = {Cliff Jones and Zhiming Liu and Jim Woodcock},
booktitle = {Formal Methods and Hybrid RealTime Systems},
publisher = {SpringerVerlag},
series = {LNCS},
volume = {4700},
doi = {10.1007/9783540752219_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 preverified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, modelchecking 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/9783540752219_6}{(c) SpringerVerlag}} } 
[inproceedings] bibtexE. R. Olderog and B. Steffen, "Formale Semantik und Programmverifikation," in Proc. InformatikHandbuch, 4. Auflage, 2006, pp. 145166.
@inproceedings{erobs06,
author = {E.R. Olderog and B. Steffen},
title = {{F}ormale {S}emantik und {P}rogrammverifikation},
booktitle = {InformatikHandbuch, 4. Auflage},
editor = {P. Rechenberg and G. Pomberger},
year = 2006, publisher = {Hanser Verlag},
pages = {145166} } 
[article] bibtexW. Damm, H. Hungar, and E. R. Olderog, "Verification of cooperating traffic agents," International Journal of Control, vol. 79, iss. 5, pp. 395421, 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 = {395421},
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 offline analysis of the worstcase 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] bibtexP. E. Sevinç, D. Basin, and E. R. Olderog, "Controlling Access to Documents: A Formal Access Control Model," in Proc. ETRICS 2006, 2006, pp. 352367.
@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 = {352367},
publisher = {SpringerVerlag},
series = {LNCS},
title = {Controlling Access to Documents: A Formal Access Control Model},
volume = 3995, year = 2006, abstract = { Current accesscontrol systems for documents suffer from one or more of the following limitations: they are coarsegrained, 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 finegrained, supporst a general class of documents, and provides a foundation for usage control. } } 
[article] bibtexE. R. Olderog and H. Wehrheim, "Specification and (property) inheritance in CSPOZ," Science of Computer Programming, vol. 55, pp. 227257, 2005.
@article{OW05,
author = {E.R. Olderog and H. Wehrheim},
title = {{Specification and (property) inheritance in CSPOZ}},
journal = {Science of Computer Programming},
year = {2005},
volume = {55},
pages = {227257},
abstract = { CSPOZ [Fis97, Fis00] is a combination of Communicating Sequential Processes (CSP) and ObjectZ (OZ). It enables the specification of systems having both a statebased and a behaviouroriented view using the objectoriented concepts of classes, instantiation and inheritance. CSPOZ has a process semantics in the failure divergence model of CSP. In this paper we explain CSPOZ 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, ObjectZ, failures divergence semantics, inheritance, safety and ``liveness'' properties, modelchecking, FDR \begin{thebibliography} \bibitem{Fis97} C.~Fischer. \newblock {CSPOZ}: A combination of {ObjectZ} and {CSP}. \newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open ObjectBased Distributed Systems (FMOODS'97)},
volume~2, pages 423438. Chapman \& Hall, 1997. \bibitem{Fis00} C.~Fischer. \newblock {\em Combination and Implementation of Processes and Data: From {CSPOZ} to {Java}}. \newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000. \bibitem{Weh02} H.~Wehrheim. \newblock Behavioural subtyping in objectoriented specification formalisms. \newblock University of Oldenburg, Habilitation Thesis, 2002. \end{thebibliography} } } 
[inproceedings] bibtexW. 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. 77110.
@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 = {77110},
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 worstcase 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 documentM. Möller, E. R. Olderog, H. Rasch, and H. Wehrheim, "Linking CSPOZ with UML and Java: A Case Study," in Proc. Integrated Formal Methods, 2004, pp. 267286.
@inproceedings{MORW04,
author = {M. M\"oller and E.R. Olderog and H. Rasch and H. Wehrheim},
title = {{Linking CSPOZ 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 = {03029743},
pages = {267286},
year = {2004},
month = {March},
abstract = { We describe how CSPOZ, an integrated formal method combining the process algebra CSP with the specification language ObjectZ, can be linked to standard software engineering languages, viz.\ UML and Java. Our aim is to generate a significant part of the CSPOZ specification from an initially developed UML model using a UML profile for CSPOZ, and afterwards transform the formal specification into assertions written in the Java Modelling Language JML complemented by CSP$_{jassda}$. The intermediate CSPOZ 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.unioldenburg.de/pub/Papers/morw04.pdf},
publists = {moeller formoos} } 
[inproceedings] bibtexE. R. Olderog and H. Wehrheim, "Specification and Inheritance in CSPOZ," in Proc. Formal Methods for Components and Objects, 2003, pp. 361379.
@inproceedings{OlWe02,
author = {E.R. Olderog and H. Wehrheim},
title = {{Specification and Inheritance in CSPOZ}},
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 = {361379},
publisher = {Springer},
year = {2003},
abstract = { CSPOZ [Fis97,Fis00] is a combination of Communicating Sequential Processes (CSP) and ObjectZ (OZ). It enables the specification of systems having both a statebased and a behaviouroriented view using the objectoriented concepts of classes, instantiation and inheritance. CSPOZ has a process semantics in the failures divergence model of CSP. In this paper we explain CSPOZ 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 {CSPOZ}: A combination of {ObjectZ} and {CSP}. \newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open ObjectBased Distributed Systems (FMOODS'97)},
volume~2, pages 423438. Chapman \& Hall, 1997. \bibitem{Fis00} C.~Fischer. \newblock {\em Combination and Implementation of Processes and Data: From {CSPOZ} to {Java}}. \newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000. \bibitem{Weh02} H.~Wehrheim. \newblock Behavioural subtyping in objectoriented specification formalisms. \newblock University of Oldenburg, Habilitation Thesis, 2002. \end{thebibliography} } } 
[article] bibtexE. R. Olderog and H. Dierks, "Moby/RT: A Tool for Specification and Verification of RealTime Systems," Journal of Universal Computer Science, vol. 9, pp. 88105, 2003.
@article{OD03,
author = {E.R. Olderog and H. Dierks},
title = {{Moby/RT: A Tool for Specification and Verification of RealTime Systems}},
journal = {Journal of Universal Computer Science},
year = {2003},
optkey = {},
volume = {9},
optnumber = {},
pages = {88105},
optmonth = {},
optnote = {},
abstract = { The tool Moby/RT supports the design of realtime systems at the levels of requirements, design specifications and programs. Requirements are expressed by constraint diagrams [Kle00], design specifications by PLCAutomata [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 MobyRT by discussing its semantic basis and its use for automatic verification by utilising the modelchecker 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 {PLCAutomata: A New Class of Implementable RealTime Automata}. \newblock {\em TCS},
253(1):6193. \end{thebibliography} } } 
[article] bibtexH. Dierks and E. R. Olderog, "Temporale Spezifikationslogiken," atAutomatisierungstechnik, vol. 51, iss. 2, p. a1a4, 2003.
@article{DO03,
author = {H. Dierks and E.R. Olderog},
title = {{Temporale Spezifikationslogiken}},
journal = {atAutomatisierungstechnik},
year = {2003},
optkey = {},
volume = {51},
number = {2},
optmonth = {},
pages = {A1A4},
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] bibtexJ. Hoenicke and E. R. Olderog, "CSPOZDC: A Combination of Specification Techniques for Processes, Data and Time," Nordic Journal of Computing, vol. 9, iss. 4, pp. 301334, 2002.
@article{HO02b,
author = {J. Hoenicke and E.R. Olderog},
title = {{CSPOZDC}: A Combination of Specification Techniques for Processes, Data and Time},
journal = {Nordic Journal of Computing},
year = {2002},
volume = {9},
number = {4},
pages = {301334},
note = {appeared March 2003},
abstract = { CSPOZDC is a new combination of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], ObjectZ [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 CSPOZDC specifications. This is done by combining the modelcheckers 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 realtime 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 232243. Springer, 1997. \bibitem{Hoa85} C.A.R. Hoare. \newblock {\em Communicating Sequential Processes}. \newblock Prentice Hall, 1985. \bibitem{Ros94} A.W. Roscoe. \newblock Modelchecking {CSP}. \newblock In A.W. Roscoe, editor, {\em A Classical Mind  Essays in Honour of C.A.R.Hoare},
pages 353378. PrenticeHall, 1994. \bibitem{Smi00} G.~Smith. \newblock {\em The ObjectZ 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):269276, 1991. \end{thebibliography} } } 
[inproceedings] bibtex  Go to documentJ. Hoenicke and E. R. Olderog, "Combining Specification Techniques for Processes Data and Time," in Proc. Integrated Formal Methods, 2002, pp. 245266.
@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.UniOldenburg.DE/~skript/pub/Papers/ho02ifm.pdf},
year = {2002},
month = {May},
pages = {245266},
abstract = { We present a new combination CSPOZDC of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], ObjectZ [Smi00], and Duration Calculus [ZHR91]. The emphasis is on a smooth integration of the underlying semantic models and its use for verifying properties of CSPOZDC specifications by a combined application of the modelcheckers 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] bibtexM. Broy and E. R. Olderog, "TraceOriented Models of Concurrency," in Proc. Handbook of Process Algebra, 2001, pp. 101195.
@inproceedings{bo01,
author = {M. Broy and E.R. Olderog},
title = {{TraceOriented Models of Concurrency}},
booktitle = {Handbook of Process Algebra},
optcrossref = {},
optkey = {},
pages = {101195},
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 indepth presentation of traceoriented 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 traceoriented models and explain methods for the specification and verification of process behaviour based on these models. } } 
[inproceedings] bibtex  Go to documentC. Fischer, E. R. Olderog, and H. Wehrheim, "A CSP view on UMLRT structure diagrams," in Proc. Fundamental Approaches to Software Engineering, 2001, pp. 91108.
@inproceedings{fow01,
author = {C. Fischer and E.R. Olderog and H. Wehrheim},
title = {{A CSP view on UMLRT structure diagrams}},
booktitle = {{Fundamental Approaches to Software Engineering}},
optcrossref = {},
optkey = {},
pages = {91108},
year = {2001},
editor = {H. Husmann},
volume = {2029},
optnumber = {},
series = lncs, optaddress = {},
optmonth = {},
optorganization = {},
publisher = springer, optnote = {},
optannote = {},
abstract = { UMLRT is an extension of UML for modelling embedded reactive and realtime 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 UMLRT structure diagrams together with the formal method CSPOZ combining CSP and ObjectZ. While CSPOZ is used for specifying the system components themselves (by CSPOZ classes), UMLRT 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 CSPOZ specifications, we develop a translation from UMLRT structure diagrams to CSP. Besides achieving a more easily accessible, graphical architecture modelling for CSPOZ, we thus also give a semantics to UMLRT structure diagrams. },
publists = {formoos},
url = {http://csd.informatik.unioldenburg.de/~wehrheim/fase01.ps} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and A. P. Ravn, "Documenting Design Refinement," in Proc. Proc. of the Third Workshop on Formal Methods in Software Practice, 2000, pp. 89100.
@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 = {89100},
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 realtime and hybrid systems. A precise semantics is given for the UML class diagrams by translation to the Z schema calculus. },
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/or00.ps} } 
[article] bibtexE.R.Olderog, "Sichere Bahnsteuerungen," Log IN, iss. 1, pp. 6465, 1999.
@article{ero99login,
author = {E.R.Olderog},
title = {Sichere {B}ahnsteuerungen},
journal = {Log {IN}},
pages = {6465},
number = {1},
year = {1999} } 
[article] bibtex  Go to documentM. Schenke and E. R. Olderog, "Transformational design of realtime systems  Part 1: from requirements to program specifications.," Acta Informatica 36, pp. 165, 1999.
@article{msero99,
author = {Michael Schenke and E.R. Olderog},
title = {Transformational design of realtime systems  Part 1: from requirements to program specifications.},
journal = {Acta Informatica 36},
pages = {165},
year = {1999},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/msero97_1.ps.gz} } 
[inproceedings] bibtexE. R. Olderog, "Correct RealTime Software for Programmable Logic Controllers," in Proc. Correct System Design  Recent Insights and Advances, 1999, pp. 342362.
@inproceedings{ero99,
author = {E.R. Olderog},
title = {{Correct RealTime 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 = {342362} } 
[inproceedings] bibtexE. R. Olderog, "Entwicklung korrekter zeitkritischer Systeme," in Proc. Formale Beschreibungstechniken für verteilte Systeme, 1999, pp. 716.
@inproceedings{ero99gi/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 = {716} } 
[inproceedings] bibtexB. KriegBrü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. 11861205.
@inproceedings{uniform99,
author = {B. KriegBr\"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 = {11861205} } 
[inproceedings] bibtexE. R. Olderog, "Formal Methods in RealTime Systems," in Proc. Proceedings of the 10th EuroMicro Workshop on Real Time Systems, 1998, pp. 254263.
@inproceedings{ero98:formalmethodrealtimesystem,
author = {E.R. Olderog},
title = {Formal Methods in RealTime Systems},
booktitle = {Proceedings of the 10th EuroMicro Workshop on Real Time Systems},
year = 1998, organization = {IEEE Computer Society},
month = {June},
pages = {254263} } 
[inproceedings] bibtexV. 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. 251260.
@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 = {InformatikBericht Nr. 104},
year = {1998},
pages = {251260},
publisher = {HumboldUniversitaet zu Berlin/Germany} } 
[inproceedings] bibtexE. R. Olderog and H. Dierks, "Decomposing RealTime Specifications," in Proc. Compositionality: The Significant Difference, 1998, pp. 465489.
@inproceedings{erohd98,
author = {E.R. Olderog and H. Dierks},
title = {{Decomposing RealTime 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 = {465489},
optannote = {},
note = {{\url{http://csd.informatik.unioldenburg.de/pub/Papers/erohd97.ps.gz} {An abstract is available online}}} } 
[article] bibtexC. Fischer, S. Kleuker, and E. R. Olderog, "Beweisbar korrekte Telekommunikationssysteme," Informationstechnik und Technische Informatik, vol. 3, pp. 2228, 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 = {2228},
note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/cfskero97a.ps.gz} {An extended abstract is available online}},
publists = {skleuker} } 
[incollection] bibtexE. R. Olderog, A. P. Ravn, and J. U. Skakkebæk, "Refining System Requirements to Program Specifications," in Formal Methods for RealTime Computing, Heitmeyer, C. and Mandrioli, D., Eds., Wiley, 1996, vol. 5, pp. 107134.
@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 RealTime Computing},
chapter = 5, pages = {107134},
publisher = {Wiley},
series = {Trends in Software},
volume = 5, year = 1996, note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/ero96.ps.gz} {An abstract is available online}} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and M. Schenke, "Design of RealTime Systems: The Interface between Duration Calculus and Program Specifications," in Proc. Structures in Concurrency Theory, 1995, pp. 3254.
@inproceedings{eroms95,
author = {E.R. Olderog and M. Schenke},
title = {Design of RealTime Systems: The Interface between Duration Calculus and Program Specifications},
editor = {J. Desel},
booktitle = {Structures in Concurrency Theory},
publisher = springer, series = wics, year = 1995, pages = {3254},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/eroms95.ps.gz} } 
[inproceedings] bibtexJ. He, C. A. R. Hoare, M. Fränzle, M. MüllerOlm, E. R. Olderog, M. Schenke, M. R. Hansen, A. P. Ravn, and H. Rischel, "Provably Correct Systems," in Proc. Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'94), 1994, pp. 288335.
@inproceedings{eroms94ftrtft,
author = {Jifeng He and C. A. R. Hoare and M. Fr\"anzle and M. M\"ullerOlm 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 RealTime and FaultTolerant Systems (FTRTFT'94)},
series = lncs, publisher = springer, year = 1994, volume = 863, pages = {288335} } 
[inproceedings] bibtexJ. P. Bowen, M. Fränzle, E. R. Olderog, and A. P. Ravn, "Developing Correct Systems," in Proc. Proceedings of the 5th EUROMICRO Workshop on RealTime Systems (Oulu, Finland), 1993, pp. 176189.
@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 RealTime Systems (Oulu, Finland)},
pages = {176189},
publisher = {IEEE Computer Society Press},
year = 1993 } 
[techreport] bibtex  Go to documentM. R. Hansen, E. R. Olderog, M. Schenke, M. Fränzle, B. von Karger, M. MüllerOlm, and H. Rischel, "A Duration Calculus Semantics for RealTime Reactive Systems," uniolfb10, 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\"ullerOlm and H. Rischel},
title = {A {Duration Calculus} Semantics for RealTime Reactive Systems},
type = {ProCoS II document},
number = {[OLD MRH 1/1]},
institution = uniolfb10, month = sep, year = 1993, url = {http://csd.informatik.unioldenburg.de/pub/Papers/eroms93.ps.gz} } 
[inproceedings] bibtexE. 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. 90104.
@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 = {90104} } 
[incollection] bibtexE. R. Olderog, "Systematic derivation of communicating programs," in Programming and Mathematical Method, Broy, M., Ed., springer, 1992, pp. 369407.
@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 = {369407} } 
[inproceedings] bibtexE. R. Olderog, "Interfaces between Languages for Communicating Systems," in Proc. Automata, Languages and Programming. Proceedings of the 19th ICALP 1992, 1992, pp. 641655.
@inproceedings{ero92icalp,
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 = {641655},
note = {Invited paper} } 
[article] bibtexE. R. Olderog, "Correctness of Concurrent Processes," tcs, vol. 80, pp. 263288, 1991.
@article{ero91correctness,
author = {E.R. Olderog},
title = {Correctness of Concurrent Processes},
journal = tcs, year = 1991, volume = 80, pages = {263288} } 
[incollection] bibtexK. 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. 363429.
@incollection{ero91intro,
author = {K. R. Apt and E.R. Olderog},
title = {Introduction to Program Verification},
booktitle = {Formal Description of Programming Concepts},
series = {IFIP StateoftheArt Reports},
publisher = springer, year = 1991, editor = {E. J. Neuhold and M. Paul},
pages = {363429} } 
[inproceedings] bibtexE. R. Olderog and K. R. Apt, "Using transformations to verify parallel programs," in Proc. Algebraic Methods II: Theory, Tools and Applications, 1991, pp. 5581.
@inproceedings{ero91algebraic,
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 = {5581} } 
[inproceedings] bibtexE. 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. 6177.
@inproceedings{ero91concur,
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 = {6177} } 
[article] bibtexC. J. J. Meyer and E. R. Olderog, "Hiding in Stream Semantics of Uniform Concurrency," acta, vol. 27, pp. 381397, 1990.
@article{ero90acta,
author = {J.J. Ch. Meyer and E.R. Olderog},
title = {Hiding in Stream Semantics of Uniform Concurrency},
journal = acta, year = 1990, volume = 27, pages = {381397} } 
[incollection] bibtexK. 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{ero90dijkstra,
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] bibtexE. 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. 592621.
@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 = {592621} } 
[article] bibtexB. 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. 6073, 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 = {6073},
month = {October},
year = 1989 } 
[article] bibtexJ. 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. 158224, 1988.
@article{ero88jcss,
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 = {158224} } 
[article] bibtexJ. A. Bergstra, J. W. Klop, and E. R. Olderog, "Readies and Failures in the Algebra of Communicating Processes," siam, vol. 17, pp. 11341177, 1988.
@article{ero88siam,
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 = {11341177} } 
[article] bibtexE. R. Olderog and K. R. Apt, "Fairness in Parallel Programs: the Transformational Approach," acmtoplas, vol. 10, pp. 420455, 1988.
@article{ero88toplas,
author = {E.R. Olderog and K. R. Apt},
title = {Fairness in Parallel Programs: the Transformational Approach},
journal = acmtoplas, year = 1988, volume = 10, pages = {420455} } 
[article] bibtexJ. 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. 87112, 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 = {87112} } 
[inproceedings] bibtexJ. 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. 77101.
@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 = {NorthHolland},
address = {Amsterdam},
pages = {77101} } 
[article] bibtexE. R. Olderog and C. A. R. Hoare, "Specificationoriented Semantics for Communicating Processes," acta, vol. 23, pp. 966, 1986.
@article{ero86,
author = {E.R. Olderog and C. A. R. Hoare},
title = {Specificationoriented Semantics for Communicating Processes},
journal = acta, year = 1986, volume = 23, pages = {966} } 
[inproceedings] bibtexJ. 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. 252262.
@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 = {252262},
note = {Providence, R.I.} } 
[article] bibtexE. R. Olderog, "Correctness of Programs with Pascallike Procedures without Global Variables," Theoretical Computer Science, vol. 30, pp. 4990, 1984.
@article{ol84,
author = {E.R. Olderog},
title = {Correctness of Programs with {P}ascallike Procedures without Global Variables},
journal = {Theoretical Computer Science},
year = {1984},
volume = {30},
pages = {4990} } 
[inproceedings] bibtexE. R. Olderog, "Hoare's logic for programs with procedureswhat has been achieved?," in Proc. Proc. Logics of Programs, 1984, pp. 383395.
@inproceedings{ol84overview,
author = {E.R. Olderog},
title = {Hoare's logic for programs with procedureswhat 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 = {383395} } 
[article] bibtexK. R. Apt and E. R. Olderog, "Proof Rules and Transformations Dealing with Fairness," Science of Computer Programming, vol. 3, pp. 65100, 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 = {65100} } 
[article] bibtexE. R. Olderog, "On the Notion of Expressiveness and the Rule of Adaptation," Theoretical Computer Science, vol. 24, pp. 337347, 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 = {337347} } 
[inproceedings] bibtexE. R. Olderog, "A Characterization of Hoare's logic for programs with Pascallike procedures," in Proc. Proc.~15th ACM Symp.~on Theory of Computing, 1983, pp. 320329.
@inproceedings{ol83phd,
author = {E.R. Olderog},
title = {A Characterization of {H}oare's logic for programs with {P}ascallike procedures},
booktitle = {Proc.~15th ACM Symp.~on Theory of Computing},
year = {1983},
publisher = {ACM Press},
month = {April},
pages = {320329},
note = {Boston, Mass.} } 
[article] bibtexE. R. Olderog, "Sound and Complete Hoarelike Calculi based on Copy Rules," Acta Informatica, vol. 16, pp. 161197, 1981.
@article{ol81msc,
author = {E.R. Olderog},
title = {Sound and Complete {H}oarelike Calculi based on Copy Rules},
journal = {Acta Informatica},
year = {1981},
volume = {16},
pages = {161197} } 
[inproceedings] bibtexH. Langmaack and E. R. Olderog, "Presentday Hoarelike systems for programming languages with procedures: power, limits and most likely extensions," in Proc. Automata, Languages and Programming (Proc.~7th ICALP), 1980, pp. 363373.
@inproceedings{lo80l4,
author = {H. Langmaack and E.R. Olderog},
title = {Presentday {H}oarelike 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 = {363373} }