Professor Georg Struth
PhD
School of Computer Science
Professor of Theoretical Computer Science
Head of the Foundations of Computation research group
+44 114 222 1846
Full contact details
School of Computer Science
Regent Court (DCS)
211 Portobello
Sheffield
S1 4DP
 Profile

Georg studied theoretical physics and philosophy at the University of Heidelberg and obtained a PhD in computer science from the Max Planck Institute for Informatics in Saarbrücken. After a series of positions at German universities he joined the University of Sheffield in 2005.
 Research interests

Georg works mainly on logical and algebraic methods in computer science, formalised mathematics with interactive theorem provers and program verification and correctness.
His interests range from foundational work on the axiomatisation and semantics of sequential and concurrent computing systems to applications in the design and implementation of program verification software.
 Publications

Books
 Modelling Computing Systems. Springer London.
 Preface. Elsevier.
Journal articles
 Determinism of multirelations. Journal of Logical and Algebraic Methods in Programming, 139, 100976100976.
 Catoids and modal convolution algebras. Algebra universalis, 84.
 Posets with interfaces as a model for concurrency. Information and Computation, 104914104914.
 Convolution and concurrency. Mathematical Structures in Computer Science.
 Predicate transformer semantics for hybrid systems: verification components for Isabelle/HOL. Journal of Automated Reasoning, 66(1), 93139. View this article in WRRO
 Languages of higherdimensional automata. Mathematical Structures in Computer Science, 31(5), 575613.
 Convolution algebras: Relational convolution, generalised modalities and incidence algebras. Logical Methods in Computer Science, 17(1), 13:113:34. View this article in WRRO
 Convolution and Concurrency.
 Relational and algebraic methods in computer science. Journal of Logical and Algebraic Methods in Programming, 106, 198199.
 Schedulers and finishers: On generating and filtering the behaviours of an event structure. Theoretical Computer Science, 744, 97112.
 Hoare Semigroups. Mathematical Structures in Computer Science. View this article in WRRO
 Kleisli, Parikh and Peleg compositions and liftings for multirelations. Journal of Logical and Algebraic Methods in Programming, 90, 84101.
 Probabilistic relyguarantee calculus. Theoretical Computer Science, 655, 120134.
 Taming Multirelations. ACM Transactions on Computational Logic, 17(4), 134.
 Developments in concurrent Kleene algebra. Journal of Logical and Algebraic Methods in Programming, 85(4), 617636.
 Building program construction and verification tools from algebraic principles. Formal Aspects of Computing, 28(2), 265293.
 Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. ACM Transactions on Computational Logic, 17(3).
 On the expressive power of Kleene algebra with domain. Information Processing Letters, 116(4), 284288.
 Concurrent Dynamic Algebra. ACM Transactions on Computational Logic, 16(4), 138.
 Completeness results for omegaregular algebras. Journal of Logical and Algebraic Methods in Programming, 84(3), 402425.
 On the FineStructure of Regular Algebra. Journal of Automated Reasoning, 54(2), 165197.
 Programming and automating mathematics in the Tarski–Kleene hierarchy. Journal of Logical and Algebraic Methods in Programming, 83(2), 87102.
 Kleene Algebra with Tests and Demonic Refinement Algebras.. Arch. Formal Proofs, 2014.
 Algebraic Principles for RelyGuarantee Style Concurrency Verification Tools, 7893.
 Kleene Algebra.. Arch. Formal Proofs, 2013.
 On Completeness of OmegaRegular Algebras. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7560 LNCS, 179194.
 Left omega algebras and regular equations. Journal of Logic and Algebraic Programming.
 Left omega algebras and regular equations. Journal of Logic and Algebraic Programming, 81(6), 705717.
 Automated analysis of regular algebra. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7364 LNAI, 271285.
 Dependently Typed Programming based on Automated Theorem Proving. CoRR, abs/1112.3833.
 Automating algebraic methods in Isabelle. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6991 LNCS, 617632.
 Omega algebras and regular equations. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6663 LNCS, 248263.
 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, 5267.
 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, 250264.
 Concurrent Kleene Algebra and its Foundations. Journal of Logic and Algebraic Programming, 80(6), 266296.
 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, 264279.
 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, 116130. View this article in WRRO
 Concurrent Kleene Algebra and its Foundations. Journal of Logic and Algebraic Programming.
 Internal axioms for domain semirings. Science of Computer Programming, 76(3), 181203.
 Relations and Kleene algebras in computer science. J LOGIC ALGEBR PROGR, 79(8), 705706.
 Algebraic notions of nontermination: Omega and divergence in idempotent semirings. J LOGIC ALGEBR PROGR, 79(8), 794811.
 Automated verification of refinement laws. ANN MATH ARTIF INTEL, 55(12), 3562. View this article in WRRO
 Relations and Kleene algebras in computer science. J LOGIC ALGEBR PROGR, 76(1), 12.
 Kleene algebra with domain. ACM T COMPUT LOG, 7(4), 798833.
 Abstract abstract reduction. J LOGIC ALGEBR PROGR, 66(2), 239270.
 Kleene algebra with domain. CoRR, cs.LO/0310054.
 Algebraic coherent confluence and higher globular Kleene algebras. Logical Methods in Computer Science, Volume 18, Issue 4.
 Domain Semirings United. Acta Cybernetica.
 Probabilistic Concurrent Kleene Algebra. Electronic Proceedings in Theoretical Computer Science, 117, 97115.
 Algebraic Notions of Termination. Logical Methods in Computer Science, Volume 7, Issue 1 (February 11, 2011) lmcs:777.
Chapters
 Categorical Information Flow, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy (pp. 329343). Springer International Publishing
 A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic, Unifying Theories of Programming (pp. 321). Springer International Publishing
 Cylindric Kleene Lattices for Program Construction, Lecture Notes in Computer Science (pp. 197225). Springer International Publishing
 Preface (pp. VVI).
Conference proceedings papers
 A Kleene Theorem for HigherDimensional Automata. Leibniz International Proceedings in Informatics, LIPIcs, Vol. 243
 $$ell r$$Multisemigroups, Modal Quantales and the Origin of Locality (pp 90107)
 Effect Algebras, Girard Quantales and Complementation in Separation Logic (pp 3753)
 Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs (pp 367386)
 Generating Posets Beyond N (pp 8299)
 Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL (pp 169186)
 Verifying Hybrid Systems with Modal Kleene Algebra (pp 225243)
 On decidability of concurrent kleene algebra. Leibniz International Proceedings in Informatics, LIPIcs, Vol. 85, 5 September 2017  8 September 2017. View this article in WRRO
 Relational and Algebraic Methods in Computer Science
 A Discrete Geometric Model of Concurrent Program Execution (pp 125) View this article in WRRO
 Schedulers and Finishers: On Generating the Behaviours of an Event Structure (pp 121138)
 Modal Kleene Algebra Applied to Program Correctness (pp 310325)
 Relational Formalisations of Compositions and Liftings of Multirelations (pp 84100)
 A Program Construction and Verification Tool for Separation Logic (pp 137158)
 Completeness theorems for biKleene algebras and seriesparallel rational pomset languages. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 8428 LNCS (pp 6582)
 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 118)
 Lightweight Program Construction and Verification Tools in Isabelle/HOL (pp 519)
 Algebraic principles for relyguarantee 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 7893)
 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 4964)
 Preface (pp ixx)
 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 197212)
 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 653667)
 Automated Reasoning in HigherOrder Regular Algebra.. RAMICS, Vol. 7560 (pp 6681)
 Correctness of Object Oriented Models by Extended Type Inference.. ICTAC, Vol. 7521 (pp 4660)
 Dependently Typed Programming Based on Automated Theorem Proving. Mathematics of Program Construction, Vol. Lecture Notes in Computer Science 7342 (pp 220240). Madrid, Spain, 25 June 2012  27 June 2012.
 A repository for TarskiKleene algebras. CEUR Workshop Proceedings, Vol. 760 (pp 3039)
 On Automated Program Construction and Verification.. MPC, Vol. 6120 (pp 2241)
 Domain and Antidomain Semigroups. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, Vol. 5827 (pp 7387)
 Foundations of Concurrent Kleene Algebra. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, Vol. 5827 (pp 166186)
 Concurrent Kleene Algebra. CONCUR 2009  CONCURRENCY THEORY, PROCEEDINGS, Vol. 5710 (pp 399414)
 Modal Tools for Separation and Refinement.. Electron. Notes Theor. Comput. Sci., Vol. 214 (pp 81101)
 Can Refinement be Automated?. Electron. Notes Theor. Comput. Sci., Vol. 201 (pp 197222)
 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 711, 2008. Proceedings. RelMiCS, Vol. 4988
 Domain axioms for a family of nearsemirings. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 5140 (pp 330345)
 On automating the calculus of relations. AUTOMATED REASONING, PROCEEDINGS, Vol. 5195 (pp 5066)
 Modal semirings revisited. MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, Vol. 5133 (pp 360387)
 Nontermination in idempotent semirings. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, Vol. 4988 (pp 206220)
 The structure of the onegenerated free domain semiring. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, Vol. 4988 (pp 234242)
 Automated reasoning in kleene algebra. Automated Deduction  CADE21, Proceedings, Vol. 4603 (pp 279294)
 Algebras of modal operators and partial correctness. THEORETICAL COMPUTER SCIENCE, Vol. 351(2) (pp 221239)
 Quantales and temporal logics. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 263277)
 Tableaux for lattices. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 323337)
 Constructing rewritebased decision procedures for embeddings and termination. MATHEMATICS OF PROGRAM CONSTRUCTION, Vol. 4014 (pp 416432)
 wp Is wlp. RELATIONAL METHODS IN COMPUTER SCIENCE, 2005, Vol. 3929 (pp 200211)
 KnuthBendix completion as a data structure. RELATIONAL METHODS IN COMPUTER SCIENCE, 2005, Vol. 3929 (pp 225236)
 Diagram Chase in Relational System Development.. Electron. Notes Theor. Comput. Sci., Vol. 127 (pp 87105)
 p Is.. RelMiCS, Vol. 3929 (pp 200211)
 Relational and KleeneAlgebraic 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 1217, 2003, Revised Selected Papers. RelMiCS, Vol. 3051
 Termination in modal Kleene algebra. EXPLORING NEW FRONTIERS OF THEORETICAL INFORMATICS, Vol. 155 (pp 647660)
 Modal Kleene algebra and partial correctness. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, Vol. 3116 (pp 379393)
 Automated elementwise reasoning with sets. PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS (pp 320329)
 Kleene modules. RELATIONAL AND KLEENEALGEBRAIC METHODS IN COMPUTER SCIENCE, Vol. 3051 (pp 112123)
 Greedylike algorithms in modal Kleene algebra. RELATIONAL AND KLEENEALGEBRAIC METHODS IN COMPUTER SCIENCE, Vol. 3051 (pp 202214)
 A calculus for setbased program development. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Vol. 2885 (pp 541559)
 Deriving focused lattice calculi. REWRITING TECHNIQUES AND APPLICATIONS, Vol. 2378 (pp 8397)
 Calculating ChurchRosser proofs in Kleene algebra. RELATIONAL METHODS IN COMPUTER SCIENCE, Vol. 2561 (pp 276290)
 KnuthBendix Completion for NonSymmetric Transitive Relations.. Electron. Notes Theor. Comput. Sci., Vol. 59 (pp 341357)
 Deriving Focused Calculi for Transitive Relations.. RTA, Vol. 2051 (pp 291305)
 An algebra of resolution. REWRITING TECHNIQUES AND APPLICATIONS, PROCEEDINGS, Vol. 1833 (pp 214228)
 On the word problem for free lattices. REWRITING TECHNIQUES AND APPLICATIONS, Vol. 1232 (pp 128141)
 Grants

Current Grants
 Verifiably Correct Transactional Memory, EPSRC, 10/2018 to 09/2021, £397,680, as coPI
 Verifying concurrent algorithms on Weak Memory Models, EPSRC, 05/2015 to 11/2018, £389,207, as CoPI
Previous Grants
 Midlands Graduate School in the Foundations of Computing Science 2010, EPSRC, 03/2010 to 03/2011, £4,704, as PI
 Verifying Concurrent Lockfree Algorithms, EPSRC, 04/2012 to 10/2015, £378,907, as CoPI
 Algebras and Proof Automation for Algorithmic Game Development, ROYAL SOCIETY, 01/2013 to 12/2014, £6,500, as PI
 Professional activities and memberships

Head of the Verification research group