Publications

Publications HAL de la structure celtique

2017

Journal articles

titre
LLFP : A Logical Framework for modeling External Evidence, Side Conditions, and Proof Irrelevance using Monads
auteur
Furio Honsell, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, Special Issue in honor of Pierre Louis Curien, <http://www.lmcs-online.org/index.php>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01146059/file/LLFP_LMCS.pdf BibTex

Conference papers

titre
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines
auteur
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt
article
LICS 2017, Jun 2017, Reykjavik, Iceland. Proceedings of LICS 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01479035/file/lics.pdf BibTex
titre
Closing the Gap – The Formally Verified Optimizing Compiler CompCert
auteur
Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, Christian Ferdinand
article
SSS’17: Safety-critical Systems Symposium 2017, Feb 2017, Bristol, United Kingdom. CreateSpace, pp.163-180, 2017, Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01399482/file/SSS2017_kaestner_et_al.pdf BibTex
titre
Non-Interference through Annotated Multisemantics
auteur
Gurvan Cabon, Alan Schmitt
article
28ièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01503094/file/cabon_schmitt.pdf BibTex

Reports

titre
Automata Completion and Regularity Preservation
auteur
Thomas Genet
article
[Research Report] IRISA, Inria Rennes. 2017
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01501744/file/main.pdf BibTex
titre
Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines
auteur
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt
article
[Research Report] RR-9052, Inria. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01507625/file/RR-9052.pdf BibTex
titre
A Short Isabelle/HOL Tutorial for the Functional Programmer
auteur
Thomas Genet
article
[Research Report] IRISA. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01208577/file/main%20%281%29.pdf BibTex

2016

Journal articles

titre
A Verified Information-Flow Architecture
auteur
Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
article
Journal of Computer Security (JCS); Special Issue on Verified Information Flow Security, 2016, 24 (6), pp.689–734. <10.3233/JCS-15784>
Accès au bibtex
https://arxiv.org/pdf/1509.06503 BibTex
titre
Using JavaScript Monitoring to Prevent Device Fingerprinting
auteur
Nataliia Bielova, Frédéric Besson, Thomas Jensen
article
ERCIM News, ERCIM, 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01353997/file/final.pdf BibTex
titre
Improving static analyses of C programs with conditional predicates
auteur
Sandrine Blazy, David Bühler, Boris Yakobowski
article
Science of Computer Programming, Elsevier, 2016, 118, <10.1145/2854065.2854082>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01242077/file/elsmain.pdf BibTex
titre
Termination criteria for tree automata completion
auteur
Thomas Genet
article
Journal of Logic and Algebraic Methods in Programming, Elsevier, 2016, 85, Issue 1, part 1, pp.3-33. <10.1016/j.jlamp.2015.05.003>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01194533/file/Genet-JLAMP15.pdf BibTex
titre
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
auteur
Sandrine Blazy, Vincent Laporte, David Pichardie
article
Journal of Automated Reasoning, Springer Verlag, 2016, 56 (3), pp.26. <10.1007/s10817-015-9359-8>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01243700/file/main.pdf BibTex

Conference papers

titre
An Abstract Memory Functor for Verified C Static Analyzers
auteur
Sandrine Blazy, Vincent Laporte, David Pichardie
article
ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. ACM, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), pp.14, 2016, <http://conf.researchr.org/home/icfp-2016/>. <10.1145/2951913.2951937>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01339969/file/main.pdf BibTex
titre
An Extended Buffered Memory Model With Full Reorderings
auteur
Gurvan Cabon, David Cachera, David Pichardie
article
FtFjp – Ecoop workshop, Jul 2016, Rome, Italy. pp.1 – 6, 2016, <10.1145/2955811.2955816>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01379514/file/versionHAL.pdf BibTex
titre
Correlating Structured Inputs and Outputs in Functional Specifications
auteur
Andreescu Oana, Thomas Jensen, Stéphane Lescuyer
article
Software Engineering and Formal Methods , Jul 2016, Vienna, Austria. Springer, Springer LNCS 9763, pp.19, 2016, 14th Int. Software Engineering and Formal Methods conference. <10.1007/978-3-319-41591-8_7>
Accès au bibtex
BibTex
titre
A Certified Compiler for Verifiable Computing
auteur
Cédric Fournet, Chantal Keller, Vincent Laporte
article
IEEE 29th Computer Security Foundations Symposium, CSF 2016, Jun 2016, Lisbonne, Portugal. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01397680/file/csf16.pdf BibTex
titre
Modeling and Abstraction of Memory Management in a Hypervisor
auteur
Pauline Bolignano, Thomas Jensen, Vincent Siles
article
Fundamental Approaches to Software Engineering (FASE’16), Apr 2016, Eindhoven, Netherlands. Springer, Springer LNCS 9633, pp.214 – 230, 2016, Proc. of Fundamental Approaches to Software Engineering (FASE’16). <10.1007/978-3-662-49665-7_13>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01394174/file/HypFASE.pdf BibTex
titre
Mechanizing conventional SSA for a verified destruction with coalescing
auteur
Delphine Demange, Yon Fernandez de Retana
article
25th International Conference on Compiler Construction, Mar 2016, Barcelona, Spain. Proceedings of the 25th International Conference on Compiler Construction
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01378393/file/main.pdf BibTex
titre
An Abstract Separation Logic for Interlinked Extensible Records
auteur
Martin Bodin, Thomas Jensen, Alan Schmitt
article
Julien Signoles. Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint-Malo, France. 27es Journées Francophones des Langages Applicatifs, 2016
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01333600/file/main.pdf BibTex
titre
CompCert – A Formally Verified Optimizing Compiler
auteur
Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, Christian Ferdinand
article
ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse, France. <http://www.erts2016.org/>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01238879/file/erts2016_compcert.pdf BibTex
titre
Formal Verification of Control-flow Graph Flattening
auteur
Sandrine Blazy, Alix Trieu
article
ACM. Certified Proofs and Programs (CPP 2016), Jan 2016, Saint-Petersburg, United States. pp.12, 2016, Certified Proofs and Programs (CPP 2016). <https://people.csail.mit.edu/adamc/cpp16/index.html>. <10.1145/2854065.2854082>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01242063/file/cpp2016.pdf BibTex
titre
Hybrid Monitoring of Attacker Knowledge
auteur
Frédéric Besson, Nataliia Bielova, Thomas Jensen
article
29th IEEE Computer Security Foundations Symposium, 2016, Lisboa, Portugal
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01310572/file/hybrid_monitoring_of_attacker_knowledge.pdf BibTex

Directions of work or proceedings

titre
Verified Software: Theories, Tools, and Experiments – 8th International Conference, VSTTE 2016, Toronto, Canada, July 17-18, 2016. Proceedings
auteur
Sandrine Blazy, Marsha Chechik
article
Blazy, Sandrine and Chéchia, Marsha. Verified Software: Theories, Tools, and Experiments – 8th International Conference, VSTTE 2016, Jul 2016, Toronto, Canada. 9971, Springer, 2016, Lecture Notes in Computer Science
Accès au bibtex
BibTex

Theses

titre
Certified semantics and analysis of JavaScript
auteur
Martin Bodin
article
Programming Languages [cs.PL]. Université Rennes 1, 2016. English. <NNT : 2016REN1S087>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01478722/file/BODIN_Martin.pdf BibTex
titre
Formally verified compilation of low-level C code
auteur
Pierre Wilke
article
Programming Languages [cs.PL]. Université Rennes 1, 2016. English. <NNT : 2016REN1S088>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01483676/file/WILKE_Pierre.pdf BibTex

2015

Journal articles

titre
Analyzing the exhaustiveness of the synapse protocol
auteur
Bojan Marinkovic, Vincenzo Ciancaglini, Zoran Ognjanovic, Paola Glavan, Luigi Liquori, Petar Maksimovic
article
Peer-to-Peer Networking and Applications, Springer, Springer, 2015, Includes a Special Issue on Cloud, Grid, P2P, and Internet Computing, 8 (5), pp.793–806. <10.1007/s12083-014-0293-z>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01146050/file/2014-p2p-net-and-apps-14.pdf BibTex
titre
Efficiently Deciding µ-calculus with Converse over Finite Trees
auteur
Pierre Genevès, Nabil Layaïda, Alan Schmitt, Nils Gesbert
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2015, 16 (2), pp.41. <http://tocl.acm.org/>. <10.1145/2724712>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00868722/file/tree-calculus.pdf BibTex

Conference papers

titre
An ω-Algebra for Real-Time Energy Problems
auteur
David Cachera, Uli Fahrenberg, Axel Legay
article
35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2015, Bengaluru, India. 2015, <http://www.fsttcs.org/>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01237667/file/main.pdf BibTex
titre
Dependency Analysis of Functional Specifications with Algebraic Data Structures
auteur
Thomas Jensen, Stephane Lescuyer, Andreescu Oana
article
17th International Conference on Formal Engineering Methods, ICFEM 2015, Nov 2015, Paris, France. Springer Verlag, Proc. of 17th International Conference on Formal Engineering Methods (ICFEM 2015), Springer LNCS vol. 9407, 9407, pp.18, 2015, Springer LNCS. <10.1007/978-3-319-25423-4_8>
Accès au bibtex
BibTex
titre
Data Tainting and Obfuscation: Improving Plausibility of Incorrect Taint
auteur
Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent
article
IEEE. Source Code Analysis and Manipulation (SCAM), Sep 2015, Bremen, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01193286/file/SCAM_v2.pdf BibTex
titre
Howe’s Method for Contextual Semantics
auteur
Sergueï Lenglet, Alan Schmitt
article
CONCUR 2015 26th International Conference on Concurrency Theory, Sep 2015, Madrid, Spain. <10.4230/LIPIcs.CONCUR.2015.212>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01192699/file/Concur%2015.pdf BibTex
titre
Hybrid Typing of Secure Information Flow in a JavaScript-like Language
auteur
José Fragoso Santos, Thomas Jensen, Tamara Rezk, Alan Schmitt
article
International Symposium on Trustworthy Global Computing, Aug 2015, Madrid, Spain. Proceedings of the 10th International Symposium on Trustworthy Global Computing (TGC 2015)
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01243029/file/paper_7.pdf BibTex
titre
Validating Dominator Trees for a Fast, Verified Dominance Test
auteur
Sandrine Blazy, Delphine Demange, David Pichardie
article
Springer. Interactive Theorem Proving, Aug 2015, Nanjing, China. Lecture Notes in Computer Science (LNCS) (9236), 2015, <10.1007/978-3-319-22102-1_6>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01193281/file/main.pdf BibTex
titre
A Concrete Memory Model for CompCert
auteur
Frédéric Besson, Sandrine Blazy, Pierre Wilke
article
Springer. ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. Lecture Notes in Computer Science (LNCS) (9236), pp.67-83, 2015, nteractive Theorem Proving. <10.1007/978-3-319-22102-1_5>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01194549/file/paper.pdf BibTex
titre
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks
auteur
Furio Honsell, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto
article
LFMTP’15. 9th International Workshop on Logical Frameworks and Meta-languages, Berlin, Germany, Aug 2015, Berlin, Germany. Electronic Proceedings in Theoretical Computer Science (EPTCS), 2015, <10.4204/EPTCS.185.1>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01170029/file/Paper-LFMTP-15.pdf BibTex
titre
HOCore in Coq
auteur
Petar Maksimovic, Alan Schmitt
article
Interactive Theorem Proving, Aug 2015, Nanjing, China. Springer, Proceedings of the 6th conference on Interactive Theorem Proving (ITP 2015), 9236, 2015, Proceedings of the 6th conference on Interactive Theorem Proving (ITP 2015). <10.1007/978-3-319-22102-1_19>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01243017/file/HOCore_ITP_final.pdf BibTex
titre
Expressive Logical Combinators for Free
auteur
Pierre Genevès, Alan Schmitt
article
International Joint Conference on Artificial Intelligence (IJCAI 2015), Jul 2015, Buenos Aires, Argentina
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00868724/file/Lean-ijcai15.pdf BibTex
titre
Attack Trees with Sequential Conjunction
auteur
Barbara Kordy, Ravi Jhawar, Sjouke Mauw, Sasa Radomirovic, Roland Trujillo-Rasua
article
Hannes Federrath; Dieter Gollmann. 30th IFIP International Information Security Conference (SEC), May 2015, Hamburg, Germany. Springer, IFIP Advances in Information and Communication Technology, AICT-455, pp.339-353, 2015, ICT Systems Security and Privacy Protection. <https://ifipsec.org/2015/>. <10.1007/978-3-319-18467-8_23>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01197256/file/337885_1_En_23_Chapter.pdf BibTex
titre
Kharon : Découvrir, comprendre et reconnaître des malware Android par suivi de flux d’information
auteur
Radoniaina Andriatsimandefitra Ratsisahanana, Thomas Genet, Laurent Guillo, Jean-François Lalande, David Pichardie, Valérie Viet Triem Tong
article
Rendez-vous de la Recherche et de l’Enseignement de la Sécurité des Systèmes d’Information, May 2015, Troyes, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01154368/file/kharon.pdf BibTex
titre
A formally-verified C static analyzer
auteur
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
article
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. ACM, pp.247-259, <10.1145/2676726.2676966>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01078386/file/verasco-popl2015.pdf BibTex
titre
Certified Abstract Interpretation with Pretty-Big-Step Semantics
auteur
Martin Bodin, Thomas Jensen, Alan Schmitt
article
Certified Programs and Proofs (CPP 2015), Jan 2015, Mumbai, India. Proceedings of the 2015 Conference on Certified Programs and Proofs. <10.1145/2676724.2693174>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01111588/file/BodinJensenSchmitt-CPP%202015-Certified%20Abstract%20Interpretation%20with%20Pretty-Big-Step%20Semantics-rpx.pdf BibTex
titre
HOCore in Coq
auteur
Martín Escarrá, Petar Maksimović, Alan Schmitt
article
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d’Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), <http://jfla.inria.fr/2015>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01099130/file/jfla15_submission_14.pdf BibTex
titre
Formal verification of compilers and static analyzers.
auteur
Sandrine Blazy
article
PLMW@POPL 2015 – Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India
Accès au bibtex
BibTex
titre
Verifying a Real-Time Language with Constraints
auteur
Anicet Bart, Charlotte Truchet, Eric Monfroy
article
27th IEEE International Conference on Tools with Artificial Intelligence, 2015, Vietri sul Mare, Italy
Accès au bibtex
BibTex
titre
Verifying Fast and Sparse SSA-based Optimizations in Coq.
auteur
Delphine Demange, David Pichardie, Léo Stefanesco
article
24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom. 2015
Accès au bibtex
BibTex
titre
Verified Validation of Program Slicing
auteur
Sandrine Blazy, Andre Maroneze, David Pichardie
article
CPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, <10.1145/2676724.2693169>
Accès au bibtex
BibTex
titre
Vers un outil de vérification formelle légere pour OCaml
auteur
Thomas Genet, Barbara Kordy, Amaury Vansyngel
article
AFADL, 2015, Bordeaux, France. pp.6
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01194538/file/GenetKordyVansyngel-AFADL15.pdf BibTex
titre
Reachability Analysis of Innermost Rewriting
auteur
Thomas Genet, Yann Salmon
article
RTA, 2015, Warshaw, Poland. pp.1-17, 2015, <10.4230/LIPIcs.RTA.2015.x>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01194530/file/GenetSalmon-RTA15.pdf BibTex

Directions of work or proceedings

titre
Static Analysis Symposium – 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015. Proceedings
auteur
Sandrine Blazy, Thomas Jensen
article
Sandrine Blazy, Thomas Jensen. Static Analysis Symposium – 22nd International Symposium, SAS 2015, Aug 2015, Saint-Malo, France. Lecture Notes in Computer Science (LNCS) (9291), Springer, pp.335, 2015, 978-3-662-48287-2. <sas2015.inria.fr>
Accès au bibtex
BibTex

Reports

titre
A Short SPAN+AVISPA Tutorial
auteur
Thomas Genet
article
[Research Report] IRISA. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01213074/file/main.pdf BibTex
titre
Howe’s Method for Contextual Semantics
auteur
Sergueï Lenglet, Alan Schmitt
article
[Research Report] RR-8750, Inria. 2015, pp.31
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01168865/file/RR-8750.pdf BibTex

Theses

titre
Analyse d’atteignabilité pour les programmes fonctionnels avec stratégie d’évaluation en profondeur
auteur
Yann Salmon
article
Théorie et langage formel [cs.FL]. Université de Rennes 1, 2015. Français. <NNT : 2015REN1S085>
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01250252/file/Final.final.pdf BibTex
titre
Analyse d’atteignabilité pour les programmes fonctionnels avec stratégie d’évaluation en profondeur
auteur
Yann Salmon
article
Performance et fiabilité [cs.PF]. Université Rennes 1, 2015. Français. <NNT : 2015REN1S085>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01293819/file/SALMON_Yann.pdf BibTex
titre
Verified static analyzes for low-level languages
auteur
Vincent Laporte
article
Programming Languages [cs.PL]. Université Rennes 1, 2015. English. <NNT : 2015REN1S078>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01285624/file/LAPORTE_Vincent.pdf BibTex

2014

Journal articles

titre
Atomicity Refinement for Verified Compilation
auteur
Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, pp.30
Accès au bibtex
BibTex
titre
Formal Verification of an SSA-based Middle-end for CompCert
auteur
Gilles Barthe, Delphine Demange, David Pichardie
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (1), pp.35. <10.1145/2579080>
Accès au bibtex
BibTex
titre
Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases
auteur
David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner
article
Science of Computer Programming, Elsevier, 2014, 93, pp.21. <10.1016/j.scico.2014.02.028>
Accès au bibtex
BibTex

Conference papers

titre
GLV/GLS Decomposition, Power Analysis, and Attacks on ECDSA Signatures with Single-Bit Nonce Bias
auteur
Diego Aranha, Pierre-Alain Fouque, Benoit Gérard, Jean-Gabriel Kammerer, Mehdi Tibouchi, Jean-Christophe Zapalowicz
article
Palash Sarkar, Tetsu Iwata. Advances in Cryptology – ASIACRYPT 2014 – 20th International Conference on the Theory and Application of Cryptology and Information Security, Dec 2014, Kaoshiung, Taiwan. Springer, Advances in Cryptologie – ASIACRYPT 2014, 8873, pp.262-281, 2014, Lecture Notes in Computer Science. <http://des.cse.nsysu.edu.tw/asiacrypt2014/>. <10.1007/978-3-662-45611-8_14>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094002/file/main.pdf BibTex
titre
System-level Non-interference for Constant-time Cryptography
auteur
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie
article
ACM SIGSAC Conference on Computer and Communications Security, CCS’14, Nov 2014, Scottsdale, United States. ACM, pp.1267 – 1279, 2014, <http://www.sigsac.org/ccs/CCS2014/>. <10.1145/2660267.2660283>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01101950/file/ccs14.pdf BibTex
titre
Synthesis of Fault Attacks on Cryptographic Implementations
auteur
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
article
ACM CCS 2014, Nov 2014, Scottsdale, United States. ACM, pp.16, 2014, ACM SIGSAC Conference on Computer and Communications Security. <http://www.sigsac.org/ccs/CCS2014/>. <10.1145/2660267.2660304>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094034/file/paper.pdf BibTex
titre
Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach
auteur
Frédéric Besson, Nataliia Bielova, Thomas Jensen
article
Nordic Conference on Secure IT Systems (NordSec 2014), Oct 2014, Tromsø, Norway. 2014, <10.1007/978-3-319-11599-3_11>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081037/file/enforcing_abstract.pdf BibTex
titre
Making RSA–PSS Provably Secure against Non-random Faults
auteur
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Mehdi Tibouchi, Jean-Christophe Zapalowicz, Benjamin Grégoire
article
Cryptographic Hardware and Embedded Systems – 2014, Sep 2014, Busan, South Korea. Springer, LNCS 8731, pp.206 – 222, 2014, CHES 2014. <http://www.chesworkshop.org/ches2014/start.php>. <10.1007/978-3-662-44709-3_12>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094057/file/FaultRSA.pdf BibTex
titre
A Probabilistic Framework for Security Scenarios with Dependent Actions
auteur
Barbara Kordy, Marc Pouly, Patrick Schweitzer
article
Elvira Albert and Emil Sekerinski. Integrated Formal Methods, Sep 2014, Bertinoro, Italy. Springer, Lecture Notes in Computer Science (8739), pp.256 – 271, 2014, Integrated Formal Methods – 11th International Conference, IFM 2014. <http://ifm2014.cs.unibo.it/>. <10.1007/978-3-319-10181-1_16>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01093276/file/iFM14.pdf BibTex
titre
Improving static analyses of C programs with conditional predicates
auteur
Sandrine Blazy, David Bühler, Boris Yakobowski
article
FMICS 2014: Formal Methods for Industrial Critical Systems, Sep 2014, Florence, Italy. Lecture Notes in Computer Science (LNCS) (8718), pp.15, 2014, FMICS 2014: Formal Methods for Industrial Critical Systems. <http://fmics2014.unifi.it>. <10.1007/978-3-319-10702-8_10>
Accès au bibtex
BibTex
titre
Binary Elligator Squared
auteur
Diego Aranha, Pierre-Alain Fouque, Chen Qian, Mehdi Tibouchi, Jean-Christophe Zapalowicz
article
Selected Areas in Cryptography 2014, Aug 2014, Montreal, Canada. Springer, LNCS 8781, pp.17, 2014, SAC 2014. <10.1007/978-3-319-13051-4_2>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094083/file/ACFT14.pdf BibTex
titre
Statistical Properties of Short RSA Distribution and Their Cryptographic Applications
auteur
Pierre-Alain Fouque, Jean-Christophe Zapalowicz
article
Computing and Combinatorics, Aug 2014, Atlanta, United States. Springer, LNCS 8591, pp.525 – 536, 2014, COCOON 2014. <10.1007/978-3-319-08783-2_45>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094059/file/micali.pdf BibTex
titre
A Formally Verified WCET Estimation Tool
auteur
André Oliveira Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut
article
14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. 2014, <http://www.uni-ulm.de/en/in/wcet2014.html>. <10.4230/OASIcs.WCET.2014.11>
Accès au bibtex
BibTex
titre
Towards Static Analysis of Functional Programs Using Tree Automata Completion
auteur
Thomas Genet
article
Workshop on Rewriting Logic and its Applications, Apr 2014, Grenoble, France. Springer, Lecture Notes in Computer Science, 8663, pp.147 – 161, 2014, 10th International Workshop on Rewriting Logic and its Applications. <10.1007/978-3-319-12904-4_8>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01089993/file/Genet-WRLA14.pdf BibTex
titre
Measuring the Robustness of Source Program Obfuscation – Studying the Impact of Compiler Optimizations on the Obfuscation of C Programs
auteur
Sandrine Blazy, Stéphanie Riaud
article
Fourth ACM Conference on Data and Application Security and Privacy – SIGSAC ACM CODASPY 2014, Mar 2014, San Antonio, United States. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00927427/file/codasp01-blazy.pdf BibTex
titre
A Trusted Mechanised JavaScript Specification
auteur
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith
article
POPL 2014 – 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00910135/file/jscert_popl.pdf BibTex
titre
Pretty-big-step-semantics-based Certified Abstract Interpretation
auteur
Martin Bodin, Thomas Jensen, Alan Schmitt
article
JFLA – 25ème Journées Francophones des Langages Applicatifs – 2014, Jan 2014, Fréjus, France. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00927400/file/essay.pdf BibTex
titre
De la KAM avec un Processus d’Ordre Supérieur
auteur
Damien Pous, Alan Schmitt
article
JFLAs 2014, Jan 2014, Fréjus, France. pp.1-12, 2014, Actes des 25èmes Journées Francophones des Langages Applicatifs
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00966097/file/breakingbad.pdf BibTex
titre
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
auteur
Sandrine Blazy, Vincent Laporte, David Pichardie
article
The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. Springer, 8558, pp.128 – 143, 2014, LNCS : Interactive Theorem Proving. <10.1007/978-3-319-08970-6_9>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102445/file/itp14.pdf BibTex
titre
SawjaCard: A Static Analysis Tool for Certifying Java Card Applications
auteur
Frédéric Besson, Thomas Jensen, Pierre Vittet
article
21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. Springer, 8858, pp.51 – 67, 2014, <10.1007/978-3-319-10936-7_4>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093327/file/sawjacard.pdf BibTex
titre
A Verified Information-Flow Architecture
auteur
Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
article
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. 2014, <10.1145/2535838.2535839>
Accès au bibtex
BibTex
titre
A Precise and Abstract Memory Model for C Using Symbolic Values
auteur
Frédéric Besson, Sandrine Blazy, Pierre Wilke
article
12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. Springer, 8858, pp.449 – 468, 2014, LNCS. <10.1007/978-3-319-12736-1_24>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093312/file/symbolic.pdf BibTex

Book sections

titre
The CompCert memory model
auteur
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart
article
Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010
Accès au bibtex
BibTex

Master thesis

titre
Security analysis of Android applications
auteur
Bertrand Bonnefoy-Claudet
article
Formal Languages and Automata Theory [cs.FL]. 2014
Accès au texte intégral et bibtex
https://dumas.ccsd.cnrs.fr/dumas-01088788/file/mri20132014_submission_85.pdf BibTex

Reports

titre
A Note on the Precision of the Tree Automata Completion
auteur
Thomas Genet
article
[Research Report] IRISA. 2014, pp.13
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091393/file/Notes.pdf BibTex
titre
Enforcing Browser Anonymity with Quantitative Information Flow
auteur
Frédéric Besson, Nataliia Bielova, Thomas Jensen
article
[Research Report] RR-8532, INRIA. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00984654/file/RR-8532.pdf BibTex

Theses

titre
Security of the pseudorandom number generators and implementations of public key signature schemes
auteur
Jean-Christophe Zapalowicz
article
Cryptography and Security [cs.CR]. Université Rennes 1, 2014. English. <NNT : 2014REN1S103>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01135998/file/ZAPALOWICZ_JeanChristophe.pdf BibTex
titre
Extensions des automates d’arbres pour la vérification de systèmes à états infinis
auteur
Valérie Murat
article
Performance et fiabilité [cs.PF]. Université Rennes 1, 2014. Français. <NNT : 2014REN1S033>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01065696/file/MURAT_Valerie.pdf BibTex

2013

Journal articles

titre
A certified lightweight non-interference Java bytecode verifier
auteur
Gilles Barthe, David Pichardie, Tamara Rezk
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (5), pp.1032-1081. <10.1017/S0960129512000850>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00915189/file/barthe_pichardie_rezk_2010_v2.pdf BibTex
titre
Survey on JavaScript Security Policies and their Enforcement Mechanisms in a Web Browser
auteur
Nataliia Bielova
article
Journal of Logic and Algebraic Programming, Elsevier, 2013, Automated Specification and Verification of Web Systems, 82 (8), pp.243-262. <10.1016/j.jlap.2013.05.001>
Accès au bibtex
BibTex

Conference papers

titre
Recovering Private Keys Generated with Weak PRNGs
auteur
Pierre-Alain Fouque, Mehdi Tibouchi, Jean-Christophe Zapalowicz
article
Cryptography and Coding – 14th International Conference, Dec 2013, Oxford, United Kingdom. Springer, LNCS 8308, pp.158 – 172, 2013, IMACC 2013. <10.1007/978-3-642-45239-0_10>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094296/file/FTZ13.pdf BibTex
titre
Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq
auteur
Jael Kriener, Andy King, Sandrine Blazy
article
Tom Schrijvers. 15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Sep 2013, Madrid, Spain. ACM, pp.37-48, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00908848/file/main.pdf BibTex
titre
Practical Pairwise Testing for Software Product Lines
auteur
Dusica Marijan, Arnaud Gotlieb, Sagar Sen, Aymeric Hervieu
article
SPLC 2013, Aug 2013, Tokyo, Japan. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00859438/file/splc2013_submission_63_2_.pdf BibTex
titre
Tree Regular Model Checking for Lattice-Based Automata
auteur
Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat
article
CIAA – 18th International Conference on Implementation and Application of Automata, Jul 2013, Halifax, Canada. Springer, 7982, 2013, LNCS
Accès au bibtex
BibTex
titre
Time/Memory/Data Tradeoffs for Variants of the RSA Problem
auteur
Pierre-Alain Fouque, Damien Vergnaud, Jean-Christophe Zapalowicz
article
Computing and Combinatorics, 19th International Conference, COCOON 2013, Jun 2013, Hangzhou, China. LNCS 7936, pp.651-662, 2013, Computing and Combinatorics, 19th International Conference, COCOON 2013, Hangzhou, China, June 21-23, 2013. Proceedings. <10.1007/978-3-642-38768-5_57>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094301/file/FVZ13.pdf BibTex
titre
Formal Verification of a C Value Analysis Based on Abstract Interpretation
auteur
Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
article
Manuel Fahndrich and Francesco Logozzo. SAS – 20th Static Analysis Symposium, Jun 2013, Seattle, United States. Springer, Lecture Notes in Computer Science, pp.324-344, 2013, 7935
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00812515/file/paper.pdf BibTex
titre
Formal Verification of Loop Bound Estimation for WCET Analysis
auteur
Sandrine Blazy, André Maroneze, David Pichardie
article
Ernie Cohen and Andrey Rybalchenko. VSTTE – Verified Software: Theories, Tools and Experiments, May 2013, Menlo Park, United States. Springer, 8164, pp.281-303, 2013, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00848703/file/paper.pdf BibTex
titre
Concurrent Flexible Reversibility
auteur
Ivan Lanese, Michaël Lienhardt, Claudio Mezzina, Alan Schmitt, Jean-Bernard Stefani
article
Matthias Felleisen and Philippa Gardner. 22nd European Symposium on Programming, ESOP 2013, Mar 2013, Rome, Italy. Springer, 7792, pp.370-390, 2013, Lecture Notes in Computer Science (LNCS); Programming Languages and Systems. <10.1007/978-3-642-37036-6_21>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00811629/file/crop.pdf BibTex
titre
Symbolic Path-Oriented Test Data Generation for Floating-Point Programs
auteur
Roberto Bagnara, Matthieu Carlier, Roberta Gori, Arnaud Gotlieb
article
Proc. of the 6th IEEE Int. Conf. on Software Testing, Verification and Validation (ICST’13), Mar 2013, Luxembourg, Luxembourg. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00807884/file/ICST2013_Symbolic_Path-Oriented_Test_Data_Generation_for_Floating-Point_Programs.pdf BibTex
titre
A Certified JavaScript Interpreter
auteur
Martin Bodin, Alan Schmitt
article
Damien Pous and Christine Tasson. JFLA – Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00779459/file/jfla2013-06.pdf BibTex
titre
Plan B: A Buffered Memory Model for Java
auteur
Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, Jan Vitek
article
Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Jan 2013, Rome, Italy. ACM, 2013
Accès au bibtex
BibTex
titre
Hybrid Information Flow Monitoring Against Web Tracking
auteur
Frédéric Besson, Nataliia Bielova, Thomas Jensen
article
CSF – 2013 IEEE 26th Computer Security Foundations Symposium, 2013, New Orleans, United States. 2013, <10.1109/CSF.2013.23>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924138/file/hybrid_information_flow_monitoring_against_web_tracking.pdf BibTex
titre
Result Certification of Static Program Analysers with Automated Theorem Provers
auteur
Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen
article
VSTTE 2013 – Fifth Working Conference on Verified Software: Theories, Tools and Experiments, 2013, Atherthon, United States. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00924167/file/result_certification_of_static_program_analysers_with_automated_theorem_provers.pdf BibTex

Books

titre
Interactive Theorem Proving – 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings
auteur
Sandrine Blazy, Christine Paulin-Mohring, David Pichardie
article
Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Springer, 7998, pp.500, 2013, Lecture Notes in Computer Science, <10.1007/978-3-642-39634-2>
Accès au bibtex
BibTex

Reports

titre
Towards Static Analysis of Functional Programs using Tree Automata Completion
auteur
Thomas Genet
article
[Research Report] 2013, pp.15
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00921814/file/main.pdf BibTex
titre
Reachability Analysis of Innermost Rewriting
auteur
Thomas Genet, Yann Salmon
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00848260/file/main.pdf BibTex
titre
Tree Automata Completion for Static Analysis of Functional Programs
auteur
Thomas Genet, Yann Salmon
article
2013
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00780124/file/main.pdf BibTex
titre
Scenario realizability with constraint optimization
auteur
Rouwaida Abdallah, Arnaud Gotlieb, Loïc Hélouët, Claude Jard
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00769656/file/FASE.pdf BibTex

Theses

titre
Static analysis of numerical properties in the presence of pointers
auteur
Zhoulai Fu
article
Other [cs.OH]. Université Rennes 1, 2013. English. <NNT : 2013REN1S060>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00918593/file/FU_Zhoulai.pdf BibTex
titre
Certification of static analysis in many-sorted first-order logic
auteur
Pierre-Emmanuel Cornilleau
article
Other [cs.OH]. École normale supérieure de Cachan – ENS Cachan, 2013. English. <NNT : 2013DENS0012>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00846347/file/Cornilleau2013.pdf BibTex

2012

Journal articles

titre
Secure the Clones
auteur
Thomas Jensen, Florent Kirchner, David Pichardie
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (2)
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00762377/file/final.pdf BibTex
titre
À propos des compilateurs
auteur
Sandrine Blazy, Joanna Jongwane
article
Interstices, INRIA, 2012
Accès au bibtex
BibTex
titre
Control-flow analysis of function calls and returns by abstract interpretation
auteur
Jan Midtgaard, Thomas Jensen
article
Information and Computation, Elsevier, 2012, 2012, pp.49-76. <10.1016/j.ic.2011.11.005>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00758152/file/artikel.pdf BibTex

Conference papers

titre
Managing Execution Environment Variability during Software Testing: an industrial experience
auteur
Aymeric Hervieu, Benoit Baudry, Arnaud Gotlieb
article
International Conference on Testing Software and Systems, Nov 2012, Aalborg, Denmark. Springer, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00726137/file/ICTSS_HBG_12.pdf BibTex
titre
Equational Abstraction Refinement for Certified Tree Regular Model Checking
auteur
Yohan Boichut, Benoit Boyer, Thomas Genet, Axel Legay
article
ICFEM, Nov 2012, Kyoto, Japan. Springer-Verlag, pp.299-315, 2012, LNCS
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00759149/file/BoichutBGL-ICFEM12.pdf BibTex
titre
Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases
auteur
David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner
article
SAS – 19th International Static Analysis Symposium – 2012, Sep 2012, Deauville, France. 2012
Accès au bibtex
BibTex
titre
Attacking RSA–CRT Signatures with Faults on Montgomery Multiplication
auteur
Pierre-Alain Fouque, Nicolas Guillermin, Delphine Leresteux, Mehdi Tibouchi, Jean-Christophe Zapalowicz
article
Cryptographic Hardware and Embedded Systems – 2012, Sep 2012, Leuven, Belgium. Springer, LNCS 7428, pp.16, 2012, CHES 2912. <10.1007/978-3-642-33027-8_26>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094316/file/ches2012.pdf BibTex
titre
Constraint-based reachability
auteur
Arnaud Gotlieb, Tristan Denmat, Nadjib Lazaar
article
Infinity workshop 2012, Aug 2012, Paris, France. 2013, <10.4204/EPTCS.107.4, Source: arXiv>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00807856/file/GotliebDenmatLazaar_Infinity2012201302070156.pdf BibTex
titre
Towards a formally verified obfuscating compiler
auteur
Sandrine Blazy, Roberto Giacobazzi
article
Christian Collberg. SSP 2012 – 2nd ACM SIGPLAN Software Security and Protection Workshop, Jun 2012, Beijing, China. ACM SIGPLAN, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00762330/file/paper-ieee.pdf BibTex
titre
Perception de l’espace d’action chez les patients hémiplégiques
auteur
M. Carlier, A. Poulain, C. Bachelet, J. Labire, Y. Martin, H. Sassaini, R. Levasseur, Yann Coello, Angela Bartolo
article
Symposium International de Neuropsychologie: Rehabilitation Cognitive et prise en charge chirurgicale, Jun 2012, Lille, France. 2012
Accès au bibtex
BibTex
titre
Tightly-Secure Signatures from Lossy Identification Schemes
auteur
Michel Abdalla, Pierre-Alain Fouque, Vadim Lyubashevsky, Mehdi Tibouchi
article
Advances in Cryptology – 2012, Apr 2012, Cambridge, United Kingdom. Springer, LNCS 7237, pp.19, 2012, EUROCRYPT 2012. <10.1007/978-3-642-29011-4_34>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094318/file/AFLT12.pdf BibTex
titre
A Formally Verified SSA-based Middle-end
auteur
Gilles Barthe, Delphine Demange, David Pichardie
article
21th European Symposium on Programming, ESOP 2012, Mar 2012, Tallin, Estonia. Springer, 7211, pp.47-66, 2012, LNCS Programming Languages and Systems. <10.1007/978-3-642-28869-2_3>
Accès au bibtex
BibTex
titre
Formalisation de HOCore en Coq
auteur
Simon Boulier, Alan Schmitt
article
JFLA – Journées Francophones des Langages Applicatifs – 2012, Feb 2012, Carnac, France. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00665945/file/paper_7.pdf BibTex
titre
Formally verified optimizing compilation in ACG-based flight control software
auteur
Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris
article
ERTS2 2012: Embedded Real Time Software and Systems, Feb 2012, Toulouse, France. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00653367/file/erts2012.pdf BibTex
titre
Proving Reachability Properties on Term Rewriting Systems with Strategies
auteur
Thomas Genet, Yann Salmon
article
Workshop on Strategies in Rewriting, Proving and Programming, 2012, London, United Kingdom. 2012
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01111038/file/GenetSalmon-IWS12.pdf BibTex

Habilitation à diriger des recherches

titre
Toward a Verified Software Toolchain for Java
auteur
David Pichardie
article
Computer Science [cs]. ENS Cachan, 2012
Accès au bibtex
BibTex

Master thesis

titre
Vérification probabiliste de résultats d’analyse statique
auteur
Antoine Bride
article
Informatique et langage [cs.CL]. 2012
Accès au texte intégral et bibtex
https://dumas.ccsd.cnrs.fr/dumas-00725213/file/Bride.pdf BibTex

Reports

titre
Logical Combinators for Rich Type Systems
auteur
Pierre Genevès, Nabil Layaïda, Alan Schmitt
article
[Research Report] RR-8010, INRIA. 2012, pp.18
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00714353/file/RR-8010.pdf BibTex
titre
The CompCert Memory Model, Version 2
auteur
Xavier Leroy, Andrew Appel, Sandrine Blazy, Gordon Stewart
article
[Research Report] RR-7987, INRIA. 2012, pp.26
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00703441/file/RR-7987.pdf BibTex
titre
Tree Regular Model Checking for Lattice-Based Automata
auteur
Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat
article
[Technical Report] RT-0424, INRIA. 2012, pp.33
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00687310/file/mainTechRep.pdf BibTex

Theses

titre
Semantic foundations of intermediate program representations
auteur
Delphine Demange
article
Other [cs.OH]. École normale supérieure de Cachan – ENS Cachan, 2012. English. <NNT : 2012DENS0053>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00905442/file/Demange2012.pdf BibTex
titre
Dioïdes et idéaux de polynômes en analyse statique
auteur
Arnaud Jobin
article
Autre [cs.OH]. École normale supérieure de Cachan – ENS Cachan, 2012. Français. <NNT : 2012DENS0004>
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00881301/file/Jobin2012.pdf BibTex

Preprints, Working Papers, …

titre
Proofs as Cryptography: a new interpretation of the Curry-Howard isomorphism for software certificates
auteur
Amrit Kumar, Pierre-Alain Fouque, Thomas Genet, Mehdi Tibouchi
article
19 pages. 2012
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00715726/file/RapportHal.pdf BibTex

2011

Journal articles

titre
On the Expressiveness and Decidability of Higher-Order Process Calculi
auteur
Ivan Lanese, Jorge Perez, Davide Sangiorgi, Alan Schmitt
article
Journal of Information and Computation, Elsevier, 2011, 209 (2), pp.29. <10.1016/j.ic.2010.10.001>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01112294/file/Lanese2011On-the-Expressivenes.pdf BibTex
titre
Programmation d’un interpréteur abstrait certifié en logique constructive
auteur
David Cachera, David Pichardie
article
Revue des Sciences et Technologies de l’Information – Série TSI : Technique et Science Informatiques, Lavoisier, 2011, pp.28. <10.3166/tsi.30.381-408>
Accès au bibtex
BibTex

Conference papers

titre
PACOGEN : Automatic Generation of Pairwise Test Configurations from Feature Models
auteur
Aymeric Hervieu, Benoit Baudry, Arnaud Gotlieb
article
Proc. of Int. Symp. on Soft. Reliability Engineering (ISSRE’11), Nov 2011, Hiroshima, Japan. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00699558/file/HBG10.pdf BibTex
titre
Filtering by ULP Maximum
auteur
Matthieu Carlier, Arnaud Gotlieb
article
Proc. of the IEEE Int. Conf. on Tools for Artificial Intelligence (ICTAI’11), Nov 2011, Floride, United States. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00699565/file/CG_ICTAI.pdf BibTex
titre
Characterizing Conclusive Approximations by Logical Formulae
auteur
Yohan Boichut, Thi-Bich-Hanh Dao, Valérie Murat
article
Giorgio Delzanno and Igor Potapov. Reachability Problems 2011, Sep 2011, Gênes, Italy. LNCS 6945, 2011, Reachability Problems (RP 2011)
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00606100/file/main.pdf BibTex
titre
A Nelson-Oppen based Proof System using Theory Specific Proof Systems
auteur
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving – PxTP 2011, Aug 2011, Wrocław, Poland. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00677193/file/paper5.pdf BibTex
titre
A Flexible Proof Format for SMT: a Proposal
auteur
Frédéric Besson, Pascal Fontaine, Laurent Théry
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving – PxTP 2011, Aug 2011, Wrocław, Poland. 2011, <http://pxtp2011.loria.fr>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642544/file/paper3.pdf BibTex
titre
Modular SMT Proofs for Fast Reflexive Checking inside Coq
auteur
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
article
First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan. 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00646960/file/CPP11.pdf BibTex
titre
Secure the Clones – Static Enforcement of Policies for Secure Object Copying
auteur
Thomas Jensen, Florent Kirchner, David Pichardie
article
ESOP 2011, 2011, Saarbrucken, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01110817/file/esop11.pdf BibTex

Habilitation à diriger des recherches

titre
Contributions à la génération de tests à base de contraintes
auteur
Arnaud Gotlieb
article
Génie logiciel [cs.SE]. Université Européenne de Bretagne, 2011
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00699260/file/hdrag.pdf BibTex

Reports

titre
Formal Verification of an SSA-based Middle-end for CompCert
auteur
Gilles Barthe, Delphine Demange, David Pichardie
article
[University works] 2011
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00634702/file/BDPreport.pdf BibTex
titre
Negation for Free!
auteur
Nadjib Lazaar, Nourredine Aribi, Arnaud Gotlieb, Yahia Lebbah
article
[Research Report] RR-7749, INRIA. 2011, pp.16
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00629657/file/RR-7749.pdf BibTex
titre
Fast inference of polynomial invariants for imperative programs
auteur
David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner
article
[Research Report] RR-7627, INRIA. 2011, pp.31
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00595783/file/RR-7627.pdf BibTex

2010

Journal articles

titre
A Uniform Random Test Data Generator for Path Testing
auteur
Arnaud Gotlieb, Matthieu Petit
article
Journal of Systems and Software, Elsevier, 2010, 83 (12), pp.2618-2626. <10.1016/j.jss.2010.08.021>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00540283/file/Gotlieb_Petit.pdf BibTex
titre
Long-Run Cost Analysis by Approximation of Linear Operators over Dioids
auteur
David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2010, 20 (4), pp.589-624. <10.1017/S0960129510000113>
Accès au bibtex
BibTex
titre
Verifying Resource Access Control on Mobile Interactive Devices
auteur
Frédéric Besson, Guillaume Dufay, Thomas Jensen, David Pichardie
article
Journal of Computer Security, IOS Press, 2010, 18 (6), pp.971-998
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537821/file/jcs.pdf BibTex
titre
Equational Approximations for Tree Automata Completion
auteur
Thomas Genet, Vlad Rusu
article
Journal of Symbolic Computation, Elsevier, 2010, 45(5):574-597, May 2010 (5), pp.574-597
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00495405/file/genet-rusu-JSC-SCSS.pdf BibTex

Conference papers

titre
Constraint-Based Test Input Generation for Java Bytecode
auteur
Florence Charreteur, Arnaud Gotlieb
article
Proc. of the 21st IEEE Int. Symp. on Softw. Reliability Engineering (ISSRE’10), Nov 2010, San Jose, CA, USA, United States. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00699236/file/ISSRE_10_CharreteurGotlieb.pdf BibTex
titre
Constraint solving on modular integers
auteur
Arnaud Gotlieb, Michel Leconte, Bruno Marre
article
ModRef Worksop, associated to CP’2010, Sep 2010, Saint-Andrews, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00699234/file/GLM_2010_CR.pdf BibTex
titre
On Testing Constraint Programs
auteur
Nadjib Lazaar, Arnaud Gotlieb, Yahia Lebbah
article
16th Int. Conf. on Principles and Practices of Constraint Programming (CP’2010), Sep 2010, St Andrews, Scotland, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00699237/file/CP10nl1.pdf BibTex
titre
Constraint Reasoning in FocalTest
auteur
Mathieu Carlier, Catherine Dubois, Arnaud Gotlieb
article
ICSOFT, Jul 2010, Athènes, Greece. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00699233/file/paper.pdf BibTex
titre
Explanation-based generalization of infeasible path
auteur
Mickaël Delahaye, Bernard Botella, Arnaud Gotlieb
article
3rd IEEE International Conference on Software Testing, Validation and Verification (ICST’10), Apr 2010, Paris, France. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00699240/file/paper2010.pdf BibTex
titre
Formal Verification of Coalescing Graph-Coloring Register Allocation
auteur
Sandrine Blazy, Benoît Robillard, Andrew W. Appel
article
Andrew Gordon. 19th European Symposium on Programming (ESOP), Mar 2010, Paphos, Cyprus. Springer, 6012, pp.145-164, 2010, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00477689/file/2010ESOP.pdf BibTex
titre
A Certified Denotational Abstract Interpreter
auteur
David Cachera, David Pichardie
article
International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. Springer-Verlag, 6172, pp.9-24, 2010, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537810/file/main.pdf BibTex
titre
A Provably Correct Stackless Intermediate Representation for Java Bytecode
auteur
Delphine Demange, Thomas Jensen, David Pichardie
article
The 8th Asian Symposium on Programming Languages and Systems (APLAS), 2010, Shangai, China. Springer-Verlag, 2010, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537815/file/main.pdf BibTex
titre
Certified Result Checking for Polyhedral Analysis of Bytecode Programs
auteur
Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin
article
The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany. Springer-Verlag, 2010, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537816/file/main.pdf BibTex
titre
Sécurité de la plate-forme d’exécution Java : limites et propositions d’améliorations
auteur
Guillaume Hiet, Frédéric Guihéry, Goulven Guiheux, David Pichardie, Christian Brunette
article
Symposium sur la sécurité des technologies de l’information et des communications (SSTIC), 2010, Rennes, France. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00537820/file/publication.pdf BibTex
titre
Sawja: Static Analysis Workshop for Java
auteur
Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
article
Beckert, Bernhard and Marché, Claude. The International Conference on Formal Verification of Object-Oriented Software, 2010, Paris, France. Springer-Verlag, 2010.13, pp.253–267, 2010, Lecture Notes in Computer Science; Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. <http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00504047/file/main.pdf BibTex
titre
Enforcing Secure Object Initialization in Java
auteur
Laurent Hubert, Thomas Jensen, Vincent Monfort, David Pichardie
article
15th European Symposium on Research in Computer Security (ESORICS), 2010, Athènes, Greece. Springer-Verlag, 6345, pp.101-115, 2010, Lecture Notes in Computer Science; Proceedings of ESORICS 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00503953/file/esorics.pdf BibTex
titre
On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver
auteur
Frédéric Besson
article
8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh, United Kingdom. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00517308/file/floating_point_simplex.pdf BibTex
titre
Fault Localization in Constraint Programs
auteur
Nadjib Lazaar, Arnaud Gotlieb, Yahia Lebbah
article
22th Int. Conf. on Tools with Artificial Intelligence (ICTAI’2010), 2010, Arras, France. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00699235/file/ictai2010_CR.pdf BibTex

Reports

titre
Equational Abstraction Refinement for Certified Tree Regular Model Checking
auteur
Yohan Boichut, Benoît Boyer, Thomas Genet, Axel Legay
article
[Technical Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00501487/file/rapportHal.pdf BibTex
titre
On Testing Constraint Programs
auteur
Nadjib Lazaar, Arnaud Gotlieb, Lebbah Yahia
article
[Research Report] RR-7291, INRIA. 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00483410/file/RR-7291.pdf BibTex
titre
A Provably Correct Stackless Intermediate Representation For Java Bytecode
auteur
Delphine Demange, Thomas Jensen, David Pichardie
article
[Research Report] RR-7021, INRIA. 2010, pp.59
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00414099/file/rr7021.pdf BibTex

Theses

titre
Modélisation par contraintes de programmes en bytecode Java pour la génération automatique de tests
auteur
Florence Charreteur
article
Informatique [cs]. Université Européenne de Bretagne, 2010. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00497785/file/these_Charreteur_v2.pdf BibTex

2009

Journal articles

titre
Modelling Dynamic Memory Management in Constraint-Based Testing
auteur
Florence Charreteur, Bernard Botella, Arnaud Gotlieb
article
Journal of Systems and Software, Elsevier, 2009, 82 (11), pp.1755-1766. <10.1016/j.jss.2009.06.029>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00540270/file/Charreteur_Gotlieb_Botella_JSS.pdf BibTex
titre
Soundly Handling Static Fields: Issues, Semantics and Analysis
auteur
Laurent Hubert, David Pichardie
article
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. <http://www.sciencedirect.com/science/article/B75H1-4XT3BCD-3/2/0c24aba371ae79c050511b1705928a1b>. <10.1016/j.entcs.2009.11.012>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00504028/file/bytecode09.pdf BibTex

Conference papers

titre
Control-flow analysis of function call and returns by abstract interpretation
auteur
Jan Midtgaard, Thomas Jensen
article
ACM International Conference on Functional Programming, Sep 2009, Edinburgh, United Kingdom. 2009, <10.1145/1596550.1596592>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00574944/file/ICFP09-ANFCFA.pdf BibTex
titre
Vers une Théorie du Test des programmes à contraintes
auteur
Nadjib Lazaar, Arnaud Gotlieb, Yahia Lebbah
article
Cinquièmes Journées Francophones de Programmation par Contraintes, Orléans, juin 2009, Jun 2009, France. pp.65-75, 2009
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00387850/file/paper_25.pdf BibTex
titre
Constraint Based Strategies
auteur
Helene Kirchner, Kirchner Florent, Claude Kirchner
article
Santiago Escobar. 18th International Workshop on Functional and Constraint Logic Programming – WFLP 2009, Jun 2009, Brasilia, Brazil. Springer Berlin / Heidelberg, 5979, pp.13-26, 2010, Lecture Notes in Computer Science; Functional and Constraint Logic Programming
Accès au bibtex
BibTex
titre
Distinguish Dynamic Basic Blocks by Structural Statistical Testing
auteur
Matthieu Petit, Arnaud Gotlieb
article
Hélène WAESELYNCK. 12th European Workshop on Dependable Computing, EWDC 2009, May 2009, Toulouse, France. 8 p., 2009
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00381557/file/Testing_3.pdf BibTex
titre
CPA beats oo-CFA
auteur
Frédéric Besson
article
FTfJP ’09 – Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, 2009, Genova, Italy. 2009, <10.1145/1557898.1557905>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00780389/file/CPA_beats_CFA.pdf BibTex
titre
Verifying Temporal Regular properties of Abstractions of Term Rewriting Systems
auteur
Benoît Boyer, Thomas Genet
article
RULE’09, 2009, France. 21, pp.99-108, 2009
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00780491/file/main2.pdf BibTex
titre
On the Unobservability of a Trust Relation in Mobile Ad Hoc Networks
auteur
Olivier Heen, Gilles Guette, Thomas Genet
article
Information Security Theory and Practice. Smart Devices, Pervasive Systems, and Ubiquitous Networks, 2009, Belgium. 5746, pp.1-11, 2009
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00780724/file/wistp2009-1.pdf BibTex
titre
Comparing Techniques for Certified Static Analysis
auteur
David Cachera, David Pichardie
article
The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. NASA Ames Research Center, pp.111-115, 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00538772/file/main.pdf BibTex
titre
Certified Static Analysis by Abstract Interpretation
auteur
Frédéric Besson, David Cachera, Thomas Jensen, David Pichardie
article
Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. Springer-Verlag, 5705, pp.223-257, 2009, Lecture Notes in Computer Science; FOSAD 2007/2008/2009 Tutorial Lectures
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00538753/file/main.pdf BibTex
titre
A Certified Data Race Analysis for a Java-like Language
auteur
Frédéric Dabrowski, David Pichardie
article
TPHOL’09, 2009, Germany. pp.212–227, 2009
Accès au bibtex
BibTex

Habilitation à diriger des recherches

titre
Reachability analysis of rewriting for software verification
auteur
Thomas Genet
article
Software Engineering [cs.SE]. Université Rennes 1, 2009
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00477013/file/Final.pdf BibTex

Reports

titre
Computing the Least Fix-point Semantics of Definite Logic Programs Using BDDs
auteur
Frédéric Besson, Thomas Jensen, Tiphaine Turpin
article
[Research Report] PI 1939, 2009, pp.25
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00433820/file/PI-1939.pdf BibTex
titre
Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation
auteur
Jan Midtgaard, Thomas P. Jensen
article
[Research Report] RR-6681, INRIA. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00328154/file/RR-6681.pdf BibTex

2008

Conference papers

titre
A Non-Null Annotation Inferencer for Java Bytecode
auteur
Laurent Hubert
article
Shriram Krishnamurthi and Michal Young. PASTE: Program analysis for software tools and engineering, Nov 2008, Atlanta, Georgia, United States. ACM, pp.10.1145/1512475.1512484, 2008, Proceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering. <10.1145/1512475.1512484>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00504006/file/main.pdf BibTex

1999

Conference papers

titre
Polyhedral Analysis for Synchronous Languages
auteur
Frédéric Besson, Thomas Jensen, Jean-Pierre Talpin
article
6th International Symposium on Static Analysis (SAS’99), Sep 1999, Venice, Italy. Springer-Verlag, pp.51-68, 1999, LNCS vol. 1694
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00544493/file/CONCUR99-besson.pdf BibTex

1998

Journal articles

titre
Dynamic optimization of interval narrowing algorithms
auteur
Olivier Lhomme, Arnaud Gotlieb, Michel Rueher
article
Journal of Logic Programming, Elsevier, 1998, 37 (1-3), pp.165-183. <10.1016/S0743-1066(98)10007-9>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00540302/file/jlp97.pdf BibTex

Comments are closed