📣 Help Shape the Future of UKRI's Gateway to Research (GtR)

We're improving UKRI's Gateway to Research and are seeking your input! If you would be interested in being interviewed about the improvements we're making and to have your say about how we can make GtR more user-friendly, impactful, and effective for the Research and Innovation community, please email gateway@ukri.org.

Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

Lead Research Organisation: University of Bath
Department Name: Computer Science

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.
 
Description Cylindrical Algebraic Decomposition is a key technique in symbolic computation, with applications in software verification. But it can be very costly. Together with the RWTH team, we developed a variant (Cylindrical Algebraic Coverings) which is generally more efficient for the soft of problems that arise in software verification. It has been implemented in the cvc5 automatic theorem prover.
Exploitation Route cvc5 is in use many people developing formally verified software, including the developers of the UK's National Air Traffic System, and some railway signalling software.
Sectors Aerospace

Defence and Marine

Digital/Communication/Information Technologies (including Software)
 
Description This project finished and contributed to Maplesoft, for inclusion in Maple, research software coming out of an EPSRC/CASE research student. The Cylindrical Algebraic Coverings method, developed by this project and the RWTH Aachen team, has been implemented in the cvc5 automated theorem prover.
First Year Of Impact 2022
Sector Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software)
Impact Types Economic
 
Title SMT-Solving Induction Proofs of Inequalities Benchmarking Repository 
Description This repository contains the full list of files and the benchmarking results that were used in the benchmarking processes described in the paper: A.K. Uncu, J.H. Davenport and M. England. "SMT-Solving Induction Proofs of Inequalities". Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation (SC^2 2022). The files are split in three branches. The Mathematica and Maple files include the calls that were made to the respective computer algebra systems, and the smt2 files are the ones used by the considered SMT solvers: Z3, CVC5 and Yices. The Benchmarking Results cvc has the results. The columns record the file names, the satisfiability outcome of the calls, then the times (in seconds) of the respective programmes. Any empty box (which the Maple:-RegularChains column has) would mean that the implementation does not accept that sort of input (this is due to rational functions - see the paper for details). Any time over 1200 seconds would mean that the program times out and the outcome of the question was not found in the given time. 
Type Of Material Database/Collection of data 
Year Produced 2023 
Provided To Others? Yes  
Impact None known 
URL https://zenodo.org/record/7777296
 
Title SMT-Solving Induction Proofs of Inequalities Benchmarking Repository 
Description This repository contains the full list of files and the benchmarking results that were used in the benchmarking processes described in the paper: A.K. Uncu, J.H. Davenport and M. England. "SMT-Solving Induction Proofs of Inequalities". Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation (SC^2 2022). The files are split in three branches. The Mathematica and Maple files include the calls that were made to the respective computer algebra systems, and the smt2 files are the ones used by the considered SMT solvers: Z3, CVC5 and Yices. The Benchmarking Results cvc has the results. The columns record the file names, the satisfiability outcome of the calls, then the times (in seconds) of the respective programmes. Any empty box (which the Maple:-RegularChains column has) would mean that the implementation does not accept that sort of input (this is due to rational functions - see the paper for details). Any time over 1200 seconds would mean that the program times out and the outcome of the question was not found in the given time. 
Type Of Material Database/Collection of data 
Year Produced 2023 
Provided To Others? Yes  
URL https://zenodo.org/record/7777297
 
Description Cylindrical Algebraic Decomposition via Regular Chains (2) 
Organisation Chinese Academy of Sciences
Department Chongqing Institute of Green and Intelligent Technology (CIGIT)
Country China 
Sector Academic/University 
PI Contribution See (1).
Start Year 2013
 
Description Dagstuhl 22072 
Organisation Fondazione Bruno Kessler
Country Italy 
Sector Private 
PI Contribution Both Bath and Coventry worked on the organisation of Dagstuhl workshop 22072.
Collaborator Contribution Helped with the organisation of Dagstuhl workshop 22072. It was an equal operation between Bath(Davenport), Coventry (England), RWTH(Abraham) and FBK(Griggio) in the organisation. Bath and Coventry each provided a local zoom-master, and Coventry the remore Zoom-master.
Impact Outputs are ongoing collaboration and paperwriting. The seminar report is published.
Start Year 2021
 
Description Dagstuhl 22072 
Organisation RWTH Aachen University
Department Department of Computer Science
Country Germany 
Sector Academic/University 
PI Contribution Both Bath and Coventry worked on the organisation of Dagstuhl workshop 22072.
Collaborator Contribution Helped with the organisation of Dagstuhl workshop 22072. It was an equal operation between Bath(Davenport), Coventry (England), RWTH(Abraham) and FBK(Griggio) in the organisation. Bath and Coventry each provided a local zoom-master, and Coventry the remore Zoom-master.
Impact Outputs are ongoing collaboration and paperwriting. The seminar report is published.
Start Year 2021
 
Description Prospects of Formal Mathematics 
Organisation Friedrich-Alexander University Erlangen-Nuremberg
Country Germany 
Sector Academic/University 
PI Contribution I participated in the original Dagstuhl workshop, which led to the "Proving an Execution" paper. As a result of this, I have been invited to the special semester at Bonn. This led to much informal collaboration, and two arXiv preprints. I have been invited to speak in Erlangen in May 2025, and a grant application is in progress.
Collaborator Contribution Invitation to Dagstuhl and Bonn (from Kohlhase at FAU). Dagstuhl participants contributed to work behind "Proving an Execution".
Impact "Proving an Execution" paper. Two arXiv preprints
Start Year 2023
 
Description Prospects of Formal Mathematics 
Organisation University of Bonn
Country Germany 
Sector Academic/University 
PI Contribution I participated in the original Dagstuhl workshop, which led to the "Proving an Execution" paper. As a result of this, I have been invited to the special semester at Bonn. This led to much informal collaboration, and two arXiv preprints. I have been invited to speak in Erlangen in May 2025, and a grant application is in progress.
Collaborator Contribution Invitation to Dagstuhl and Bonn (from Kohlhase at FAU). Dagstuhl participants contributed to work behind "Proving an Execution".
Impact "Proving an Execution" paper. Two arXiv preprints
Start Year 2023
 
Title Hybrid CAD Maple Package 
Description A Maple package for CAD, largely implemented by Zak Tonks (EPSRC CASE(Maplesoft) student) but finished by Davenport and Uncu 
Type Of Technology Software 
Year Produced 2022 
Impact It's in the 2023 production version of Maple