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
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.
Faculty involved: Manuel Carro, Manuel Hermenegildo, Pedro López-García and José Francisco Morales
Ciao: a general-purpose, multi-paradigm programming language which supports logic (including full ISO-Prolog), constraint, functional, higher-order, and object-oriented programming styles.
Faculty involved: Manuel Carro, Manuel Hermenegildo, Pedro López-García and José Francisco Morales
s(CASP): Implementation of a top-down evaluation method for Answer Set Programming, enabling the use of free variables, arbitrary data structures, and constraints.
Faculty involved: Manuel Carro. External members: Joaquín Arias
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