Averist: Algorithmic Verifier of Stability.
Member involved: Miriam García
AVClass: malware labeling tool.
Faculty involved: Juan Caballero
CacheAudit: A Tool for the Static Analysis of Cache Side Channels.
Faculty involved: Boris Köpf
Prolog (Ciao): a general-purpose programming language which supports logic, constraint, functional, higher-order, and object-oriented programming styles.
Faculty involved: Manuel Carro, Manuel Hermenegildo, Pedro López-García and José Francisco Morales
HTT: a verification system which incorporates Hoare style specifications via preconditions and postconditions, into types.
Faculty involved: Aleks Nanevski
FCSL: a framework for mechanized verification of full functional correctness of fine-grained concurrent programs.
Faculty involved: Aleks Nanevski
RHTT: a verification system capable of expressing and verifying rich information flow and access control policies via dependent types.
Faculty involved: Aleks Nanevski
mist: a safety checker for Petri Nets and monotonic extensions.
Faculty involved: Pierre Ganty
LHornSolver: a linear Horn clause solver for non-linear Horn clauses.
Faculty involved: Pierre Ganty,John Gallagher and José Francisco Morales
EasyCrypt: Computer-Aided Cryptographic Proofs
Faculty involved: Pierre Yves Strub and Gilles Barthe
Leap: a theorem prover for the temporal parametrized verification of concurrent data types
Faculty involved: César Sánchez
ConstraintSpecialisation: specialise a set of Horn clause with respect to a goal
Faculty involved: John Gallagher
DFTA: Determinisation and Completion of Finite Tree Automata
Faculty involved: John Gallagher
RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata
Faculty involved: John Gallagher
SMACK: Software Verifier And Verification Toolchain
Former Faculty involved: Michael Emmi
