Automated Reasoning with Theories

Christoph Sticksel, School of Computer Science, Formal Methods Group

How can we be sure that software which we entrust more and more vital tasks to is free of flaws? Incidents of software maliciously being exploited or accidentally failing have had consequences that range from severe financial losses to threats to the lives of people. Good engineering is just a weak safeguard, and in particular in an ever faster paced and more complex world no guarantee that no flaw in the final product has been overlooked. Only formal verification can prove that a program will always behave as specified or that a specification is actually without loopholes.

Unfortunately, verification of real world applications is tantamount to finding a needle in a haystack. The problems are too large and too complex to tackle for any one person even with all human intuition and creativity. This is where automated reasoning comes in. It offers a mechanisation of the process of finding logical conclusions, sifting through the haystack and in relevant practical cases actually finding a needle. Then, either defects in the implementation or specification can be fixed, or the reliability of the software has been formally established.

This research is focused on a recent approach to automated reasoning that has already shown success in a range of cases. The goal is to allow specifications to use more expressive theories, leading to more concise formulations, in turn making the automated reasoning process more powerful. Ultimately, automated reasoning for verification will have an integral place in design processes, resulting in better and safer software.

My entry to the EPS Lay Summary Competition 2009, Postgrad category. Read the winning entries