Professor Georg Struth
PhD
Department of Computer Science
Professor of Theoretical Computer Science
Head of the Verification research group
+44 114 222 1846
Full contact details
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
- Modelling Computing Systems. Springer London.
- Preface. Elsevier.
Journal articles
- Relational and algebraic methods in computer science. Journal of Logical and Algebraic Methods in Programming, 106, 198-199.
- Schedulers and finishers: On generating and filtering the behaviours of an event structure. Theoretical Computer Science, 744, 97-112.
- 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, 84-101.
- Probabilistic rely-guarantee calculus. Theoretical Computer Science, 655, 120-134.
- Taming Multirelations. ACM Transactions on Computational Logic, 17(4), 1-34.
- Developments in concurrent Kleene algebra. Journal of Logical and Algebraic Methods in Programming, 85(4), 617-636.
- Building program construction and verification tools from algebraic principles. Formal Aspects of Computing, 28(2), 265-293.
- 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), 284-288.
- Concurrent Dynamic Algebra. ACM Transactions on Computational Logic, 16(4), 1-38.
- Completeness results for omega-regular algebras. Journal of Logical and Algebraic Methods in Programming, 84(3), 402-425.
- On the Fine-Structure of Regular Algebra. Journal of Automated Reasoning, 54(2), 165-197.
- Programming and automating mathematics in the Tarski–Kleene hierarchy. Journal of Logical and Algebraic Methods in Programming, 83(2), 87-102.
- Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools, 78-93.
- 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.
- Left omega algebras and regular equations. Journal of Logic and Algebraic Programming, 81(6), 705-717.
- 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.
- 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.
- 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.
- 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.
- 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.
- Concurrent Kleene Algebra and its Foundations. Journal of Logic and Algebraic Programming, 80(6), 266-296.
- 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.
- 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
- Internal axioms for domain semirings. Science of Computer Programming, 76(3), 181-203.
- Relations and Kleene algebras in computer science. J LOGIC ALGEBR PROGR, 79(8), 705-706.
- Algebraic notions of nontermination: Omega and divergence in idempotent semirings. J LOGIC ALGEBR PROGR, 79(8), 794-811.
- Automated verification of refinement laws. ANN MATH ARTIF INTEL, 55(1-2), 35-62. View this article in WRRO
- Relations and Kleene algebras in computer science. J LOGIC ALGEBR PROGR, 76(1), 1-2.
- Abstract abstract reduction. J LOGIC ALGEBR PROGR, 66(2), 239-270.
- Probabilistic Concurrent Kleene Algebra. Electronic Proceedings in Theoretical Computer Science, 117, 97-115.
- 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. 329-343). Springer International Publishing
- A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic, Unifying Theories of Programming (pp. 3-21). Springer International Publishing
- Cylindric Kleene Lattices for Program Construction, Lecture Notes in Computer Science (pp. 197-225). Springer International Publishing
- Non-termination in Idempotent Semirings, Relations and Kleene Algebra in Computer Science (pp. 206-220). Springer Berlin Heidelberg
- 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
- Generating Posets Beyond N (pp 82-99)
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL (pp 169-186)
- Verifying Hybrid Systems with Modal Kleene Algebra (pp 225-243)
- 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 1-25) View this article in WRRO
- Schedulers and Finishers: On Generating the Behaviours of an Event Structure (pp 121-138)
- Modal Kleene Algebra Applied to Program Correctness (pp 310-325)
- Relational Formalisations of Compositions and Liftings of Multirelations (pp 84-100)
- A Program Construction and Verification Tool for Separation Logic (pp 137-158)
- 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)
- 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)
- Lightweight Program Construction and Verification Tools in Isabelle/HOL (pp 5-19)
- 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)
- 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)
- Preface (pp ix-x)
- 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)
- 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)
- 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.
- Algebras of modal operators and partial correctness. THEORETICAL COMPUTER SCIENCE, Vol. 351(2) (pp 221-239)
- Modelling Computing Systems. Springer London.
- 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