Skip to main content

Concurrency and Protocol Verification

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:
  • Concurrency in Operating Systems: We aim to provide frameworks for reasoning about concurrency in code for operating systems. In particular, our main two projects are to model and verify the eChronos RTOS and a 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

2017

Abstract to be published 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), pp. 17, Berlin, August, 2017
Abstract to be published Wan Fokkink and Rob van Glabbeek
Precongruence formats with lookahead through modal decomposition
26th EACSL Annual Conference on Computer Science Logic (CSL'17), pp. 20 p., Stockholm, Sweden, August, 2017
Abstract to be published Rob van Glabbeek
Lean and full congruence formats for recursion
Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 11 p., Reykjavik, Iceland, August, 2017
Abstract PDF Rob van Glabbeek
Lean and full congruence formats for recursion
Proceedings 32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, June, 2017
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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, March, 2017
Abstract PDF Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong
COMPLX: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138-150, Paris, France, January, 2017
Abstract PDF 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

Abstract PDF 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
Abstract PDF Rob van Glabbeek
An algebraic treatment of recursion
Liber Amicorum for Jan A. Bergstra, pp. 58-59, Informatics Institute, University of Amsterdam, 2016
Abstract to be published Rob van Glabbeek
An algebraic treatment of recursion
Liber Amicorum for Jan Bergstra, pp. 58-59, University of Amsterdam, 2016
Abstract PDF 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
Abstract PDF Rob van Glabbeek, Peter Hoefner, Marius Portmann and Wee Lum Tan
Modelling and verifying the AODV routing protocol
Distributed Computing, Volume 29, Number 4, pp. 279-315, August, 2016
Abstract PDF Wan Fokkink and Rob van Glabbeek
Divide and congruence II: delay and weak bisimilarity
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 778-787, New York City, USA, July, 2016
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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

Abstract
Slides
PDF 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
Abstract PDF Rob van Glabbeek, Jan Friso Groote and Peter Hoefner
Preface: Proceedings of the workshop on models for formal analysis of real systems
Electronic Proceedings in Theoretical Computer Science, pp. -, Open Publishing Association, 2015
Abstract PDF Peter Hoefner
Using process algebra to design better protocols (abstract)
Forum “Math-for-Industry” 2015, pp. 31-33, Fukuoka, Japan, October, 2015
Abstract PDF 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
Abstract PDF 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
Abstract PDF Rob van Glabbeek
Structure preserving bisimilarity, supporting an operational petri net semantics of CCSP
Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, pp. 99-130, Oldenburg, Germany, September, 2015
Abstract PDF Rob van Glabbeek, Taolue Chen and Wan Fokkink
On the axiomatizability of impossible futures
Logical Methods in Computer Science, Volume 11, Number 3, pp. 1-31, September, 2015
Abstract PDF 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
Abstract PDF 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, pp. 283-284, 2015
Abstract PDF Rob van Glabbeek and Peter Hoefner
CCS: It's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
Acta Informatica, Volume 52, Number 2-3, pp. 175-205, April, 2015
Abstract PDF 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
Abstract PDF Rob van Glabbeek, Ursula Goltz and Ernst-Rüdiger Olderog
Special issue on "Combining Compositionality and Concurrency": Part 1
Acta Informatica, pp. 3-4, Springer, 2015
Abstract PDF Rob van Glabbeek and Peter Hoefner
Progress, fairness and justness in process algebra
Technical Report 8501, NICTA, January, 2015

2014

Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Rudolf Berghammer, Peter Hoefner and Insa Stucke
Automated verification of relational while-programs
14th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2014), pp. 16, Marienstatt im Westerwald, Germany, April, 2014
Abstract PDF 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

Abstract PDF 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
Abstract PDF Rob van Glabbeek, Peter Hoefner, Wee Lum Tan and Marius Portmann
Sequence numbers do not guarantee loop freedom - AODV can yield routing loops
16th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems, pp. 91-100, Barcelona, Spain, November, 2013
Abstract PDF 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
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke-Uffmann
On characterising distributability
Logical Methods in Computer Science, Volume 9, Number 3, pp. 1-58, September, 2013
Abstract PDF Tyler Crain, Vincent Gramoli and Michel Raynal
A contention-friendly binary search tree
19th International Conference on Parallel Processing, pp. 229-240, Aachen, Germany, August, 2013
Abstract PDF Ansgar Fehnker, Peter Hoefner, Maryam Kamali and Vinay Mehta
Topology-based mobility models for wireless networks
10th International Conference on Quantitative Evaluation of SysTems (QEST 2013), pp. 16, Buenos Aires, Argentina, August, 2013
Abstract PDF Peter Hoefner and Maryam Kamali
Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking
11th International Conference on Formal Modeling and Analysis of Timed Systems (Formats '13), pp. 15, Buenos Aires, Argentina, August, 2013
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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
Abstract PDF Peter Hoefner, Bernhard Möller and Andreas Zelend
Foundations of coloring algebra with consequences for feature-oriented programming
13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 13), pp. 16, Cambridge, UK, September, 2012
Abstract PDF Peter Hoefner
Towards a representation theorem for coloring algebra
Abstract, Workshop on Lattices and Relations, August, 2012.
Abstract PDF Peter Hoefner
Kleene modules for routing procedures
Abstract, Workshop on Lattices and Relations, August, 2012.
Abstract PDF Rob van Glabbeek
Musings on encodings and expressiveness
Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structural Operational Semantics, pp. 81–98, Newcastle upon Tyne, United Kingdom, August, 2012
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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 (I&C), Volume 214, Number , pp. 59-85, May, 2012
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
A process algebra for wireless mesh networks
22nd European Symposium on Programming (ESOP 2012), pp. 295-315, Tallinn, Estonia, March, 2012
Abstract PDF Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan
Automated analysis of AODV using UPPAAL
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), pp. 173-187, Tallinn, Estonia, March, 2012
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke-Uffmann
On distributability of petri nets (extended abstract)
15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), pp. 331–345, Tallinn, Estonia, March, 2012

2011

Abstract PDF Rob van Glabbeek
Bisimulation
Encyclopedia of Parallel Computing, pp. 136-139, Volume 1 in , Springer, 2011
Abstract PDF 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
Abstract PDF 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
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
On causal semantics of petri nets (extended abstract)
22nd International Conference on Concurrency Theory, pp. 43-59, Aachen, Germany, September, 2011
Abstract PDF 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
Abstract PDF 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
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
Abstract processes of place/transition systems
Information Processing Letters, Volume 111, Number 13, pp. 626-633, July, 2011
Abstract PDF 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
Abstract PDF Peter Hoefner and Bernhard Möller
Fixing zeno gaps
Theoretical Computer Science, Volume 412, Number 28, pp. 3303-3322, June, 2011
Abstract PDF Rob van Glabbeek
On cool congruence formats for weak bisimulations
Theoretical Computer Science, Volume 412, Number 28, pp. 3283-3302, June, 2011
Abstract PDF 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

Abstract PDF Yuxin Deng and Rob van Glabbeek
Characterising probabilistic processes logically (extended abstract)
Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 278-293, Yogyakarta, Indonesia, October, 2010
Abstract PDF Rob van Glabbeek
The coarsest precongruences respecting safety and liveness properties
Theoretical Computer Science 2010, pp. 32-52, Brisbane, September, 2010
Abstract PDF Rob van Glabbeek and Gordon Plotkin
On CSP and the algebraic theory of effects
Reflections on the Work of C.A.R. Hoare, pp. 333-369, Volume in History of Computing, Springer, 2010

2009

Abstract PDF Rob van Glabbeek, Bas Luttik and Nikola Trčka
Computation tree logic with deadlock detection
Logical Methods in Computer Science, Volume 5, Number 4:5, pp. 1-24, December, 2009
Abstract PDF Rob van Glabbeek and Gordon Plotkin
Configuration structures, event structures and petri nets
Theoretical Computer Science, Volume 410, Number 41, pp. 4111-4159, September, 2009
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Testing finitary probabilistic processes (extended abstract)
20th International Conference on Concurrency Theory (CONCUR 2009), pp. 274-288, Bologna, Italy, August, 2009
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
Symmetric and asymmetric asynchronous interaction
Electronic Notes in Theoretical Computer Science, Volume 229, Number 3, pp. 77-95, July, 2009
Abstract PDF Rob van Glabbeek, Bas Luttik and Nikola Trčka
Branching bisimilarity with explicit divergence
Fundamenta Informaticae, Volume 93, Number 4, pp. 371-392, June, 2009
Abstract PDF Rob van Glabbeek and Peter D. Mosses
Preface, special issue on structural operational semantics
Information and Computation, pp. 83-84, Elsevier, 2009
Abstract PDF 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

Abstract PDF 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
Abstract PDF 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
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
On synchronous and asynchronous interaction in distributed systems
33nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2008), pp. 16-35, Torun, Poland, August, 2008
Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke
Symmetric and asymmetric asynchronous interaction
First Interaction and Concurrency Experience (ICE'08): Synchronous and Asynchronous Interactions in Concurrent Distributed Systems, pp. 5-22, Reykjavik, Iceland, July, 2008
Best student/young researcher paper.
Abstract PDF Rob van Glabbeek and Bas Ploeger
Correcting a space-efficient simulation algorithm
20th International Conference on Computer Aided Verification, CAV 2008, pp. 517-529, Princeton, USA, July, 2008
Abstract PDF Rob van Glabbeek and Bas Ploeger
Five determinisation algorithms
13th International Conference on Implementation and Application of Automata, pp. 161-170, San Francisco, July, 2008

2007

Abstract PDF Rob van Glabbeek and Matthew Hennessy
Preface, proceedings of the 4th workshop on structural operational semantics
Electronic Notes in Theoretical Computer Science, pp. 1-3, Elsevier, 2007
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang
Characterising testing preorders for finite probabilistic processes
22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 313-322, Wroclaw, Poland, July, 2007
Abstract PDF Rob van Glabbeek and Peter D. Mosses
Preface, proceedings of the 3rd workshop on structural operational semantics
Electronic Notes in Theoretical Computer Science, pp. 1-2, Elsevier, 2007
Abstract PDF 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
Abstract PDF Yuxin Deng, Rob van Glabbeek, Carroll Morgan and Chenyi Zhang
Scalar outcomes suffice for finitary probabilistic testing
16th European Symposium on Programming, ESOP 2007, pp. 363-378, Braga, Portugal, March, 2007

Contact

Peter Höfner, Peter.Hoefner <at> data61.csiro.au
Served by Apache on Linux on seL4.