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 firstorder theorem proving, firstorder 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 designtime verification of complex systems
 Dynamic systems verification at designtime and at runtime based on temporal logic
 Automated theorem proving as backend reasoners embedded in verification tools
A neighboring project develops the Goanna bugfinding tool.
Latest News
 Paper: Peter Baumgartner, Josh Bax and Uwe Waldmann. Beagle  A Hierarchic Superposition Theorem Prover, presented at at CADE25. Also available are the slides of the talk. [7/8/2015]
 Paper: Peter Baumgartner. SMTtoTPTP  A Converter for Theorem Proving Formats, presented at at CADE25. 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 CADE25 [28/4/2015]
 Paper: Peter Baumgartner. SMTtoTPTP  A Converter for Theorem Proving Formats, accepted at CADE25 [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 PAAR2014 workshop [19/5/2014]
 Paper: Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish. Beagle as a HOL4 external ATP method. Accepted at PAAR2014 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 LPAR19 [15/12/2013]
 Paper: Peter Baumgartner and Uwe Waldmann. Hierarchic Superposition: Completeness without Compactness presented at MACIS2013 [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 firstorder 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 DataCentric Processes published in Proceedings TABLEAUX 2013. [16/9/2013]
 Paper: Peter Baumgartner and Uwe Waldmann. Hierarchic Superposition With Weak Abstraction published in Proceedings CADE24. [10/6/2013]
 Paper: Michael Norrish and Brian Huffmann. "Ordinals in HOL: Transfinite Arithmetic up to (and beyond) ω1". To appear in Proceedings of 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 quantifierfree logic, we emphasize the role of firstorder logic for supporting more faithful system modelling. Development of automated theorem proving methods for fragments of CTL* over firstorder logic modulo background theories, the Fitzroy system.
 Developing runtime verification methods over firstorder logic
 Applications: business rules and process verification, Android security, analysing models from the NICTA Security Architecture project
 Automated theorem proving
We focus on methods and tools for automated theorem proving in firstorder 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 backend reasoners for interactive theorem proving and for dynamic systems verification
People
Past

Publications

Peter Baumgartner SMTtoTPTP  a converter for theorem proving formats International Conference on Automated Deduction, pp. 285294, Berlin, Germany, August, 2015  
Peter Baumgartner, Joshua Bax and Uwe Waldmann Beagle  a hierarchic superposition theorem prover International Conference on Automated Deduction, pp. 367377, Berlin, Germany, August, 2015  
Peter Baumgartner, Joshua Bax and Uwe Waldmann Finite quantification in hierarchic theorem proving International Joint Conference on Automated Reasoning (IJCAR), pp. 152167, Vienna, Austria, July, 2014  
Aditi Barthwal and Michael Norrish A mechanisation of some contextfree language theory in HOL4 Journal of Computer and System Sciences, Volume 80, Number 2, pp. 346–362, March, 2014  
Peter Baumgartner Model evolution based theorem proving IEEE Intelligent Systems Magazine (IEEE ISM), Volume 29, Number 1, pp. 410, February, 2014  

Peter Baumgartner and Uwe Waldmann Hierarchic superposition with weak abstraction and the beagle theorem prover Deduction and Arithmetic (Dagstuhl Seminar 13411), pp. 7, Dagstuhl, Germany,, February, 2014  
Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens CakeML: A verified implementation of ML ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014  
Peter Baumgartner Automatische inferenz Handbuch der Kuenstlichen Intelligenz, pp. 129167, Oldenbourg Verlag, 2013  
Peter Baumgartner and Joshua Bax Proving infinite satisfiability Logic Programming and Automated Reasoning (LPAR), pp. 8695, Stellenbosch, South Africa, December, 2013  
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  
Peter Baumgartner and Uwe Waldmann Hierarchic superposition: Completeness without compactness Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2013), pp. 812, Nanning, China, November, 2013  
Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish Tableaux for verification of datacentric processes Automated Reasoning with Analytic Tableaux and Related Methods, pp. 2843, Nancy, France, September, 2013  
Andreas Bauer, JanChristoph Kuester and Gil Vegliach From propositional to firstorder monitoring 4th International Conference on Runtime Verification (RV), Rennes, France, September, 2013  

Michael Norrish and Brian Huffman Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁ International Conference on Interactive Theorem Proving, pp. 133146, Rennes, France, July, 2013  
Peter Baumgartner and Uwe Waldmann Hierarchic superposition with weak abstraction Conference on Automated Deduction, pp. 3957, Lake Placid, New York, USA, June, 2013  
HingLun Chan and Michael Norrish A string of pearls: Proofs of fermat’s little theorem International Conference on Certified Programs and Proofs, pp. 188207, Kyoto, Japan, October, 2012  
Peter Baumgartner, Bjoern Pelzer and Cesare Tinelli Model evolution with equality  revised and implemented Journal of Symbolic Computation, Volume 47, Number 9, pp. 10111045, September, 2012  
Andreas Bauer and Ylies Falcone Decentralised LTL monitoring International Symposium on Formal Methods (FM), pp. 88100, Paris/France, August, 2012 Best Paper Award!  
Andreas Bauer, JanChristoph Kuester and Gil Vegliach Runtime verification meets android security 4th NASA Formal Methods Symposium (NFM), pp. 174180, Norfolk, Virginia, USA, April, 2012  
Geoff Sutcliffe, Stephan Schulz, Koen Claessen and Peter Baumgartner The TPTP typed firstorder form and arithmetic The 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR18), pp. 406419, Merida, Venezuela, March, 2012  
Peter Baumgartner and Uwe Waldmann A combined superposition and model evolution calculus Journal of Automated Reasoning, Volume 47, Number 2, pp. 191227, August, 2011  

Michael Norrish Mechanised computability theory International Conference on Interactive Theorem Proving, pp. 297–311, Nijmegen, The Netherlands, August, 2011  
Andreas Bauer and Martin Leucker The theory and practice of SALT NASA Formal Methods Symposium (NFM), pp. 28, Pasadena, CA, USA, April, 2011  
Andreas Bauer, Martin Leucker and Christian Schallhart Runtime verification for LTL and TLTL ACM Transactions on Software Engineering and Methodology, Volume 20, Number 4, pp. 75, April, 2011  
Peter Baumgartner and Cesare Tinelli Model evolution with equality modulo builtin theories International Conference on Automated Deduction, pp. 85100, Wroclaw, Poland, April, 2011  
Aditi Barthwal and Michael Norrish A formalisation of the normal forms of contextfree grammars in HOL4 19th EACSL Annual Conferences on Computer Science Logic, pp. 95109, Brno, Czech Republic, August, 2010  
Andreas Bauer and Patrik Haslum LTL goal specifications revisited European Conference on Artificial Intelligence, Lisbon, Portugal, August, 2010  

Ramana Kumar and Michael Norrish (nominal) unification by recursive descent with triangular substitutions International Conference on Interactive Theorem Proving, pp. 5166, Edinburgh, United Kingdom, July, 2010  
Andreas Bauer, Martin Leucker and Christian Schallhart Comparing LTL semantics for runtime verification Journal of Logic and Computation, Volume 20, Number 3, pp. 651674, June, 2010  
Peter Baumgartner and Evgenij Thorstensen Instance based methods  an overview Künstliche Intelligenz, Volume 24, Number 1, pp. 3542, April, 2010  
Andreas Bauer, Martin Leucker, Christian Schallhart and Michael Tautschnig Don't care in SMT  building flexible yet efficient abstraction/refinement solvers International Journal on Software Tools for Technology Transfer (STTT, Springer), Volume 12, Number 1, pp. 2337, February, 2010  
Peter Baumgartner, Ulrich Furbach and Bjoern Pelzer The hyper tableaux calculus with equality and an application to finite model computation Journal of Logic and Computation, Volume 20, Number 1, pp. 77101, February, 2010  
Franz Baader, Andreas Bauer and Alwen Tiu Matching trace patterns with regular policies 3rd International Conference on Language and Automata Theory and Applications (LATA), pp. 105116, Spain, November, 2009  
Franz Baader, Andreas Bauer, Peter Baumgartner, Anne Cregan, Alfredo Gabaldon, Krystian Ji, Kevin Lee, David Rajaratnam and Rolf Schwitter A novel architecture for situation awareness systems TABLEAUX 2009  The 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp. 7792, Oslo, Norway, July, 2009  
Peter Baumgartner and John Slaney Constraint modelling: A challenge for first order automated reasoning International Workshop on FirstOrder Theorem Proving (FTP'09), pp. 418, Oslo, Norway, July, 2009  
Peter Baumgartner and Uwe Waldmann Superposition and model evolution combined Automated Deduction  CADE22, pp. 1734, Montreal, Canada, July, 2009  
Peter Baumgartner, Alexander Fuchs, Hans de Nivelle and Cesare Tinelli Computing finite models by reduction to functionfree clause logic Journal of Applied Logic, Volume 7, Number 1, pp. 5874, January, 2009  
Peter Baumgartner, Alexander Fuchs and Cesare Tinelli ME(LIA)  model evolution with linear integer arithmetic constraints LPAR 2008, pp. 258273, Doha, Qatar, November, 2008  
Peter Baumgartner, Alessandro Armando and Gilles Dowek Automated reasoning  4th international conference, IJCAR 2008 Volume 5195 in Lecture Notes in Artificial Intelligence, Springer, 2008  
Konrad Slind and Michael Norrish A brief overview of HOL4 International Conference on Theorem Proving in Higher Order Logics, pp. 2832, 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  
Peter Baumgartner and Cesare Tinelli The model evolution calculus as a firstorder DPLL method Artificial Intelligence, Volume 172, Number 45, pp. 591632, January, 2008  
Peter Baumgartner Logical engineering with instancebased methods CADE21  The 21st International Conference on Automated Deduction, pp. 404409, July, 2007  
Peter Baumgartner, Ulrich Furbach and Bjoern Pelzer Hyper tableaux with equality CADE21 – The 21st International Conference on Automated Deduction, pp. 492507, Bremen, Germany, July, 2007  
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough Engineering with logic: HOL specification and symbolicevaluation testing for TCP implementations ACM SIGPLANSIGACT 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. 7186, Rome, September, 2003 