Personal tools
You are here: Home Events Lab lunch by Paul Jackson

Lab lunch by Paul Jackson

— filed under:

Finding bugs in axioms used in formal software verification

What
  • Upcoming events
When Feb 04, 2014
from 01:00 PM to 02:00 PM
Where MF2
Add event to calendar vCal
iCal

A common approach to formally checking assertions inserted into a program is to first generate verification conditions, logical sentences that, if then proven, ensure the assertions are correct. Sometimes verification conditions are augmented with axioms that capture aspects of the program's specification or can be hints to help automatic provers.  There is always the danger of mistakes in these axioms.  In the worst case these mistakes introduce inconsistencies and verification conditions become erroneously provable.

I'll discuss work I've been doing with Altran UK (formerly Praxis) to debug axioms introduced by users of their toolkit for formally verifying programs in the SPARK subset of Ada.  The work involves the use of an SMT solver to audit these axioms.  For example, the SMT solver is used to check for inconsistencies in axioms and to verify expected relationships between axioms.

Document Actions