Français Anglais
Accueil Annuaire Plan du site
Home > Groups > Research groups > Toccata (Toccata)
Toccata (Toccata)
Page no more maintained

as of 30 September 2013
please refer to the new team

The objective of the team is to propose methods and tools that can be integrated into the software development cycle and that make it possible to produce code that is proven to be correct with respect to its expected behavior.

The team develops a generic program proof environment (the Why platform), that is able to generate proof demands that can then be delegated to automatic or interactive provers. Dedicated environments to prove C programs (Caduceus) and Java programs (Krakatoa) annoted with formulas describing the expected behavior, are constructed on top of this tool.

Group Members
  Group leader
    MARCHÉ Claude

Research activities
  Data centric languages and systems

Software & patents
  Caduceus: Caduceus Tool for C Program Verification
  EdiFlow: EdiFlow: interactive workflows for data analytics

Recent Ph.D. dissertations & faculty habilitations
  Compilation certifiée de scade/lustre
  Certification of a Tool Chain for Deductive Program Verification
  SMT Techniques and their Applications: from Alt-Ergo to Cubicle

Exposés en l'honneur de Laurence Puel
Jean-Christophe Filliâtre & Delia Kesner
24 October 2012 15h00

Freedom Before Commitment – A Lightweight Type System for Object Initialization
Peter Muller
14 October 2011 11h00

Lieurs canoniques en Coq
Alan Schmiitt
11 March 2011 10h00

Tactiques pour la réécriture modulo AC en Coq
Thomas Braibant
4 March 2011 10h00

Trust and cooperation in anonymity networks
Vladimiro Sassone
11 February 2011 14h00

Extending the lambda-calculus with unbind and rebind
Mariangiola Dezani
3 December 2010 10h00

Proving the Church-Turing Thesis
Nachum Dershowitz
29 November 2010 10h00

Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park)
Olivier Danvy
26 November 2010 10h00

Software engineering of abstract interpretation tools
Bertrand Jeannet
8 October 2009 10h30

Discovering Properties about Arrays in Simple Programs
Mathias Péron
17 July 2008 10h30

Extraction de programme classique dans le Calcul des Constructions
Alexandre Miquel
1 February 2008 14h00

Towards an environment for collaborative proving
Pierre Corbineau
25 January 2008 10h00

HOL-Boogie : An interactive Proof-Environment for Program-Verification via Boogie
Burkhart Wolff
18 January 2008 10h00

Résultats majeurs
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
5 July 2012

Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
22 March 2012

EATCS Award for Best ETAPs Paper 2011
30 March 2011
S. Conchon, E. Contejean and M. Iguernelala received the EATCS Award for the best paper in TCS at ETAPS'11.

Formal Verification of Floating-Point Programs
25 June 2007
By Sylvie Boldo and Jean-Christophe Filliâtre.
18th IEEE Symposium on Computer Arithmetic.

Optimizing XML querying using type-based document projection
14 October 2012
Article@ACM Transactions on Database Systems (TODS) V. Benzaken, G. Castagna, D. Colazzo, K. Nguyễn

Semantic subtyping: dealing set theoretically with function union intersection and negation types
1 September 2008
Journal of the ACM, by Benzaken, Castagna and Frisch

Static and Dynamic Semantics of NoSQL Languages, accepted at ACM POPL 2013
1 October 2012
Véronique Benzaken, Giuseppe Castagna, Kim Nguyễn, Jérôme Siméon .

Software & patents