Ohloh by Black Duck

 Follow @ Meta   Join Now

Jean-Christophe Filliatre

Managed Projects

Showing page 1 of 1

Why3

Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification apart from generation of verification conditions for programs. It features a rich library of proof task transformations that can be chained to produce a suitable input for a ... [More] large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants. [Less]

5.0
 
  0 reviews  |  3 users  |  375,598 lines of code  |  11 current contributors  |  Analyzed 4 days ago
  logic verification programming
 
 

Why

Why is a software verification platform. This platform contains several tools: * a general-purpose verification condition generator (VCG), Why, which is used as a back-end by other verification tools (see below) but which can also be used directly to verify programs (see for instance these ... [More] examples) ; * a tool Krakatoa for the verification of Java programs; * a tool Caduceus for the verification of C programs; note that Caduceus is somewhat obsolete now and users should turn to Frama-C instead. One of the main features of Why is to be integrated with many existing provers (proof assistants such as Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and decision procedures such as Simplify, Alt-Ergo, Yices, Z3, CVC3, etc.). [Less]

5.0
 
  0 reviews  |  2 users  |  337,659 lines of code  |  4 current contributors  |  Analyzed 6 days ago
 
 

OCaml library combine

A OCaml library for combinatorics

0
 
  0 reviews  |  1 user  |  5,991 lines of code  |  3 current contributors  |  Analyzed 1 day ago
 
 

bitv

OCaml bit vector library

0
 
  0 reviews  |  0 users  |  898 lines of code  |  2 current contributors  |  Analyzed 3 days ago
 
 
 
 

Creative Commons License Copyright © 2013 Black Duck Software, Inc. and its contributors, Some Rights Reserved. Unless otherwise marked, this work is licensed under a Creative Commons Attribution 3.0 Unported License . Ohloh ® and the Ohloh logo are trademarks of Black Duck Software, Inc. in the United States and/or other jurisdictions. All other trademarks are the property of their respective holders.