Formal methods for software verification

Abstract

The growing importance of software in every aspect of our life has fostered the development of techniques aimed at certifying that a given software product has a particular property. This is especially important in critical application areas such as health care and telecommunications, where software security certification can improve a software product's appeal and reduce users and adopters concern over the risks created by software faults. In this chapter, we shall deal with a wide range of formal and semi-formal techniques used for verifying software systems' reliability, safety and security properties. A central notion is the one of a certificate i.e. a metadata item containing all information necessary for an independent assessment of all properties claimed for a software artifact. Here we focus on the notion of model-based certification, that is, on providing formal proofs that an abstract model (e.g., a set of logic formulas, or a formal computational model, such as a finite state automaton), representing a software system, has a particular property. We start by laying out some of the work that has been done in the context of formal method verification, including in particular the areas of model checking, static analysis, and security-by-contract. Then, we go on discuss the formal methods that have been used for analyzing/certifying large-scale, C-based open source software.