The paper describes cvc5, a software verification tool and automated theorem prover.
By Mr John Stevenson (Senior Communications Officer), Published
A research paper co-authored by City, University of London's software reliability academic Dr Martin Nyx Brain in the Department of Computer Science, has won the Best Tool Paper Award at the recent European Joint Conference on the Theory & Practice of Software (ETAPS).
The paper, cvc5: A Versatile and Industrial-Strength SMT Solver, demonstrates cvc5, a software verification tool and method for mathematically proving that software does not crash and is bug free before testing. It emerges out of the work that he and his international team of colleagues have been carrying out to develop the next generation of tools for solving a series of ‘logic puzzles’ or equations.
Dr Brain, a Lecturer in Computer Science, explains:
If we want to build a cleaner, greener, safer and better world one of the best tools we have is the computer control of physical systems and software. Advanced collision management systems in cars that protect passengers and pedestrians in a crash, high efficiency aircraft engines, automated control of ground and air traffic, precision control of wind turbines for maximum efficiency and even artificial organs and medical prothesis - all of these instances rely on software to work and deliver the benefits the world needs.
Risk enters into the picture, however, if the software is faulty or insecure - which can lead to people’s lives being put in serious danger and grave environmental damage. City’s Centre for Software Reliability, has, over the years, been developing and working with industry to use a variety of different tools, methods and techniques to make critical infrastructure software safer, more secure and more robust.
“One of these layers of defence is software verification; tools and methods for mathematically proving that software will not crash and is bug-free before it is tested. Software is reduced to a series of ‘logic puzzles’ or equations. If there are solutions to the equations, there are ways the software can crash or be hacked. If there are no solutions then the system is safe. This is a powerful technique but it needs a fast way of solving the millions or billions of equations generated by a typical piece of industrial control software”, Dr Brain adds.