69 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
Chakib Foulani
Dorian Lesbre
Frédéric Recoules
Guillaume Girol
Josselin Feist
Lesly-Ann Daniel
Manh-Dung Nguyen
Mathéo Vergnolle
Mathilde Ollivier
Matthieu Lemerre
Olivier Nicole
Richard Bonichon
Robin David
Sébastien Bardin
Soline Ducousso
Ta Thanh Dinh
Yaëlle Vinçont
0.6.3
LGPL-2.1-or-later
Used by 0 other packages
broken
The Broken package is a simple testsuite framework.
bsbnative
bsb-native is BuckleScript's bsb but for ocamlc and ocamlopt
camlrack
S-Expression parsing for OCaml
cconv
Combinators for Type Conversion in OCaml
cconv-ppx
Combinators for Type Conversion in OCaml
conf-opencc0
Virtual package relying on opencc v0 (libopencc.so.1) installation
conf-opencc1
Virtual package relying on opencc v1 (libopencc.so.2) installation
conf-opencc1_1
Virtual package relying on opencc v1.1 (libopencc.so.1.1) installation
configuration
Analyse configuration files
containers-data
A set of advanced datatypes for containers
coq-of-ocaml
Compile a subset of OCaml to Coq
datalog
An in-memory datalog implementation for OCaml
dolmen_bin
A linter for logic languages
dolmen_loop
A tool library for automated deduction tools
dolmen_lsp
A LSP server for automated deduction languages
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
Nicolas Stouls
Kostyantyn Vorobyov
Boris Yakobowski
26.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
frama-c-e-acsl
This package contains the Frama-C's E-ACSL plug-in.
frama-c-metacsl
MetAcsl plugin of Frama-C for writing pervasives properties
funfields
Functional bit field library
gasoline
Unix-ish application development framework
genet
Genet is tool to build a continuous integration platform.
interface-prime
Interfaces for common design patterns
interface-prime-lwt
Interfaces for common design patterns (LWT implementation)
ip2location
IP2Location OCaml module to get geolocation data
kdl
An implementation of the KDL document laguage
lablgtk-extras
A collection of additional tools and libraries to develop ocaml applications based on Lablgtk2.
lbfgs
Bound-constrainted optimization in many variables
0.9.3
LGPL-3.0-only WITH OCaml-LGPL-linking-exception
Used by 2 other packages
llopt
Just a tiny LLVM-IR optimizer for testing stuff.
lz4
Bindings to the LZ4 compression algorithm
maki
Persistent incremental computations, for repeatable tests and benchmarks.
mesh
Triangular mesh generation and manipulation
mesh-easymesh
Triangular mesh generation with EasyMesh
msgpck
Fast MessagePack (http://msgpack.org) library
ocf
OCaml library to read and write configuration files in JSON syntax
olinq
LINQ inspired queries on in-memory data
opencc
Bindings for OpenCC (v1) - Open Chinese Convert
opencc0
Bindings for OpenCC (v0) - Open Chinese Convert
opencc1
Bindings for OpenCC (v1) - Open Chinese Convert
opencc1_1
Bindings for OpenCC (v1.1) - Open Chinese Convert
opentelemetry
Instrumentation for https://opentelemetry.io
opentelemetry-lwt
Lwt-compatible instrumentation for https://opentelemetry.io
optimization1d
Find extrema of 1D functions
0.6.1
LGPL-3.0-only WITH OCaml-LGPL-linking-exception
Used by 0 other packages
orsetto
A library of assorted structured data interchange languages
phylogenetics
Algorithms and datastructures for phylogenetics
ppx_camlrack
PPX for matching S-Expressions
prc
Utilities for precision-recall curves
scfg
OCaml library and executable to work with the scfg configuration file format
scgi
Simple Common Gateway Interface (SCGI) protocol support for interface with HTTP servers
Mike Wells <https://github.com/mwells>
Martin Jambon <https://github.com/mjambon>
Bikal Lem <https://github.com/bikallem>
1.0
BSD-3-Clause
Used by 0 other packages
sfml
Bindings to the SFML multimedia library
stog-rdf
Plugin for Stog. Define and query RDF graphs in rewrite rules.
stog-writing
Stog plugin adding new rewrite rules to use footnotes and bibliographies in documents
sundialsml
Interface to the Sundials suite of numerical solvers
6.1.1p1
BSD-3-Clause
Used by 1 other packages
testrunner
Simple framework to run tests and create test reports for OCaml libraries.
tsdl
Thin bindings to SDL for OCaml
tsdl-mixer
SDL2_Mixer bindings to go with Tsdl
uunf
Unicode text normalization for OCaml
uuseg
Unicode text segmentation for OCaml
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.1
LGPL-2.1-only
Used by 8 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.1
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.1
LGPL-2.1-only
Used by 0 other packages
ws
Generic websocket implementation for OCaml
zipperposition
A fully automatic theorem prover for typed higher-order and beyond
2.1
BSD-2-Clause
Used by 0 other packages