Automated Reasoning

The Automated Reasoning activity is part of the Trustworthy Systems.

Aim

The aim of this activitiy is to provide and further develop general automated and interactive reasoning tools for sofware verification. As opposed to specific automation activities in the Trustworthy Systems project, such as File System Verification, Binary Verification, or Automated C Code Abstraction, this activity has a more general scope, looking at fundamental automated reasoning techniques such as automated first-order theorem proving, first-order model checking, and development on the interactive theorem prover HOL4.

Approach

In order to support a wide spectrum of verification tasks and application areas, our research covers a variety of methods:

• Interactive theorem proving for design-time verification of complex systems
• Dynamic systems verification at design-time and at runtime based on temporal logic
• Automated theorem proving as back-end reasoners embedded in verification tools

A neighboring project develops the Goanna bug-finding tool.

Latest News

• Paper: Peter Baumgartner, Josh Bax and Uwe Waldmann. Beagle - A Hierarchic Superposition Theorem Prover, presented at at CADE-25. Also available are the slides of the talk. [7/8/2015]
• Paper: Peter Baumgartner. SMTtoTPTP - A Converter for Theorem Proving Formats, presented at at CADE-25. Also available are the slides of the talk. [7/8/2015]
• Paper: Peter Baumgartner, Josh Bax and Uwe Waldmann. Beagle - A Hierarchic Superposition Theorem Prover, accepted at CADE-25 [28/4/2015]
• Paper: Peter Baumgartner. SMTtoTPTP - A Converter for Theorem Proving Formats, accepted at CADE-25 [28/4/2015]
• Beagle and SMTtoTPTP are now hosted at Bitbucket, see here for beagle and here for SMTtoTPTP [12/2/2015]
• Award: The Beagle theorem prover received a 'best improved system' award at the automated theorem prover world championship held in conjunction with IJCAR 2014. Beagle scored third, in a very close run. [22/7/2014]
• Paper: Peter Baumgartner. Model Evolution Based Theorem Proving, published in IEEE Intelligent Systems [21/5/2014]
• Paper: Joshua Bax. A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories. Accepted at PAAR-2014 workshop [19/5/2014]
• Paper: Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish. Beagle as a HOL4 external ATP method. Accepted at PAAR-2014 workshop [19/5/2014]
• Paper: Peter Baumgartner, Joshua Bax and Uwe Waldmann. Finite Quantification in Hierarchic Theorem Proving. Accepted at IJCAR 2014 [10/4/2014]
• Paper: Peter Baumgartner and Joshua Bax. Proving Infinite Satisfiability published in Proceedings LPAR-19 [15/12/2013]
• Paper: Peter Baumgartner and Uwe Waldmann. Hierarchic Superposition: Completeness without Compactness presented at MACIS-2013 [13/12/2013]
• Book Chapter: Peter Baumgartner. Automatische Inferenz published in Handbuch der Künstlichen Intelligenz.
  This ‘Handbook of Artificial Intelligence’ is now in its 5 German edition and is widely used for teaching at German speaking universities. The chapter provides an introductory survey of modern methods for automated reasoning in propositional and first-order logic. [1/12/2013]
• Paper: Peter Baumgartner. Model Evolution Based Theorem Proving, IEEE online preprint available [22/11/2013]
• Event: Peter attends a Dagstuhl Seminar on Deduction and Arithmetic and gave a talk on Hierarchic superposition with weak abstraction and the Beagle theorem prover [7/10/2013]
• Software release: The Beagle theorem prover and the accompanying problem format translator SMTtoTPTP [September 2013]
• Paper: Andreas Bauer, Peter Baumgartner, Martin Diller and Michael Norrish. Tableaux for Verification of Data-Centric Processes published in Proceedings TABLEAUX 2013. [16/9/2013]
• Paper: Peter Baumgartner and Uwe Waldmann. Hierarchic Superposition With Weak Abstraction published in Proceedings CADE-24. [10/6/2013]
• Paper: Michael Norrish and Brian Huffmann. Ordinals in HOL: Transfinite Arithmetic up to (and beyond) ω1 ITP 2013

Technical Research Challenges

• Interactive Theorem Proving
  We are developing the HOL4 interactive theorem prover.
  • Better linkage between HOL4 proofs, theories and tools, and the Isabelle/HOL infrastructure.
  • Further improve and maintain our automatic translation from C to Isabelle/HOL
  • Automatically abstract the semantics of C code to higher abstraction levels
• Dynamic systems verification
  In contrast to most mainstream approaches, which are grounded in propositional or quantifier-free logic, we emphasize the role of first-order logic for supporting more faithful system modelling.
  • Development of automated theorem proving methods for fragments of CTL* over first-order logic modulo background theories, the Fitzroy system.
  • Developing runtime verification methods over first-order logic
  • Applications: business rules and process verification, Android security, analysing models from the Security Architecture project
• Automated theorem proving
  We focus on methods and tools for automated theorem proving in first-order logic modulo background theories (such as integer arithmetic).
  • Providing better alternatives to SMT solvers to reason with quantified formulas
  • Calculi and implemented systems, in particular based on Model Evolution and Superposition calculi (the Beagle theorem prover); see here for implemented systems.
  • Embedding automated theorem provers as back-end reasoners for interactive theorem proving and for dynamic systems verification

People

Publications

		Aditi Barthwal and Michael Norrish A mechanisation of some context-free language theory in HOL4 Journal of Computer and System Sciences, Volume 80, Number 2, pp. 346–362, March, 2014
		Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens CakeML: A verified implementation of ML ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014
		Joseph Chan and Michael Norrish A string of pearls: Proofs of fermat's little theorem Journal of Formal Reasoning, Volume 6, Number 1, pp. 63–87, December, 2013
		Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish Tableaux for verification of data-centric processes Automated Reasoning with Analytic Tableaux and Related Methods, pp. 28–43, Nancy, France, September, 2013
		Michael Norrish and Brian Huffman Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$ International Conference on Interactive Theorem Proving, pp. 133–146, Rennes, France, July, 2013
		Hing-Lun Chan and Michael Norrish A string of pearls: Proofs of fermat’s little theorem International Conference on Certified Programs and Proofs, pp. 188–207, Kyoto, Japan, October, 2012
		Michael Norrish Mechanised computability theory International Conference on Interactive Theorem Proving, pp. 297—311, Nijmegen, The Netherlands, August, 2011
		Aditi Barthwal and Michael Norrish A formalisation of the normal forms of context-free grammars in HOL4 19th EACSL Annual Conferences on Computer Science Logic, pp. 95–109, Brno, Czech Republic, August, 2010
		Ramana Kumar and Michael Norrish (nominal) unification by recursive descent with triangular substitutions International Conference on Interactive Theorem Proving, pp. 51–66, Edinburgh, United Kingdom, July, 2010
		Konrad Slind and Michael Norrish A brief overview of HOL4 International Conference on Theorem Proving in Higher Order Logics, pp. 28–32, Montréal, Canada, August, 2008
		Tom Ridge, Michael Norrish and Peter Sewell A rigorous approach to networking: TCP, from implementation to protocol to service International Symposium on Formal Methods (FM), pp. 294—309, Turku, Finland, May, 2008
		Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 55—66, Charleston, South Carolina, USA, January, 2006
		Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets ACM Conference on Communications, pp. 265–276, Philadelphia, August, 2005
		Michael Norrish Complete integer decision procedures as derived rules in HOL International Conference on Theorem Proving in Higher Order Logics, pp. 71–86, Rome, September, 2003