Report
Certified Satisfiability Modulo Theories (SMT) Solving for System Verification
New York University
01/2017
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.
Details
- Title: Subtitle
- Certified Satisfiability Modulo Theories (SMT) Solving for System Verification
- Creators
- Clark BarrettBurak EkiciLiana HadareanGuy KatzChantel KellerAlain MebsoutAndrew ReynoldsCesare Tinelli
- Resource Type
- Report
- Publisher
- New York University; New York, New York, USA
- Number of pages
- 72 pages
- Comment
- Technical Report,01 Aug 2013, 01 Jul 2016 AFRL-RI-RS-TR-2017-007
- Language
- English
- Date published
- 01/2017
- Academic Unit
- Computer Science
- Record Identifier
- 9984259477802771
Metrics
12 Record Views