CELTIQUE - 2011 - Annual activity report

CELTIQUE

CELTIQUE - 2011

Project-Team Celtique

Members

Overall Objectives

Project overview
Highlights of the Year

Scientific Foundations

Static program analysis
Software certification

Software

Javalib
SAWJA
Timbuk

New Results

Control-Flow Analysis by Abstract Interpretation
Modular SMT Proofs for Fast Reflexive Checking inside Coq
Secure the Clones: Static Enforcement of Policies for Secure Object Copying
Fault localization and correction in Constraint Programs
Floating-point constraint solving
Fast inference of polynomial invariants

Contracts and Grants with Industry

ANR DECERT project
ANR CAVERN project
ANR PiCoq project
ANR U3CAT project
The FRAE ASCERT project

Partnerships and Cooperations

Regional Initiatives
European Initiatives
International Initiatives

Dissemination

Animation of the scientific community
Teaching

Bibliography

Major publications
Publications of the year
References in notes

Home | Next next

2011 Project-Team Activity Report

CELTIQUE

Software certification with semantic analysis

Research centre: Rennes - Bretagne-Atlantique

In partnership with: CNRS, Université Rennes 1, Ecole normale supérieure de Cachan

In collaboration with: Institut de recherche en informatique et systèmes aléatoires (IRISA)

Field: Algorithmics, Programming, Software and Architecture

Theme: Programs, Verification and Proofs

Keywords: Programming Languages, Object Oriented Programming, Formal Methods, Proofs Of Programs, Security, Interactive Theorem Proving