Software

See also this page

  • Alt-Ergo



    • Automated theorem prover for software verification


    • Alt-Ergo is an automatic solver of formulas based on SMT technology. It is especially designed to prove mathematical formulas generated by program verification tools, such as Frama-C for C programs, or SPARK for Ada code. Initially developed in Toccata research team, Alt-Ergo's distribution and support are provided by OCamlPro since September 2013.


    • https://alt-ergo.ocamlpro.com/
  • Bibtex2HTLM

  • Coquelicot



    • The Coquelicot library for real analysis in Coq


    • Coquelicot is library aimed for supporting real analysis in the Coq proof assistant. It is designed with three principles in mind. The first is the user-friendliness, achieved by implementing methods of automation, but also by avoiding dependent types in order to ease the stating and readability of theorems. This latter part was achieved by defining total function for basic operators, such as limits or integrals. The second principle is the comprehensiveness of the library. By experimenting on several applications, we ensured that the available theorems are enough to cover most cases. We also wanted to be able to extend our library towards more generic settings, such as complex analysis or Euclidean spaces. The third principle is for the Coquelicot library to be a conservative extension of the Coq standard library, so that it can be easily combined with existing developments based on the standard library.


    • http://coquelicot.saclay.inria.fr/
  • Cubicle



    • The Cubicle model checker modulo theories


    • Cubicle is an open source model checker for verifying safety properties of array-based systems, which corresponds to a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems.


    • https://github.com/cubicle-model-checker/cubicle
  • Flocq



    • The Flocq formalization of floating-point arithmetic for the Coq proof assistant


    • The Flocq library for the Coq proof assistant is a comprehensive formalization of floating-point arithmetic: core definitions, axiomatic and computational rounding operations, high-level properties. It provides a framework for developers to formally verify numerical applications.

      Flocq is currently used by the CompCert verified compiler to support floating-point computations.



    • https://flocq.gitlabpages.inria.fr/
  • functory

  • mlpost




    • Mlpost is an objective Caml API to the metapost graphical tool.metapost allows the design of pictures which include LaTeX elements.The objective Caml API allows the design of high-level graphical libraries on top of metapost.


    • http://mlpost.lri.fr/
  • OCamlGraph




    • OCamlGraph is a graph library for Objective Caml



  • Why3



    • The Why3 environment for deductive verification


    • Why3 is an environment for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.


    • https://www.why3.org/
  • Gappa



    • The Gappa tool for automated proofs of arithmetic properties


    • Gappa is a tool intended to help formally verifying numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to verify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why3 software verification plateform or as an automatic tactic for the Coq proof assistant.


    • https://gappa.gitlabpages.inria.fr/
  • CoqInterval



    • Interval package for Coq


    • CoqInterval is a library for the proof assistant Coq.

      It provides several tactics for proving theorems on enclosures of real-valued expressions. The proofs are performed by an interval kernel which relies on a computable formalization of floating-point arithmetic in Coq.

      The Marelle team developed a formalization of rigorous polynomial approximation using Taylor models in Coq. In 2014, this library has been included in CoqInterval.



    • https://coqinterval.gitlabpages.inria.fr/
  • coq-num-analysis



    • Formal developments and proofs in Coq of numerical analysis problems.


    • Formal developments and proofs in Coq of numerical analysis problems.
      The current long-term goal is to formally prove parts of a C++ library implementing the Finite Element Method.


    • https://lipn.univ-paris13.fr/coq-num-analysis/


Comments are closed.