Cesare Tinelli

Formal methods tools have been shown to be effective at finding defects in safety-critical digital systems including avionics systems. The publication of DO-178C and the accompanying formal methods supplement DO-333 allows applicants to obtain certification credit for the use of formal methods without providing justification for them as an alternative method. This project conducted an extensive study of existing formal methods tools, identifying obstacles to their qualification and proposing mitigations for those obstacles. Further, it interprets the qualification guidance for existing formal methods tools and provides case study examples for open source tools. This project also investigates the feasibility of verifying formal methods tools by generating proof certificates which capture proof of the formal methods tool's claim, which can be checked by an independent, proof certificate checking tool. Finally, the project investigates the feasibility of qualifying this proof certificate checker, in the DO-330 framework, in lieu of qualifying the model checker itself.

Modern society relies increasingly on software. Many software systems, however, are unacceptably unreliable as they often contain conceptual or implementation errors and are therefore vulnerable to security attacks. It is now widely recognized that dramatically improving the reliability of computer software is going to be one of the most important scientific and technological challenges of this century. In model-based development, software systems, in particular embedded ones, are developed by first constructing a mathematical model of the system; then verifying desired functional properties against the model; and finally implementing the model. Increasingly, the property-checking phase can be handled formally and automatically using model-checking and verification techniques that rely on automated reasoning engines. Despite the success of these techniques, the complexity of the verification tools involved makes their trustworthiness an important issue. Incorrect results from the automated reasoning engines may compromise the whole verification process. In addition, even if the trustworthiness of a particular reasoning engine can be assured, a large verification task may require multiple reasoners to work together. Thus, the compositionality of trustworthiness is also a critical capability: tools must be able to trust and use the results of other tools. One approach for ensuring trustworthy results from a complex reasoning engine, and for supporting compositionality, is to have the engine emit an independently checkable proof. Compositionality can then be facilitated by using a proof format that can easily be processed by other verification tools. This report describes the results of efforts to do exactly this. CVC4, a modern, open-source solver for Satisfiability Modulo Theories (SMT), has been instrumented with the ability to generate independently checkable proofs for any verification condition it is able to prove.