Professor Georg Struth

PhD

School of Computer Science

Professor of Theoretical Computer Science

Head of the Foundations of Computation research group

g.struth@sheffield.ac.uk
+44 114 222 1846

Full contact details

Professor Georg Struth
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

Journal articles

Chapters

Conference proceedings papers

  • 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 RIS download Bibtex download
  • 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) RIS download Bibtex download
  • Bannister C, Höfner P & Struth G (2021) Effect Algebras, Girard Quantales and Complementation in Separation Logic (pp 37-53) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • Fahrenberg U, Johansen C, Struth G & Bahadur Thapa R (2020) Generating Posets Beyond N (pp 82-99) RIS download Bibtex download
  • Foster S, Huerta y Munive JJ & Struth G (2020) Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL (pp 169-186) RIS download Bibtex download
  • Huerta y Munive JJ & Struth G (2018) Verifying Hybrid Systems with Modal Kleene Algebra (pp 225-243) RIS download Bibtex download
  • Brunet P, Pous D & Struth G (2017) 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 RIS download Bibtex download
  • (2017) Relational and Algebraic Methods in Computer Science RIS download Bibtex download
  • Möller B, Hoare T, Müller ME & Struth G (2017) A Discrete Geometric Model of Concurrent Program Execution (pp 1-25) View this article in WRRO RIS download Bibtex download
  • McIver A, Rabehaja T & Struth G (2016) Schedulers and Finishers: On Generating the Behaviours of an Event Structure (pp 121-138) RIS download Bibtex download
  • Gomes VBF & Struth G (2016) Modal Kleene Algebra Applied to Program Correctness (pp 310-325) RIS download Bibtex download
  • Furusawa H, Kawahara Y, Struth G & Tsumagari N (2015) Relational Formalisations of Compositions and Liftings of Multirelations (pp 84-100) RIS download Bibtex download
  • Dongol B, Gomes VBF & Struth G (2015) A Program Construction and Verification Tool for Separation Logic (pp 137-158) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • Armstrong A, Gomes VBF & Struth G (2014) Lightweight Program Construction and Verification Tools in Isabelle/HOL (pp 5-19) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • Williams IH & Williams NH (2014) Preface (pp ix-x) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • Armstrong A & Struth G (2012) Automated Reasoning in Higher-Order Regular Algebra.. RAMICS, Vol. 7560 (pp 66-81) RIS download Bibtex download
  • Foster S, Rypacek O & Struth G (2012) Correctness of Object Oriented Models by Extended Type Inference.. ICTAC, Vol. 7521 (pp 46-60) RIS download Bibtex download
  • 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. RIS download Bibtex download
  • Guttmann W, Struth G & Weber T (2011) A repository for Tarski-Kleene algebras. CEUR Workshop Proceedings, Vol. 760 (pp 30-39) RIS download Bibtex download
  • Berghammer R & Struth G (2010) On Automated Program Construction and Verification.. MPC, Vol. 6120 (pp 22-41) RIS download Bibtex download
  • Desharnais J, Jipsen P & Struth G (2009) Domain and Antidomain Semigroups. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, Vol. 5827 (pp 73-87) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • Hoare CART, Moller B, Struth G & Wehrman I (2009) Concurrent Kleene Algebra. CONCUR 2009 - CONCURRENCY THEORY, PROCEEDINGS, Vol. 5710 (pp 399-414) RIS download Bibtex download
  • Struth G (2008) Modal Tools for Separation and Refinement.. Electron. Notes Theor. Comput. Sci., Vol. 214 (pp 81-101) RIS download Bibtex download
  • Höfner P & Struth G (2008) Can Refinement be Automated?. Electron. Notes Theor. Comput. Sci., Vol. 201 (pp 197-222) RIS download Bibtex download
  • (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 RIS download Bibtex download
  • Desharnais J & Struth G (2008) Domain axioms for a family of near-semirings. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 5140 (pp 330-345) RIS download Bibtex download
  • Hofner P & Struth G (2008) On automating the calculus of relations. AUTOMATED REASONING, PROCEEDINGS, Vol. 5195 (pp 50-66) RIS download Bibtex download
  • Desharnais J & Struth G (2008) Modal semirings revisited. MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, Vol. 5133 (pp 360-387) RIS download Bibtex download
  • Hofner P & Struth G (2008) Non-termination in idempotent semirings. RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, Vol. 4988 (pp 206-220) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • Hofner P & Struth G (2007) Automated reasoning in kleene algebra. Automated Deduction - CADE-21, Proceedings, Vol. 4603 (pp 279-294) RIS download Bibtex download
  • Moller B & Struth G (2006) Algebras of modal operators and partial correctness. THEORETICAL COMPUTER SCIENCE, Vol. 351(2) (pp 221-239) RIS download Bibtex download
  • Moller B, Hofner P & Struth G (2006) Quantales and temporal logics. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 263-277) RIS download Bibtex download
  • Struth G (2006) Tableaux for lattices. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 323-337) RIS download Bibtex download
  • Struth G (2006) Constructing rewrite-based decision procedures for embeddings and termination. MATHEMATICS OF PROGRAM CONSTRUCTION, Vol. 4014 (pp 416-432) RIS download Bibtex download
  • Moller B & Struth G (2006) wp Is wlp. RELATIONAL METHODS IN COMPUTER SCIENCE, 2005, Vol. 3929 (pp 200-211) RIS download Bibtex download
  • Struth G (2006) Knuth-Bendix completion as a data structure. RELATIONAL METHODS IN COMPUTER SCIENCE, 2005, Vol. 3929 (pp 225-236) RIS download Bibtex download
  • Ebert M & Struth G (2005) Diagram Chase in Relational System Development.. Electron. Notes Theor. Comput. Sci., Vol. 127 (pp 87-105) RIS download Bibtex download
  • Möller B & Struth G (2005) p Is.. RelMiCS, Vol. 3929 (pp 200-211) RIS download Bibtex download
  • (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 RIS download Bibtex download
  • Desharnais J, Moller B & Struth G (2004) Termination in modal Kleene algebra. EXPLORING NEW FRONTIERS OF THEORETICAL INFORMATICS, Vol. 155 (pp 647-660) RIS download Bibtex download
  • Moller B & Struth G (2004) Modal Kleene algebra and partial correctness. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, Vol. 3116 (pp 379-393) RIS download Bibtex download
  • Struth G (2004) Automated element-wise reasoning with sets. PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS (pp 320-329) RIS download Bibtex download
  • Ehm T, Moller B & Struth G (2003) Kleene modules. RELATIONAL AND KLEENE-ALGEBRAIC METHODS IN COMPUTER SCIENCE, Vol. 3051 (pp 112-123) RIS download Bibtex download
  • 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) RIS download Bibtex download
  • Struth G (2003) A calculus for set-based program development. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Vol. 2885 (pp 541-559) RIS download Bibtex download
  • Struth G (2002) Deriving focused lattice calculi. REWRITING TECHNIQUES AND APPLICATIONS, Vol. 2378 (pp 83-97) RIS download Bibtex download
  • Struth G (2002) Calculating Church-Rosser proofs in Kleene algebra. RELATIONAL METHODS IN COMPUTER SCIENCE, Vol. 2561 (pp 276-290) RIS download Bibtex download
  • Struth G (2001) Knuth-Bendix Completion for Non-Symmetric Transitive Relations.. Electron. Notes Theor. Comput. Sci., Vol. 59 (pp 341-357) RIS download Bibtex download
  • Struth G (2001) Deriving Focused Calculi for Transitive Relations.. RTA, Vol. 2051 (pp 291-305) RIS download Bibtex download
  • Struth G (2000) An algebra of resolution. REWRITING TECHNIQUES AND APPLICATIONS, PROCEEDINGS, Vol. 1833 (pp 214-228) RIS download Bibtex download
  • Struth G (1997) On the word problem for free lattices. REWRITING TECHNIQUES AND APPLICATIONS, Vol. 1232 (pp 128-141) RIS download Bibtex download
Grants

Current Grants

  • Verifiably Correct Transactional Memory, EPSRC, 10/2018 to 09/2021, £397,680, as co-PI
  • Verifying concurrent algorithms on Weak Memory Models, EPSRC, 05/2015 to 11/2018, £389,207, as Co-PI

Previous Grants

  • Midlands Graduate School in the Foundations of Computing Science 2010, EPSRC, 03/2010 to 03/2011, £4,704, as PI
  • Verifying Concurrent Lock-free Algorithms, EPSRC, 04/2012 to 10/2015, £378,907, as Co-PI
  • 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