Français Anglais
Accueil Annuaire Plan du site
Accueil > Equipes > Toutes les équipes > Toccata (Toccata)
Equipes
Toccata (Toccata)
Page non-maintenue

depuis le 30 septembre 2013
se référer à la nouvelle équipe
VALS


L'objectif de l'équipe Toccata est de proposer des méthodes et des outils pouvant s'intégrer dans le cycle de développement logiciel et permettant de produire du code correct vis-à-vis de comportements attendus.

L'équipe développe une plateforme générique de vérification de programmes (la platforme Why), qui produit des obligations de preuve à partir de programmes annotés de spécifications formelles et les transmet ensuite à des outils de preuve, interactifs ou automatiques. Des instances pour les langages C (Caduceus) et Java (Krakatoa) sont bâties sur cette infrastructure générique.

Composition de l'équipe
  Responsable
    MARCHÉ Claude

Activités de recherche
  Vérification
  Logique
  Algorithmique
  Langages et systèmes centrés données

Logiciels et brevets
  Caduceus : Outil Caduceus de vérification de programmes C
  EdiFlow : EdiFlow: workflows intéractifs pour l'analyse de données

Thèses et habilitabions récentes
  Compilation certifiée de scade/lustre
  Certification d'une chaine de vérification déductive de programmes
  SMT Techniques and their Applications: from Alt-Ergo to Cubicle

Séminaires
Exposés en l'honneur de Laurence Puel
Jean-Christophe Filliâtre & Delia Kesner
Mer. 24 octobre 2012 - 15h00


Freedom Before Commitment – A Lightweight Type System for Object Initialization
Peter Muller
Ven. 14 octobre 2011 - 11h00


Lieurs canoniques en Coq
Alan Schmiitt
Ven. 11 mars 2011 - 10h00


Tactiques pour la réécriture modulo AC en Coq
Thomas Braibant
Ven. 04 mars 2011 - 10h00


Trust and cooperation in anonymity networks
Vladimiro Sassone
Ven. 11 février 2011 - 14h00


Extending the lambda-calculus with unbind and rebind
Mariangiola Dezani
Ven. 03 décembre 2010 - 10h00


Proving the Church-Turing Thesis
Nachum Dershowitz
Lun. 29 novembre 2010 - 10h00


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


Software engineering of abstract interpretation tools
Bertrand Jeannet
Jeu. 08 octobre 2009 - 10h30


Discovering Properties about Arrays in Simple Programs
Mathias Péron
Jeu. 17 juillet 2008 - 10h30


Extraction de programme classique dans le Calcul des Constructions
Alexandre Miquel
Ven. 01 février 2008 - 14h00


Towards an environment for collaborative proving
Pierre Corbineau
Ven. 25 janvier 2008 - 10h00


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


Résultats majeurs
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
05 juillet 2012
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. IJCAR 2012

Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems
22 mars 2012
Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi, CAV 2012

EATCS Award for Best ETAPS Paper 2011
30 mars 2011
S. Conchon, E. Contejean et M. Iguernelala obtiennent le EATCS Award pour le meilleur article en informatique théorique à ETAPS'11.

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

Optimizing XML querying using type-based document projection Article@ACM Transactions on Database Systems (TODS) V. Benzaken, G. Castagna, D. Colazzo, K. Nguyễn
14 octobre 2012
XML data projection (or pruning) is a natural optimization for main memory query engines: given a query Q over a document D, the subtrees of D that are not necessary to evaluate Q are pruned, thus producing a smaller document on which Q is executed.

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

Static and Dynamic Semantics of NoSQL Languages, Accepted at ACM POPL 2013, Véronique Benzaken, Giuseppe Castagna, Kim Nguyễn, Jérôme Siméon .
01 octobre 2012
NoSQL languages are very popular in the context of cloud computing and big data analytics. The aim is to define a general framework that can both express and type such languages via an encoding into a core calculus. Each such language can in this way pres

Logiciels et brevets