Start date 01/09/2014
End date 01/09/2018

Generating and Proving Program Properties via Symbol Elimination

Complex computers systems have become an essential part of our lives. Banks, hospitals, organisations and individuals are using such systems and heavily depend on them. Such systems, including Internet, networking, online payment systems, etc., rely on software used in them.

The problem of creating reliable software attracts the attention of computer scientists for decades now. This problem is hard due to the complexity of software and the underlying mathematical foundations.

The objective of our project is to develop new verification methods by using computer reasoning in new ways. Our research is based on our symbol elimination method in computer reasoning, and will address the following directions:

  • Automatically derive program properties and hints that prevent programmers from introducing errors while making changes in programs.
  • Design new algorithms that supporting automated reasoning over program properties and implement them in the award-winning theorem proving tool Vampire.

We expect our project to have a deep and long-lasting impact in reasoning-based formal verification, yielding novel methods and scientific breakthroughs in automated reasoning and formal verification.

Published: Tue 28 Jan 2014. Modified: Mon 14 Apr 2014