Environments to develop and check programs

I have put under this category software that can be applied to real world programs (in languages like C or Ada for example) to prove properties on them. I also lists environments that help to check algorithms, etc.


Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.

Rewriting logic is a logic of concurrent change that can naturally deal with state and with concurrent computations. It has good properties as a general semantic framework for giving executable semantics to a wide range of languages and models of concurrency. In particular, it supports very well concurrent object-oriented computation. The same reasons making rewriting logic a good semantic framework make it also a good logical framework, that is, a metalogic in which many other logics can be naturally represented and executed.


Sparkle is a proof tool specially constructed for Clean (a state-of-the-art pure and lazy functional programming language). The tool knows the Clean 2.0 syntax and semantics. It comes with a rich set of proof tactics and a powerful hint mechanism to aid the user in proving properties of Clean programs.


SPARK is a formally-defined computer programming language based on the Ada programming language, intended to be secure and to support the development of high integrity software used in applications and systems where predictable and highly reliable operation is essential either for reasons of safety (e.g., avionics in aircraft/spacecraft, or medical systems and process control software in nuclear powerplants) or for business integrity (for example financial software for banking and insurance companies).

There are four versions of the SPARK language; based on Ada 83, Ada 95, Ada 2005 and Ada 2012. The SPARK language consists of a highly restricted, well-defined subset of the Ada language that uses annotated meta information (in the form of Ada comments up to Ada 2005, with aspects in Ada 2012) that describe desired component behavior and individual runtime requirements, thereby optionally facilitating mandatory use of Design by Contract principles to accurately formalize and validate expected runtime behavior.

Because the annotations are in commentary, SPARK programs are generally also valid Ada programs and can be compiled by an appropriate Ada compiler. The most recent revision of the implementation, RavenSPARK, includes the Ravenscar tasking profile which aims to support concurrency in high integrity applications. The formal, unambiguous definition of SPARK allows and encourages a variety of static analysis techniques to be applied to SPARK programs.


Set of free software tools aiming at implementing the B method, for both software and hardware.


ImProve is an imperative programming language for high assurance applications. ImProve uses infinite state, unbounded model checking to verify programs adhere to specifications. Yices (required) is the backend SMT solver. ImProve compiles to C, Ada, Simulink, and Modelica.


The goal of the Saturn project is to statically and automatically verify properties of large (meaning multi-million line) software systems. The focus of much of our work is simultaneously achieving scalability, precision, and a straightforward way of expressing analyses that is easy to reason about. We plan to use these techniques to verify properties of a full operating system.


Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.

If you have a C program and need to

  • validate it formally
  • look for potential runtime errors
  • audit or review it
  • reverse engineer it to understand its structure
  • generate formal documentation

One or more of the following Frama-C tools may be of assistance to you:

  • A parser, a type checker and source level linker for C code optionally annotated with ACSL formulas.
  • A set of builtin static analysis plugins:
    • A runtime error detection plug-in based on abstract interpretation techniques
    • A dependencies computation plug-in
    • An interactive value analysis plug-in
    • A Use/Defs computation plug-in
    • A slicing plug-in
    • A weakest precondition calculus plug-in based on Floyd-Hoare logic
  • List of alarms detected by the value analysis is “uninitialized access, use of a dangling pointer, overflows in signed integer arithmetics, invalid memory access, invalid comparison of pointers, division by zero, undefined logical shift, overflows in conversions from floating-point to integer, infinite or NaN resulting from a floating-point operation, undefined side-effects in expressions”


CIL is a framework to analyse and manipulate C programs.


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.


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.


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$-160% 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.


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.


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 copy_to_user() while the kernel was locked. If the script saw a place that called lock_kernel() then it would record the state as locked. If the script saw a place that called unlock_kernel() it would set the state to unlocked. If the state was locked and the script saw a place that called copy_to_user() the script would print out an error message.


Sparse, the semantic parser, provides a compiler frontend capable of parsing most of ANSI C as well as many GCC extensions, and a collection of sample compiler backends, including a static analyzer also called “sparse”. Sparse provides a set of annotations designed to convey semantic information about types, such as what address space pointers point to, or what locks a function acquires or releases.



  • Error-finding tool based on static analysis.
  • Target language is C (ANSI C99), but extensible to C#/C++/Java.
  • Full ANSI C99 support, including most GNU C extensions.
  • Modular structure, easy extensibility, fast development.
  • Easy to use interface and error path inspection.
  • Makefile support and batch execution.

Errors detected:

  • Memory allocation errors (null pointers, memory leaks, dangling pointers)
  • Bad locking discipline (double locks/unlocks, locks not released etc.)
  • Interrupt handling (cli/sti-style).
  • And all the errors which can be described by state automata.


Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. The tool can be loaded into GCC as a plug-in. This way you can easily analyse C code sources, using the existing build system, without manually preprocessing them first. The analysis itself is, however, not ready for complex projects yet. The plug-in is based on Code Listener infrastructure (included). Although the tool is intended to be as portable as GCC is, we support only Linux for now.


Dafny is a programming language with a program verifier. As you type in your program, the verifier constantly looks over your shoulders and flags any errors.

The language itself draws pieces of influence from:

  • Euclid (from the mindset of a designing a language whose programs are to be verified),
  • Eiffel (like the built-in contract features),
  • CLU (like its iterators, and inpiration for the out-parameter syntax),
  • Java and C# (like the classes, although Dafny does not support subclassing),
  • ML (like the module system, and its functions and inductive datatypes, but Dafny does not support higher-order features), and
  • Coq (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).

Sireum Bakar

Bakar is a toolset for analyzing Spark Ada programs (Bakar means “spark” in Indonesian).

Sireum Bakar currently includes:

  • Alir: an information flow analysis tool for reasoning about Spark’s derive clauses/information flow (Alir means “flow” in Indonesian). Alir visualizes information flows to ease engineers in understanding information dependencies crucial for specifying and verifying Spark’s derive clauses. Please see our SCAM12 tool paper that describes Sireum/Bakar Alir.
  • Kiasan: a fully automated tool for verifying functional behaviors of Spark programs specified as software contract (Kiasan means “symbolic” in Indonesian). Kiasan is an explicating symbolic execution tool that provides various helpful feedback including generation of counter example for contract refutation, test cases for an evidence of contract satisfaction, verification reports, visual graphs illustrating pre/post states of Spark procedures/functions, etc. Please see our SigAda paper that describes Sireum Bakar Kiasan and our technical report that describes Sireum Bakar Kiasan as an explicating symbolic execution tool.


CPAchecker is a tool for configurable software verification. Our implementation is guided by the concepts described in the CAV'07 paper “Configurable Software Verification” and in the ASE'08 paper “Program Analysis with Dynamic Precision Adjustment”.


HipSpec is an inductive theorem prover for Haskell programs. It will (try to) conjecture essential lemmas to prove tricky properties. It supports all algebraic Haskell 98 data types and polymorphism. We assume that functions terminate on finite input and produce finite output. All quantification is only over total and finite values.


The BToolkit is a toolkit supporting software development with the B-method.

The B-Method was initially devised by Jean-Raymond Abrial during his time at the Programming Research Group at the University of Oxford. Then the B tools were developed at BP Research. BP assigned the rights for these tools to B-Core (UK) Ltd. The B-Toolkit was developed at B-Core by Ib Sorensen and David Neilson from 1992.

The source code to the B-Toolkit has been posted in memory of Ib Sorensen.

B-Core no longer supports or maintains the B-Toolkit.


We present a new symbolic execution tool, KLEE, capable of automatically generating tests that achieve high coverage on a diverse set of complex and environmentally-intensive programs. We used KLEE to thoroughly check all 89 stand-alone programs in the GNU COREUTILS utility suite, which form the core user-level environment installed on millions of Unix systems, and arguably are the single most heavily tested set of open-source programs in existence. KLEE-generated tests achieve high line coverage — on average over 90% per tool (median: over 94%) — and significantly beat the coverage of the developers' own hand-written test suites. When we did the same for 75 equivalent tools in the BUSYBOX embedded system suite, results were even better, including 100% coverage on 31 of them. We also used KLEE as a bug finding tool, applying it to 452 applications (over 430K total lines of code), where it found 56 serious bugs, including three in COREUTILS that had been missed for over 15 years. Finally, we used KLEE to cross-check purportedly identical BUSY-BOX and COREUTILS utilities, finding functional correctness errors and a myriad of inconsistencies.


Cppcheck is a static analysis tool for C/C++ code. Unlike C/C++ compilers and many other analysis tools it does not detect syntax errors in the code. Cppcheck primarily detects the types of bugs that the compilers normally do not detect. The goal is to detect only real errors in the code (i.e. have zero false positives).

  • Out of bounds checking
  • Check the code for each class
  • Checking exception safety
  • Memory leaks checking
  • Warn if obsolete functions are used
  • Check for invalid usage of STL
  • Check for uninitialized variables and unused functions

Overture tools (VDM)

The Overture community supports the modelling method The Vienna Development Method (VDM) which is a set of modelling techniques that have a long and successful history in both research and industrial application in the development of computer-based systems.

The Overture Tool is an open-source integrated development environment (IDE) for developing and analysing VDM models. The tool suite is written entirely in Java and built on top of the Eclipse platform.


Leon is an automated system for synthesizing and verifying functional Scala programs.


What is Infer?

Facebook Infer is a static analysis tool - if you give Infer some Objective-C, Java, or C code, it produces a list of potential bugs.

Anyone can use Infer to intercept critical bugs before they have shipped to people's phones, and help prevent crashes or poor performance.


Android and Java

Infer reports null pointer exceptions and resource leaks in Android and Java code.


In addition to this, it reports memory leak problems in iOS and C code.

Who Uses Infer?

It is used as part of the Facebook development process, where it runs on code changes for mobile apps - these include the main Facebook apps for Android and iOS, Facebook Messenger, Instagram, and other apps which are used by over a billion people.


Verify Your Java Programs with JML

The Java Modeling Language is a mature program specification language with over a decade of history. OpenJML is capable of checking Java programs annotated with specifications in the Java Modeling Language and provides robust support for many of JML's features.

The goal of the OpenJML project is to implement a full tool for JML and current Java that is easy for practitioners and students to use to specify and verify Java programs. In addition, the project seeks to advance the theory and experience of software verification in practical, industrially-relevant contexts.

Support for Static and Runtime Checking

Verification in OpenJML can be performed either by using our extended static checking facilities or by using our runtime assertion checking features. Runtime assertion checking is often easier to write specifications for whereas static checking gives stronger guarantees about program behavior.

Integrates with Most Popular SMT Solvers

OpenJML is not a theorem prover or model checker itself. OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers. OpenJML supports major SMT solvers such as Z3, CVC4 and Yices. The success of the proofs will depend on the capability of the SMT colver (e.g., which logics it supports), the particular logical encoding of the code+specifications, and the complexity and style in which the code and specifications are written.


Stainless is a tool for verifying mostly functional programs developed by LARA at EPFL. Stainless accepts as its inputs programs in a subset of Scala. Stainless can verify that your program is correct for all inputs and it can also report counterexample inputs for invalid programs.

Stainless supports verifying:

  • Assertions which should hold at the place where they are stated, but are checked statically
  • Postconditions using ensuring function: assertions for return values of functions
  • Preconditions using require function: assertions on function parameters
  • Loop invariants: inductive assertions that hold in each loop iteration after the while condition check passes
  • Algebraic data type class invariants: assertions on immutable parameters of constructors (which remain true for all constructed values)
  • Automatic checks done for the absence of runtime failures: completeness of pattern matching, division by zero, array bounds checks, map domain checks

Stainless ensures that the input program belongs to a subset of Scala. This subset syntactically prevents:

  • the creation of null values or unininitalized local variables or fields (therefore, dereferencing fields in Stainless programs cannot lead to null dereference error)
  • explicitly throwing an exception.

The choice of the subset of Scala along with the checks for runtime errors rules out most known sources of errors in Scala programs. An exception are resource exhaustion errors (but see resource bound analysis in Leon documentation below).

Stainless correctly models integral types such as Int with an appropriate level of bits and takes overflow into account (for unbounded integers, use BigInt).

Stainless performs non-trivial termination checks for its functions and supports specifying decreasing measure functions.

astuces/program_dev_check_environments.txt · Dernière modification: Le 30/01/2019 à 18:13 par jaxom     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó