Jessie

The Jessie plug-in allows deductive verification of C programs annotated with ACSL. It uses internally the languages and tools of the Why platform. The generated verification conditions can be submitted to external automatic provers such as Simplify, Alt-Ergo, Z3, Yices, CVC3.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 3 articles )

Showing results 1 to 3 of 3.
Sorted by year (citations)

  1. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
  2. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  3. Bobot, François; Paskevich, Andrei: Expressing polymorphic types in a many-sorted language (2011)