Automatic Proof Procedures for Polynomials and Special Functions
Lead Research Organisation:
University of Edinburgh
Department Name: Sch of Informatics
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
People |
ORCID iD |
| Paul Jackson (Principal Investigator) |
Publications
Benzmüller C
(2015)
The Higher-Order Prover Leo-II.
in Journal of automated reasoning
Bridge J
(2012)
Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions
in Journal of Automated Reasoning
Bridge J
(2014)
Machine Learning for First-Order Theorem Proving Learning to Select a Good Heuristic
in Journal of Automated Reasoning
De Moura L
(2013)
Automated Reasoning and Mathematics
Ghorbal K
(2014)
Static Analysis
Ghorbal K
(2017)
A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
in Computer Languages, Systems & Structures
Ghorbal K
(2015)
Verification, Model Checking, and Abstract Interpretation
Huang Zongyan
(2015)
Machine learning and computer algebra
Imtiaz Q
(2022)
CuO-based materials for thermochemical redox cycles: the influence of the formation of a CuO percolation network on oxygen release and oxidation kinetics.
in Discover chemical engineering
Jackson P
(2014)
NASA Formal Methods
Li W
(2017)
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
in Journal of Automated Reasoning
Mitsch S
(2014)
Collaborative Verification-Driven Engineering of Hybrid Systems
in Mathematics in Computer Science
Mitsch, S
(2014)
A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems
in Proceedings of Enabling Domain Experts to use Formalised Reasoning - Symposium AISB, Do-Form
Passmore G
(2012)
Intelligent Computer Mathematics
Passmore G
(2012)
How the World Computes
Sogokon A
(2018)
Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants
in Journal of Automated Reasoning
Sogokon A
(2017)
Operational Models for Piecewise-Smooth Systems
in ACM Transactions on Embedded Computing Systems
Sogokon A
(2017)
NASA Formal Methods
| Description | We made major advances in the power of our theorem prover tool MetiTarski for reasoning about problems involving transcendental functions. These advances included optimising the approach to backtracking, exploiting machine learning to select and configure underlying decision procedures, and employing counter-example models from decision procedures to speed search. We also took forward ideas in our RAHD tool for non-linear real arithmetic reasoning in exciting directions. This was primarily in collaboration with one of the principal developers of the Z3 SMT solver, a world leading automatic theorem prover from Microsoft Research with widespread uses in formal verification applications and beyond. For example, the heuristic approach to combining reasoning techniques in RAHD inspired a similar new top-level architecture for Z3. We also created a Z3 library that could handle non-linear polynomial arithmetic with reals, extended with infinitessimal numbers, and used this to handle reasoning problems with more complicated, alternating quantifier structure. For our verification tools to be used effectively in formal verification applications, integration of them into other verification tools was seen as essential. To this end, we integrated MetiTarski and RAHD into the KeYmaera semi-automated theorem proving environment from Carnegie Mellon University. KeYmaera is tailored for reasoning about hybrid systems, common mathematical models of cyber-physical systems (e.g. the control systems for aircraft), and successful use of it relies heavily on the strength of underlying theorem provers for non-linear real arithmetic. Our tools have also been integrated into the PVS theorem prover and MetiTarski has been used in the Why3 software verification platform. When identifying KeYmaera applications that could make good use of MetiTarski, we realised there were a number of ways in which the core inference rules used in KeYmaera could be much improved, and we put significant effort into this, partly in collaboration with the KeyMaera developers. For example, we explored how to efficiently automatically discover invariants with rich structure. The discovery of invariants is essential for most of the verification tasks KeYmaera is used for. Our work on automatic invariant discovery is now incorporated into the Pegasus automatic invariant generation tool which is integrated into KeYmaera X, the latest version of KeYmaera. We also significantly generalised rules used in KeYmaera for establishing invariants and for showing liveness properties. Through the course of our work, we have accumulated large collections of challenge problems involving non-linear polynomial arithmetic, arithmetic with transcendental functions, and invariants of non-linear dynamical systems, and we have made these collections publicly available. Already the Z3 developers have used our challenge problems to test and refine Z3's core procedures for non-linear polynomial arithmetic reasoning. |
| Exploitation Route | Researchers both in academia and industry can take our work forward by reading our papers and experimenting with our publicly released tools and challenge problems. The primary way in which our results could be put to use is through our tools being integrated into formal verification tools and environments that then can be employed by those needing the strong assurances of correctness that formal verification can provide. To date one of the most significant integrations is of MetiTarski into the KeYmaera hybrid theorem prover and the related Sphinx verification-driven engineering toolset. Also our MetiTarksi-related research has had influence on the development of the Z3 SMT solver tool which is used as a reasoning engine in a wide variety of formal verification applications. And our research on automatic generation of continuous invariants is now available for use in the Pegasus tool which is integrated into KeYmaera X, an enhanced complete re-implementation of the original KeYmaera system. |
| Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Electronics,Financial Services, and Management Consultancy,Manufacturing, including Industrial Biotechology,Pharmaceuticals and Medical Biotechnology,Transport,Other |
| Description | At the current time, probably the most significant impact outside of academia has been been the influence on the support for non-linear arithmetic reasoning in the Z3 theorem prover software tool from Microsoft Research. This Z3 tool is used as an automatic reasoning engine in a variety of applications, many related to the formal verification of software. For example, in the UK, the company Altran UK (one of our industrial collaborators) now uses Z3 in their formal verification toolkit for software written in the SPARK subset of the Ada language. Projects this toolkit is deployed on include software for UK air traffic control which is co-developed by Altran UK. This toolkit helps to ensure that this software is free of runtime exception bugs. |
| First Year Of Impact | 2015 |
| Sector | Aerospace, Defence and Marine |
| Impact Types | Economic |
| Description | CMU - KeYmaera group |
| Organisation | Carnegie Mellon University |
| Department | School of Computer Science (SCS) |
| Country | United States |
| Sector | Academic/University |
| PI Contribution | We have integrated our software tools (RAHD and MetiTarski) into the KeYmaera hybrid-systems theorem prover and the Sphinx verification-driven engineering environment which incorporates KeYmaera, both developed at CMU. We experimented with how to engineer the integration with our tools and other similar tools in order to significantly increase the scale of verification problems we could deploy these tools on. We also enhanced the reasoning principles used in KeYmaera, exploring better rules for invariant reasoning, for reasoning about liveness, and the automatic synthesis of invariants. |
| Collaborator Contribution | CMU hosted visits, provided expertise on KeYmaera, and collaborated on joint publications. |
| Impact | This collaboration resulted in enhancements to the KeYmaera tool and Sphinx engineering environment that are developed and distributed by CMU. It also resulted in the published papers with following DOIs: 10.1007/978-3-662-46081-8_24 10.1007/978-3-319-10936-7_10 10.1016/j.cl.2015.11.003 10.1007/978-3-319-19249-9_32 10.1007/978-3-319-06200-6_14 10.1007/s11786-014-0176-y |
| Start Year | 2012 |
| Description | MSR - Z3 group |
| Organisation | Microsoft Research |
| Department | Research in Software Engineering (RiSE) |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | We developed ideas for enhancing the non-linear arithmetic reasoning of Microsoft Research's Z3 SMT solver software tool, of which some were specifically tailored to improve the performance of our MetiTarski software tool. (MetiTarski makes use of Z3.) We also inspired the top-level coordination of Z3's heuristics and provided the Z3 developers with a set of non-linear arithmetic challenge problems. |
| Collaborator Contribution | Microsoft Research provided the time of one of the principal developers of Z3, and implemented our ideas and jointly developed ideas in the Z3 tool. |
| Impact | One set of outcomes is various enhancements to Microsoft's Z3 software tool. Publications describing these are listed elsewhere and have the following DOIs: 10.1007/978-3-642-31374-5_24 10.1007/978-3-642-36675-8_2 10.1007/978-3-642-38574-2_12 |
| Start Year | 2012 |
| Title | MetiTarski |
| Description | MetiTarski is an automatic theorem prover tailored for proving problems involving non-linear real arithmetic with polynomial and transcendental expressions. Funding from this grant enabled major enhancements to MetiTarski's performance which allow it now to handle much larger problems. |
| Type Of Technology | Software |
| Year Produced | 2011 |
| Open Source License? | Yes |
| Impact | The main impact we envisage for MetiTarski is in the formal verification of software and other engineering systems. To this end we have integrated MetiTarski into other formal verification tools such as the KeYmaera and PVS theorem provers and the Why3 software verification toolkit. At the current time the case studies that have been undertaken which involve use of these tools in conjunction with MetiTarski are all of a preliminary experimental nature. |
| URL | http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html |