Issues, Challenges and Opportunities in the Qualification of Formal Method Tools

Presented as part of the 2015 HCSS conference.

Abstract:

Formal methods have matured enough in the last decade to have made their way into several commercial tools for the development of safety-critical software. Recent revisions of software development standards by certifications authorities such as the FAA and EASA recognize this progress by providing explicit guidance on the use of formal methods in software development. For instance, the DO-333 Formal Methods Supplement of the DO-178C standard requires the production of evidence of logical soundness for any formal method used in the creation of the software system under certification. Any tools used to support the method must be themselves qualified according to a number of criteria.

This talk focused on our on-going investigations on tool qualification issues for modern SMT-based model checkers used to verify safety-properties of embedded software. Qualifying such tools is challenging because of their own complexity and that of the external SMT solvers they invoke. We will discuss a few approaches for developing certifying model checkers from certifying SMT solvers. Such tools produce proof certificates for each property they claim to have proved. In principle, these certificates can be checked by an external proof checker, with the effect of shifting the qualification effort to a much simpler tool. This solution is not realistic, however, because of the complexity of instrumenting a model checker to be fully certifying and because of scalability problems associated with fully detailed certificates. We will present a space of hybrid proof-engineering solutions where some components of the model checker are formally verified while others are proof-producing. We will report on our efforts with collaborators at Rockwell Collins and NYU to implement these solutions in the Kind 2 model checker and the CVC4 SMT-solver.

Certifying SMT solvers can also be incorporated into interactive theorem provers to increase these provers' level of automation without compromising their high trustworthiness. We will also report on related work with collaborators at NYU and Inria to integrate CVC4 into Coq.

Biography:

Cesare Tinelli is a professor of Computer Science and collegiate scholar at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. His research interests include automated reasoning, formal methods, software verification, foundations of programming languages, and applications of logic in computer science.

He has done seminal work in automated reasoning, in particular in Satisfiability Modulo Theory (SMT), a field he helped establish through his research and service activities. He leads the development of the Kind 2 SMT-based model checker, and co-leads the development of the widely used CVC4 SMT solver. He is also a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers.

His research has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and corporations (Intel, Rockwell Collins, and United Technologies). He received an NSF CAREER award in 2003 and a Haifa Verification Conference award in 2010. He is an associate editor of the Journal of Automated Reasoning and a founder the SMT workshop series and the Midwest Verification Day series. He has served in the program committee of numerous conferences and workshops, and in the steering committee of CADE, ETAPS, FTP, FroCoS, IJCAR, and SMT. He was PC chair of FroCoS'11 and of TACAS'15.