8 Search Results
binsec
Semantic analysis of binary executables
binary code analysis
symbolic execution
deductive
program verification
formal specification
automated theorem prover
plugins
abstract interpretation
dataflow analysis
linking
disassembly
Adel Djoudi
Benjamin Farinier
Frédéric Recoules
Josselin Feist
Lesly-Ann Daniel
Manh-Dung Nguyen
Mathilde Ollivier
Matthieu Lemerre
Olivier Nicole
Richard Bonichon
Robin David
Ta Thanh Dinh
Yaëlle Vinçont
Guillaume Girol
0.5.0
LGPL-2.1-or-later
Used by 0 other packages
frama-c
Platform dedicated to the analysis of source code written in C
deductive
program verification
formal specification
automated theorem prover
interactive theorem prover
C
plugins
abstract interpretation
slicing
weakest precondition
ACSL
dataflow analysis
runtime verification
Michele Alberti
Thibaud Antignac
Gergö Barany
Patrick Baudin
Thibaut Benjamin
Allan Blanchard
Lionel Blatter
François Bobot
Richard Bonichon
Quentin Bouillaguet
David Bühler
Zakaria Chihani
Loïc Correnson
Julien Crétin
Pascal Cuoq
Zaynah Dargaye
Basile Desloges
Jean-Christophe Filliâtre
Philippe Herrmann
Maxime Jacquemin
Florent Kirchner
Tristan Le Gall
Jean-Christophe Léchenet
Matthieu Lemerre
Dara Ly
David Maison
Claude Marché
André Maroneze
Thibault Martin
Fonenantsoa Maurica
Melody Méaulle
Benjamin Monate
Yannick Moy
Anne Pacalet
Valentin Perrelle
Guillaume Petiot
Dario Pinto
Virgile Prevosto
Armand Puccetti
Félix Ridoux
Virgile Robles
Muriel Roger
Julien Signoles
Kostyantyn Vorobyov
Boris Yakobowski
25.0
LGPL-2.1-only
Used by 3 other packages
frama-c-base
Platform dedicated to the analysis of source code written in C.
deductive
program verification
formal specification
automated theorem prover
interactive theorem prover
C
plugins
abstract interpretation
slicing
weakest precondition
ACSL
dataflow analysis
runtime verification
Michele Alberti
Gergö Barany
Patrick Baudin
François Bobot
Richard Bonichon
David Bühler
Loïc Correnson
Julien Crétin
Pascal Cuoq
Zaynah Dargaye
Jean-Christophe Filliâtre
Philippe Herrmann
Florent Kirchner
Tristan Le Gall
Jean-Christophe Léchenet
Matthieu Lemerre
David Maison
Claude Marché
André Maroneze
Benjamin Monate
Yannick Moy
Anne Pacalet
Valentin Perrelle
Guillaume Petiot
Virgile Prevosto
Armand Puccetti
Muriel Roger
Julien Signoles
Kostyantyn Vorobyov
Boris Yakobowski
15.0
LGPL-2.1-only
Used by 2 other packages
why
Why is a software verification platform.
deductive
program verification
specification
automated theorem prover
interactive theorem prover
Java
JML
C
ACSL
2.41
LGPL-2.1-only
Used by 0 other packages
why3
Why3 environment for deductive program verification
deductive
program verification
formal specification
automated theorem prover
interactive theorem prover
1.5.0
LGPL-2.1-only
Used by 7 other packages
why3-base
Why3 environment for deductive program verification (base)
deductive
program verification
formal specification
automated theorem prover
interactive theorem prover
0.88.3
LGPL-2.1-only
Used by 1 other packages
why3-coq
Why3 environment for deductive program verification
deductive
program verification
formal specification
automated theorem prover
interactive theorem prover
1.5.0
LGPL-2.1-only
Used by 0 other packages
why3-ide
Why3 environment for deductive program verification
deductive
program verification
formal specification
automated theorem prover
interactive theorem prover
1.5.0
LGPL-2.1-only
Used by 0 other packages