Professor Georg Struth

Books

• Moller F & Struth G (2013) Modelling Computing Systems. Springer London.
• PINCUS G, THIMANN KV & ASTWOOD EB (1964) Preface. Elsevier.

Journal articles

• Furusawa H, Guttmann W & Struth G (2026) On the inner structure of multirelations. Journal of Logical and Algebraic Methods in Programming, 148.
• Struth G & Ziemiański K (2025) Presheaf automata. Annals of Pure and Applied Logic, 103660-103660.
• Calk C, Malbos P, Pous D & Struth G (2025) Higher catoids, higher quantales and their correspondences. Applied Categorical Structures, 33(4). View this article in WRRO
• Furusawa H, Guttmann W & Struth G (2025) Modal algebra of multirelations. Journal of Logic and Computation, 35(3).
• Huerta y Munive JJ, Foster S, Gleirscher M, Struth G, Pardillo Laursen C & Hickman T (2024) IsaVODEs: interactive verification of cyber-physical systems at scale. Journal of Automated Reasoning, 68(4). View this article in WRRO
• Malbos P, Massacrier T & Struth G (2024) Single-set cubical categories and their formalisation with a proof assistant. Journal of Automated Reasoning, 68(4). View this article in WRRO
• Furusawa H, Guttmann W & Struth G (2024) Determinism of multirelations. Journal of Logical and Algebraic Methods in Programming, 139, 100976-100976.
• Cranch J & Struth G (2024) Interacting Monoidal Structures with Applications in Computing.. CoRR, abs/2411.03821.
• Fahrenberg U, Johansen C, Struth G & Ziemiański K (2023) Catoids and modal convolution algebras. Algebra universalis, 84(2).
• Fahrenberg U, Johansen C, Struth G & Ziemiański K (2022) Posets with interfaces as a model for concurrency. Information and Computation, 285, 104914-104914.
• Huerta y Munive JJ & Struth G (2022) Predicate transformer semantics for hybrid systems: verification components for Isabelle/HOL. Journal of Automated Reasoning, 66(1), 93-139.
• Cranch J, Doherty S & Struth G (2021) Convolution and concurrency. Mathematical Structures in Computer Science, 31(8), 918-949.
• Fahrenberg U, Johansen C, Struth G & Ziemiański K (2021) Languages of higher-dimensional automata. Mathematical Structures in Computer Science, 31(5), 575-613.
• Dongol B, Hayes IJ & Struth G (2021) Convolution algebras: Relational convolution, generalised modalities and incidence algebras. Logical Methods in Computer Science, 17(1), 13:1-13:34.
• Cranch J, Doherty S & Struth G (2020) Convolution and Concurrency.
• Höfner P, Pous D & Struth G (2019) Relational and algebraic methods in computer science. Journal of Logical and Algebraic Methods in Programming, 106, 198-199.
• McIver A, Rabehaja T & Struth G (2018) Schedulers and finishers: On generating and filtering the behaviours of an event structure. Theoretical Computer Science, 744, 97-112.
• Struth G (2018) Hoare semigroups. Mathematical Structures in Computer Science, 28(6). View this article in WRRO
• Furusawa H, Kawahara Y, Struth G & Tsumagari N (2017) Kleisli, Parikh and Peleg compositions and liftings for multirelations. Journal of Logical and Algebraic Methods in Programming, 90, 84-101.
• McIver A, Rabehaja T & Struth G (2016) Probabilistic rely-guarantee calculus. Theoretical Computer Science, 655, 120-134.
• Furusawa H & Struth G (2016) Taming Multirelations. ACM Transactions on Computational Logic, 17(4), 1-34.
• Hoare T, van Staden S, Möller B, Struth G & Zhu H (2016) Developments in concurrent Kleene algebra. Journal of Logical and Algebraic Methods in Programming, 85(4), 617-636.
• Armstrong A, Gomes VBF & Struth G (2016) Building program construction and verification tools from algebraic principles. Formal Aspects of Computing, 28(2), 265-293.
• Dongol B, Hayes IJ & Struth G (2016) Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. ACM Transactions on Computational Logic, 17(3).
• Struth G (2016) On the expressive power of Kleene algebra with domain. Information Processing Letters, 116(4), 284-288.
• Furusawa H & Struth G (2015) Concurrent Dynamic Algebra. ACM Transactions on Computational Logic, 16(4), 1-38.
• Cranch J, Laurence MR & Struth G (2015) Completeness results for omega-regular algebras. Journal of Logical and Algebraic Methods in Programming, 84(3), 402-425.
• Foster S & Struth G (2015) On the Fine-Structure of Regular Algebra. Journal of Automated Reasoning, 54(2), 165-197.
• Armstrong A, Struth G & Weber T (2014) Programming and automating mathematics in the Tarski–Kleene hierarchy. Journal of Logical and Algebraic Methods in Programming, 83(2), 87-102.
• Armstrong A, Gomes VBF & Struth G (2014) Kleene Algebra with Tests and Demonic Refinement Algebras.. Arch. Formal Proofs, 2014.
• Armstrong A, Gomes VBF & Struth G (2014) Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools, 78-93.
• Armstrong A, Struth G & Weber T (2013) Kleene Algebra.. Arch. Formal Proofs, 2013.
• Laurence MR & Struth G (2012) On Completeness of Omega-Regular Algebras. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 7560 LNCS, 179-194.
• Laurence M & Struth G (2012) Left omega algebras and regular equations. Journal of Logic and Algebraic Programming.
• Laurence M & Struth G (2012) Left omega algebras and regular equations. Journal of Logic and Algebraic Programming, 81(6), 705-717.
• Foster S & Struth G (2012) Automated analysis of regular algebra. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 7364 LNAI, 271-285.
• Guttmann W, Struth G & Weber T (2011) Automating algebraic methods in Isabelle. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 6991 LNCS, 617-632.
• Hoare CAR, Hussain A, Möller B, O'Hearn PW, Petersen RL & Struth G (2011) On locality and the exchange law for concurrent processes. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 6901 LNCS, 250-264.
• Hoare T, Möller B, Struth G & Wehrman I (2011) Concurrent Kleene Algebra and its Foundations. Journal of Logic and Algebraic Programming, 80(6), 266-296.
• Hoare T, Möller B, Struth G & Wehrman I (2011) Concurrent Kleene Algebra and its Foundations. Journal of Logic and Algebraic Programming.
• Laurence MR & Struth G (2011) Omega algebras and regular equations. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 6663 LNCS, 248-263.
• Foster S, Struth G & Weber T (2011) Automated engineering of relational and algebraic methods in Isabelle/HOL (invited tutorial). Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 6663 LNCS, 52-67.
• McIver A, Rabehaja TM & Struth G (2011) On probabilistic Kleene algebras, automata and simulations. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 6663 LNCS, 264-279.
• Foster S & Struth G (2011) Integrating an automated theorem prover into Agda. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 6617 LNCS, 116-130.
• Desharnais J & Struth G (2011) Internal axioms for domain semirings. Science of Computer Programming, 76(3), 181-203.
• Armstrong A, Foster S & Struth G (2011) Dependently Typed Programming based on Automated Theorem Proving. CoRR, abs/1112.3833.
• Jules D, Moeller B & Georg S (2010) Algebraic Notions of Termination. Logical Methods in Computer Science, Volume 7, Issue 1 (February 11, 2011) lmcs:777.
• Berghammer R, Moller B & Struth G (2010) Relations and Kleene algebras in computer science. J LOGIC ALGEBR PROGR, 79(8), 705-706.
• Hofner P & Struth G (2010) Algebraic notions of nontermination: Omega and divergence in idempotent semirings. J LOGIC ALGEBR PROGR, 79(8), 794-811.
• Hofner P, Struth G & Sutcliffe G (2009) Automated verification of refinement laws. ANN MATH ARTIF INTEL, 55(1-2), 35-62.
• Schmidt RA & Struth G (2008) Relations and Kleene algebras in computer science. J LOGIC ALGEBR PROGR, 76(1), 1-2.
• Desharnais J, Moller B & Struth G (2006) Kleene algebra with domain. ACM T COMPUT LOG, 7(4), 798-833.
• Struth G (2006) Abstract abstract reduction. J LOGIC ALGEBR PROGR, 66(2), 239-270.
• Desharnais J, Möller B & Struth G (2003) Kleene algebra with domain. CoRR, cs.LO/0310054.
• Fahrenberg U, Johansen C, Struth G & Ziemiański K () Kleene Theorem for Higher-Dimensional Automata. Logical Methods in Computer Science, Volume 20, Issue 4.
• Calk C, Goubault E, Malbos P & Struth G () Algebraic coherent confluence and higher globular Kleene algebras. Logical Methods in Computer Science, Volume 18, Issue 4.
• Fahrenberg U, Johansen C, Struth G & Ziemiański K () Domain Semirings United. Acta Cybernetica.
• McIver A, Rabehaja T & Struth G () Probabilistic Concurrent Kleene Algebra. Electronic Proceedings in Theoretical Computer Science, 117, 97-115.

Book chapters

• Rabehaja T, McIver A, Morgan C & Struth G (2019) Categorical Information Flow, Lecture Notes in Computer Science (pp. 329-343). Springer International Publishing
• Hoare T, Struth G & Woodcock J (2019) A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic, Lecture Notes in Computer Science (pp. 3-21). Springer International Publishing
• Dongol B, Hayes I, Meinicke L & Struth G (2019) Cylindric Kleene Lattices for Program Construction, Lecture Notes in Computer Science (pp. 197-225). Springer International Publishing
• Höfner P, Pous D & Struth G (2017) Preface (pp. V-VI).

Conference proceedings

• Fahrenberg U, Johansen C, Struth G & Ziemiański K (2022) A Kleene Theorem for Higher-Dimensional Automata. Leibniz International Proceedings in Informatics Lipics, Vol. 243
• Foster S, Huerta y Munive JJ, Gleirscher M & Struth G (2021) Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs (pp 367-386)
• Calk C, Fahrenberg U, Johansen C, Struth G & Ziemiański K (2021) $$ell r$$-Multisemigroups, Modal Quantales and the Origin of Locality (pp 90-107)
• Bannister C, Höfner P & Struth G (2021) Effect Algebras, Girard Quantales and Complementation in Separation Logic (pp 37-53)
• Fahrenberg U, Johansen C, Struth G & Bahadur Thapa R (2020) Generating Posets Beyond N (pp 82-99)
• Foster S, Huerta y Munive JJ & Struth G (2020) Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL (pp 169-186)
• Huerta y Munive JJ & Struth G (2018) Verifying Hybrid Systems with Modal Kleene Algebra (pp 225-243)
• Brunet P, Pous D & Struth G (2017) On decidability of concurrent Kleene algebra. LIPIcs, Vol. 85(28). Berlin, Germany, 5 September 2018 - 5 September 2018. View this article in WRRO
• Möller B, Hoare T, Müller ME & Struth G (2017) A discrete geometric model of concurrent program execution. International Symposium on Unifying Theories of Programming, Vol. 10134 (pp 1-25). Reykjavik, Iceland View this article in WRRO
• (2017) Relational and Algebraic Methods in Computer Science
• Gomes VBF & Struth G (2016) Modal Kleene Algebra Applied to Program Correctness (pp 310-325)
• McIver A, Rabehaja T & Struth G (2016) Schedulers and Finishers: On Generating the Behaviours of an Event Structure (pp 121-138)
• Furusawa H, Kawahara Y, Struth G & Tsumagari N (2015) Relational Formalisations of Compositions and Liftings of Multirelations (pp 84-100)
• Dongol B, Gomes VBF & Struth G (2015) A Program Construction and Verification Tool for Separation Logic (pp 137-158)
• Laurence MR & Struth G (2014) Completeness theorems for bi-Kleene algebras and series-parallel rational pomset languages. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, Vol. 8428 LNCS (pp 65-82)
• Hoare T, Van Staden S, Möller B, Struth G, Villard J, Zhu H & O'Hearn P (2014) Developments in Concurrent Kleene Algebra. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, Vol. 8428 LNCS (pp 1-18)
• Armstrong A, Gomes VBF & Struth G (2014) Lightweight Program Construction and Verification Tools in Isabelle/HOL (pp 5-19)
• Armstrong A, Gomes VBF & Struth G (2014) Algebraic principles for rely-guarantee style concurrency verification tools. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 8442 LNCS (pp 78-93)
• Armstrong A, Gomes VBF & Struth G (2014) Algebras for program correctness in Isabelle/HOL. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, Vol. 8428 LNCS (pp 49-64)
• Williams IH & Williams NH (2014) Preface (pp ix-x)
• McIver A, Rabehaja T & Struth G (2013) An event structure model for probabilistic concurrent Kleene algebra. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, Vol. 8312 LNCS (pp 653-667)
• Armstrong A, Struth G & Weber T (2013) Program analysis and verification based on Kleene algebra in Isabelle/HOL. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, Vol. 7998 LNCS (pp 197-212)
• Armstrong A & Struth G (2012) Automated Reasoning in Higher-Order Regular Algebra.. RAMiCS, Vol. 7560 (pp 66-81)
• Foster S, Rypacek O & Struth G (2012) Correctness of Object Oriented Models by Extended Type Inference.. ICTAC, Vol. 7521 (pp 46-60)
• Armstrong A, Foster S & Struth G (2012) Dependently Typed Programming Based on Automated Theorem Proving. Mathematics of Program Construction, Vol. Lecture Notes in Computer Science 7342 (pp 220-240). Madrid, Spain, 25 June 2012 - 27 June 2012.
• Guttmann W, Struth G & Weber T (2011) A repository for Tarski-Kleene algebras. Ceur Workshop Proceedings, Vol. 760 (pp 30-39)
• Berghammer R & Struth G (2010) On Automated Program Construction and Verification.. MPC, Vol. 6120 (pp 22-41)
• Desharnais J, Jipsen P & Struth G (2009) Domain and Antidomain Semigroups. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, Vol. 5827 (pp 73-87)
• Hoare CAR, Moller B, Struth G & Wehrman I (2009) Foundations of Concurrent Kleene Algebra. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, Vol. 5827 (pp 166-186)
• Hoare CART, Moller B, Struth G & Wehrman I (2009) Concurrent Kleene Algebra. CONCUR 2009 - CONCURRENCY THEORY, PROCEEDINGS, Vol. 5710 (pp 399-414)
• Hofner P & Struth G (2008) On automating the calculus of relations. AUTOMATED REASONING, PROCEEDINGS, Vol. 5195 (pp 50-66)
• Desharnais J & Struth G (2008) Domain axioms for a family of near-semirings. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 5140 (pp 330-345)
• Desharnais J & Struth G (2008) Modal semirings revisited. MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, Vol. 5133 (pp 360-387)
• Struth G (2008) Modal Tools for Separation and Refinement.. Refine@FM (pp 81-101)
• (2008) Relations and Kleene Algebra in Computer Science, 10th International Conference on Relational Methods in Computer Science, and 5th International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2008, Frauenwörth, Germany, April 7-11, 2008. Proceedings. RelMiCS, Vol. 4988
• Hofner P & Struth G (2008) Non-termination in idempotent semirings. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, Vol. 4988 (pp 206-220)
• Jipsen P & Struth G (2008) The structure of the one-generated free domain semiring. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, Vol. 4988 (pp 234-242)
• Höfner P & Struth G (2007) Can Refinement be Automated?. REFINE@IFM (pp 197-222)
• Hofner P & Struth G (2007) Automated reasoning in kleene algebra. Automated Deduction - CADE-21, Proceedings, Vol. 4603 (pp 279-294)
• Struth G (2006) Knuth-Bendix completion as a data structure. RELATIONAL METHODS IN COMPUTER SCIENCE, 2005, Vol. 3929 (pp 225-236)
• Moller B & Struth G (2006) Algebras of modal operators and partial correctness. THEORETICAL COMPUTER SCIENCE, Vol. 351(2) (pp 221-239)
• Moller B, Hofner P & Struth G (2006) Quantales and temporal logics. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 263-277)
• Struth G (2006) Tableaux for lattices. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 323-337)
• Struth G (2006) Constructing rewrite-based decision procedures for embeddings and termination. MATHEMATICS OF PROGRAM CONSTRUCTION, Vol. 4014 (pp 416-432)
• Moller B & Struth G (2006) wp Is wlp. RELATIONAL METHODS IN COMPUTER SCIENCE, 2005, Vol. 3929 (pp 200-211)
• Möller B & Struth G (2005) p Is.. RelMiCS, Vol. 3929 (pp 200-211)
• Ebert M & Struth G (2004) Diagram Chase in Relational System Development.. VLFM, Vol. 127 (pp 87-105)
• Struth G (2004) Automated element-wise reasoning with sets. PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS (pp 320-329)
• (2004) Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12-17, 2003, Revised Selected Papers. RelMiCS, Vol. 3051
• Desharnais J, Moller B & Struth G (2004) Termination in modal Kleene algebra. EXPLORING NEW FRONTIERS OF THEORETICAL INFORMATICS, Vol. 155 (pp 647-660)
• Moller B & Struth G (2004) Modal Kleene algebra and partial correctness. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, Vol. 3116 (pp 379-393)
• Ehm T, Moller B & Struth G (2003) Kleene modules. RELATIONAL AND KLEENE-ALGEBRAIC METHODS IN COMPUTER SCIENCE, Vol. 3051 (pp 112-123)
• Moller B & Struth G (2003) Greedy-like algorithms in modal Kleene algebra. RELATIONAL AND KLEENE-ALGEBRAIC METHODS IN COMPUTER SCIENCE, Vol. 3051 (pp 202-214)
• Struth G (2003) A calculus for set-based program development. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Vol. 2885 (pp 541-559)
• Struth G (2002) Calculating Church-Rosser proofs in Kleene algebra. RELATIONAL METHODS IN COMPUTER SCIENCE, Vol. 2561 (pp 276-290)
• Struth G (2002) Deriving focused lattice calculi. REWRITING TECHNIQUES AND APPLICATIONS, Vol. 2378 (pp 83-97)
• Struth G (2001) Knuth-Bendix Completion for Non-Symmetric Transitive Relations.. RULE@PLI, Vol. 59 (pp 341-357)
• Struth G (2001) Deriving Focused Calculi for Transitive Relations.. RTA, Vol. 2051 (pp 291-305)
• Struth G (2000) An algebra of resolution. REWRITING TECHNIQUES AND APPLICATIONS, PROCEEDINGS, Vol. 1833 (pp 214-228)
• Struth G (1997) On the word problem for free lattices. REWRITING TECHNIQUES AND APPLICATIONS, Vol. 1232 (pp 128-141)

Preprints

• Cranch J & Struth G (2024) Interacting Monoidal Structures with Applications in Computing, arXiv.