Bibliography

Major publications by the team in recent years

• 1F. Besson, N. Bielova, T. Jensen.
  
  Hybrid Information Flow Monitoring Against Web Tracking, in: CSF - 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, United States, 2013. [ DOI : 10.1109/CSF.2013.23 ]
  
  http://hal.inria.fr/hal-00924138
• 2F. Besson, T. Jensen, D. Pichardie.
  
  Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression, in: Theoretical Computer Science, 2006, vol. 364, n^o 3, pp. 273–291.
• 3M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith.
  
  A Trusted Mechanised JavaScript Specification, in: POPL 2014 - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, United States, November 2013.
  
  http://hal.inria.fr/hal-00910135
• 4B. Boyer, T. Genet, T. Jensen.
  
  Certifying a Tree Automata Completion Checker, in: 4th International Joint Conference, IJCAR 2008, Lectures Notes in Computer Science, Springer-Verlag, 2008, vol. 5195, pp. 347–362.
• 5D. Cachera, T. Jensen, A. Jobin, P. Sotin.
  
  Long-Run Cost Analysis by Approximation of Linear Operators over Dioids, in: Mathematical Structures in Computer Science, 2010, vol. 20, n^o 4, pp. 589-624.
• 6D. Cachera, T. Jensen, D. Pichardie, V. Rusu.
  
  Extracting a Data Flow Analyser in Constructive Logic, in: Theoretical Computer Science, 2005, vol. 342, n^o 1, pp. 56–78.
• 7D. Demange, V. Laporte, L. Zhao, D. Pichardie, S. Jagannathan, J. Vitek.
  
  Plan B: A Buffered Memory Model for Java, in: Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, ACM, 2013.
  
  http://hal.inria.fr/hal-00924716
• 8J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, A. Schmitt.
  
  Combinators for Bi-Directional Tree Transformations: A Linguistic Approach to the View Update Problem, in: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, Long Beach, CA, USA, 2005, pp. 233–246, Most Influential POPL Paper Award, 2015. Extended version available as University of Pennsylvania technical report MS-CIS-03-08. Earlier version presented at the Workshop on Programming Language Technologies for XML (PLAN-X), 2004.
• 9T. Genet, V. Rusu.
  
  Equational Approximations for Tree Automata Completion, in: Journal of Symbolic Computation, 2010, vol. 45(5):574-597, May 2010, n^o 5, pp. 574-597.
• 10L. Hubert, T. Jensen, V. Monfort, D. Pichardie.
  
  Enforcing Secure Object Initialization in Java, in: 15th European Symposium on Research in Computer Security (ESORICS), Lecture Notes in Computer Science, Springer, 2010, vol. 6345, pp. 101-115.

Publications of the year

Doctoral Dissertations and Habilitation Theses

• 11Y. Salmon.
  
  Reachability Analysis for Functional Programs with call-by-value evaluation strategy, Université de Rennes 1, December 2015.
  
  https://hal.inria.fr/tel-01250252

Articles in International Peer-Reviewed Journals

• 12S. Blazy, D. Bühler, B. Yakobowski.
  
  Improving static analyses of C programs with conditional predicates, in: Science of Computer Programming, January 2016, Accepted manuscript. Available online 30 November 2015.Extended version of the FMICS 2014 paper.
  
  https://hal.inria.fr/hal-01242077
• 13S. Blazy, V. Laporte, D. Pichardie.
  
  Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code, in: Journal of Automated Reasoning, 2016, Version étendue de l'article de la conférence ITP 2014, accepté pour publication.
  
  https://hal.inria.fr/hal-01243700
• 14T. Genet.
  
  Termination criteria for tree automata completion, in: Journal of Logic and Algebraic Methods in Programming, 2016, vol. 85, Issue 1, part 1, pp. 3-33. [ DOI : 10.1016/j.jlamp.2015.05.003 ]
  
  https://hal.inria.fr/hal-01194533
• 15P. Genevès, N. Layaïda, A. Schmitt, N. Gesbert.
  
  Efficiently Deciding µ-calculus with Converse over Finite Trees, in: ACM Transactions on Computational Logic, March 2015, vol. 16, n^o 2, 41 p. [ DOI : 10.1145/2724712 ]
  
  https://hal.inria.fr/hal-00868722
• 16B. Marinkovic, V. Ciancaglini, Z. Ognjanovic, P. Glavan, L. Liquori, P. Maksimovic.
  
  Analyzing the exhaustiveness of the synapse protocol, in: Peer-to-Peer Networking and Applications, Springer, July 2015, vol. 8, n^o 5, pp. 793–806. [ DOI : 10.1007/s12083-014-0293-z ]
  
  https://hal.inria.fr/hal-01146050

International Conferences with Proceedings

• 17S. Blazy, A. Maroneze, D. Pichardie.
  
  Verified Validation of Program Slicing, in: CPP 2015 : Conference on Certified Programs and Proofs, Mumbai, India, 2015, pp. 109-117. [ DOI : 10.1145/2676724.2693169 ]
  
  https://hal.inria.fr/hal-01110821
• 18S. Blazy, A. Trieu.
  
  Formal Verification of Control-flow Graph Flattening, in: Certified Proofs and Programs (CPP 2016), Saint-Petersburg, United States, ACM (editor), January 2016, 12 p, A paraître.
  
  https://hal.inria.fr/hal-01242063
• 19M. Bodin, T. Jensen, A. Schmitt.
  
  Certified Abstract Interpretation with Pretty-Big-Step Semantics, in: Certified Programs and Proofs (CPP 2015), Mumbai, India, January 2015. [ DOI : 10.1145/2676724.2693174 ]
  
  https://hal.inria.fr/hal-01111588
• 20D. Demange, D. Pichardie, L. Stefanesco.
  
  Verifying Fast and Sparse SSA-based Optimizations in Coq, in: 24th International Conference on Compiler Construction, CC 2015, London, United Kingdom, 2015.
  
  https://hal.inria.fr/hal-01110779
• 21J. Fragoso Santos, T. Jensen, T. Rezk, A. Schmitt.
  
  Hybrid Typing of Secure Information Flow in a JavaScript-like Language, in: International Symposium on Trustworthy Global Computing - (TGC 2015), Madrid, Spain, August 2015.
  
  https://hal.archives-ouvertes.fr/hal-01243029
• 22T. Genet, Y. Salmon.
  
  Reachability Analysis of Innermost Rewriting, in: RTA, Warshaw, Poland, 2015, pp. 1-17. [ DOI : 10.4230/LIPIcs.RTA.2015.x ]
  
  https://hal.inria.fr/hal-01194530
• 23P. Genevès, A. Schmitt.
  
  Expressive Logical Combinators for Free, in: International Joint Conference on Artificial Intelligence (IJCAI 2015), Buenos Aires, Argentina, July 2015.
  
  https://hal.inria.fr/hal-00868724
• 24F. Honsell, L. Liquori, P. Maksimovic, I. Scagnetto.
  
  Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks , in: LFMTP'15. 9th International Workshop on Logical Frameworks and Meta-languages, Berlin, Germany, Berlin, Germany, August 2015, vol. Electronic Proceedings in Theoretical Computer Science (EPTCS). [ DOI : 10.4204/EPTCS.185.1 ]
  
  https://hal.archives-ouvertes.fr/hal-01170029
• 25T. Jensen, S. Lescuyer, A. Oana.
  
  Dependency Analysis of Functional Specifications with Algebraic Data Structures, in: 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, Springer LNCS, Springer Verlag, November 2015, vol. 9407, 18 p. [ DOI : 10.1007/978-3-319-25423-4_8 ]
  
  https://hal.inria.fr/hal-01243002
• 26J.-H. Jourdan, V. Laporte, S. Blazy, X. Leroy, D. Pichardie.
  
  A formally-verified C static analyzer, in: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India, ACM, January 2015, pp. 247-259. [ DOI : 10.1145/2676726.2676966 ]
  
  https://hal.inria.fr/hal-01078386
• 27B. Kordy, R. Jhawar, S. Mauw, S. Radomirovic, R. Trujillo-Rasua.
  
  Attack Trees with Sequential Conjunction, in: IFIP SEC 2015 - International Conference on ICT Systems Security and Privacy Protection, Hamburg, Germany, H. Federrath, D. Gollmann (editors), Springer, May 2015, vol. IFIP Advances in Information and Communication Technology, n^o 455, pp. 339-353. [ DOI : 10.1007/978-3-319-18467-8_23 ]
  
  https://hal.inria.fr/hal-01197256
• 28P. Maksimovic, A. Schmitt.
  
  HOCore in Coq, in: The 6th conference on Interactive Theorem Proving - (ITP 2015), Nanjing, China, Springer, August 2015, vol. 9236. [ DOI : 10.1007/978-3-319-22102-1_19 ]
  
  https://hal.archives-ouvertes.fr/hal-01243017

National Conferences with Proceedings

• 29M. Escarrá, M. Petar, A. Schmitt.
  
  HOCore in Coq, in: Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Le Val d'Ajol, France, D. Baelde, J. Alglave (editors), January 2015.
  
  https://hal.inria.fr/hal-01099130

Conferences without Proceedings

• 30R. Andriatsimandefitra Ratsisahanana, T. Genet, L. Guillo, J.-F. Lalande, D. Pichardie, V. Viet Triem Tong.
  
  Kharon : Découvrir, comprendre et reconnaître des malware Android par suivi de flux d'information, in: Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information, Troyes, France, May 2015.
  
  https://hal.inria.fr/hal-01154368
• 31A. BART, C. Truchet, E. Monfroy.
  
  Verifying a Real-Time Language with Constraints, in: 27th IEEE International Conference on Tools with Artificial Intelligence, Vietri sul Mare, Italy, 2015.
  
  https://hal.archives-ouvertes.fr/hal-01234188
• 32F. Besson, S. Blazy, P. Wilke.
  
  A Concrete Memory Model for CompCert, in: ITP 2015 : 6th International Conference on Interactive Theorem Proving, Nanjing, China, Springer (editor), August 2015, vol. Lecture Notes in Computer Science (LNCS), n^o 9236, pp. 67-83. [ DOI : 10.1007/978-3-319-22102-1_5 ]
  
  https://hal.inria.fr/hal-01194549
• 33S. Blazy.
  
  Formal verification of compilers and static analyzers. , in: PLMW@POPL 2015 - Programming Languages Mentoring Workshop, Mumbai, India, January 2015.
  
  https://hal.inria.fr/hal-01242094
• 34S. Blazy, D. Demange, D. Pichardie.
  
  Validating Dominator Trees for a Fast, Verified Dominance Test, in: Interactive Theorem Proving, Nanjing, China, Springer (editor), August 2015, vol. Lecture Notes in Computer Science (LNCS), n^o 9236. [ DOI : 10.1007/978-3-319-22102-1_6 ]
  
  https://hal.inria.fr/hal-01193281
• 35S. Blazy, S. Riaud, T. Sirvent.
  
  Data Tainting and Obfuscation: Improving Plausibility of Incorrect Taint, in: Source Code Analysis and Manipulation (SCAM), Bremen, Germany, IEEE (editor), September 2015.
  
  https://hal.inria.fr/hal-01193286
• 36D. Cachera, U. Fahrenberg, A. Legay.
  
  An ω-Algebra for Real-Time Energy Problems, in: 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Bengaluru, India, December 2015.
  
  https://hal.inria.fr/hal-01237667
• 37T. Genet, B. Kordy, A. Vansyngel.
  
  Vers un outil de vérification formelle légere pour OCaml, in: AFADL, Bordeaux, France, 2015, 6 p.
  
  https://hal.inria.fr/hal-01194538
• 38S. Lenglet, A. Schmitt.
  
  Howe's Method for Contextual Semantics , in: CONCUR 2015 26th International Conference on Concurrency Theory, Madrid, Spain, September 2015. [ DOI : 10.4230/LIPIcs.CONCUR.2015.212 ]
  
  https://hal.inria.fr/hal-01192699
• 39X. Leroy, S. Blazy, D. Kästner, B. Schommer, M. Pister, C. Ferdinand.
  
  CompCert - A Formally Verified Optimizing Compiler, in: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Toulouse, France, SEE, January 2016.
  
  https://hal.inria.fr/hal-01238879

Scientific Books (or Scientific Book chapters)

• 40T. J. Sandrine Blazy (editor)
  
  Static Analysis Symposium - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015. Proceedings, Springer, Saint-Malo, France, August 2015, vol. Lecture Notes in Computer Science (LNCS), n^o 9291, 335 p.
  
  https://hal.inria.fr/hal-01194558

Internal Reports

• 41T. Genet.
  
  A Short Isabelle/HOL Tutorial for the Functional Programmer, IRISA, 2015.
  
  https://hal.inria.fr/hal-01208577
• 42T. Genet.
  
  A Short SPAN+AVISPA Tutorial, IRISA, October 2015.
  
  https://hal.inria.fr/hal-01213074
• 43S. Lenglet, A. Schmitt.
  
  Howe's Method for Contextual Semantics, Inria, June 2015, n^o RR-8750, 31 p.
  
  https://hal.inria.fr/hal-01168865

Other Publications

• 44F. Honsell, L. Liquori, P. Maksimovic, I. Scagnetto.
  
  LLFP : A Logical Framework for modeling External Evidence, Side Conditions, and Proof Irrelevance using Monads, January 2015, working paper or preprint. [ DOI : 10.4204/EPTCS.185.1 ]
  
  https://hal.inria.fr/hal-01146059

References in notes

• 45The Coq Proof Assistant, 2009.
  
  http://coq.inria.fr/
• 46E. Albert, P. Arenas, S. Genaim, G. Puebla, D. Zanardini.
  
  COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode, in: FMCO, 2007, pp. 113-132.
• 47D. Aspinall, L. Beringer, M. Hofmann, Hans-Wolfgang. Loidl, A. Momigliano.
  
  A Program Logic for Resource Verification, in: In Proceedings of the 17th International Conference on Theorem Proving in Higher-Order Logics, (TPHOLs 2004), volume 3223 of LNCS, Springer, 2004, pp. 34–49.
• 48D. F. Bacon, P. F. Sweeney.
  
  Fast Static Analysis of C++ Virtual Function Calls, in: OOPSLA'96, 1996, pp. 324-341.
• 49P. Baillot, P. Coppola, U. D. Lago.
  
  Light Logics and Optimal Reduction: Completeness and Complexity, in: LICS, 2007, pp. 421-430.
• 50E. Balland, Y. Boichut, T. Genet, P.-E. Moreau.
  
  Towards an Efficient Implementation of Tree Automata Completion, in: Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Lectures Notes in Computer Science, Springer-Verlag, 2008, vol. 5140, pp. 67-82.
• 51G. Barthe, D. Demange, D. Pichardie.
  
  Formal Verification of an SSA-based Middle-end for CompCert, in: ACM Transactions on Programming Languages and Systems (TOPLAS), 2014, 35 p.
  
  https://hal.inria.fr/hal-01097677
• 52F. Besson, S. Blazy, P. Wilke.
  
  A Precise and Abstract Memory Model for C Using Symbolic Values, in: 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), Singapore, Singapore, LNCS, Springer, 2014, vol. 8858, pp. 449 - 468. [ DOI : 10.1007/978-3-319-12736-1_24 ]
  
  https://hal.inria.fr/hal-01093312
• 53F. Besson, T. Jensen.
  
  Modular Class Analysis with DATALOG, in: SAS'2003, 2003, pp. 19-36.
• 54D. Cachera, T. Jensen, A. Jobin, P. Sotin.
  
  Long-Run Cost Analysis by Approximation of Linear Operators over Dioids, in: Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Lectures Notes in Computer Science, Springer-Verlag, 2008, vol. 5140, pp. 122-138.
• 55D. Cachera, T. Jensen, D. Pichardie, V. Rusu.
  
  Extracting a Data Flow Analyser in Constructive Logic, in: Theoretical Computer Science, 2005, vol. 342, n^o 1, pp. 56–78.
• 56D. Cachera, T. Jensen, D. Pichardie, G. Schneider.
  
  Certified Memory Usage Analysis, in: Proc. of 13th International Symposium on Formal Methods (FM'05), LNCS, Springer-Verlag, 2005.
• 57P. Cousot, R. Cousot.
  
  Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, in: Proc. of POPL'77, 1977, pp. 238–252.
• 58A. Ermedahl, C. Sandberg, J. Gustafsson, S. Bygde, B. Lisper.
  
  Loop Bound Analysis based on a Combination of Program Slicing, Abstract Interpretation, and Invariant Analysis, in: Seventh International Workshop on Worst-Case Execution Time Analysis, (WCET'2007), July 2007.
  
  http://www.mrtc.mdh.se/index.php?choice=publications&id=1317
• 59G. Feuillade, T. Genet, V. Viet Triem Tong.
  
  Reachability Analysis over Term Rewriting Systems, in: Journal of Automated Reasoning, 2004, vol. 33, n^o 3–4, pp. 341–383.
• 60M. Fähndrich, K. R. M. Leino.
  
  Declaring and checking non-null types in an object-oriented language, in: OOPSLA, 2003, pp. 302-312.
• 61T. Genet.
  
  Decidable Approximations of Sets of Descendants and Sets of Normal forms, in: RTA'98, LNCS, Springer, 1998, vol. 1379, pp. 151–165.
• 62T. Genet, V. Viet Triem Tong.
  
  Reachability Analysis of Term Rewriting Systems with Timbuk, in: LPAR'01, LNAI, Springer, 2001, vol. 2250, pp. 691-702.
• 63D. Grove, C. Chambers.
  
  A framework for call graph construction algorithms, in: Toplas, 2001, vol. 23, n^o 6, pp. 685–746.
• 64D. Grove, G. DeFouw, J. Dean, C. Chambers.
  
  Call graph construction in object-oriented languages, in: ACM SIGPLAN Notices, 1997, vol. 32, n^o 10, pp. 108–124.
• 65M. Hofmann, S. Jost.
  
  Static prediction of heap space usage for first-order functional programs, in: POPL, 2003, pp. 185-197.
• 66L. Hubert.
  
  A Non-Null annotation inferencer for Java bytecode, in: Proc. of the Workshop on Program Analysis for Software Tools and Engineering (PASTE'08), ACM, 2008.
• 67L. Hubert, T. Jensen, D. Pichardie.
  
  Semantic foundations and inference of non-null annotations, in: Proc. of the 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), Lecture Notes in Computer Science, Springer-Verlag, 2008, vol. 5051, pp. 132-149.
• 68X. Leroy.
  
  A formally verified compiler back-end, in: Journal of Automated Reasoning, December 2009, vol. 43, n^o 4, pp. 363-446. [ DOI : 10.1007/s10817-009-9155-4 ]
  
  https://hal.inria.fr/inria-00360768
• 69O. Lhoták, L. J. Hendren.
  
  Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation, in: ACM Trans. Softw. Eng. Methodol., 2008, vol. 18, n^o 1.
• 70V. B. Livshits, M. S. Lam.
  
  Finding Security Errors in Java Programs with Static Analysis, in: Proc. of the 14th Usenix Security Symposium, 2005, pp. 271–286.
• 71A. Milanova, A. Rountev, B. G. Ryder.
  
  Parameterized object sensitivity for points-to analysis for Java, in: ACM Trans. Softw. Eng. Methodol., 2005, vol. 14, n^o 1, pp. 1–41.
• 72M. Naik, A. Aiken.
  
  Conditional must not aliasing for static race detection, in: POPL'07, ACM, 2007, pp. 327-338.
• 73M. Naik, A. Aiken, J. Whaley.
  
  Effective static race detection for Java, in: PLDI'2006, ACM, 2006, pp. 308-319.
• 74F. Nielson, H. Nielson, C. Hankin.
  
  Principles of Program Analysis, Springer, 1999.
• 75J. Palsberg, M. Schwartzbach.
  
  Object-Oriented Type Inference, in: OOPSLA'91, 1991, pp. 146-161.
• 76J. Palsberg, M. Schwartzbach.
  
  Object-Oriented Type Systems, John Wiley & Sons, 1994.
• 77D. Pichardie.
  
  Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certiés, Université Rennes 1, Rennes, France, dec 2005.
• 78A. D. Pierro, H. Wiklicky.
  
  Operator Algebras and the Operational Semantics of Probabilistic Languages, in: Electr. Notes Theor. Comput. Sci., 2006, vol. 161, pp. 131-150.
• 79P. Sotin, D. Cachera, T. Jensen.
  
  Quantitative Static Analysis over semirings: analysing cache behaviour for Java Card, in: 4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006), Electronic Notes in Theoretical Computer Science, Elsevier, 2006, vol. 164, pp. 153-167.
• 80F. Tip, J. Palsberg.
  
  Scalable propagation-based call graph construction algorithms, in: OOPSLA, 2000, pp. 281-293.
• 81J. Whaley, M. S. Lam.
  
  Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, in: PLDI '04, ACM, 2004, pp. 131–144.