The following software are published by the LSV.

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 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 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.
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.
Tool for automatic verification of cryptographic protocols (preliminary version). Documentation.
An entropy checker for ciphered network connections. This Tool detects the attacks done on software implementing security layers (SSH, SSL, VPN, ...).
ORCHIDS is a real-time, multi-event, multi-source intrusion detection tool based on efficient temporal model-checking algorithms (in development).
Securify is an automatic verification tool for cryptographic protocols. It can prove secrecy properties for an unbounded number of sessions and participants.
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 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.
The Cunf tool is a contextual Petri net unfolder.
PRALINE is a tool to compute pure Nash equilibria in concurrent games.
Shrinktech is a tool for robustness analysis of timed automata.
QuantiS is a tool for evaluating quantitative specifications.

About LSV