Professor Georg Struth

PhD

Department of Computer Science

Professor of Theoretical Computer Science

Head of the Verification research group

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

Regent Court (DCS)

Full contact details

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

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

Journal articles

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 (2017) Hoare Semigroups. Mathematical Structures in Computer Science. 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.
Armstrong A, Foster S & Struth G (2011) Dependently Typed Programming based on Automated Theorem Proving. CoRR, abs/1112.3833.
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.
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.
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.
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. View this article in WRRO
Hoare T, Möller B, Struth G & Wehrman I (2011) Concurrent Kleene Algebra and its Foundations. Journal of Logic and Algebraic Programming.
Desharnais J & Struth G (2011) Internal axioms for domain semirings. Science of Computer Programming, 76(3), 181-203.
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. View this article in WRRO
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.
McIver A, Rabehaja T & Struth G () Probabilistic Concurrent Kleene Algebra. Electronic Proceedings in Theoretical Computer Science, 117, 97-115.
Jules D, Moeller B & Georg S () Algebraic Notions of Termination. Logical Methods in Computer Science, Volume 7, Issue 1 (February 11, 2011) lmcs:777.

Chapters

Rabehaja T, McIver A, Morgan C & Struth G (2019) Categorical Information Flow, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy (pp. 329-343). Springer International Publishing
Hoare T, Struth G & Woodcock J (2019) A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic, Unifying Theories of Programming (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).
Höfner P & Struth G () Non-termination in Idempotent Semirings, Relations and Kleene Algebra in Computer Science (pp. 206-220). Springer Berlin Heidelberg
Jipsen P & Struth G () The Structure of the One-Generated Free Domain Semiring, Relations and Kleene Algebra in Computer Science (pp. 234-242). Springer Berlin Heidelberg

Conference proceedings papers

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. Leibniz International Proceedings in Informatics, LIPIcs, Vol. 85, 5 September 2017 - 8 September 2017. View this article in WRRO
(2017) Relational and Algebraic Methods in Computer Science
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
McIver A, Rabehaja T & Struth G (2016) Schedulers and Finishers: On Generating the Behaviours of an Event Structure (pp 121-138)
Gomes VBF & Struth G (2016) Modal Kleene Algebra Applied to Program Correctness (pp 310-325)
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)
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)
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 (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)
Struth G (2008) Modal Tools for Separation and Refinement.. Electron. Notes Theor. Comput. Sci., Vol. 214 (pp 81-101)
Höfner P & Struth G (2008) Can Refinement be Automated?. Electron. Notes Theor. Comput. Sci., Vol. 201 (pp 197-222)
(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
Desharnais J & Struth G (2008) Domain axioms for a family of near-semirings. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 5140 (pp 330-345)
Hofner P & Struth G (2008) On automating the calculus of relations. AUTOMATED REASONING, PROCEEDINGS, Vol. 5195 (pp 50-66)
Desharnais J & Struth G (2008) Modal semirings revisited. MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, Vol. 5133 (pp 360-387)
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)
Hofner P & Struth G (2007) Automated reasoning in kleene algebra. Automated Deduction - CADE-21, Proceedings, Vol. 4603 (pp 279-294)
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)
Struth G (2006) Knuth-Bendix completion as a data structure. RELATIONAL METHODS IN COMPUTER SCIENCE, 2005, Vol. 3929 (pp 225-236)
Ebert M & Struth G (2005) Diagram Chase in Relational System Development.. Electron. Notes Theor. Comput. Sci., Vol. 127 (pp 87-105)
Möller B & Struth G (2005) p Is.. RelMiCS, Vol. 3929 (pp 200-211)
(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)
Struth G (2004) Automated element-wise reasoning with sets. PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS (pp 320-329)
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) Deriving focused lattice calculi. REWRITING TECHNIQUES AND APPLICATIONS, Vol. 2378 (pp 83-97)
Struth G (2002) Calculating Church-Rosser proofs in Kleene algebra. RELATIONAL METHODS IN COMPUTER SCIENCE, Vol. 2561 (pp 276-290)
Struth G (2001) Knuth-Bendix Completion for Non-Symmetric Transitive Relations.. Electron. Notes Theor. Comput. Sci., 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)

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: Head of the Verification research group