Averist: Algorithmic Verifier of Stability.
AVClass: malware labeling tool.
CacheAudit: A Tool for the Static Analysis of Cache Side Channels.
CiaoPP: a program analyzer/verifier which performs static and dynamic verification cooperatively for a rich set of properties, including resources. Includes also a partial evaluator and parallelizer.
HTT: a verification system which incorporates Hoare style specifications via preconditions and postconditions, into types.
FCSL: a framework for mechanized verification of full functional correctness of fine-grained concurrent programs.
RHTT: a verification system capable of expressing and verifying rich information flow and access control policies via dependent types.
mist: a safety checker for Petri Nets and monotonic extensions.
LHornSolver: a linear Horn clause solver for non-linear Horn clauses.
EasyCrypt: Computer-Aided Cryptographic Proofs
Leap: a theorem prover for the temporal parametrized verification of concurrent data types
ConstraintSpecialisation: specialise a set of Horn clause with respect to a goal
DFTA: Determinisation and Completion of Finite Tree Automata
RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata