Software
The following software are published by the LSV.
- Csur
- Csur is a project about automatic analysis of cryptographic protocols written in C.
It uses a new hybrid analysis of C code: programs represent roles of agents in protocols.
Secrecy properties of protocols can be analyzed using a Dolev-Yao model. Bugs in the implementation
can also be found using our techniques.
- Cosmos
- COSMOS is a statistical model checker for the Hybrid Automata Stochastic Logic (HASL).
HASL employs Linear Hybrid Automata (LHA), a generalization of Deterministic Timed Automata (DTA),
to describe accepting execution paths of a Discrete Event Stochastic Process (DESP), a class of stochastic models which
includes, but is not limited to, Markov chains. As a result HASL verification turns out to be a unifying framework where
sophisticated temporal reasoning is naturally blended with elaborate reward-based analysis.
- evatrans v.2
- evatrans is the second version of a environment developed for the
purpose of the project EVA for
parsing, type-checking and compiling
cryptographic protocols specified in an high level abstract language
into various formats understandable by verification tools.
- FAST
- FAST is a model-checker for infinite systems modelled by
counter automata. Symbolic methods and acceleration techniques allow to
verify automatically safety properties by computing rechability sets.
- H1
- A library for tree automata, set constraints and automated deduction to handle clause set in
the decidable class H1.
The project is developped mostly in HimML.
- ISpi
- Tool for automatic verification of cryptographic protocols (preliminary version).
Documentation.
- Net-Entropy
- An entropy checker for ciphered network connections. This Tool detects
the attacks done on software implementing security layers (SSH, SSL, VPN, ...).
- ORCHIDS
- ORCHIDS is a real-time, multi-event, multi-source intrusion detection tool
based on efficient temporal model-checking algorithms (in development).
- Securify
- Securify is an automatic verification tool for cryptographic protocols. It
can prove secrecy properties for an unbounded number of sessions
and participants.
- IMITATOR
- IMITATOR (standing for Inverse Method for Inferring Time AbstracT behaviOR)
is an implementation of the inverse method for parametric timed automata. It allows
to generalize a concrete behavior of a Parametric Timed Automata, by synthesizing
a constraint on the parameters.
- Heap-Hop
-
Heap-Hop is a prover for concurrent heap-manipulating programs that use
Hoare monitors and message-passing synchronization. Programs are
annotated with pre and post-conditions and loop invariants, written in a
fragment of separation logic. Communications are governed by a form of
session types called contracts. Heap-Hop can prove safety and
race-freedom and, thanks to contracts, absence of memory leaks and
deadlock-freedom.
- Cunf
-
The Cunf tool is a contextual Petri net unfolder.
- PRALINE
-
PRALINE is a tool to compute pure Nash equilibria in concurrent games.
- Shrinktech
-
Shrinktech is a tool for robustness analysis of timed automata.
- QuantiS
-
QuantiS is a tool for evaluating quantitative specifications.