Software being developed with the support from IMDEA
-
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.
- Ciao: a general-purpose, multi-paradigm programming language which supports logic (including full ISO-Prolog), constraint, functional, higher-order, and object-oriented programming styles.
- s(CASP): Implementation of a top-down evaluation method for Answer Set Programming, enabling the use of free variables, arbitrary data structures, and constraints.
-
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.
-
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
Software previously developed with the support from IMDEA
- SMACK: Software Verifier And Verification Toolchain
Former Faculty involved: Michael Emmi