Automatic Proof Procedures for Polynomials and Special Functions

Lead Research Organisation: University of Edinburgh
Department Name: Sch of Informatics


An engineering design is expected to satisfy safety constraints, many of which can be expressed as mathematical and logical formulas. Computer software exists that can check some such formulas automatically, but although they can have a large and complicated logical structure, the mathematical component currently has to be linear: in other words, involving nothing more complicated than addition. Real-world engineering problems involve sophisticated mathematical concepts, such as polynomials and transcendental functions.The investigators have developed software (called MetiTarski and RAHD) that can solve such problems in many cases. The current project will extend the scope of this software, increasing its power and targeting it at specific real-world application areas. One such application is analogue circuitry, which is widespread in consumer electronics. The project will investigate many other potential applications In engineering and the mathematical sciences.
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 use for. We also significantly generalised the rules used 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 publically 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 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.
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/ 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.