Trustworthy Systems

Paper/Talk Abstract plain text Paper in PDF format PDF
Presentation slides Slides Video of the presentation Presentation
A reference to a location Link Paper yet to be published to be published

Publications related to Formal Methods @ TS

To appear

Abstract to be published Robert van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke-Uffmann
Abstract processes and conflicts in place/transition systems
Information and Computation, Volume 281

2025

Abstract PDF Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish and Gernot Heiser
Verifying device drivers with Pancake
arXiv preprint, January, 2025

2023

Abstract PDF Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Tsun Wang Sau, Benjamin Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus O. Myreen, Michael Norrish and Gernot Heiser
Pancake: verified systems programming made sweeter
Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023
Abstract PDF Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola and Riccardo Zanetti
PureCake: A verified compiler for a lazy functional language
Proceedings of the ACM on Programming Languages, Volume 7, Number PLDI, pp. 952–976, 2023

2022

Abstract PDF Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker and Michael Norrish
Kalas: A verified, end-to-end compiler for a choreographic language
International Conference on Interactive Theorem Proving, pp. 27:1–27:18, Haifa, Israel, August, 2022

2021

Abstract to be published Michael Norrish and Hing-Lun Chan
Mechanisation of the AKS algorithm
Journal of Automated Reasoning, Volume 65, Issue 2, pp. 205–256, February, 2021
Abstract to be published Elliot Catt and Michael Norrish
On the formalisation of kolmogorov complexity
Certified Proofs and Programs, pp. 291–299, Online, January, 2021
Abstract PDF Richard S. Bird, Jeremy Gibbons, Ralf Hinze, Peter Höfner, 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

Abstract PDF Robert 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
Abstract PDF Robert 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
Abstract PDF Robert 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
Abstract PDF Michael Norrish and Yiming Xu
Mechanised modal model theory
International Joint Conference on Automated Reasoning, pp. 518-533, Paris, July, 2020
Abstract PDF Robert van Glabbeek, Vincent Gramoli and Pierre Tholoniat
Feasibility of cross-chain payment with success guarantees
Annual ACM Symposium on Parallelism in Algorithms and Architectures, pp. 579-581, July, 2020
Abstract PDF Robert van Glabbeek and Kees Middelburg
On infinite guarded recursive specifications in process algebra
Technical Report, Data61, CSIRO, May, 2020
Abstract PDF Ryan Barry, Robert van Glabbeek and Peter Höfner
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
Abstract PDF Jack Drury, Peter Höfner and Weiyou Wang
Formal models of the OSPF routing protocol
MARS2020, pp. 72–120, Dublin, Ireland, April, 2020

2019

Abstract PDF Robert van Glabbeek, Vincent Gramoli and Pierre Tholoniat
Cross-chain payment protocols with success guarantees
Technical Report, Data61, CSIRO, December, 2019
Abstract PDF Robert 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
Abstract PDF Wan Fokkink, Robert 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
Abstract PDF Wan Fokkink and Robert 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
Abstract PDF Robert 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
Abstract PDF Robert 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
Abstract PDF Robert van Glabbeek and Peter Höfner
Progress, justness and fairness
ACM Computing Surveys, Volume 52, Issue 4, pp. 69:1–69:38, August, 2019
Abstract PDF Robert 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
Abstract PDF Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus Myreen, Michael Norrish, Oskar Abrahamsson and Anthony Fox
Verified compilation on a verified processor
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 1041-1053, Phoenix, AZ, US, June, 2019
Abstract PDF Peter Höfner, Robert van Glabbeek and Michael Markl
A process algebra for link layer protocols
European Symposium on Programming, Prague, Czech Republic, April, 2019
Abstract PDF Robert 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
Abstract PDF Hing-Lun Chan and Michael Norrish
Proof pearl: Bounding least common multiples with triangles
Journal of Automated Reasoning, Volume 62, Issue 2, pp. 171-192, February, 2019
Abstract PDF Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish
The verified CakeML compiler backend
Journal of Functional Programming, Volume 29, February, 2019
Abstract PDF Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith and Keith Wanbrough
Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the sockets API
Journal of the ACM, Volume 66, Issue 1, January, 2019
Abstract PDF Nick Fischer and Robert 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

Abstract PDF Milad Ghale, Dirk Pattinson, Ramana Kumar and Michael Norrish
Verified certificate checking for counting votes
Verified Software: Theories, Tools and Experiments, pp. 69–87, Oxford, December, 2018
Abstract PDF Callum Bannister and Peter Höfner
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
Abstract PDF Robert van Glabbeek and Peter Hofner
Progress, justness and fairness
Technical Report, Data61, CSIRO, October, 2018
Abstract PDF Robert van Glabbeek
On the validity of encodings of the synchronous in the asynchronous π-calculus
Information Processing Letters, Volume 137, pp. 17-25, September, 2018
Abstract PDF Robert van Glabbeek
Is speed-independent mutual exclusion implementable?
International Conference on Concurrency Theory (CONCUR), Beijing, China, September, 2018
Abstract PDF Robert van Glabbeek, Peter Höfner 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
Abstract PDF Callum Bannister, Peter Höfner and Gerwin Klein
Backwards and forwards with separation logic
International Conference on Interactive Theorem Proving, pp. 68–87, Oxford, July, 2018
Abstract PDF Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus Myreen, Yong Kiam Tan and Michael Norrish
Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
International Joint Conference on Automated Reasoning, pp. 646-662, Oxford, July, 2018
Abstract PDF Simon Jantsch and Michael Norrish
Verifying the LTL to Büchi automata translation via very weak alternating automata
International Conference on Interactive Theorem Proving, pp. 306-323, Oxford, July, 2018
Abstract PDF Robert 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
Abstract PDF John Gallager, Robert 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
Abstract PDF Kunshan Wang, Stephen Blackburn, Tony Hosking and Michael Norrish
Hop, skip, & jump: Practical on-stack replacement for a cross-platform language-neutral VM
International Conference on Virtual Execution Environments, pp. 1-16, Williamsburg, VA, March, 2018
Abstract PDF Rudolf Berghammer, Hitoshi Furusawa, Walter Guttmann and Peter Höfner
Relational characterisations of paths
Technical Report, Data61, CSIRO, January, 2018

2017

Abstract PDF Robert 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
Abstract PDF Wan Fokkink, Robert 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
Abstract PDF Scott Owens, Michael Norrish, Ramana Kumar, Yong Kiam Tan and Magnus Myreen
Verifying efficient function calls in CakeML
International Conference on Functional Programming, Oxford, September, 2017
Abstract PDF Victor Dyseryn, Robert van Glabbeek and Peter Höfner
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
Abstract PDF Wan Fokkink and Robert van Glabbeek
Precongruence formats with lookahead through modal decomposition
26th EACSL Annual Conference on Computer Science Logic (CSL'17), Stockholm, Sweden, August, 2017
Abstract PDF Robert van Glabbeek
Lean and full congruence formats for recursion
Annual IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, August, 2017
Abstract PDF Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish
Verified characteristic formulae for CakeML
European Symposium on Programming, pp. 584-610, Uppsala, April, 2017
plain text PDF Holger Hermanns and Peter Höfner
Preface: Proceedings of the 2nd workshop on models for formal analysis of real systems
Electronic Proceedings in Theoretical Computer Science, 2017
plain text PDF Peter Höfner, 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 Robert van Glabbeek and Peter Höfner
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
Abstract PDF Peter Höfner 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
Abstract PDF Robert 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 Höfner and Insa Stucke
Cardinality of relations with applications
Discrete Mathematics, Volume 339, Number 12, pp. 3089–3115, December, 2016
Abstract PDF Robert van Glabbeek
An algebraic treatment of recursion
Liber Amicorum for Jan Bergstra, pp. 58-59, University of Amsterdam, 2016
Abstract PDF Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish
A new verified compiler backend for CakeML
International Conference on Functional Programming, pp. 14, Nara, Japan, September, 2016
Abstract PDF Wan Fokkink and Robert 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
plain text PDF Peter Höfner 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 Yi Lin, Steve Blackburn, Tony (Antony) Hosking and Michael Norrish
Rust as a language for high performance GC implementation
International Symposium on Memory Management, pp. 89–98, Santa Barbara, California, USA, June, 2016
Abstract PDF Rudolf Berghammer, Peter Höfner 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, Robert van Glabbeek and Peter Höfner
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 Robert 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, Robert van Glabbeek and Peter Höfner
Mechanizing a process algebra for network protocols
Journal of Automated Reasoning, Volume 56, Number 3, pp. 309–341, March, 2016
Abstract PDF Emile Bres, Robert van Glabbeek and Peter Höfner
A timed process algebra for wireless networks with an application in routing
Technical Report, NICTA, February, 2016

2015

plain text PDF Peter Höfner
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 Höfner 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 Höfner, Maryam Kamali and Luigia Petre
Formal analysis of proactive, distributed routing
Software Engineering and Formal Methods, pp. 15, York, UK, September, 2015
Abstract PDF Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Verified over-approximation of the diameter of propositionally factored transition systems
International Conference on Interactive Theorem Proving, pp. 1–16, Nanjing, China, August, 2015
Abstract PDF Joseph Chan and Michael Norrish
Mechanisation of AKS algorithm: Part 1 — the main theorem
International Conference on Interactive Theorem Proving, pp. 117–136, Nanjing, China, August, 2015
Abstract PDF Kirstin Peters and Robert 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 Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Exploiting symmetries by planning for a descriptive quotient
International Joint Conference on Artificial Intelligence, pp. 1479–1486, Buenos Aires, July, 2015
Abstract PDF Yi Lin, Stephen M. Blackburn, Kunshan Wang, Tony (Antony) Hosking and Michael Norrish
Stop and go: Understanding yieldpoint behavior
International Symposium on Memory Management, pp. 70–80, Portland, OR, USA, June, 2015
Abstract PDF Wolfram Kahl, Timothy G. Griffin and Peter Höfner
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
Abstract PDF Michael Norrish and Michelle Mills Strout
An approach for proving the correctness of inspector/executor transformations
Languages and Compilers for Parallel Computing, pp. 131–145, Hillsboro, Oregon, USA, May, 2015
Abstract PDF Kunshan Wang, Yi Lin, Stephen M Blackburn, Michael Norrish and Tony (Antony) Hosking
Draining the swamp: Micro virtual machines as a solid foundation for language development
SNAPL, pp. 321–336, Asilomar, California, May, 2015
Abstract PDF Don Batory, Peter Höfner, 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

Abstract PDF Timothy Bourke, Robert van Glabbeek and Peter Höfner
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, Robert van Glabbeek and Peter Höfner
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, Robert 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 Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish
Beagle as a HOL4 external ATP method
Practical Aspects of Automated Reasoning, pp. 50–59, Vienna, July, 2014
Abstract
Slides 		PDF Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Mechanising theoretical upper bounds in planning
Workshop on Knowledge Engineering for Planning and Scheduling, Portsmouth, USA, June, 2014
plain text PDF Peter Höfner, 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 Höfner 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
plain text PDF Peter Höfner 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
Abstract PDF Aditi Barthwal and Michael Norrish
A mechanisation of some context-free language theory in HOL4
Journal of Computer and System Sciences, Volume 80, Number 2, pp. 346–362, March, 2014
Abstract PDF Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens
CakeML: A verified implementation of ML
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014

2013

Abstract PDF Joseph Chan and Michael Norrish
A string of pearls: Proofs of fermat's little theorem
Journal of Formal Reasoning, Volume 6, Number 1, pp. 63–87, December, 2013
Abstract PDF Ansgar Fehnker, Robert van Glabbeek, Peter Höfner, 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 Don Batory, Peter Höfner, 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 Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish
Tableaux for verification of data-centric processes
Automated Reasoning with Analytic Tableaux and Related Methods, pp. 28–43, Nancy, France, September, 2013
Abstract PDF Ansgar Fehnker, Peter Höfner, 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
plain text PDF Peter Höfner 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
Abstract
Slides 		PDF Michael Norrish and Brian Huffman
Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω1
International Conference on Interactive Theorem Proving, pp. 133–146, Rennes, France, July, 2013
plain text PDF Peter Höfner 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 Hing-Lun Chan and Michael Norrish
A string of pearls: Proofs of fermat’s little theorem
International Conference on Certified Programs and Proofs, pp. 188–207, Kyoto, Japan, October, 2012
plain text PDF Peter Höfner 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
plain text PDF Peter Höfner, Robert 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 Nick Barnes, Peter Baumgartner, Tiberio Caetano, Hugh Durrant-Whyte, Gerwin Klein, Penelope Sanderson, Abdul Sattar, Peter Stuckey, Sylvie Thiebaux, Pascal Van Hentenryck and Toby Walsh
AI @ NICTA
AI Magazine, Volume 33, Number 3, pp. 115–127, September, 2012
plain text PDF Peter Höfner, 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
Abstract PDF James Cheney, Michael Norrish and René Vestergaard
Formalizing adequacy: A case study for higher-order abstract syntax
Journal of Automated Reasoning, Volume 49, Number 2, pp. 209–239, August, 2012
plain text PDF Peter Höfner
Towards a representation theorem for coloring algebra
Abstract, Workshop on Lattices and Relations, August, 2012.
plain text PDF Peter Höfner
Kleene modules for routing procedures
Abstract, Workshop on Lattices and Relations, August, 2012.
plain text PDF Peter Höfner, Robert 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
plain text PDF Peter Höfner 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, Robert 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
Abstract PDF Ansgar Fehnker, Robert van Glabbeek, Peter Höfner, 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
Abstract PDF Ansgar Fehnker, Robert van Glabbeek, Peter Höfner, 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

Abstract PDF Ansgar Fehnker, Robert van Glabbeek, Peter Höfner, 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
plain text PDF Peter Höfner, Don Batory and Jongwook Kim
Feature interactions, products, and composition
Generative Programming and Component Engineering (GPCE'11), pp. 13–22, Portland, OR, US, October, 2011
Abstract
Slides 		PDF Michael Norrish
Mechanised computability theory
International Conference on Interactive Theorem Proving, pp. 297—311, Nijmegen, The Netherlands, August, 2011
Abstract PDF Yuxin Deng, Robert 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
plain text PDF Peter Höfner, 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 Han-Hing Dang, Bernhard Möller and Peter Höfner
Algebraic separation logic
The Journal of Logic and Algebraic Programming, Volume 80, Number 6, pp. 221–247, June, 2011
plain text PDF Peter Höfner and Bernhard Möller
Fixing zeno gaps
Theoretical Computer Science, Volume 412, Number 28, pp. 3303–3322, June, 2011
plain text PDF Peter Höfner 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 Robert 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
Abstract PDF Aditi Barthwal and Michael Norrish
A formalisation of the normal forms of context-free grammars in HOL4
19th EACSL Annual Conferences on Computer Science Logic, pp. 95–109, Brno, Czech Republic, August, 2010
Abstract PDF Aditi Barthwal and Michael Norrish
Mechanisation of PDA and grammar equivalence for context-free languages
17th Workshop on Logic, Language, Information and Computation , pp. 125–135, Brasília, Brazil, July, 2010
Abstract
Slides 		PDF Ramana Kumar and Michael Norrish
(nominal) unification by recursive descent with triangular substitutions
International Conference on Interactive Theorem Proving, pp. 51–66, Edinburgh, UK, July, 2010
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107–115, June, 2010
Research Highlights paper

2009

Abstract PDF Ralf Huuck, Gerwin Klein and Schlich Bastian
Proc. 4th international workshop on system software verification (SSV09)
Electronic Notes in Theoretical Computer Science, Volume 254, pp. 1–3, October, 2009
Abstract
Slides 		PDF
Presentation Video		 Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Best Paper Award
Hall of Fame Award
Abstract PDF Michael Norrish
Rewriting conversions implemented with continuations
Journal of Automated Reasoning, Volume 43, Number 3, pp. 305–336, October, 2009
Abstract PDF Yuxin Deng, Robert 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
Abstract PDF Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish
Mind the gap: A verification framework for low-level C
International Conference on Theorem Proving in Higher Order Logics, pp. 500–515, Munich, Germany, August, 2009
Abstract PDF Gerwin Klein, Ralf Huuck and Bastian Schlich
Operating system verification
Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123–124, April, 2009
Abstract PDF Aditi Barthwal and Michael Norrish
Verified, executable parsing
European Symposium on Programming, pp. 160–174, York, March, 2009
Abstract PDF James Cheney, René Vestergaard and Michael Norrish
Formalizing adequacy
2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming, York, March, 2009
Abstract PDF Taolue Chen, Wan Fokkink and Robert 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 Robert 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, Robert 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 to be published Ansgar Fehnker, Ralf Huuck, Felix Rauch and Sean Seefried
Some assembly required – program analysis of embedded system code
Eighth IEEE International Working Conference on Source Code Analysis and Manipulation, pp. 15–24, Beijing, China, September, 2008
Abstract PDF Konrad Slind and Michael Norrish
A brief overview of HOL4
International Conference on Theorem Proving in Higher Order Logics, pp. 28–32, Montréal, Canada, August, 2008
Abstract PDF Tom Ridge, Michael Norrish and Peter Sewell
A rigorous approach to networking: TCP, from implementation to protocol to service
International Symposium on Formal Methods (FM), pp. 294—309, Turku, Finland, May, 2008

2007

Abstract PDF Michael Norrish
A formal semantics for c++
Technical Report, NICTA, November, 2007
Abstract PDF Michael Norrish and René Vestergaard
Proof pearl: de bruijn terms really do work
International Conference on Theorem Proving in Higher Order Logics, pp. 207–222, Kaiserslautern, September, 2007
Abstract PDF Yuxin Deng, Robert 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
Abstract PDF Ansgar Fehnker, Ralf Huuck, Sean Seefried and Felix Rauch
Analysing embedded system software
Proceedings of C/C++ Verification Workshop, July, 2007
Abstract PDF Ansgar Fehnker, Ralf Huuck, Michel Lussenburg, Felix Rauch and Patrick Jayet
Model checking software at compile time
TASE '07: Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, pp. 45–56, June, 2007
Abstract PDF Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser
Verifying a high-performance micro-kernel
Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
Abstract PDF Yuxin Deng, Robert 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, Robert 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
Abstract PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97–108, Nice, France, January, 2007

2006

Abstract PDF Ansgar Fehnker, Ralf Huuck, Michel Lussenburg, Felix Rauch and Patrick Jayet
Goanna — a static model checker
Formal Methods: Applications and Technology, 11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers, pp. 297–300, August, 2006
Abstract PDF Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 55—66, Charleston, South Carolina, USA, January, 2006

2005

Abstract PDF Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco
L4cars
Embedded Security in Cars Conference (escar), Cologne, DE, November, 2005
Abstract PDF Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets
ACM Conference on Communications, pp. 265–276, Philadelphia, August, 2005

2004

Abstract
Slides 		PDF Michael Norrish
Recursive function definition for types with binders
International Conference on Theorem Proving in Higher Order Logics, pp. 241—256, Park City, UT, US, September, 2004

2003

Abstract
Slides 		PDF Michael Norrish
Complete integer decision procedures as derived rules in HOL
International Conference on Theorem Proving in Higher Order Logics, pp. 71–86, Rome, September, 2003