Skip to main content

Automated Reasoning

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.

VTA

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

Technical Research Challenges

  • Interactive Theorem Proving
    We are developing the HOL4 interactive theorem prover. Contact: Michael Norrish, michael.norrish<at>nicta.com.au

  • Dynamic systems verification Fitzroy
    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 NICTA Security Architecture project
    Contact: Peter Baumgartner, peter.baumgartner<at>nicta.com.au

  • 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
    Contact: Peter Baumgartner, peter.baumgartner<at>nicta.com.au

People

Past

  • Andreas Bauer
  • Jan-Christoph Kuester
  • Joshua Bax
  • Michael Norrish
  • Peter Baumgartner

Publications

Abstract PDF Peter Baumgartner
SMTtoTPTP - a converter for theorem proving formats
International Conference on Automated Deduction, pp. 285-294, Berlin, Germany, August, 2015
Abstract PDF Peter Baumgartner, Joshua Bax and Uwe Waldmann
Beagle - a hierarchic superposition theorem prover
International Conference on Automated Deduction, pp. 367-377, Berlin, Germany, August, 2015
Abstract PDF Peter Baumgartner, Joshua Bax and Uwe Waldmann
Finite quantification in hierarchic theorem proving
International Joint Conference on Automated Reasoning (IJCAR), pp. 152-167, Vienna, Austria, July, 2014
Abstract PDF 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
Abstract PDF Peter Baumgartner
Model evolution based theorem proving
IEEE Intelligent Systems Magazine (IEEE ISM), Volume 29, Number 1, pp. 4-10, February, 2014
Abstract PDF 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
Abstract PDF 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
Abstract to be published Peter Baumgartner
Automatische inferenz
Handbuch der Kuenstlichen Intelligenz, pp. 129-167, Oldenbourg Verlag, 2013
Abstract PDF Peter Baumgartner and Joshua Bax
Proving infinite satisfiability
Logic Programming and Automated Reasoning (LPAR), pp. 86-95, Stellenbosch, South Africa, December, 2013
Abstract PDF 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
Abstract PDF Peter Baumgartner and Uwe Waldmann
Hierarchic superposition: Completeness without compactness
Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2013), pp. 8-12, Nanning, China, November, 2013
Abstract PDF 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
Abstract PDF Andreas Bauer, Jan-Christoph Kuester and Gil Vegliach
From propositional to first-order monitoring
4th International Conference on Runtime Verification (RV), Rennes, France, September, 2013
Abstract PDF Michael Norrish and Brian Huffman
Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁
International Conference on Interactive Theorem Proving, pp. 133-146, Rennes, France, July, 2013
Abstract PDF Peter Baumgartner and Uwe Waldmann
Hierarchic superposition with weak abstraction
Conference on Automated Deduction, pp. 39-57, Lake Placid, New York, USA, June, 2013
Abstract PDF 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
Abstract PDF Peter Baumgartner, Bjoern Pelzer and Cesare Tinelli
Model evolution with equality - revised and implemented
Journal of Symbolic Computation, Volume 47, Number 9, pp. 1011-1045, September, 2012
Abstract PDF Andreas Bauer and Ylies Falcone
Decentralised LTL monitoring
International Symposium on Formal Methods (FM), pp. 88-100, Paris/France, August, 2012
Best Paper Award!
Abstract PDF Andreas Bauer, Jan-Christoph Kuester and Gil Vegliach
Runtime verification meets android security
4th NASA Formal Methods Symposium (NFM), pp. 174-180, Norfolk, Virginia, USA, April, 2012
Abstract PDF Geoff Sutcliffe, Stephan Schulz, Koen Claessen and Peter Baumgartner
The TPTP typed first-order form and arithmetic
The 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-18), pp. 406-419, Merida, Venezuela, March, 2012
Abstract PDF Peter Baumgartner and Uwe Waldmann
A combined superposition and model evolution calculus
Journal of Automated Reasoning, Volume 47, Number 2, pp. 191-227, August, 2011
Abstract PDF Michael Norrish
Mechanised computability theory
International Conference on Interactive Theorem Proving, pp. 297–311, Nijmegen, The Netherlands, August, 2011
Abstract PDF Andreas Bauer and Martin Leucker
The theory and practice of SALT
NASA Formal Methods Symposium (NFM), pp. 28, Pasadena, CA, USA, April, 2011
Abstract PDF 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
Abstract PDF Peter Baumgartner and Cesare Tinelli
Model evolution with equality modulo built-in theories
International Conference on Automated Deduction, pp. 85-100, Wroclaw, Poland, April, 2011
Abstract PDF 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
Abstract PDF Andreas Bauer and Patrik Haslum
LTL goal specifications revisited
European Conference on Artificial Intelligence, Lisbon, Portugal, August, 2010
Abstract PDF 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
Abstract PDF Andreas Bauer, Martin Leucker and Christian Schallhart
Comparing LTL semantics for runtime verification
Journal of Logic and Computation, Volume 20, Number 3, pp. 651-674, June, 2010
Abstract PDF Peter Baumgartner and Evgenij Thorstensen
Instance based methods - an overview
Künstliche Intelligenz, Volume 24, Number 1, pp. 35-42, April, 2010
Abstract PDF 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. 23-37, February, 2010
Abstract file not found 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. 77-101, February, 2010
Abstract PDF 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. 105-116, Spain, November, 2009
Abstract PDF 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. 77-92, Oslo, Norway, July, 2009
Abstract PDF Peter Baumgartner and John Slaney
Constraint modelling: A challenge for first order automated reasoning
International Workshop on First-Order Theorem Proving (FTP'09), pp. 4-18, Oslo, Norway, July, 2009
Abstract PDF Peter Baumgartner and Uwe Waldmann
Superposition and model evolution combined
Automated Deduction - CADE-22, pp. 17-34, Montreal, Canada, July, 2009
Abstract file not found Peter Baumgartner, Alexander Fuchs, Hans de Nivelle and Cesare Tinelli
Computing finite models by reduction to function-free clause logic
Journal of Applied Logic, Volume 7, Number 1, pp. 58-74, January, 2009
Abstract PDF Peter Baumgartner, Alexander Fuchs and Cesare Tinelli
ME(LIA) - model evolution with linear integer arithmetic constraints
LPAR 2008, pp. 258-273, Doha, Qatar, November, 2008
Abstract PDF Peter Baumgartner, Alessandro Armando and Gilles Dowek
Automated reasoning - 4th international conference, IJCAR 2008
Volume 5195 in Lecture Notes in Artificial Intelligence, Springer, 2008
Abstract PDF 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
Abstract PDF 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
Abstract file not found Peter Baumgartner and Cesare Tinelli
The model evolution calculus as a first-order DPLL method
Artificial Intelligence, Volume 172, Number 4-5, pp. 591-632, January, 2008
Abstract file not found Peter Baumgartner
Logical engineering with instance-based methods
CADE-21 - The 21st International Conference on Automated Deduction, pp. 404-409, July, 2007
Abstract file not found Peter Baumgartner, Ulrich Furbach and Bjoern Pelzer
Hyper tableaux with equality
CADE-21 – The 21st International Conference on Automated Deduction, pp. 492-507, Bremen, Germany, July, 2007
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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