Certified Satisfiability Modulo Theories (SMT) Solving for System Verification
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2017
- Accession Number
- AD1025330
Entities
People
- Alain Mebsout
- Andrew Reynolds
- Burak Ekici
- Cesare Tinelli
- Chantel Keller
- Clark Barrett
- Guy Katz
- Liana Hadarean
Organizations
- New York University