Concurrency and Protocol Verification

• Context: We do research on formal models of concurrency and distributed systems, and their applications in specification, analysis and verification.
• Collaboration: We cooperate with many universities and institutes, such as VU Amsterdam, U Augsburg, TU Braunschweig, Cambridge U, Trinity College Dublin, U Edinburgh, TU Eindhoven, INRIA, Shanghai Jiaotong U and Stanford U.

Activities

Current focus is on the following projects:

• Multicore seL4 Verification: We aim to provide frameworks for reasoning about concurrency in code for operating systems. In particular, our main project is to model and verify the multicore version of seL4.
• Formal Specification, Analysis and Verification of Mesh Protocols: We strive to develop methods and formalisms for protocol specification, analysis and verification. Amongst others we apply those methods and formalisms to routing protocols for wireless mesh networks, such as AODV, the Ad hoc On-demand Distance Vector routing protocol. Additionally, we work on improvements of existing protocols and/or creation of new ones.
• Analysis of Protocols for High-assurance Networks: We aim to provide authentication and reliable communication protocols for unmanned aerial vehicles (UAVs). This covers both internal communication within the UAV and external communication between a ground station and the vehicle.
• Process Algebra: We study process algebraic languages and their semantics, in order to provide a firm theoretical basis for the specification, analysis and verification of concurrent systems.
• Asynchronous Communication in Distributed Systems: We aim to discover which systems can be implemented in a distributed way—and how—using only asynchronous communication between components, while preserving desirable properties that may be specified in terms of synchronous communication. In connection with this, we try to establish an expressiveness hierarchy of specification formalisms with different communication paradigms.
• Probability and Nondeterminism: The goal of this project is to build a theory of processes that faithfully integrates probabilities and nondeterminism.

Recent Publications

To appear

Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke-Uffmann Abstract processes and conflicts in place/transition systems Information and Computation

2021

Richard S. Bird, Jeremy Gibbons, Ralf Hinze, Peter Hoefner, Johan Jeuring, Lambert G. L. T. Meertens, Bernhard Möller, Carroll Morgan, Tom Schrijvers, Wouter Swierstra and Nicolas Wu Algorithmics Volume 600 in IFIP Advances in Information and Communication Technology. Springer, 2021

2020

		Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality Logical Methods in Computer Science, Volume 16, Issue 4, pp. 16:1-16:28, December, 2020
		Rob van Glabbeek Reactive bisimulation semantics for a process algebra with time-outs 31st International Conference on Concurrency Theory (CONCUR 20), pp. 6:1-6:23, Online, August, 2020
		Rob van Glabbeek Reactive temporal logic Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics (EXPRESS/SOS 2020), pp. 51-68, Online, August, 2020
		Rob van Glabbeek, Bas Luttik and Linda Spaninks Rooted divergence-preserving branching bisimilarity is a congruence Logical Methods in Computer Science, Volume 16, Issue 3, pp. 14:0-14;16, August, 2020
		Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat Feasibility of cross-chain payment with success guarantees 32nd ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2020, pp. 579-581, Virtual event, July, 2020
		Rob van Glabbeek and Kees Middelburg On infinite guarded recursive specifications in process algebra Technical Report, Data61, CSIRO, May, 2020
		Ryan Barry, Rob van Glabbeek and Peter Hoefner Formalising the optimised link state routing protocol 4th Workshop on Models for Formal Analysis of Real Systems (MARS 2020), pp. 40-71, Dublin, Ireland, April, 2020
		Jack Drury, Peter Hoefner and Weiyou Wang Formal models of the OSPF routing protocol MARS2020, pp. 72–120, Dublin, Ireland, April, 2020

2019

		Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat Cross-chain payment protocols with success guarantees Technical Report, Data61, CSIRO, December, 2019
		Rob van Glabbeek, Ursula Goltz, Christopher Lippert and Mennicke Stephan Stronger validity criteria for encoding synchrony The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy — Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pp. 182-205, Paris, November, 2019
		Wan Fokkink, Rob van Glabbeek and Bas Luttik Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence Information and Computation, Volume 268, October, 2019
		Rob Sison and Toby Murray Verifying that a compiler preserves concurrent value-dependent information-flow security International Conference on Interactive Theorem Proving, pp. 27:1–27:19, Portland, USA, September, 2019
		Wan Fokkink and Rob van Glabbeek Proceedings 30th international conference on concurrency theory (CONCUR 2019) Volume 140 in Leibniz International Proceedings in Informatics (LIPIcs) 140. Schloss Dagstuhl—Leibniz-Zentrum für Informatik, Amsterdam, August, 2019
		Rob van Glabbeek Ensuring liveness properties of distributed systems: Open problems Journal of Logical and Algebraic Methods in Programming, Volume 109, pp. 1-19, August, 2019
		Rob van Glabbeek On the meaning of transition system specifications Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics, pp. 69–85, Amsterdam, The Netherlands, August, 2019
		Rob van Glabbeek and Peter Hoefner Progress, justness and fairness ACM Computing Surveys, Volume 52, Issue 4, pp. 69:1–69:38, August, 2019
		Rob van Glabbeek Reward testing equivalences for processes Models, Languages, and Tools for Concurrent and Distributed Programming, Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, pp. 45-70, Volume 11665 in Lecture Notes in Computer Science, Springer, 2019
		Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality FORTE 2019: International Conference on Formal Techniques for Distributed Systems, pp. 3-20, Lyngby, Denmark, June, 2019 Best paper award
		Johannes Åman Pohjola Psi-calculi revisited: Connectivity and compositionality Technical Report, Data61, CSIRO, April, 2019
		Peter Hoefner, Rob van Glabbeek and Michael Markl A process algebra for link layer protocols European Symposium on Programming, Prague, Czech Republic, April, 2019
		Rob van Glabbeek Justness: A completeness criterion for capturing liveness properties International Conference on Foundations of Software Science and Computational Structures, pp. 505-522, Prague, Czech Republic, April, 2019
		Nick Fischer and Rob van Glabbeek Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours Journal of Logical and Algebraic Methods in Programming, Volume 102, pp. 64-102, January, 2019

2018

		Callum Bannister and Peter Hoefner False failure: Creating failure models for separation logic 17th International Conference on Relational and Algebraic Methods in Computer Science, pp. 263-279, Groningen, October, 2018
		Alejandro Gomez-Londono and Johannes Åman Pohjola Connecting choreography languages with verified stacks at Nordic Workshop on Programming Theory, Oslo, Norway, October, 2018
		Rob van Glabbeek and Peter Hoefner Progress, justness and fairness Technical Report, Data61, CSIRO, October, 2018
		Rob van Glabbeek On the validity of encodings of the synchronous in the asynchronous π-calculus Information Processing Letters, Volume 137, pp. 17-25, September, 2018
		Rob van Glabbeek Is speed-independent mutual exclusion implementable? International Conference on Concurrency Theory (CONCUR), Beijing, China, September, 2018
		Rob van Glabbeek, Peter Hoefner and Djurre van der Wal Analysing AWN-specifications using mCRL2 (extended abstract) 14th International Conference on integrated Formal Methods, pp. 398-418, Maynooth, September, 2018
		Callum Bannister, Peter Hoefner and Gerwin Klein Backwards and forwards with separation logic International Conference on Interactive Theorem Proving, pp. 68–87, Oxford, July, 2018
		Toby Murray, Rob Sison and Kai Engelhardt COVERN: A logic for compositional verification of information flow control European Conference on Security and Privacy (EuroS&P), London, United Kingdom, April, 2018
		Rob van Glabbeek A theory of encodings and expressiveness International Conference on Foundations of Software Science and Computational Structures, pp. 183-202, Thessaloniki, Greece, April, 2018
		John Gallager, Rob van Glabbeek and Wendelin Serwe Proceedings third workshop on models for formal analysis of real systems and sixth international workshop on verification and program transformation Volume 268 in EPTCS 268. Open Publishing Association, Thessaloniki, Greece, March, 2018
		Rudolf Brghammer, Hitoshi Furusawa, Walter Guttmann and Peter Hoefner Relational characterisations of paths Technical Report, Data61, CSIRO, January, 2018
		Annabelle McIver, Carroll Morgan, Benjamin Kaminski and Joost-Pieter Katoen A new proof rule for almost-sure termination ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, January, 2018
		Rob Sison Per-thread compositional compilation for confidentiality-preserving concurrent programs 2nd Workshop on Principles of Secure Compilation, Los Angeles, January, 2018

2017

		Rob van Glabbeek and Wan Fokkink Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity Information and Computation, Volume 257, pp. 79-113, December, 2017
		June Andronick From Hoare logic to Owicki-Gries and rely-guarantee for interruptible eChronos and multicore seL4 International Colloquium on Theoretical Aspects of Computing (ICTAC), pp. XIII-XV, Hanoi, Vietnam, October, 2017
		Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson Secure mathematically-assured composition of control models Technical Report, Data61, CSIRO, September, 2017
		Wan Fokkink, Rob van Glabbeek and Bas Luttik Divide and congruence III: Stability & divergence International Conference on Concurrency Theory (CONCUR), pp. 15:1-15:16, Berlin, Germany, September, 2017
		June Andronick Reasoning about concurrency in high-assurance, high-performance software systems International Conference on Automated Deduction, pp. 1–7, Gothenburg, August, 2017
		Victor Dyseryn, Rob van Glabbeek and Peter Hoefner Analysing mutual exclusion using process algebra with signals Combined International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics (EXPRESS/SOS), Berlin, August, 2017
		Wan Fokkink and Rob van Glabbeek Precongruence formats with lookahead through modal decomposition 26th EACSL Annual Conference on Computer Science Logic (CSL'17), Stockholm, Sweden, August, 2017
		Rob van Glabbeek Lean and full congruence formats for recursion Annual IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, August, 2017
		Holger Hermanns and Peter Hoefner Preface: Proceedings of the 2nd workshop on models for formal analysis of real systems Electronic Proceedings in Theoretical Computer Science, pp. -, 2017
		Peter Hoefner, Damien Pous and Georg Struth Preface: Proceedings of the 16th conference on relational and algebraic methods in computer science Lecture Notes in Computer Science, pp. 2, 2017
		Rob van Glabbeek and Peter Hoefner Split, send, reassemble: A formal specification of a CAN bus protocol stack 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), pp. 14-52, Uppsala, Sweden, April, 2017
		Peter Hoefner and Holger Hermanns Proceedings of the 2nd workshop on models for formal analysis of real systems 2nd Workshop on Models for Formal Analysis of Real Systems, Uppsala, Sweden, March, 2017
		Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joey Tuong COMPLX: A verification framework for concurrent imperative programs International Conference on Certified Programs and Proofs, pp. 138–150, Paris, France, January, 2017
		Rob van Glabbeek A branching time model of CSP Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 272-293, Volume 10160 in Lecture Notes in Computer Science, Springer, 2017

2016

		Rudolf Berghammer, Nikita Danilenko, Peter Hoefner and Insa Stucke Cardinality of relations with applications Discrete Mathematics, Volume 339, Number 12, pp. 3089–3115, December, 2016
		Rob van Glabbeek An algebraic treatment of recursion Liber Amicorum for Jan Bergstra, pp. 58-59, University of Amsterdam, 2016
		June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah Proof of OS scheduling behavior in the presence of interrupt-induced concurrency International Conference on Interactive Theorem Proving, pp. 52–68, Nancy, France, August, 2016
		Wan Fokkink and Rob van Glabbeek Divide and congruence II: delay and weak bisimilarity Annual IEEE Symposium on Logic in Computer Science, pp. 778–787, New York City, USA, July, 2016
		Peter Hoefner and Bernhard Möller Extended feature algebra Journal of Logical and Algebraic Methods in Programming, Volume 85, Number 5, pp. 952–971, June, 2016
		Rudolf Berghammer, Peter Hoefner and Insa Stucke Cardinality of relations and relational approximation algorithms Journal of Logical and Algebraic Methods in Programming, Volume 85, Number 2, pp. 269–286, May, 2016
		Emile Bres, Rob van Glabbeek and Peter Hoefner A timed process algebra for wireless networks with an application in routing (extended abstract) European Symposium on Programming, pp. 95–122, Eindhoven, The Netherlands, April, 2016
		Wan Fokkink and Rob van Glabbeek Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity Technical Report 9351, NICTA, April, 2016
		Timothy Bourke, Rob van Glabbeek and Peter Hoefner Mechanizing a process algebra for network protocols Journal of Automated Reasoning, Volume 56, Number 3, pp. 309–341, March, 2016
		Emile Bres, Rob van Glabbeek and Peter Hoefner A timed process algebra for wireless networks with an application in routing Technical Report, NICTA, February, 2016

2015

		June Andronick, Corey Lewis and Carroll Morgan Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10–24, Suva, Fiji, November, 2015
		Peter Hoefner Using process algebra to design better protocols (abstract) Forum “Math-for-Industry” 2015, pp. 31–33, Fukuoka, Japan, October, 2015
		Rudolf Berghammer, Peter Hoefner and Insa Stucke Tool-based verification of a relational vertex coloring program International Conference on Relational and Algebraic Methods in Computer Science, pp. 18, Braga, September, 2015
		Mojgan Kamali, Peter Hoefner, Maryam Kamali and Luigia Petre Formal analysis of proactive, distributed routing Software Engineering and Formal Methods, pp. 15, York, UK, September, 2015
		Kirstin Peters and Rob van Glabbeek Analysing and comparing encodability criteria Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, pp. 46–60, Madrid, Spain, August, 2015
		Wolfram Kahl, Timothy G. Griffin and Peter Hoefner Preface: Special issue on relational and algebraic methods in computer science Journal of Logical and Algebraic Methods in Programming, Volume 84, Number 3, pp. 283–284, May, 2015
		Don Batory, Peter Hoefner, Dominik Köppl and Bernhard Möller Structured document algebra in action Lecture Notes in Computer Science, Volume 8950, pp. 291–311, March, 2015

2014

		Timothy Bourke, Rob van Glabbeek and Peter Hoefner A mechanized proof of loop freedom of the (untimed) AODV routing protocol International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 47–63, Sydney, Australia, November, 2014
		Timothy Bourke, Rob van Glabbeek and Peter Hoefner Showing invariance compositionally for a process algebra for network protocols International Conference on Interactive Theorem Proving, pp. 44–59, Vienna, Austria, July, 2014
		Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan Real reward testing for probabilistic processes Theoretical Computer Science, Volume 538, pp. 16–36, July, 2014
		Peter Hoefner, Peter Jipsen, Wolfram Kahl and Martin Eric Müller Preface: Relational and algebraic methods in computer science Lecture Notes in Computer Science, pp. 2, 2014
		Rudolf Berghammer, Peter Hoefner and Insa Stucke Automated verification of relational while-programs International Conference on Relational and Algebraic Methods in Computer Science, pp. 16, Marienstatt im Westerwald, Germany, April, 2014
		Peter Hoefner and Annabelle McIver Hopscotch—reaching the target hop by hop Journal of Logical and Algebraic Methods in Programming (JLAMP), Volume 83, Number 2, pp. 212–224, April, 2014

2013

		Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV Technical Report 5513, NICTA, December, 2013
		Don Batory, Peter Hoefner, Bernhard Möller and Andreas Zelend Features, modularity, and variation points Fifth International Workshop on Feature-Oriented Software Development (FOSD), pp. 8, Indianapolis, Indiana, USA, October, 2013
		Ansgar Fehnker, Peter Hoefner, Maryam Kamali and Vinay Mehta Topology-based mobility models for wireless networks International Conference on Quantitative Evaluation of SysTems, pp. 16, Buenos Aires, Argentina, August, 2013
		Peter Hoefner and Maryam Kamali Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking International Conference on Formal Modeling and Analysis of Timed Systems, pp. 15, Buenos Aires, Argentina, August, 2013
		Peter Hoefner and Annabelle McIver Statistical model checking of wireless mesh routing protocols 5th NASA Formal Methods Symposium (NFM 2013), pp. 15, Moffett Field, CA, USA, May, 2013

2012

		Peter Hoefner and Sarah Edenhofer Towards a rigorous analysis of AODVv2 (DYMO) 2nd International Workshop on Rigorous Protocol Engineering (WRiPE 2012), pp. 1–6, Austin, Texas, October, 2012
		Peter Hoefner, Rob van Glabbeek, Wee Lum Tan, Marius Portmann, Annabelle McIver and Ansgar Fehnker A rigorous analysis of AODV and its variants 15th ACM/IEEE International Conference on Modelling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM 2012), pp. 203–212, Paphos, Cyprus, October, 2012
		Peter Hoefner, Bernhard Möller and Andreas Zelend Foundations of coloring algebra with consequences for feature-oriented programming International Conference on Relational and Algebraic Methods in Computer Science, pp. 16, Cambridge, UK, September, 2012
		Peter Hoefner Towards a representation theorem for coloring algebra Abstract, Workshop on Lattices and Relations, August, 2012.
		Peter Hoefner Kleene modules for routing procedures Abstract, Workshop on Lattices and Relations, August, 2012.
		Peter Hoefner, Rob van Glabbeek and Ian Hayes Preface—Morgan: A suitable case for treatment Formal Aspects of Computing, Volume 24, Number 4-6, pp. 417–422, July, 2012
		Peter Hoefner and Bernhard Möller Dijkstra, Floyd and Warshall meet Kleene Formal Aspects of Computing (FAOC), Volume 24, Number 4-6, pp. 459–476, July, 2012
		Wan Fokkink, Rob van Glabbeek and Paulien de Wind Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity Information and Computation, Volume 214, Number , pp. 59–85, May, 2012
		Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan A process algebra for wireless mesh networks European Symposium on Programming, pp. 295–315, Tallinn, Estonia, March, 2012
		Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan Automated analysis of AODV using UPPAAL International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 173–187, Tallinn, Estonia, March, 2012

2011

		Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan Modelling and analysis of AODV in UPPAAL 1st International Workshop on Rigorous Protocol Engineering, pp. 1–6, Vancouver, October, 2011
		Peter Hoefner, Don Batory and Jongwook Kim Feature interactions, products, and composition Generative Programming and Component Engineering (GPCE'11), pp. 13–22, Portland, OR, United States, October, 2011
		Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan Real reward testing for probabilistic processes (extended abstract) Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), pp. 61–73, Saarbrücken, Germany, July, 2011
		Peter Hoefner, Ridha Khedri and Bernhard Möller Supplementing product families with behaviour International Journal of Software and Informatics (IJSI), Volume 5, Number 1-2, Part II, pp. 245–266, July, 2011
		Han-Hing Dang, Bernhard Möller and Peter Hoefner Algebraic separation logic The Journal of Logic and Algebraic Programming, Volume 80, Number 6, pp. 221–247, June, 2011
		Peter Hoefner and Bernhard Möller Fixing zeno gaps Theoretical Computer Science, Volume 412, Number 28, pp. 3303–3322, June, 2011
		Peter Hoefner and Annabelle McIver Towards an algebra of routing tables 12th International Conference on Relational and Algebraic Methods in Computer Science, pp. 212–229, Rotterdam, Netherlands, May, 2011

2010

Yuxin Deng and Rob van Glabbeek Characterising probabilistic processes logically (extended abstract) International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 278–293, Yogyakarta, Indonesia, October, 2010

2009

		Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan Testing finitary probabilistic processes (extended abstract) International Conference on Concurrency Theory (CONCUR), pp. 274–288, Bologna, Italy, August, 2009
		Taolue Chen, Wan Fokkink and Rob van Glabbeek On finite bases for weak semantics: Failures versus impossible futures 35th Conference on Current Trends in Theory and Practice of Computer Science, pp. 167–180, Spindleruv Mlyn, Czech Republic , January, 2009

2008

		Taolue Chen, Wan Fokkink and Rob van Glabbeek Ready to preorder: The case of weak process semantics Information Processing Letters, Volume 109, Number 2, pp. 104–111, December, 2008
		Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan Characterising testing preorders for finite probabilistic processes Logical Methods in Computer Science, Volume 4, Number 4, pp. 1–33, October, 2008

2007

		Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang Characterising testing preorders for finite probabilistic processes Annual IEEE Symposium on Logic in Computer Science, pp. 313–322, Wroclaw, Poland, July, 2007
		Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang Remarks on testing probabilistic processes Electronic Notes in Theoretical Computer Science, Volume 172, Number , pp. 359–397, April, 2007
		Yuxin Deng, Rob van Glabbeek, Carroll Morgan and Chenyi Zhang Scalar outcomes suffice for finitary probabilistic testing European Symposium on Programming, pp. 363–378, Braga, Portugal, March, 2007