Publications

Books

2009

• Algebraic Calculi for Hybrid Systems
  — Books on Demand
  Details BibTeX Link

  @book{hoefner2009_phd,
  author = {H{\"o}fner, Peter},
  title     = {{Algebraic Calculi for Hybrid Systems}},
  publisher = {Books on Demand},
  year = {2009},
  Isbn = {9783839125106},
  note ={(Phd Thesis)},
  doi = {}
  }
  

Book Chapters

2024

• Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures
  with Robert J. Colvin, Ian J. Hayes, Scott Heiner, Larissa Meinicke, Roger C. Su
  The Practice of Formal Methods (I) (pp. 65-87) — Springer (Lecture Notes in Computer Science 14780)
  Details BibTeX DOI arXiv PDF ©

  @incollection{hoefner2025_fm,
  author    = {Colvin, Robert J. and
  Hayesm Ian J. and
  Heiner, Scott and
  H{\"o}fner, Peter and
  Meinicke, Larissa and
  Su, Roger C.},
  title     = {{Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures}},
  year      = {2024},
  booktitle = {The Practice of Formal Methods (I)},
  editor       = {Cavalcanti, Ana and
  Baxter, James},
  series    = {Lecture Notes in Computer Science},
  volume    = {14780},
  publisher = {Springer},
  pages     = {65--87},
  doi       = {10.1007/978-3-031-66676-6_4},
  }
  

2021

• Algorithmics
  with Richard Bird, Jeremy Gibbons, Ralf Hinze, Johan Jeuring, Lambert Meertens, Bernhard Möller, Carroll Morgan, Tom Schrijvers, Wouter Swierstra, Nicolas Wu
  — Springer (IFIP Advances in Information and Communication Technology 600)
  Details BibTeX DOI PDF ©

  @inbook{hoefner2021_acit,
  author = {Bird, Richard and 
  Gibbons, Jeremy and 
  Hinze, Ralf and 
  H{\"o}fner, Peter and 
  Jeuring, Johan and 
  Meertens, Lambert and 
  M{\"o}ller, Bernhard and 
  Morgan, Carroll and 
  Schrijvers, Tom and 
  Swierstra, Wouter and 
  Wu, Nicolas},
  editor = {Goedicke, Michael and Neuhold, Erich and Rannenberg, Kai},
  title     = {{Algorithmics}},
  booktitle = {Advancing Research in Information and Communication Technology},
  series = {IFIP Advances in Information and Communication Technology},
  volume = {600},
  pages = {59-98},
  publisher = {Springer},
  year = {2021},
  doi = {10.1007/978-3-030-81701-5_3}
  }
  

2016

• Using Process Algebra to Design Better Protocols
  — Springer (Mathematics for Industry 25)
  Details BibTeX DOI PDF ©

  @inbook{hoefner2016-11,
  author = {H{\"o}fner, P.},
  editor = {Anderssen, B. and Broadbridge, P. and Fukumoto, Y. and Kamiyama, N. and Mizoguchi, Y. and Polthier, K. and Saeki, O.},
  title     = {{Using Process Algebra to Design Better Protocols}},
  booktitle = {The Role and Importance of Mathematics in Innovation},
  series = {Mathematics for Industry},
  volume = {25},
  pages = {87-101},
  publisher = {Springer},
  year = {2016},
  doi = {10.1007/978-981-10-0962-4_8}
  }
  

Journal Articles

2024

• Shoggoth: A Formal Foundation for Strategic Rewriting
  with Xueying Qin, Liam O'Connor, Rob van Glabbeek, Ohad Kammar, Michel Steuwer
  Proceedings of the ACM on Programming Languages , vol. 8 , pp. 61-89
  Details BibTeX DOI PDF ©

  @article{hoefner2024_popl,
  author    = {Qin, Xueying and
  O'Connor, Liam and
  van Glabbeek, Rob and
  H{\"o}fner, Peter and
  Kammar, Ohad and
  Steuwer, Michel},
  title     = {{Shoggoth}: A Formal Foundation for Strategic Rewriting},
  year      = {2024},
  journal   = {Proceedings of the {ACM} on Programming Languages (POPL)},
  volume    = {8},    
  pages     = {61--89},
  doi       = {10.1145/3633211},
  }
  

2020

• Relational Characterisations of Paths
  with Rudolf Berghammer, Furusawa Hitoshi, Walter Guttmann
  Journal of Logic and Algebraic Methods in Programming , vol. 117 — Elsevier
  Details BibTeX DOI arXiv PDF ©

  @article{hoefner2020-3,
  author = {Berghammer, Rudolf and Furusawa, Hitoshi and Guttmann, Walter and H{\"o}fner, Peter},
  title     = {{Relational Characterisations of Paths}},
  journal = {Journal of Logic and Algebraic Methods in Programming},
  volume = {117},
  year = {2020},
  publisher = {Elsevier},
  doi = {10.1016/j.jlamp.2020.100590}
  }
  

• Festschrift for Rob van Glabbeek - Preface
  with Carroll Morgan, Vaughan Pratt
  Acta Informatica , vol. 57 , no. 3-5 — Springer [Special issue / Festschrift]
  Details BibTeX Link PDF ©

  @article{hoefner2020_acta,
  author    = {H{\"o}fner, Peter and Morgan, Carroll and Pratt, Vaughan},
  editor    = {H{\"o}fner, Peter and Morgan, Carroll and Pratt, Vaughan},
  title     = {{Preface}},
  Booktitle     = {Festschrift for Rob van Glabbeek},
  journal   = {Acta Informatica},
  volume    = {57},
  pages ={05–311},
  year      = {2020},
  publisher = {Springer}
  }
  

2019

• Progress, Justness and Fairness
  with Rob van Glabbeek
  ACM Computing Surveys , vol. 52 , no. 4 , pp. 69:1-69:38 — ACM
  Details BibTeX DOI arXiv PDF ©

  @article{hoefner2019_csur,
  author = {van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{Progress, Justness and Fairness}},
  journal = {ACM Computing Surveys},
  number = {4},
  volume = {52},
  pages = {69:1-69:38},
  year = {2019},
  publisher = {ACM},
  doi = {10.1145/3329125}
  }
  

2016

• Cardinality of Relations with Applications
  with Rudolf Berghammer, Nikita Danilenko, Insa Stucke
  Discrete Mathematics , vol. 339 , no. 12 , pp. 3089-3115 — Elsevier
  Details BibTeX DOI PDF ©

  @article{hoefner2016_dm,
  author = {Berghammer, Rudolf and Danilenko, Nikita and H{\"o}fner, Peter and Stucke, Insa},
  title     = {{Cardinality of Relations with Applications}},
  journal = {Discrete Mathematics},
  number = {12},
  volume = {339},
  pages = {3089-3115},
  year = {2016},
  publisher = {Elsevier},
  doi = {10.1016/j.disc.2016.06.019}
  }
  

• Modelling and Verifying the AODV Routing Protocol
  with Rob van Glabbeek, Marius Portmann, Wee Lum Tan
  Distributed Computing , vol. 29 , no. 4 , pp. 279-315 — Springer
  Details BibTeX DOI arXiv PDF ©

  @article{hoefner2016_dc,
  author    = {van Glabbeek, Rob and H{\"o}fner, Peter and Portmann, Marius and Tan, Wee Lum},
  title     = {{Modelling and Verifying the {AODV} Routing Protocol}},
  journal   = {Distributed Computing},
  number    = {4},
  volume    = {29},
  pages     = {279-315},
  year      = {2016},
  publisher = {Springer},
  doi       = {10.1007/s00446-015-0262-7}
  }
  

• Cardinality of Relations and Relational Approximation Algorithms
  with Rudolf Berghammer, Insa Stucke
  Journal of Logic and Algebraic Methods in Programming , vol. 85 , no. 2 , pp. 269-286 — Elsevier
  Details BibTeX DOI PDF ©

  @article{hoefner2016_jlamp,
  author = {Berghammer, Rudolf and H{\"o}fner, Peter and Stucke, Insa},
  title     = {{Cardinality of Relations and Relational Approximation Algorithms}},
  journal = {Journal of Logic and Algebraic Methods in Programming},
  number = {2},
  volume = {85},
  pages = {269-286},
  year = {2016},
  publisher = {Elsevier},
  doi = {10.1016/j.jlamp.2015.12.001}
  }
  

• Extended Feature Algebra
  with Bernhard Möller
  Journal of Logic and Algebraic Methods in Programming , vol. 85 , no. 5 , pp. 952-971 — Elsevier
  Details BibTeX DOI PDF ©

  @article{hoefner2016_jlamp2,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhrd},
  title     = {{Extended Feature Algebra}},
  journal = {Journal of Logic and Algebraic Methods in Programming},
  number = {5},
  volume = {85},
  pages = {952-971},
  year = {2016},
  publisher = {Elsevier},
  doi = {10.1016/j.jlamp.2015.12.002}
  }
  

• Mechanizing a Process Algebra for Network Protocols
  with Timothy Bourke, Rob van Glabbeek
  Journal of Automated Reasoning , vol. 56 , no. 3 , pp. 309-341 — Springer
  Details BibTeX DOI arXiv PDF ©

  @article{hoefner2016_jar,
  author = {Bourke, Timothy and van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{Mechanizing a Process Algebra for Network Protocols}},
  journal = {Journal of Automated Reasoning},
  number = {3},
  volume = {56},
  pages = {309-341},
  year = {2016},
  publisher = {Springer},
  doi = {10.1007/s10817-015-9358-9}
  }
  

2015

• Structured Document Algebra in Action
  with Don Batory, Dominik Köppl, Bernhard Möller, Andreas Zelend
  Software, Services and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Emeritation , vol. 8950 , pp. 291-311 — Springer
  Details BibTeX DOI PDF ©

  @article{hoefner2015-1,
  author = {Batory, Don and H{\"o}fner, Peter and K{\"o}ppl, Dominik and M{\"o}ller, Bernhard and Zelend, Andreas},
  title     = {{Structured Document Algebra in Action}},
  journal = {Software, Services and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Emeritation},
  volume = {8950},
  pages = {291-311},
  year = {2015},
  publisher = {Springer},
  doi = {10.1007/978-3-319-15545-6_19}
  }
  

• CCS: It's not Fair!—Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
  with Rob van Glabbeek
  Acta Informatica , vol. 52 , no. 2-3 , pp. 175-205 — Springer
  Details BibTeX DOI arXiv PDF ©

  @article{hoefner2015_acta,
  author = {van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{CCS: It's not Fair!

2014

• Hopscotch—Reaching the Target Hop by Hop
  with Annabelle McIver
  Journal of Logic and Algebraic Methods in Programming , vol. 83 , no. 2 , pp. 212-224 — Elsevier
  Details BibTeX DOI PDF ©

  @article{hoefner2014_jlamp,
  author = {H{\"o}fner, Peter and McIver, Annabelle},
  title     = {{Hopscotch

2012

• Festschrift in honour of Carroll Morgan
  ed. Peter Höfner, Rob van Glabbeek, Ian J. Hayes
  Formal Aspects of Computing , vol. 24 , no. 4-6 — Springer [Special issue / Festschrift]
  Details BibTeX Link PDF ©

  @misc{hoefner2012_facpre,
  editor    = {H{\"o}fner, Peter and van Glabbeek, Rob and Hayes, Ian J.},
  title     = {{Festschrift in Honour of Carroll Morgan}},
  journal   = {Formal Aspects of Computing},
  volume    = {24},
  number    = {4-6},
  year      = {2012},
  publisher = {Springer}
  }
  

• Dijkstra, Floyd and Warshall meet Kleene
  with Bernhard Möller
  Formal Aspects of Computing , vol. 24 , no. 4-6 , pp. 459-476 — Springer
  Details BibTeX DOI PDF ©

  @article{hoefner2012_fac,
  author    = {H{\"o}fner, Peter and
  M{\"o}ller, Bernhard},
  title     = {{{Dijkstra}, {Floyd} and {Warshall} meet {Kleene}}},
  journal   = {Formal Aspects of Computing},
  volume    = {24},
  number    = {4--6},
  pages     = {459--476},
  year      = {2012},
  publisher = {Springer},
  doi       = {10.1007/s00165-012-0245-4},
  }
  

• Morgan: a suitable case for treatment (Preface)
  with Rob van Glabbeek, Ian J. Hayes
  Formal Aspects of Computing , vol. 24 , no. 4-6 , pp. 417-422 — Springer
  Details BibTeX DOI PDF ©

  @article{hoefner2012_facs,
  author = {H{\"o}fner, Peter and van Glabbeek, Rob and Hayes, Ian J.},
  title     = {{Morgan: a suitable case for treatment (Preface)}},
  journal = {Formal Aspects of Computing},
  number = {4-6},
  volume = {24},
  pages = {417-422},
  year = {2012},
  publisher = {Springer},
  doi = {10.1007/s00165-012-0257-0}
  }
  

2011

• Fixing Zeno Gaps
  with Bernhard Möller
  Theoretical Computer Science , vol. 412 , no. 28 , pp. 3303-3322 — Elsevier
  Details BibTeX DOI PDF ©

  @article{hoefner2011_tcs,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Fixing Zeno Gaps}},
  journal = {Theoretical Computer Science},
  number = {28},
  volume = {412},
  pages = {3303-3322},
  year = {2011},
  publisher = {Elsevier},
  doi = {10.1016/j.tcs.2011.03.018}
  }
  

• An Algebra of Product Families
  with Ridha Khedri, Bernhard Möller
  Software & Systems Modeling , vol. 10 , no. 2 , pp. 161-182 — Springer
  Details BibTeX DOI PDF ©

  @article{hoefner2011_sosym,
  author = {H{\"o}fner, Peter and Khedri, Ridha and M{\"o}ller, Bernhard},
  title     = {{An Algebra of Product Families}},
  journal = {Software & Systems Modeling},
  number = {2},
  volume = {10},
  pages = {161-182},
  year = {2011},
  doi = {10.1007/s10270-009-0127-2}
  }
  

• Algebraic Separation Logic
  with Han Hing Dang, Bernhard Möller
  Journal of Logic and Algebraic Programming , vol. 80 , no. 6 , pp. 221-247 — Elsevier
  Details BibTeX DOI PDF ©

  @article{dang2011,
  author    = {Han Hing Dang and
  Peter H{\"o}fner and
  Bernhard M{\"o}ller},
  title     = {{Algebraic Separation Logic}},
  year      = {2011},
  journal   = {Journal of Logic and Algebraic Programming},
  volume    = {80},
  number    = {6},
  publisher = {Elsevier},
  pages     = {221--247},
  doi       = {10.1016/j.jlap.2011.04.003},
  }
  

• Supplementing Product Families with Behaviour
  with Ridha Khedri, Bernhard Möller
  International Journal of Software and Informatics , vol. 5 , no. 1-2 , pp. 245-266 — Institute of Software, Chinese Academy of Sciences
  Details BibTeX Link PDF ©

  @article{hoefner2011_ijsi,
  author = {H{\"o}fner, Peter and Khedri, Ridha and M{\"o}ller, Bernhard},
  title     = {{Supplementing Product Families with Behaviour}},
  journal = {International Journal of Software and Informatics},
  number = {1-2},
  volume = {5},
  pages = {245-266},
  year = {2011},
  publisher = {Institute of Software, Chinese Academy of Sciences},
  }
  

2010

• Algebraic Notions of Nontermination: Omega and Divergence in Idempotent Semirings
  with Georg Struth
  Journal of Logic and Algebraic Programming , vol. 79 , no. 8 , pp. 794-811 — Springer
  Details BibTeX DOI PDF ©

  @article{hoefner2010-1,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{Algebraic Notions of Nontermination: Omega and Divergence in Idempotent Semirings}},
  journal = {Journal of Logic and Algebraic Programming},
  number = {8},
  volume = {79},
  pages = {794-811},
  year = {2010},
  publisher = {Springer},
  doi = {10.1016/j.jlap.2010.07.016}
  }
  

2009

• Automated Verification of Refinement Laws
  with Georg Struth, Geoff Sutcliffe
  Annals of Mathematics and Artificial Intelligence , vol. 55 , no. 1-2 , pp. 35-62 — Springer
  Details BibTeX DOI PDF ©

  @article{hoefner2009_amai,
  author = {H{\"o}fner, Peter and Struth, Georg and Sutcliffe, Geoff},
  title     = {{Automated Verification of Refinement Laws}},
  journal = {Annals of Mathematics and Artificial Intelligence},
  number = {1-2},
  volume = {55},
  pages = {35-62},
  year = {2009},
  publisher = {Springer},
  doi = {10.1007/s10472-009-9151-8}
  }
  

• An Algebra of Hybrid Systems
  with Bernhard Möller
  Journal of Logic and Algebraic Programming , vol. 78 , no. 2 , pp. 74-97 — Springer
  Details BibTeX DOI PDF ©

  @article{hoefner2009-1,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{An Algebra of Hybrid Systems}},
  journal = {Journal of Logic and Algebraic Programming},
  number = {2},
  volume = {78},
  pages = {74-97},
  year = {2009},
  publisher = {Springer},
  doi = {10.1016/j.jlap.2008.08.005}
  }
  

2008

• Algebraic Neighbourhood Logic
  with Bernhard Möller
  Journal of Logic and Algebraic Programming , vol. 76 , no. 1 , pp. 35-59 — Springer
  Details BibTeX DOI PDF ©

  @article{hoefner2008-3,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Algebraic Neighbourhood Logic}},
  journal = {Journal of Logic and Algebraic Programming},
  number = {1},
  volume = {76},
  pages = {35-59},
  year = {2008},
  publisher = {Springer},
  doi = {10.1016/j.jlap.2007.10.004}
  }
  

• Algebraic Structure of Web Services
  with Florian Lautenbacher
  Electronic Notes in Theoretical Computer Science , vol. 200 , no. 3 , pp. 171-187 — Elsevier
  Details BibTeX DOI PDF ©

  @article{hoefner2008_entcs,
  author = {H{\"o}fner, Peter and Lautenbacher, Florian},
  title     = {{Algebraic Structure of Web Services}},
  journal = {Electronic Notes in Theoretical Computer Science},
  number = {3},
  volume = {200},
  pages = {171-187},
  year = {2008},
  publisher = {Elsevier},
  doi = {10.1016/j.entcs.2008.04.099}
  }
  

• Can Refinement be Automated?
  with Georg Struth
  Electronic Notes in Theoretical Computer Science , vol. 201 , pp. 197-222 — Elsevier
  Details BibTeX DOI PDF ©

  @article{hoefner2008-2,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{Can Refinement be Automated?}},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {201},
  pages = {197-222},
  year = {2008},
  publisher = {Elsevier},
  doi = {10.1016/j.entcs.2008.02.021}
  }
  

2007

• Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic
  Electronic Notes in Theoretical Computer Science , vol. 191 , pp. 49-72 — Elsevier
  Details BibTeX DOI PDF ©

  @article{hoefner2007-1,
  author = {H{\"o}fner, Peter},
  title     = {{Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic}},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {191},
  pages = {49-72},
  year = {2007},
  publisher = {Elsevier},
  doi = {10.1016/j.entcs.2006.09.040}
  }
  

Conference Papers

2025

• Rely-Guarantee Verification of Queue Locks with Proof Support in Isabelle/HOL
  with Robert J. Colvin, Scott Heiner, Roger C. Su
  — Springer (Lecture Notes in Computer Science) [in press]
  Details BibTeX Link PDF ©

  @inproceedings{hoefner2025_vstte,
  author = {Colvin, Robert J. and Heiner, Scott and H{\"o}fner, Peter and  Su, Roger C.},
  title     = {{Rely-Guarantee Verification of Queue Locks with Proof Support in Isabelle/HOL}},
  booktitle = {Verified Software: Theories, Tools, and Experiments (VSTTE 2025)},
  editor = {Pit-Claudel, Cl{\'e}ment and Kosaian, Katherine},
  series = {Lecture Notes in Computer Science},
  year = {2025},
  publisher = {Springer},
  note = {(in press)}
  }
  

2023

• A Lean-Congruence Format for EP-Bisimilarity
  with Rob van Glabbeek, Weiyou Wang
  Expressiveness in Concurrency and Structural Operational Semantics (pp. 59-75) — Open Publishing Association (Electronic Proceedings in Theoretical Computer Science 387)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2023_express,
  author    = {van Glabbeek,Rob  and
  H{\"o}fner, Peter and
  Wang, Weiyou},
  title     = {{A Lean-Congruence Format for EP-Bisimilarity}},
  editor ={Mezzina, Claudio Antares and
  Caltais, Georgiana},
  year      = {2023},
  booktitle = {Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2023)},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {387},
  publisher = {Open Publishing Association},
  pages     = {59--75},
  doi       = {10.4204/EPTCS.387.6}
  }
  

2022

• Advanced Models for the OSPF Routing Protocol
  with Courtney Darville, Franc Ivankovic, Adam Pam
  Models for Formal Analysis of Real Systems (pp. 13-26) — Open Publishing Association (Electronic Proceedings in Theoretical Computer Science 355)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2022_mars,
  author    = {Darville, Courtney and
  H{\"o}fner, Peter and
  Ivankovic, Franc and
  Pam, Adam},
  title     = {{Advanced Models for the OSPF Routing Protocol}},
  editor = {Dubslaff, Clemens and Luttik, Bas},
  year      = {2022},
  booktitle = {Models for Formal Analysis of Real Systems},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {355},
  publisher = {Open Publishing Association},
  pages     = {13--26},
  doi       = {10.4204/EPTCS.355.2},
  }
  

2021

• Enabling Preserving Bisimulation Equivalence
  with Rob van Glabbeek, Weiyou Wang
  Concurrency Theory (pp. 33:1-33:20) — Schloss Dagstuhl -- Leibniz-Zentrum für Informatik (Leibniz International Proceedings in Informatics (LIPIcs) 203)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2021_concur,
  author = {van Glabbeek, Rob and H{\"o}fner, Peter and Wang, Weiyou},
  title     = {{Enabling Preserving Bisimulation Equivalence}},
  booktitle = {Concurrency Theory (CONCUR 2021)},
  editor = {Haddad, Serge and Varacca, Daniele},
  series = {LIPIcs},
  volume = {203},
  pages = {33:1-33:20},
  year = {2021},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
  doi = {10.4230/LIPIcs.CONCUR.2021.33}
  }
  

• Effect Algebras, Girard Quantales and Complementation in Separation Logic
  with Callum Bannister, Georg Struth
  — Springer (Lecture Notes in Computer Science 13027)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2021_ramics,
  author = {Bannister, Callum and H{\"o}fner, Peter and Struth, Georg},
  title     = {{Effect Algebras, Girard Quantales and Complementation in Separation Logic}},
  booktitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2021)},
  editor = {Fahrenberg, Uli and Gehrke, Mai and Santocanale, Luigi and Winter, Michael},
  series = {Lecture Notes in Computer Science},
  volume = {13027},
  pages = {37-53},
  year = {2021},
  publisher = {Springer},
  doi = {10.1007/978-3-030-88701-8_3}
  }
  

• Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom
  with Rob van Glabbeek, Ross Horne
  Logic in Computer Science (pp. 1-13) — IEEE
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2021_lics,
  author = {van Glabbeek, Rob and H{\"o}fner, Peter and Horne, Ross},
  title     = {{Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom}},
  booktitle = {Logic in Computer Science (LICS 2021)},
  volume = {0},
  pages = {1-13},
  year = {2021},
  publisher = {IEEE},
  doi = {10.1109/LICS52264.2021.9470531}
  }
  

2020

• Formal Models of the OSPF Routing Protocol
  with Jack Drury, Weiyou Wang
  Models for Formal Analysis of Real Systems (MARS 2020) (pp. 72-120) — Open Publishing Association (Electronic Proceedings in Theoretical Computer Science 316)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2020_mars,
  author    = {Drury, Jack and H{\"o}fner, Peter and Wang, Weiyou},
  title     = {{Formal Models of the {OSPF} Routing Protocol}},
  booktitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
  editor = {Fehnker, Ansgar and Garaval, Hubert},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {316},
  pages     = {72-120},
  year = {2020},
  publisher = {Open Publishing Association},
  doi = {10.4204/EPTCS.316.4}
  }
  

• Formalising the Optimised Link State Routing Protocol
  with Ryan Barry, Rob van Glabbeek
  Models for Formal Analysis of Real Systems (MARS 2020) (pp. 40-71) — Open Publishing Association (Electronic Proceedings in Theoretical Computer Science 316)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2020_mars,
  author = {Barry, Ryan and van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{Formalising the Optimised Link State Routing Protocol}},
  booktitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
  editor = {Fehnker, Ansgar and Garaval, Hubert},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {316},
  pages = {40-71},
  year = {2020},
  publisher = {Open Publishing Association},
  doi = {10.4204/EPTCS.316.3}Adam
  }
  

2019

• A Process Algebra for Link Layer Protocols
  with Rob van Glabbeek, Michael Markl
  Programming Languages and Systems (pp. 668-693) — Springer (Lecture Notes in Computer Science 11423)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2019-3,
  author = {van Glabbeek, Rob and H{\"o}fner, Peter and Markl, Michael},
  title     = {{A Process Algebra for Link Layer Protocols}},
  booktitle = {Programming Languages and Systems (ESOP 2019)},
  editor = {Caires, L.},
  series = {Lecture Notes in Computer Science},
  volume = {11423},
  pages = {668-693},
  year = {2019},
  publisher = {Springer},
  doi = {10.1007/978-3-030-17184-1_24}
  }
  

2018

• Backwards and Forwards with Separation Logic
  with Callum Bannister, Gerwin Klein
  Interactive Theorem Proving (pp. 68-87) — Springer (Lecture Notes in Computer Science 10895)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2018_itp,
  author = {Bannister, Callum and H{\"o}fner, Peter and Klein, Gerwin},
  title     = {{Backwards and Forwards with Separation Logic}},
  booktitle = {Interactive Theorem Proving (ITP 2018)},
  editor = {Avigad, Jeremy and Mahboubi, Aassia},
  series = {Lecture Notes in Computer Science},
  volume = {10895},
  pages = {68-87},
  year = {2018},
  publisher = {Springer},
  doi = {10.1007/978-3-319-94821-8_5}
  }
  

• Analysing AWN-specifications using mCRL2 (extended abstract)
  with Rob van Glabbeek, Djurre van der Wal
  Integrated Formal Methods (iFM 2018) (pp. 398-418) — Springer (Lecture Notes in Computer Science 11023)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2018-3,
  author    = {van Glabbeek, Rob and H{\"o}fner, Peter and van der Wal, Djurre},
  title     = {{Analysing {AWN}-specifications using {mCRL2} (extended abstract)}},
  booktitle = {Integrated Formal Methods (iFM 2018)},
  editor    = {Furia, Carlo A. and Winter, Kirsten},
  series    = {Lecture Notes in Computer Science},
  volume    = {11023},
  pages     = {398-418},
  year      = {2018},
  publisher = {Springer},
  doi       = {10.1007/978-3-319-98938-9_23}
  }
  

• False Failure: Creating Failure Models for Separation Logic
  with Callum Bannister
  Relational and Algebraic Methods in Computer Science (pp. 263-279) — Springer (Lecture Notes in Computer Science 11194)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2018_ramics,
  author = {Bannister, Callum and H{\"o}fner, Peter},
  title     = {{False Failure: Creating Failure Models for Separation Logic}},
  booktitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2018)},
  editor = {Desharnais, Jules and Guttmann, Walter and Joosten, Stef},
  series = {Lecture Notes in Computer Science},
  volume = {11194},
  pages = {263-279},
  year = {2018},
  publisher = {Springer},
  doi = {10.1007/978-3-030-02149-8_16}
  }
  

2017

• Analysing Mutual Exclusion using Process Algebra with Signals
  with Victor Dyseryn, Rob van Glabbeek
  Expressiveness in Concurrency and Structural Operational Semantics (pp. 18-34) — Open Publishing Association (Electronic Proceedings in Theoretical Computer Science 255)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2017_express,
  author    = {Dyseryn, Victor and
  van Glabbeek, Rob and
  H{\"o}fner, Peter},
  title     = {{Analysing Mutual Exclusion using Process Algebra with Signals}},
  year      = {2017},
  booktitle = {Expressiveness in Concurrency and Structural Operational Semantics},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {255},
  publisher = {Open Publishing Association},
  pages     = {18--34},
  doi       = {10.4204/EPTCS.255.2},
  }
  

• Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack
  with Rob van Glabbeek
  Models for Formal Analysis of Real Systems (MARS 2017) (pp. 14-52) — Open Publishing Association (Electronic Proceedings in Theoretical Computer Science 244)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2017_mars,
  author    = {van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{Split, Send, Reassemble: A Formal Specification of a {CAN} Bus Protocol Stack}},
  booktitle = {Models for Formal Analysis of Real Systems (MARS 2017)},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {244},
  pages     = {14-52},
  year      = {2017},
  publisher = {Open Publishing Association},
  doi       = {10.4204/EPTCS.244.2}
  }
  

2016

• A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract)
  with Emile Bres, Rob van Glabbeek
  Programming Languages and Systems (pp. 95-122) — Springer (Lecture Notes in Computer Science 9632)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2016_esop,
  author = {Bres, Emile and van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract)}},
  booktitle = {Programming Languages and Systems (ESOP 2016)},
  editor = {Thiemann, Peter},
  series = {Lecture Notes in Computer Science},
  volume = {9632},
  pages = {95-122},
  year = {2016},
  publisher = {Springer},
  doi = {10.1007/978-3-662-49498-1_5}
  }
  

2015

• Using Process Algebra to Design Better Protocol (extended abstract); invited
  Forum "Math-for-Industry" 2015 - The Role and Importance of Mathematics in Innovation — Kyushu University (MI Lecture Notes 65)
  Details BibTeX Link PDF ©

  @inproceedings{hoefner2015_fmi,
  author = {H{\"o}fner, P.},
  title     = {{Using Process Algebra to Design Better Protocol (extended abstract); invited}},
  booktitle = {Forum "Math-for-Industry" 2015 - The Role and Importance of Mathematics in Innovation (FMI 2015)},
  series = {MI Lecture Notes},
  volume = {65},
  year = {2015},
  publisher = {Kyushu University},
  doi = {}
  }
  

• Formal Analysis of Proactive, Distributed Routing
  with Mojgan Kamali, Maryam Kamali, Luigia Petre
  Software Engineering and Formal Methods (pp. 175-189) — Springer (Lecture Notes in Computer Science 9276)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2015_sefm,
  author = {Kamali, Mojgan and H{\"o}fner, Peter and Kamali, Maryam and Petre, Luigia},
  title     = {{Formal Analysis of Proactive, Distributed Routing}},
  booktitle = {Software Engineering and Formal Methods (SEFM 2015)},
  editor = {Calinescu, Radu and Rumpe, Bernhard},
  series = {Lecture Notes in Computer Science},
  volume = {9276},
  pages = {175-189},
  year = {2015},
  publisher = {Springer},
  doi = {10.1007/978-3-319-22969-0_13}
  }
  

• Tool-Based Verification of a Relational Vertex Coloring Program
  with Rudolf Berghammer, Insa Stucke
  Relational and Algebraic Methods in Computer Science (pp. 275-292) — Springer (Lecture Notes in Computer Science 9348)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2015_ramics,
  author = {Berghammer, Rudolf and H{\"o}fner, Peter and Stucke, Insa},
  title     = {{Tool-Based Verification of a Relational Vertex Coloring Program}},
  booktitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2015)},
  editor = {Kahl, Wolfram and Oliveira, Jos{\'e} N. and Winter, Michael},
  series = {Lecture Notes in Computer Science},
  volume = {9348},
  pages = {275-292},
  year = {2015},
  publisher = {Springer},
  doi = {10.1007/978-3-319-24704-5_17}
  }
  

2014

• Automated Verification of Relational While-Programs
  with Rudolf Berghammer, Insa Stucke
  Relational and Algebraic Methods in Computer Science (pp. 173-190) — Springer (Lecture Notes in Computer Science 8428)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2014_ramics,
  author = {Berghammer, Rudolf and H{\"o}fner, Peter and Stucke, Insa},
  title     = {{Automated Verification of Relational While-Programs}},
  booktitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2014)},
  editor = {H{\"o}fner, Peter and Jipsen, Peter and Kahl, Wolfram and M{\"u}ller, Martin E.},
  series = {Lecture Notes in Computer Science},
  volume = {8428},
  pages = {173-190},
  year = {2014},
  publisher = {Springer},
  doi = {10.1007/978-3-319-06251-8_11}
  }
  

• Showing Invariance Compositionally for a Process Algebra of Network Protocols
  with Timothy Bourke, Rob van Glabbeek
  Interactive Theorem Proving (pp. 144-159) — Springer (Lecture Notes in Computer Science 8558)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2014_itp,
  author = {Bourke, Tim and van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{Showing Invariance Compositionally for a Process Algebra of Network Protocols}},
  booktitle = {Interactive Theorem Proving (ITP 2014)},
  editor = {Klein, Gerwin and Gamboa, Ruben},
  series = {Lecture Notes in Computer Science},
  volume = {8558},
  pages = {144-159},
  year = {2014},
  publisher = {Springer},
  doi = {10.1007/978-3-319-08970-6_10}
  }
  

• A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol
  with Timothy Bourke, Rob van Glabbeek
  Automated Technology for Verification and Analysis (ATVA 2014) (pp. 47-63) — Springer (Lecture Notes in Computer Science 8837)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2014_atva,
  author    = {Bourke, Timothy and van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{A Mechanized Proof of Loop Freedom of the (Untimed) {AODV} Routing Protocol}},
  booktitle = {Automated Technology for Verification and Analysis (ATVA 2014)},
  editor    = {Cassez, Franck and Raskin, Jean-Francois},
  series    = {Lecture Notes in Computer Science},
  volume    = {8837},
  pages     = {47-63},
  year      = {2014},
  publisher = {Springer},
  doi       = {10.1007/978-3-319-11936-6_5}
  }
  

2013

• Topology-based Mobility Models for Wireless Networks
  with Ansgar Fehnker, Maryam Kamali, Vinay Mehta
  Quantitative Evaluation of Systems (pp. 368-383) — Springer (Lecture Notes in Computer Science 8054)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2013_qest,
  author = {Fehnker, Aansgar and H{\"o}fner, Peter and Kamali, Maryam and Mehta, Vinay},
  title     = {{Topology-based Mobility Models for Wireless Networks}},
  booktitle = {Quantitative Evaluation of Systems (QEST 2013)},
  editor = {Kaustubh, Joshi and Siegle, Markius and Stoelinga, Mari{\"e}lle and D’Argenio, Pedro R.},
  series = {Lecture Notes in Computer Science},
  volume = {8054},
  pages = {368-383},
  year = {2013},
  publisher = {Springer},
  doi = {10.1007/978-3-642-40196-1_32}
  }
  

• Statistical Model Checking of Wireless Mesh Routing Protocols
  with Annabelle McIver
  NASA Formal Methods Symposium (pp. 322-336) — Springer (Lecture Notes in Computer Science 7871)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2013_nfm,
  author = {H{\"o}fner, Peter and McIver, Annabelle},
  title     = {{Statistical Model Checking of Wireless Mesh Routing Protocols}},
  booktitle = {NASA Formal Methods Symposium (NFM 2013)},
  editor = {Brat, Guillaume and Rungta, Neha and Venet, Arnaud},
  series = {Lecture Notes in Computer Science},
  volume = {7871},
  pages = {322-336},
  year = {2013},
  publisher = {Springer},
  doi = {10.1007/978-3-642-38088-4_22}
  }
  

• Sequence Numbers Do Not Guarantee Loop Freedom —AODV Can Yield Routing Loops—
  with Rob van Glabbeek, Marius Portmann, Wee Lum Tan
  Modeling, Analysis and Simulation of Wireless and Mobile Systems (pp. 91-100) — ACM
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2013_mswim,
  author = {van Glabbeek, Rob and H{\"o}fner, Peter and Portmann, Marius and Tan, Wee Lum},
  title     = {{Sequence Numbers Do Not Guarantee Loop Freedom 

• Quantitative Analysis of AODV and its Variants on Dynamic Topologies using Statistical Model Checking
  with Maryam Kamali
  Formal Modelling and Analysis of Timed Systems (FORMATS 2013) (pp. 121-136) — Springer (Lecture Notes in Computer Science 8053)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2013_formats,
  author = {H{\"o}fner, Peter and Kamali, Maryam},
  title     = {{Quantitative Analysis of {AODV} and its Variants on Dynamic Topologies using Statistical Model Checking}},
  booktitle = {Formal Modelling and Analysis of Timed Systems (FORMATS 2013)},
  editor = {Braberman, V{\'i}tor and Fribourg, Laurent},
  series = {Lecture Notes in Computer Science},
  volume = {8053},
  pages = {121-136},
  year = {2013},
  publisher = {Springer},
  doi = {10.1007/978-3-642-40229-6_9}
  }
  

• Features, Modularity, and Variation Points
  with Don Batory, Bernhard Möller, Andreas Zelend
  Workshop on Feature-Oriented Software Development (pp. 9-16) — ACM
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2013-6,
  author = {Batory, Don and H{\"o}fner, Peter and M{\"o}ller, Bernhard and Zelend, Andreas},
  title     = {{Features, Modularity, and Variation Points}},
  booktitle = {Workshop on Feature-Oriented Software Development (FOSD 2013)},
  editor = {},
  series = {},
  volume = {0},
  pages = {9-16},
  year = {2013},
  publisher = {ACM},
  doi = {10.1145/2528265.2528269}
  }
  

2012

• Foundations of Coloring Algebra with Consequences for Feature-oriented Programming
  with Bernhard Möller, Andreas Zelend
  Relational and Algebraic Methods in Computer Science (pp. 33-49) — Springer (Lecture Notes in Computer Science 7560)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2012-6,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard and Zelend, Andreas},
  title     = {{Foundations of Coloring Algebra with Consequences for Feature-oriented Programming}},
  booktitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2012)},
  editor = {Kahl, Wolfram and Griffin, Timothy G.},
  series = {Lecture Notes in Computer Science},
  volume = {7560},
  pages = {33-49},
  year = {2012},
  publisher = {Springer},
  doi = {10.1007/978-3-642-33314-9_3}
  }
  

• A Rigorous Analysis of AODV and its Variants
  with Rob van Glabbeek, Wee Lum Tan, Marius Portmann, Annabelle McIver, Ansgar Fehnker
  Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2012) (pp. 203-212) — ACM [Nominated for best paper award]
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2012-7,
  author    = {H{\"o}fner, Peter and van Glabbeek, Rob and Tan, Wee Lum and Portmann, Marius and McIver, Annabelle and Fehnker, Ansgar},
  title     = {{A Rigorous Analysis of {AODV} and its Variants}},
  booktitle = {Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2012)},
  pages     = {203-212},
  year      = {2012},
  publisher = {ACM},
  doi       = {10.1145/2387238.2387274}
  }
  

• A Process Algebra for Wireless Mesh Networks
  with Ansgar Fehnker, Rob van Glabbeek, Annabelle McIver, Marius Portmann, Wee Lum Tan
  Programming Languages and Systems (ESOP'12) (pp. 295-315) — Springer (Lecture Notes in Computer Science 7211)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2012_esop,
  author = {Fehnker, Aansgar and van Glabbeek, Rob and H{\"o}fner, Peter and McIver, Annabelle and Portmann, Marius and Tan, Wee Lum},
  title     = {{A Process Algebra for Wireless Mesh Networks}},
  booktitle = {Programming Languages and Systems (ESOP'12) (ESOP 2012)},
  editor = {Seidl, Helmut},
  series = {Lecture Notes in Computer Science},
  volume = {7211},
  pages = {295-315},
  year = {2012},
  publisher = {Springer},
  doi = {10.1007/978-3-642-28869-2_15}
  }
  

• Towards a Representation Theorem for Coloring Algebra
  Workshop on Lattices and Relations (L&R 2012) [Abstract]
  Details BibTeX Link PDF ©

  @misc{hoefner2012_lr,
  author = {H{\"o}fner, Peter},
  howpublished = {Workshop on Lattices and Relations (L\&R 2012)},
  note = {(Abstract)},
  title     = {{Towards a Representation Theorem for Coloring Algebra}},
  year = {2012}
  }
  

• Kleene Modules for Routing Procedures
  Workshop on Lattices and Relations (L&R 2012) [Abstract]
  Details BibTeX Link PDF ©

  @misc{hoefner2012_lr2,
  author = {H{\"o}fner, Peter},
  howpublished = {Workshop on Lattices and Relations (L\&R 2012)},
  note = {(Abstract)},
  title     = {{Kleene Modules for Routing Procedures}},
  year = {2012}
  }
  

• Towards a Rigorous Analysis of AODVv2 (DYMO)
  with Sarah Edenhofer
  Rigorous Protocol Engineering (WRiPE 2012) — IEEE
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2012_wripe,
  author    = {Edenhofer, Sarah and
  H{\"o}fner, Peter},
  title     = {{Towards a Rigorous Analysis of {AODVv2} ({DYMO})}},
  booktitle = {Rigorous Protocol Engineering (WRiPE 2012)},
  editor    = {Foster, Nate and Gurney, Alexander},
  year      = {2012},
  publisher = {IEEE},
  doi       = {10.1109/ICNP.2012.6459942},
  }
  

• Automated Analysis of AODV using UPPAAL
  with Ansgar Fehnker, Rob van Glabbeek, Annabelle McIver, Marius Portmann, Wee Lum Tan
  Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012) (pp. 173-187) — Springer (Lecture Notes in Computer Science 7214)
  Details BibTeX DOI arXiv PDF ©

  @inproceedings{hoefner2012-1,
  author = {Fehnker, Ansgar and van Glabbeek, Rob and H{\"o}fner, Peter and McIver, Annabelle and Portmann, Marius and Tan, Wee Lum},
  title     = {{Automated Analysis of AODV using UPPAAL}},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)},
  editor = {Flanagan, Cormac and K{\"o}nig, Barbara},
  series = {Lecture Notes in Computer Science},
  volume = {7214},
  pages = {173-187},
  year = {2012},
  publisher = {Springer},
  doi = {10.1007/978-3-642-28756-5_13}
  }
  

2011

• Feature Interactions, Products, and Composition
  with Don Batory, Jongwook Kim
  Generative Programming and Component Engineering (pp. 13-22) — ACM
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2011-8,
  author = {Batory, Don and H{\"o}fner, Peter and Kim, Jongwook},
  title     = {{Feature Interactions, Products, and Composition}},
  booktitle = {Generative Programming and Component Engineering (GPCE 2011)},
  editor = {},
  series = {},
  volume = {0},
  pages = {13-22},
  year = {2011},
  publisher = {ACM},
  doi = {10.1145/2047862.2047867}
  }
  

• Modelling and Analysis of AODV in UPPAAL
  with Ansgar Fehnker, Rob van Glabbeek, Annabelle McIver, Marius Portmann, Wee Lum Tan
  Rigorous Protocol Engineering (WRiPE'11) — IEEE
  Details BibTeX Link arXiv PDF ©

  @inproceedings{hoefner2011-7,
  author = {Fehnker, Ansgar and van Glabbeek, Rob and H{\"o}fner, Peter and McIver, Annabelle and Portmann, Marius and Tan, Wee Lum},
  title     = {{Modelling and Analysis of {AODV} in {UPPAAL}}},
  booktitle = {Rigorous Protocol Engineering (WRiPE'11) (WRiPE 2011)},
  year = {2011},
  publisher = {IEEE}
  }
  

• Towards an Algebra of Routing Tables
  with Annabelle McIver
  Relational and Algebraic Methods in Computer Science (pp. 212-229) — Springer (Lecture Notes in Computer Science 6663)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2011-5,
  author = {H{\"o}fner, Peter and McIver, Annabelle},
  title     = {{Towards an Algebra of Routing Tables}},
  booktitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2011)},
  editor = {de Swart, Harrie},
  series = {Lecture Notes in Computer Science},
  volume = {6663},
  pages = {212-229},
  year = {2011},
  publisher = {Springer},
  doi = {10.1007/978-3-642-21070-9_17}
  }
  

• Variable Side Conditions and Greatest Relations in Algebraic Separation Logic
  with Han Hing Dang
  Relational and Algebraic Methods in Computer Science (pp. 125-140) — Springer (Lecture Notes in Computer Science 6663)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2011_ramics,
  author = {Dang, Han Hinf and H{\"o}fner, Peter},
  title     = {{Variable Side Conditions and Greatest Relations in Algebraic Separation Logic}},
  booktitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2011)},
  editor = {de Swart, H.},
  series = {Lecture Notes in Computer Science},
  volume = {6663},
  pages = {125-140},
  year = {2011},
  publisher = {Springer},
  doi = {10.1007/978-3-642-21070-9_11}
  }
  

2010

• Automated Higher-order Reasoning about Quantales
  with Han Hing Dang
  Workshop on Practical Aspects of Automated Reasoning (PAAR'10) (pp. 40-51) — EasyChair (EasyChair Proceedings in Computing 9)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2010paar,
  author    = {Dang, Han Hing and H{\"o}fner, Peter},
  title     = {{Automated Higher-order Reasoning about Quantales}},
  booktitle = {{Workshop on Practical Aspects of Automated Reasoning (PAAR 2010)}},
  editor    = {Konev, Boris and Schmidt, Renate A. and Schulz, Stephan},
  series    = {EasyChair Proceedings in Computing},
  volume    = {9},
  pages    = {40-51},
  year    = {2010},
  publisher    = {EasyChair},
  doi    = {doi.org/10.29007/l2sz}
  }
  

2009

• Towards Algebraic Separation Logic
  with Han Hing Dang, Bernhard Möller
  Relations and Kleene Algebra in Computer Science (RelmiCS/AKA'09) (pp. 59-72) — Springer (Lecture Notes in Computer Science 5827)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2009-3,
  author = {Dang, Han Hing and H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Towards Algebraic Separation Logic}},
  booktitle = {Relations and Kleene Algebra in Computer Science (RelmiCS/AKA'09)},
  editor = {Berghammer, Rudolf and Jaoua, Ali M. and M{\"o}ller, Bernhard},
  series = {Lecture Notes in Computer Science},
  volume = {5827},
  pages = {59-72},
  year = {2009},
  publisher = {Springer},
  doi = {10.1007/978-3-642-04639-1_5}
  }
  

• An Extension of Feature Algebra [Extended Abstract]
  with Bernhard Möller
  Workshop on Feature-Oriented Software Development (FOSD'09) (pp. 75-80) — ACM
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2009-4,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{An Extension of Feature Algebra [Extended Abstract]}},
  booktitle = {Workshop on Feature-Oriented Software Development (FOSD'09)},
  editor = {Apel, Sven and Cook, William R. and Czarnecki, Krzysztof and K{\"a}stner, Christian and Loughran, Neil and Nierstrasz, Oscar},
  series = {},
  volume = {0},
  pages = {75-80},
  year = {2009},
  publisher = {ACM},
  doi = {10.1145/1629716.1629731}
  }
  

2008

• Algebraic View Reconciliation
  with Ridha Khedri, Bernhard Möller
  Software Engineering and Formal Methods (SEFM'08) (pp. 85-94) — IEEE
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2008_sefm,
  author = {H{\"o}fner, Peter and Khedri, Ridha and M{\"o}ller, Bernhard},
  title     = {{Algebraic View Reconciliation}},
  booktitle = {Software Engineering and Formal Methods (SEFM'08)},
  editor = {Cerone, Antonio and Gruner, Stefan},
  series = {},
  volume = {0},
  pages = {85-94},
  year = {2008},
  publisher = {IEEE},
  doi = {10.1109/SEFM.2008.36}
  }
  

• Automated Reasoning for Hybrid Systems — Two Case Studies —
  Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08) (pp. 191-205) — Springer (Lecture Notes in Computer Science 4988)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2008_relmics2,
  author = {H{\"o}fner, Peter},
  title     = {{Automated Reasoning for Hybrid Systems 

• Non-termination in Idempotent Semirings
  with Georg Struth
  Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08) (pp. 206-220) — Springer (Lecture Notes in Computer Science 4988)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2008_relmics,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{Non-termination in Idempotent Semirings}},
  booktitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08)},
  editor = {Berghammer, Rudolf and M{\"o}ller, Bernhard and Struth, Georg},
  series = {Lecture Notes in Computer Science},
  volume = {4988},
  pages = {206-220},
  year = {2008},
  publisher = {Springer},
  doi = {10.1007/978-3-540-78913-0_16}
  }
  

• On Automating the Calculus of Relations
  with Georg Struth
  Automated Reasoning (pp. 50-66) — Springer (Lecture Notes in Artificial Intelligence 5195)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2008_ijcar,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{On Automating the Calculus of Relations}},
  booktitle = {Automated Reasoning},
  editor = {Armando, Alessandro and Baumgartner, Peter and Dowek, Gilles},
  series = {Lecture Notes in Artificial Intelligence},
  volume = {5195},
  pages = {50-66},
  year = {2008},
  publisher = {Springer},
  doi = {10.1007/978-3-540-71070-7_5}
  }
  

2007

• Automated Reasoning in Kleene Algebra
  with Georg Struth
  Automated Deduction (CADE21) (pp. 279-294) — Springer (Lecture Notes in Artificial Intelligence 4603)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2007_cade,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{Automated Reasoning in Kleene Algebra}},
  booktitle = {Automated Deduction (CADE21)},
  editor = {Pfenning, Frank},
  series = {Lecture Notes in Artificial Intelligence},
  volume = {4603},
  pages = {279-294},
  year = {2007},
  publisher = {Springer},
  doi = {10.1007/978-3-540-73595-3_19}
  }
  

2006

• Lazy Semiring Neighbours and Some Applications
  with Bernhard Möller
  Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06) (pp. 207-221) — Springer (Lecture Notes in Computer Science 4136)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2006-9,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Lazy Semiring Neighbours and Some Applications}},
  booktitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06)},
  editor = {Schmidt, Renate A.},
  series = {Lecture Notes in Computer Science},
  volume = {4136},
  pages = {207-221},
  year = {2006},
  publisher = {Springer},
  doi = {10.1007/11828563_14}
  }
  

• Omega Algebra, Demonic Refinement Algebra and Commands
  with Bernhard Möller, Kim Solin
  Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06) (pp. 222-234) — Springer (Lecture Notes in Computer Science 4136)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2006_relmics2,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard and Solin, Kim},
  title     = {{Omega Algebra, Demonic Refinement Algebra and Commands}},
  booktitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06)},
  editor = {Schmidt, Renate A.},
  series = {Lecture Notes in Computer Science},
  volume = {4136},
  pages = {222-234},
  year = {2006},
  publisher = {Springer},
  doi = {10.1007/11828563_15}
  }
  

• Towards an Algebra of Hybrid Systems
  with Bernhard Möller
  Relational Methods in Computer Science (RelMiCS8/AKA3) (pp. 121-133) — Springer (Lecture Notes in Computer Science 3929)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2006_relmics,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Towards an Algebra of Hybrid Systems}},
  booktitle = {Relational Methods in Computer Science (RelMiCS8/AKA3)},
  editor = {MacCaull, Wendy and Winter, Michael and D{\"u}ntsch, Ivo},
  series = {Lecture Notes in Computer Science},
  volume = {3929},
  pages = {121-133},
  year = {2006},
  publisher = {Springer},
  doi = {10.1007/11734673_10}
  }
  

• Feature Algebra
  with Ridha Khedri, Bernhard Möller
  Formal Methods (FM'06) (pp. 300-315) — Springer (Lecture Notes in Computer Science 4085)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2006-5,
  author = {H{\"o}fner, Peter and Khedri, Ridha and M{\"o}ller, Bernhard},
  title     = {{Feature Algebra}},
  booktitle = {Formal Methods (FM'06)},
  editor = {Misra, Jayadev and Nipkow, Tobias and Sekerinski, Emil},
  series = {Lecture Notes in Computer Science},
  volume = {4085},
  pages = {300-315},
  year = {2006},
  publisher = {Springer},
  doi = {10.1007/11813040_21}
  }
  

• Quantales and Temporal Logics
  with Bernhard Möller, Georg Struth
  Algebraic Methodology and Software Technology (AMAST'06) (pp. 263-277) — Springer (Lecture Notes in Computer Science 4019)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2006_amast,
  author = {M{\"o}ller, Bernhard and H{\"o}fner, Peter and Struth, Georg},
  title     = {{Quantales and Temporal Logics}},
  booktitle = {Algebraic Methodology and Software Technology (AMAST'06)},
  editor = {Johnson, Michael and Vene, Varno},
  series = {Lecture Notes in Computer Science},
  volume = {4019},
  pages = {263-277},
  year = {2006},
  publisher = {Springer},
  doi = {10.1007/11784180_21}
  }
  

2005

• Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System
  with Alfons Huhn, Werner Kießling
  Research and Advanced Technology for Digital Libraries (ECDL'05) (pp. 498-499) — Springer (Lecture Notes in Computer Science 3652)
  Details BibTeX DOI PDF ©

  @inproceedings{hoefner2005_ecdl,
  author = {Huhn, Alfons and H{\"o}fner, Peter and Kie{\ss}ling, Werner},
  title     = {{Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System}},
  booktitle = {Research and Advanced Technology for Digital Libraries (ECDL'05)},
  editor = {Rauber, Andreas and Christodoulakis, Stavros and Tjoa, A Min},
  series = {Lecture Notes in Computer Science},
  volume = {3652},
  pages = {498-499},
  year = {2005},
  publisher = {Springer},
  doi = {10.1007/11551362_53}
  }
  

• An Algebraic Semantics for Duration Calculus
  Proceedings of the 10th ESSLLI Student Session (pp. 99-111) (European Summer School in Logic, Language and Information (ESSLLI))
  Details BibTeX Link PDF ©

  @inproceedings{hoefner2005_essli,
  author    = {Peter H{\"o}fner},
  title     = {{An Algebraic Semantics for Duration Calculus}},
  booktitle = {Proceedings of the 10th ESSLLI Student Session},
  series    = {European Summer School in Logic, Language and Information},
  volume    = {17},
  pages     = {99--111},
  year      = {2005},
  address   = {Heriot-Watt University Edinburgh, Scotland},
  note      = {8--19 August 2005},
  }
  

• Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic
  IFM2005—Doctoral Symposium on Integrated Formal Methods (pp. 6-13) — TU/e technische universiteit eindhoven (Computer Science Reports 05-29)
  Details BibTeX Link PDF ©

  @misc{hoefner2005_ifm,
  author = {H{\"o}fner, Peter},
  title     = {{Semiring Neighbours: An Algebraic Embedding and Extension of {Neighbourhood Logic}}},
  editor = {Romijn, Judi and Smith, Graeme and van~de~Pol, Jaco},
  booktitle = {IFM2005—Doctoral Symposium on Integrated Formal Methods},
  series = {Computer Science Reports 05-29, TU/e technische universiteit eindhoven},
  pages = {6-13},
  year = {2005}
  }
  

Archive of Formal Proofs

2025

• Rely-Guarantee Extensions and Locks
  with Robert J. Colvin, Scott Heiner, Roger C. Su
  Archive of Formal Proofs
  Details BibTeX Link PDF ©

  @article{hoefner2025_afp_locks,
  author  = {Colvin, Robert J. and Heiner, Scott and H{\"o}fner, Peter and Su, Roger C.},
  title     = {{Rely-Guarantee Extensions and Locks}},
  journal = {Archive of Formal Proofs},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/RG_Locks.html},
  Formal proof development},
  ISSN    = {2150-914x},
  }
  

2020

• Relational Characterisations of Paths
  with Walter Guttmann
  Archive of Formal Proofs
  Details BibTeX Link PDF ©

  @misc{guttmann2020,
  author    = {Guttmann, Walter and
  H{\"o}fner, Peter},
  title     = {{Relational Characterisations of Paths}},
  journal = {Archive of Formal Proofs},
  year      = {2020},
  note    = {\url{https://isa-afp.org/entries/Relational_Paths.html},
  Formal proof development},
  }
  

2016

• Kleene Algebras with Domain
  with Victor B. F. Gomes, Walter Guttmann, Georg Struth, Tjark Weber
  Archive of Formal Proofs
  Details BibTeX Link PDF ©

  @misc{hoefner2016_afp_kad,
  author    = {Gomes, Victor B. F. and
  Guttmann, Walter and
  H{\"o}fner, Peter and
  Struth, Georg and
  Weber, Tjark},
  title     = {{Kleene Algebras with Domain}},
  journal = {Archive of Formal Proofs},
  year      = {2016},
  note    = {\url{https://isa-afp.org/entries/KAD.html},
  Formal proof development}
  }
  

2014

• Loop Freedom of the (Untimed) AODV Routing Protocol
  with Timothy Bourke
  Archive of Formal Proofs
  Details BibTeX Link

  @article{hoefner2014_afp_atva,
  author  = {Bourke, Timothy and H{\"o}fner, Peter},
  title     = {{Loop Freedom of the (Untimed) {AODV} Routing Protocol}},
  journal = {Archive of Formal Proofs},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/AODV.html},
  Formal proof development},
  }
  

Miscellaneous

2020

• Festschrift for Rob van Glabbeek
  ed. Peter Höfner, Carroll Morgan, Vaughan Pratt
  — Springer [Special issue / Festschrift]
  Details BibTeX Link PDF ©

  @book{hoefner2020_acta2,
  editor    = {H{\"o}fner, Peter and Morgan, Carroll and Pratt, Vaughan},
  title     = {{Festschrift for Rob van Glabbeek}},
  journal   = {Acta Informatica},
  volume    = {57},
  number    = {3-5},
  year      = {2020},
  publisher = {Springer}
  }
  

2019

• Special Issue on Relational and Algebraic Methods in Computer Science
  ed. Peter Höfner, Damien Pous, Georg Struth
  — Elsevier
  Details BibTeX Link PDF ©

  @book{hoefner2019_jlamp,
  editor = {H{\"o}fner, Peter and Pous, Damien and Struth, Georg}
  title     = {{Special Issue on Relational and Algebraic Methods in Computer Science}},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  volume = {106},
  number = {2},
  year      = {2019},
  publisher = {Elsevier}
  }
  

2017

• Relational and Algebraic Methods in Computer Science
  ed. Peter Höfner, Damien Pous, Georg Struth
  — Springer (Lecture Notes in Computer Science 10226)
  Details BibTeX DOI PDF ©

  @book{hoefner2017_ramics,
  author    = {H{\"o}fner, Peter and Pous, Damien and Struth, Georg},
  title     = {{Relational and Algebraic Methods in Computer Science}},
  year      = {2017},
  series ={Lecture Notes in Computer Science},
  volume    = {10226},
  publisher = {Springer},
  doi       = {10.1007/978-3-319-57418-9}
  }
  

• 2nd Workshop on Models for Formal Analysis of Real Systems
  ed. Holger Hermanns, Peter Höfner
  — Open Publishing Association (Electronic Proceedings in Theoretical Computer Science 244)
  Details BibTeX DOI arXiv PDF ©

  @book{hoefner2017_mars,
    editor    = {Hermanns, Holger and H{\"o}fner,Peter},
    title     = {{2nd Workshop on Models for Formal Analysis of Real Systems}},
    year      = {2017},
    series ={Electronic Proceedings in Theoretical Computer Science},
    volume = {244},
    publisher = {Open Publishing Association},
    doi = {10.4204/EPTCS.244}
  }
  

2016

• Special Issue on Relational and Algebraic Methods in Computer Science (RAMiCS 2014)
  ed. Peter Höfner, Peter Jipsen, Wolfram Kahl, Martin E. Müller
  — Elsevier
  Details BibTeX Link PDF ©

  @book{hoefner2016_jlamppre,
  editor    = {H{\"o}fner, Peter and Jipsen, Peter and Kahl, Wolfram and M{\"u}ller, Martin E.},
  title     = {{Special Issue on Relational and Algebraic Methods in Computer Science (RAMiCS 2014)}},
  journal = "Journal of Logical and Algebraic Methods in Programming",
  volume = {85},
  number = {2},
  year      = {2016},
  publisher = {Elsevier}
  }
  

2015

• 1st Workshop on Models for Formal Analysis of Real Systems
  ed. Rob van Glabbeek, Jan Friso Groote, Peter Höfner
  — Open Publishing Association (Electronic Proceedings in Theoretical Computer Science 196)
  Details BibTeX DOI PDF ©

  @book{hoefner2015_mars,
  editor    = {van Glabbeek, Rob and Groote, Jan Friso and H{\"o}fner,Peter},
  title     = {{1st Workshop on Models for Formal Analysis of Real Systems}},
  year      = {2015},
  series ={Electronic Proceedings in Theoretical Computer Science},
  volume = {196},
  publisher = {Open Publishing Association},
  doi = {10.4204/EPTCS.196}
  }
  

• 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2012)
  ed. Wolfram Kahl, Timothy Griffin, Peter Höfner
  — Elsevier
  Details BibTeX Link PDF ©

  @book{hoefner2015_jlamp,
  author    = {Kahl, Wolfram and Griffin, Timothy G. and H{\"o}fner, Peter},
  title     = {{13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2012)}},
  year      = {2015},
  series = {Journal of Logical and Algebraic Methods in Programming},
  volume = {84},
  publisher = {Elsevier}
  }
  

2014

• Relational and Algebraic Methods in Computer Science
  ed. Peter Höfner, Peter Jipsen, Wolfram Kahl, Martin E. Müller
  — Springer (Lecture Notes in Computer Science 8428)
  Details BibTeX DOI PDF ©

  @book{hoefner2014_ramics2,
  editor    = {H{\"o}fner, Peter and Jipsen, Peter and Kahl, Wolfram and M{\"u}ller, Martin E.},
  title     = {{Relational and Algebraic Methods in Computer Science}},
  series    = {Lecture Notes in Computer Science},
  volume = {8428},
  year      = {2014},
  publisher = {Springer}
  }
  

2012

• ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation
  ed. Jacques Fleuriot, Peter Höfner, Annabelle McIver, Alan Smaill
  — EasyChair Proceedings: EPiC Series 17
  Details BibTeX Link PDF ©

  @book{hoefner2012_atx,
  author    = {Fleuriot, Jacques and H{\"o}fner, Peter and Mciver, Annabelle and Smaill, Alan}
  title     = {{ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation}},
  volume = {17},
  series = {EasyChair Proceedings: EPiC Serie},
  publisher = {EasyChair},
  year      = {2012}
  }
  

2011

• Proceedings of Workshop on Automated Theory Engineering (ATE 2011)
  ed. Peter Höfner, Annabelle McIver, Georg Struth
  (CEUR Proceedings Vol-760)
  Details BibTeX Link PDF ©

  @book{hoefner2011_ate,
  editor    = {H{\"o}fner, Peter and McIver, Annabelle and Struth, Georg},
  title     = {{Proceedings of Workshop on Automated Theory Engineering (ATE 2011)}},
  volume = {760},
  series = {CEUR Proceedings},
  publisher = {CEUR},
  year      = {2011}
  }
  

2008

• Towards an Algebraic Composition of Semantic Web Services
  with Florian Lautenbacher
  Relations and Kleene algebra in Computer Science - PhD Programme (pp. 68-72) — Institute of Computer Science, University of Augsburg (Technical Report 2008-04)
  Details BibTeX Link PDF ©

  @misc{hoefner2008-8,
  author = {Lautenbacher, Florian and H{\"o}fner, Peter},
  title     = {{Towards an Algebraic Composition of Semantic Web Services}},
  editor = {Berghammer, Rudolf and M{\"o}ller, Bernhard and Struth, Georg},
  booktitle = {Relations and Kleene algebra in Computer Science (RelMiCS10/AKA5) — PhD Programme},
  series = {Technical Report 2008-04, Institute of Computer Science, University of Augsburg},
  pages = {68-72},
  year = {2008}
  }
  

• First-Order Theorem Prover Evaluation w.r.t. Relation- and Kleene Algebra
  with Han Hing Dang
  Relations and Kleene algebra in Computer Science - PhD Programme (pp. 48-52) — Institute of Computer Science, University of Augsburg (Technical Report 2008-04)
  Details BibTeX Link PDF ©

  @misc{hoefner2008_relmics_phd,
  author = {Dang, Han Hing and H{\"o}fner, Peter},
  title     = {{First-Order Theorem Prover Evaluation w.r.t. Relation- and {K}leene Algebra}},
  editor = {Berghammer, Rudolf and M{\"o}ller, Bernhard and Struth, Georg},
  booktitle = {Relations and Kleene algebra in Computer Science (RelMiCS10/AKA5) — PhD Programme},
  series = {Technical Report 2008-04, Institute of Computer Science, University of Augsburg},
  pages = {48-52},
  year = {2008}
  }
  

2007

• Proof Automation in Kleene Algebra
  14. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'07) (pp. 87-92) — Institutes for Computer Science and Mathematics, University of Lübeck (Technical Report A-07-07, Schriftenreihe A)
  Details BibTeX Link PDF ©

  @misc{hoefner2006-10,
  author = {H{\"o}fner, Peter},
  title     = {{Proof Automation in Kleene Algebra}},
  editor = {Dosch, Walter and Grelck, Clemens and St{\"u}mpel, Annette},
  booktitle = {14. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'07)},
  series = {Technical Report A-07-07, Schriftenreihe A, Institutes for Computer Science and Mathematics, University of Lübeck},
  pages = {87-92},
  year = {2007}
  }
  

2006

• f-Generated Kleene Algebra
  Relations and Kleene algebra in Computer Science - PhD Programme (pp. 55-59) — University of Sheffield, United Kingdom (Technical Report CS-06-09)
  Details BibTeX Link PDF ©

  @misc{hoefner2006_relmics_phd,
  author = {H{\"o}fner, Peter},
  title     = {{$f$-Generated Kleene Algebra}},
  editor = {Schmidt, Renate and Struth, Georg},
  booktitle = {Relations and Kleene algebra in Computer Science (RelMiCS/AKA 2006) — PhD Programme},
  series = {Technical Report CS-06-09, Department of Computer Science, University of Sheffield},
  pages = {55-59},
  year = {2006}
  }
  

2003

• Von sequentieller Algebra zu Kleene-Algebra: Intervalloperatoren und Zeitdauer-Kalkül (in German)
  Details BibTeX Link PDF ©

  @misc{hoefner2003_da,
  author = {H{\"o}fner, Peter},
  title = {{Von sequentieller Algebra zu Kleene-Algebra: Intervalloperatoren und Zeitdauer-Kalk\"ul}},
  school = {Universit\"at Augsburg},
  year = {2003},
  address = {Universit\"at Augsburg, Institut f\"ur Informatik}
  }
  

Technical Reports (incomplete)

2019

• A New Correctness Proof for Prim's Algorithm
  with Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2019_tr02_ua,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{A New Correctness Proof for Prim's Algorithm}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2019-02},
  year = {2019}
  }
  

2016

• A Timed Process Algebra for Wireless Networks with an Application in Routing
  with Emile Bres, Rob van Glabbeek
  Details BibTeX Link arXiv PDF ©

  @techreport{hoefner2016-8,
  author = {Bres, Emile and van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{A Timed Process Algebra for Wireless Networks with an Application in Routing}},
  institution = {NICTA},
  number = {9145},
  year = {2016}
  }
  

2015

• Progress, Fairness and Justness in Process Algebra
  with Rob van Glabbeek
  Details BibTeX Link arXiv PDF ©

  @techreport{hoefner2015_tr8501_nicta,
  author = {van Glabbeek, Rob and H{\"o}fner, Peter},
  title     = {{Progress, Fairness and Justness in Process Algebra}},
  institution = {NICTA},
  number = {8501},
  year = {2015}
  }
  

2013

• A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV
  with Ansgar Fehnker, Rob van Glabbeek, Marius Portmann, Annabelle McIver, Wee Lum Tan
  Details BibTeX Link arXiv PDF ©

  @techreport{hoefner2013_tr5513_nicta,
  author      = {Fehnker, Annabelle and van Glabbeek, Rob and H{\"o}fner, Peter and Portmann, Marius and McIver, Annabelle and Tan, Wee Lum},
  title     = {{A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing {AODV}}},
  institution = {NICTA},
  number      = {5513},
  year        = {2013}
  }
  

• Features, Modularity, and Variation Points
  with Don Batory, Bernhard Möller, Andreas Zelend
  Details BibTeX Link PDF ©

  @techreport{hoefner2013-7,
  author = {Batory, Don and H{\"o}fner, Peter and M{\"o}ller, Bernhard and Zelend, Andreas},
  title     = {{Features, Modularity, and Variation Points}},
  institution = {University of Texas at Austin},
  number = {TR-2147},
  year = {2013}
  }
  

2012

• Foundations of Coloring Algebra with Consequences for Feature-Oriented Programming
  with Bernhard Möller, Andreas Zelend
  Details BibTeX Link PDF ©

  @techreport{hoefner2012_tr06_ua,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard and Zelend, Andreas},
  title     = {{Foundations of Coloring Algebra with Consequences for Feature-Oriented Programming}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2012-06},
  year = {2012}
  }
  

2010

• Supplementing Product Families with Behaviour
  with Ridha Khedri, Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2010_tr13_ua,
  author = {H{\"o}fner, Peter and Khedri, Ridha and M{\"o}ller, Bernhard},
  title     = {{Supplementing Product Families with Behaviour}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2010-13},
  year = {2010}
  }
  

• Requirements in Feature Algebra
  with Sven Mentl, Bernhard Möller, Wolfgang Scholz
  Details BibTeX Link PDF ©

  @techreport{hoefner2010_tr12_ua,
  author = {H{\"o}fner, Peter and Mentl, Sven and M{\"o}ller, Bernhard and Scholz, Wolfgang},
  title     = {{Requirements in Feature Algebra}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2010-12},
  year = {2010}
  }
  

• Fixing Zeno Gaps
  with Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2010_tr11_ua,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Fixing Zeno Gaps}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2010-11},
  year = {2010}
  }
  

• ATPPortal: A User-friendly Webbased Interface for Automated Theorem Provers and for Automatically Generated Proofs
  with Martin E. Müller, Stephan Zeissler
  Details BibTeX Link PDF ©

  @techreport{hoefner2010_tr10_ua,
  author = {H{\"o}fner, Peter and M{\"u}ller, Martin E. and Zeissler, Stephan},
  title = {{ATPPortal}: A User-friendly Webbased Interface for Automated Theorem Provers and for Automatically Generated Proofs},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2010-10},
  year = {2010}
  }
  

• An Extension of Feature Algebra
  with Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2010-5,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{An Extension of Feature Algebra}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2010-09},
  year = {2010}
  }
  

• Algebraic Separation Logic
  with Han Hing Dang, Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2010-4,
  author = {Dang, Han Hing and H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Algebraic Separation Logic}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2010-06},
  year = {2010}
  }
  

• Automated Higher-Order Reasoning in Quantales
  with Han Hing Dang
  Details BibTeX Link PDF ©

  @techreport{hoefner2010-3,
  author = {Dang, Han Hing and H{\"o}fner, Peter},
  title     = {{Automated Higher-Order Reasoning in Quantales}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2010-03},
  year = {2010}
  }
  

2009

• Towards Algebraic Separation Logic
  with Han Hing Dang, Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2009_tr12_ua,
  author = {Dang, Han Hing and H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Towards Algebraic Separation Logic}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2009-12},
  year = {2009}
  }
  

2008

• On Automating the Calculus of Relations
  with Georg Struth
  Details BibTeX Link PDF ©

  @techreport{hoefner2008_tr05,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{On Automating the Calculus of Relations}},
  institution = {Department of Computer Science, University of Sheffield},
  number = {CS-08-05},
  year = {2009}
  }
  

2007

• Algebraic View Reconciliation
  with Ridha Khedri, Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hfner2007,
  author    = {Peter H{\"o}fner and
  Ridha Khedri and
  Bernhard M{\"o}ller},
  title     = {{Algebraic View Reconciliation}},
  year      = {2007},
  institution = {Institute of Computer Science, University of Augsburg},
  number    = {2007-13},
  }
  

• Algebraic Structure of Web Services
  with Florian Lautenbacher
  Details BibTeX Link PDF ©

  @techreport{hoefner2007__tr12_ua,
  author = {H{\"o}fner, P. and Lautenbacher, F.},
  title     = {{Algebraic Structure of Web Services}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2007-12},
  year = {2007}
  }
  

• An Algebra of Hybrid Systems
  with Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2007_tr08_ua,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{An Algebra of Hybrid Systems}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2007-08},
  year = {2007}
  }
  

• Can Refinement be Automated?
  with Georg Struth
  Details BibTeX Link PDF ©

  @techreport{hoefner2007_tr08_su,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{Can Refinement be Automated?}},
  institution = {Department of Computer Science, University of Sheffield},
  number = {CS-07-08},
  year = {2007}
  }
  

• Automated Reasoning in Kleene Algebra
  with Georg Struth
  Details BibTeX Link PDF ©

  @techreport{hoefner2007_tr04_su,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{Automated Reasoning in Kleene Algebra}},
  institution = {Department of Computer Science, University of Sheffield},
  number = {CS-07-04},
  year = {2007}
  }
  

2006

• Algebraic Notions of Non-Termination
  with Georg Struth
  Details BibTeX Link PDF ©

  @techreport{hoefner2006-11,
  author = {H{\"o}fner, Peter and Struth, Georg},
  title     = {{Algebraic Notions of Non-Termination}},
  institution = {Department of Computer Science, University of Sheffield},
  number = {CS-06-12},
  year = {2006}
  }
  

• Omega Algebra, Demonic Refinement Algebra and Commands
  with Bernhard Möller, Kim Solin
  Details BibTeX Link PDF ©

  @techreport{hoefner2006_tr11_ua,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard and Solin, Kim},
  title     = {{Omega Algebra, Demonic Refinement Algebra and Commands}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2006-11},
  year = {2006}
  }
  

• Lazy Semiring Neighbours and some Applications
  with Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2006-6,
  author = {H{\"o}fner, Peter and M{\"o}ller, Bernhard},
  title     = {{Lazy Semiring Neighbours and some Applications}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2006-09},
  year = {2006}
  }
  

• Quantales and Temporal Logics
  with Bernhard Möller, Georg Struth
  Details BibTeX Link PDF ©

  @techreport{hoefner2006_tr06_ua,
  author = {M{\"o}ller, Bernhard and H{\"o}fner, Peter and Struth, Georg},
  title     = {{Quantales and Temporal Logics}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2006-06},
  year = {2006}
  }
  

• Feature Algebra
  with Ridha Khedri, Bernhard Möller
  Details BibTeX Link PDF ©

  @techreport{hoefner2006_tr04_ua,
  author = {H{\"o}fner, Peter and Khedri, Ridha and M{\"o}ller, Bernhard},
  title     = {{Feature Algebra}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2006-04},
  year = {2006}
  }
  

2005

• Semiring Neighbours
  Details BibTeX Link PDF ©

  @techreport{hoefner2005_tr19_ua,
  author = {H{\"o}fner, Peter},
  title     = {{Semiring Neighbours}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2005-19},
  year = {2005}
  }
  

• Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System
  with Alfons Huhn, Werner Kießling
  Details BibTeX Link PDF ©

  @techreport{hoefner2005_tr07_ua,
  author = {Huhn, Alfons and H{\"o}fner, Peter and Kie{\ss}ling, Werner},
  title     = {{Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2005-07},
  year = {2005}
  }
  

• From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus
  Details BibTeX Link PDF ©

  @techreport{hoefner2005_tr05_ua,
  author = {H{\"o}fner, Peter},
  title     = {{From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus}},
  institution = {Institute of Computer Science, University of Augsburg},
  number = {2005-05},
  year = {2005}
  }