<\body> |David Mentré>|>|||>> We are now living in 2004<\footnote> Well, now we are in 2006. :-) . We should no longer make software as in the sixties or seventies, with a few tests. We are now able to make software without bugs. This is possible using specialised tools called . Such tools are able to match a computer program against a specification, i.e. a formal description of the expected behavior of the program. If the specification is correct and the formal verification can be done, then the program is guaranted to be bug free. Of course, this is the ideal case and we are far from guaranteed bug free programs in the real world. But, as developer of free software, we should try to be as close as possible of this goal. As a first step, I list here free software tools that can help verification of computer programs. Proof assistants are computer programs that aids a human to prove things (so they are sometimes called ). Generally, they understand several formal logics with there rules and are able to apply those rules, automatically or guided by the human verifier. Such tools are at the core of the verification process. Coq is a proof assistant environment. <\itemize-dot> License: GNU LGPL 2.1 Web site: Debian packages: ACL2 is an environment where programs are described using an applicative subset of Common Lisp. Each function of the program entered in the environment is formally proven (termination, ...). <\itemize-dot> License: GNU GPL Web site: Debian packages: PhoX is a proof assistant based on High Order logic and it is eXtensible. One of the principle of this proof assistant is to be as user friendly as possible and so to need a minimal learning time. The current version is still expirimental but starts to be really usable. It is a good idea to try it and make comments to improve the final version. <\itemize-dot> License: ?? Web site: HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness. <\itemize-dot> License: BSD like Web site: \ Providing a high degree of automation to discharge proof obligations in (fragments of) first-order logic is a crucial activity in many verification efforts. Unfortunately, this is quite a difficult task. On the one hand, reasoning modulo ubiquitous theories (such as lists, arrays, and Presburger arithmetic) is essential. On the other hand, to effectively incorporate this theory specific reasoning in boolean manipulations requires a substantial work. The system haRVey implements a simple technique to cope with such difficulties whose aim is to check the validity of universally quantified formulae with arbitrary boolean structure modulo an equational theory. The approach combines BDDs with refutation theorem proving. The former allows us to compactly represent the boolean structure of formulae, the latter to effectively mechanize the reasoning in equational theories. <\itemize-dot> License: GNU LGPL 2.1 Web site: Set of free software tools aiming at implementing the B method, for both software and hardware. <\itemize-dot> License: GNU LGPL Web site: HOL 4 is the latest version of the HOL automated proof system for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. <\itemize-dot> License: BSD like Web site: Model checkers are tool that verify all possible states of a formal model, i.e. a formal description of a system. Compared to proof assistant, they can be less powerful but easier to use. NuSMV is a reimplementation and extension of SMV, the first model checker based on BDDs. NuSMV has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas. <\itemize-dot> License: GNU LGPL 2.1 Web site: Murphi also has a formal verifier based on explicit state enumeration. The verifier performs depth- or breadth-first search in the state graph defined by a Murphi description, storing all the states it encounters in a large hash table. When a state is generated that is already in the hash table, the search algorithm does not expand its successor states (they were expanded whenever the state was originally inserted in the table). <\itemize-dot> License: BSD like Web site: Mec 5 is a model-checker for finite AltaRica models, using a very expressive specification language (systems of fixpoint equations over finite relations with first-order quantifiers and equality testing). <\itemize-dot> License: Public domain Web site: I have put under this category software that can be applied to real world programs (in language like C for example) to prove properties on them. Why is a verification conditions generator (VCG) back-end for other verification tools. It understands ML, C and Java languages (with the help of other programs). <\itemize-dot> License: GNU GPL Web site: CIL is a framework to analyse and manipulate C programs. <\itemize-dot> License: BSD like Web site: Splint is a tool for statically checking C programs for security vulnerabilities and coding mistakes. With minimal effort, Splint can be used as a better lint. If additional effort is invested adding annotations to programs, Splint can perform stronger checking than can be done by any standard lint. <\itemize-dot> License: GNU GPL Web site: Debian packages: Cqual is a type-based analysis tool that provides a lightweight, practical mechanism for specifying and checking properties of C programs. Cqual extends the type system of C with extra user-defined type qualifiers. The programmer adds type qualifier annotations to their program in a few key places, and Cqual performs qualifier inference to check whether the annotations are correct. The analysis results are presented with a user interface that lets the programmer browse the inferred qualifiers and their flow paths. <\itemize-dot> License: GNU GPL Web site: CCured is a source-to-source translator for C. It analyzes the C program to determine the smallest number of run-time checks that must be inserted in the program to prevent all memory safety violations. The resulting program is memory safe, meaning that it will stop rather than overrun a buffer or scribble over memory that it shouldn't touch. Many programs can be made memory-safe this way while losing only 10--60% run-time performance (the performance cost is smaller for cleaner programs, and can be improved further by holding CCured's hand on the parts of the program that it does not understand by itself). Using CCured we have found bugs that Purify misses with an order of magnitude smaller run-time cost. <\itemize-dot> License: BSD like Web site: CHIC is a modular verifier for behavioral compatibility checking of software and hardware components. The goal of CHIC is to be able to check that the interfaces for software or hardware components provide guarantees that satisfy the assumptions they make about each other. CHIC supports a variety of interface property specification formalisms. <\itemize-dot> License: BSD like Web site: Smatch is C source checker but mainly focused checking the Linux kernel code. It is based on the papers about the Stanford Checker. Basically, Smatch uses a modified gcc to generate .c.sm files. The .c.sm files are piped through individual Smatch scripts that print out error messages. For example, someone might want to write a Smatch script that looked for code that called while the kernel was locked. If the script saw a place that called then it would record the state as locked. If the script saw a place that called it would set the state to unlocked. If the state was locked and the script saw a place that called the script would print out an error message. <\itemize-dot> License: GNU GPL Web site: Sparse is a parsing and analysis library for the C language. One could put a number of different backends onto it; for example, a code-generation backend would turn it into a simple compiler. For the purposes of the kernel, however, the backend of interest is the analysis code which looks for various types of errors. The analyzer checks for quite a few different types of errors. <\itemize-dot> License: OSL v1.1 ("Open Software License") Web site: none, however here is a Source: Mailing-list: Focal (formerly known as FoC) is a language for software-proof codesign. In Focal, code, specifications, and proofs are developped together in the same source files, using a novel object-oriented module system. The compiler analyses the dependencies in order to ensure the consistency of the source, then translates the code to Objective Caml, and the proofs to Coq. <\itemize-dot> License: BSD like Web site: \ The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects. <\itemize-dot> License: GNU GPL Web site: It remains to test all those programs. A hard task that is not yet done. <\initial> <\collection> <\references> <\collection> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > <\auxiliary> <\collection> <\associate|toc> |math-font-series||1Proof assistants> |.>>>>|> |1.1Coq |.>>>>|> > |1.2ACL2 |.>>>>|> > |1.3Phox |.>>>>|> > |1.4HOL Light |.>>>>|> > |1.5haRVey |.>>>>|> > |1.6Brillant |.>>>>|> > |math-font-series||2Model checkers> |.>>>>|> |2.1NuSMV |.>>>>|> > |2.2Murphi |.>>>>|> > |math-font-series||3Tools to help verification of real programs> |.>>>>|> |3.1Why |.>>>>|> > |3.2CIL |.>>>>|> > |3.3Splint |.>>>>|> > |3.4Cqual |.>>>>|> > |3.5CCured |.>>>>|> > |3.6CHIC |.>>>>|> > |3.7Smatch!!! |.>>>>|> > |3.8Sparse |.>>>>|> > |3.9Focal |.>>>>|> > |math-font-series||4Conclusion> |.>>>>|>