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.

  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

Software previously developed with the support from IMDEA

• SMACK: Software Verifier And Verification Toolchain

  Former Faculty involved: Michael Emmi