Publications de l'équipe CELTIQUE

2012

Articles dans des revues avec comité de lecture

Titre

Control-flow analysis of function calls and returns by abstract interpretation

Auteurs

Jan Midtgaard; Thomas Jensen

Détail

Information and Computation, Elsevier, 2012, 2012, pp. 49-76

Accès au texte intégral et bibtex

Communications avec actes

Titre

Managing Execution Environment Variability during Software Testing: an industrial experience

Auteurs

Aymeric Hervieu; Benoit Baudry; Arnaud Gotlieb

Détail

International Conference on Testing Software and Systems, Nov 2012, Aalborg, Denmark. Springer

Accès au texte intégral et bibtex

Titre

Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases

Auteurs

David Cachera; Thomas Jensen; Arnaud Jobin; Florent Kirchner

Détail

SAS - 19th International Static Analysis Symposium - 2012, Sep 2012, Deauville, France.

Accès au bibtex

Titre

Formalisation de HOCore en Coq

Auteurs

Simon Boulier; Alan Schmitt

Détail

JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France.

Accès au texte intégral et bibtex

Titre

Equational Abstraction Refinement for Certified Tree Regular Model Checking

Auteurs

Yohan Boichut; Benoit Boyer; Thomas Genet; Axel Legay

Détail

ICFEM, Nov 2012, Kyoto, Japan. Springer-Verlag, pp. 299-315, LNCS

Accès au texte intégral et bibtex

Communications sans actes

Titre

Formally verified optimizing compilation in ACG-based flight control software

Auteurs

Ricardo Bedin França; Sandrine Blazy ; Denis Favre-Felix; Xavier Leroy ; Marc Pantel ; Jean Souyris

Détail

ERTS2 2012: Embedded Real Time Software and Systems, Feb 2012, Toulouse, France.

Accès au texte intégral et bibtex

Mémoires

Titre

Vérification probabiliste de résultats d'analyse statique

Auteurs

Antoine Bride

Accès au texte intégral et bibtex

Rapports

Titre

Logical Combinators for Rich Type Systems

Auteurs

Pierre Genevès ; Nabil Layaïda; Alan Schmitt

Détail

[Research Report], 2012, pp. 18. RR-8010

Accès au texte intégral et bibtex

Titre

The CompCert Memory Model, Version 2

Auteurs

Xavier Leroy ; Andrew Appel ; Sandrine Blazy ; Gordon Stewart

Détail

[Research Report], 2012, pp. 26. RR-7987

Accès au texte intégral et bibtex

Titre

Tree Regular Model Checking for Lattice-Based Automata

Auteurs

Thomas Genet; Tristan Le Gall; Axel Legay; Valérie Murat

Détail

[Technical Report], 2012, pp. 33. RT-0424

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

Proofs as Cryptography: a new interpretation of the Curry-Howard isomorphism for software certificates

Auteurs

Amrit Kumar; Pierre-Alain Fouque; Thomas Genet; Mehdi Tibouchi

Détail

Jul. 2012. 19 pages

Accès au texte intégral et bibtex

2011

Communications avec actes

Titre

PACOGEN : Automatic Generation of Pairwise Test Configurations from Feature Models

Auteurs

Aymeric Hervieu; Baudry Benoit; Arnaud Gotlieb

Détail

ISSRE, Nov 2011, Hiroshima, Japan.

Accès au bibtex

Titre

Modular SMT Proofs for Fast Reflexive Checking inside Coq

Auteurs

Frédéric Besson; Pierre-Emmanuel Cornilleau; David Pichardie

Détail

First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan, Province Of China.

Accès au texte intégral et bibtex

Titre

PACOGEN : Automatic Generation of Pairwise Test Configurations from Feature Models

Auteurs

Aymeric Hervieu; Benoit Baudry; Arnaud Gotlieb

Détail

Proc. of Int. Symp. on Soft. Reliability Engineering (ISSRE'11), Nov 2011, Hiroshima, Japan.

Accès au texte intégral et bibtex

Titre

Filtering by ULP Maximum

Auteurs

Matthieu Carlier; Arnaud Gotlieb

Détail

Proc. of the IEEE Int. Conf. on Tools for Artificial Intelligence (ICTAI'11), Nov 2011, Floride, United States.

Accès au texte intégral et bibtex

Titre

Characterizing Conclusive Approximations by Logical Formulae

Auteurs

Yohan Boichut; Thi-Bich-Hanh Dao; Valérie Murat

Détail

Giorgio Delzanno and Igor Potapov. Reachability Problems 2011, Sep 2011, Gênes, Italy. Reachability Problems (RP 2011), LNCS 6945

Accès au texte intégral et bibtex

Communications sans actes

Titre

A Flexible Proof Format for SMT: a Proposal

Auteurs

Frédéric Besson; Pascal Fontaine ; Laurent Théry

Détail

Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland.

Accès au texte intégral et bibtex

Titre

A Nelson-Oppen based Proof System using Theory Specific Proof Systems

Auteurs

Frédéric Besson; Pierre-Emmanuel Cornilleau; David Pichardie

Détail

Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland.

Accès au texte intégral et bibtex

HDR

Titre

Contributions à la génération de tests à base de contraintes

Auteurs

Arnaud Gotlieb

Détail

Université Européenne de Bretagne, Dec. 2011. French

Accès au texte intégral et bibtex

Rapports

Titre

A formally verified SSA-based compiler middle-end

Auteurs

Gilles Barthe; Delphine Demange; David Pichardie

Détail

[Research Report], 2011

Accès au texte intégral et bibtex

Titre

Negation for Free!

Auteurs

Nadjib Lazaar; Nourredine Aribi; Arnaud Gotlieb; Yahia Lebbah

Détail

[Research Report], 2011, pp. 16. RR-7749

Accès au texte intégral et bibtex

Titre

Fast inference of polynomial invariants for imperative programs

Auteurs

David Cachera; Thomas Jensen; Arnaud Jobin; Florent Kirchner

Détail

[Research Report], 2011, pp. 31. RR-7627

Accès au texte intégral et bibtex

2010

Articles dans des revues avec comité de lecture

Titre

Long-Run Cost Analysis by Approximation of Linear Operators over Dioids

Auteurs

David Cachera; Thomas Jensen; Arnaud Jobin; Pascal Sotin

Détail

Mathematical Structures in Computer Science, Cambridge University Press, 2010, 20 (4), pp. 589-624

Accès au bibtex

Titre

A Uniform Random Test Data Generator for Path Testing

Auteurs

Arnaud Gotlieb; Matthieu Petit

Détail

The Journal of Systems and Software, Elsevier, 2010, 83 (12), pp. 2618-2626

Accès au texte intégral et bibtex

Titre

Equational Approximations for Tree Automata Completion

Auteurs

Thomas Genet; Vlad Rusu

Détail

Journal of Symbolic Computation, Elsevier, 2010, 45(5):574-597, May 2010 (5), pp. 574-597

Accès au texte intégral et bibtex

Titre

Verifying Resource Access Control on Mobile Interactive Devices

Auteurs

Frédéric Besson; Guillaume Dufay; Thomas Jensen; David Pichardie

Détail

Journal of Computer Security, IOS press, 2010, 18 (6), pp. 971-998

Accès au texte intégral et bibtex

Communications avec actes

Titre

Constraint solving on modular integers

Auteurs

Arnaud Gotlieb ; Michel Leconte; Bruno Marre

Détail

ModRef Worksop, associated to CP'2010, Sep 2010, Saint-Andrews, United Kingdom.

Accès au texte intégral et bibtex

Titre

Constraint Reasoning in FocalTest

Auteurs

Mathieu Carlier; Catherine Dubois; Arnaud Gotlieb

Détail

ICSOFT, Jul 2010, Athènes, Greece.

Accès au texte intégral et bibtex

Titre

Formal Verification of Coalescing Graph-Coloring Register Allocation

Auteurs

Sandrine Blazy; Benoît Robillard; Andrew W. Appel

Détail

Andrew Gordon. 19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. Springer, 6012, pp. 145-164, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Fault Localization in Constraint Programs

Auteurs

Nadjib Lazaar; Arnaud Gotlieb; Yahia Lebbah

Détail

22th Int. Conf. on Tools with Artificial Intelligence (ICTAI'2010), 2010, Arras, France.

Accès au texte intégral et bibtex

Titre

Constraint-Based Test Input Generation for Java Bytecode

Auteurs

Florence Charreteur; Arnaud Gotlieb

Détail

Proc. of the 21st IEEE Int. Symp. on Softw. Reliability Engineering (ISSRE'10), Nov 2010, San Jose, CA, USA, United States.

Accès au texte intégral et bibtex

Titre

On Testing Constraint Programs

Auteurs

Nadjib Lazaar; Arnaud Gotlieb; Yahia Lebbah

Détail

16th Int. Conf. on Principles and Practices of Constraint Programming (CP'2010), Sep 2010, St Andrews, Scotland, United Kingdom.

Accès au texte intégral et bibtex

Titre

Explanation-based generalization of infeasible path

Auteurs

Michael Delahaye; Bernard Botella; Arnaud Gotlieb

Détail

3rd IEEE International Conference on Software Testing, Validation and Verification (ICST'10), Apr 2010, Paris, France.

Accès au texte intégral et bibtex

Titre

Constraint Based Strategies

Auteurs

Helene Kirchner; Kirchner Florent; Claude Kirchner

Détail

Santiago Escobar. 18th International Workshop on Functional and Constraint Logic Programming - WFLP 2009, Jun 2009, Brasilia, Brazil. Springer Berlin / Heidelberg, Functional and Constraint Logic Programming, 5979, pp. 13-26, 2010, Lecture Notes in Computer Science

Accès au bibtex

Titre

Enforcing Secure Object Initialization in Java

Auteurs

Laurent Hubert; Thomas Jensen; Vincent Monfort; David Pichardie

Détail

15th European Symposium on Research in Computer Security (ESORICS), 2010, Athènes, Greece. Springer-Verlag, Proceedings of ESORICS 2010, 6345, pp. 101-115, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Sawja: Static Analysis Workshop for Java

Auteurs

Laurent Hubert; Nicolas Barré; Frédéric Besson; Delphine Demange; Thomas Jensen; Vincent Monfort; David Pichardie; Tiphaine Turpin

Détail

Beckert, Bernhard and Marché, Claude. The International Conference on Formal Verification of Object-Oriented Software, 2010, Paris, France. Springer-Verlag, Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France, 2010.13, pp. 253-267, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

A Certified Denotational Abstract Interpreter

Auteurs

David Cachera; David Pichardie

Détail

International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. Springer-Verlag, 6172, pp. 9-24, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

A Provably Correct Stackless Intermediate Representation for Java Bytecode

Auteurs

Delphine Demange; Thomas Jensen; David Pichardie

Détail

The 8th Asian Symposium on Programming Languages and Systems (APLAS), 2010, Shangai, China. Springer-Verlag, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Certified Result Checking for Polyhedral Analysis of Bytecode Programs

Auteurs

Frédéric Besson; Thomas Jensen; David Pichardie; Tiphaine Turpin

Détail

The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany. Springer-Verlag, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Sécurité de la plate-forme d'exécution Java : limites et propositions d'améliorations

Auteurs

Guillaume Hiet; Frédéric Guihéry; Goulven Guiheux; David Pichardie; Christian Brunette

Détail

Symposium sur la sécurité des technologies de l'information et des communications (SSTIC), 2010, Rennes, France.

Accès au texte intégral et bibtex

Communications sans actes

Titre

On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver

Auteurs

Frédéric Besson

Détail

8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh, United Kingdom.

Accès au texte intégral et bibtex

Rapports

Titre

Equational Abstraction Refinement for Certified Tree Regular Model Checking

Auteurs

Yohan Boichut; Benoît Boyer; Thomas Genet; Axel Legay

Détail

[Technical Report], 2010

Accès au texte intégral et bibtex

Titre

On Testing Constraint Programs

Auteurs

Nadjib Lazaar; Arnaud Gotlieb; Lebbah Yahia

Détail

[Research Report], 2010. RR-7291

Accès au texte intégral et bibtex

Titre

A Provably Correct Stackless Intermediate Representation For Java Bytecode

Auteurs

Delphine Demange; Thomas Jensen; David Pichardie

Détail

[Research Report], 2010, pp. 59. RR-7021

Accès au texte intégral et bibtex

Thèses

Titre

Modélisation par contraintes de programmes en bytecode Java pour la génération automatique de tests

Auteurs

Florence Charreteur

Détail

Université Européenne de Bretagne, Mar. 2010. French

Accès au texte intégral et bibtex

2009

Articles dans des revues avec comité de lecture

Titre

Modelling Dynamic Memory Management in Constraint-Based Testing

Auteurs

Florence Charreteur; Bernard Botella; Arnaud Gotlieb

Détail

Journal of Systems and Software, Elsevier Science Inc. New York, NY, USA, 2009, 82 (11), pp. 1755-1766

Accès au texte intégral et bibtex

Titre

Soundly Handling Static Fields: Issues, Semantics and Analysis

Auteurs

Laurent Hubert; David Pichardie

Détail

Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of the Fourth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2009), 253 (5), pp. 15 - 30

Accès au texte intégral et bibtex

Communications avec actes

Titre

Control-flow analysis of function call and returns by abstract interpretation

Auteurs

Jan Midtgaard; Thomas Jensen

Détail

ACM International Conference on Functional Programming, Sep 2009, Edinburgh, United Kingdom.

Accès au texte intégral et bibtex

Titre

Vers une Théorie du Test des programmes à contraintes

Auteurs

Nadjib Lazaar; Arnaud Gotlieb; Yahia Lebbah

Détail

Cinquièmes Journées Francophones de Programmation par Contraintes, Orléans, juin 2009, Jun 2009, France. pp. 65-75

Accès au texte intégral et bibtex

Titre

Distinguish Dynamic Basic Blocks by Structural Statistical Testing

Auteurs

Matthieu Petit; Arnaud Gotlieb

Détail

Hélène WAESELYNCK. 12th European Workshop on Dependable Computing, EWDC 2009, May 2009, Toulouse, France. 8 p.

Accès au texte intégral et bibtex

Titre

A Certified Data Race Analysis for a Java-like Language

Auteurs

Frédéric Dabrowski; David Pichardie

Détail

TPHOL'09, 2009, Germany. pp. 212-227

Accès au bibtex

Titre

Certified Static Analysis by Abstract Interpretation

Auteurs

Frédéric Besson; David Cachera; Thomas Jensen; David Pichardie

Détail

Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. Springer-Verlag, FOSAD 2007/2008/2009 Tutorial Lectures, 5705, pp. 223-257, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Comparing Techniques for Certified Static Analysis

Auteurs

David Cachera; David Pichardie

Détail

The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. NASA Ames Research Center, pp. 111-115

Accès au texte intégral et bibtex

HDR

Titre

Analyse d'atteignabilité en réécriture pour la vérification de programmes

Auteurs

Thomas Genet

Détail

Université Rennes 1, Nov. 2009. English

Accès au texte intégral et bibtex

Rapports

Titre

Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation

Auteurs

Jan Midtgaard; Thomas P. Jensen

Détail

[Research Report], 2009. RR-6681

Accès au texte intégral et bibtex

Titre

Computing the Least Fix-point Semantics of Definite Logic Programs Using BDDs

Auteurs

Frédéric Besson; Thomas Jensen; Tiphaine Turpin

Détail

[Research Report], 2009, pp. 25. PI 1939

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

Equational Approximations for Tree Automata Completion

Auteurs

Thomas Genet; Vlad Rusu

Détail

Mar. 2009. 33 pages

Accès au texte intégral et bibtex

2008

Communications avec actes

Titre

A Non-Null Annotation Inferencer for Java Bytecode

Auteurs

Laurent Hubert

Détail

Shriram Krishnamurthi and Michal Young. PASTE: Program analysis for software tools and engineering, Nov 2008, Atlanta, Georgia, United States. ACM, Proceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp. 10.1145/1512475.1512484

Accès au texte intégral et bibtex

1999

Communications avec actes

Titre

Polyhedral Analysis for Synchronous Languages

Auteurs

Frédéric Besson; Thomas Jensen; Jean-Pierre Talpin

Détail

6th International Symposium on Static Analysis (SAS'99), Sep 1999, Venice, Italy. Springer-Verlag, pp. 51-68, LNCS vol. 1694

Accès au texte intégral et bibtex

1998

Articles dans des revues avec comité de lecture

Titre

Dynamic optimization of interval narrowing algorithms

Auteurs

Olivier Lhomme; Arnaud Gotlieb; Michel Rueher

Détail

The Journal of Logic Programming, Elsevier, 1998, 37 (1-3), pp. 165-183

Accès au texte intégral et bibtex