Domain Theory in Logical Form, Annals of Pure and Applied Logic, vol.51, pp.1-2, 1991. ,
Inferring Frame Conditions with Static Correlation Analysis, Proc. ACM Program. Lang. 3, POPL, Article, vol.47, 2019. ,
Engineering Formal Metatheory, Proceedings of the 35 th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages -POPL '08, 2008. ,
Modular Control-Flow Analysis with Rank 2 Intersection Types, Mathematical Structures in Computer Science, vol.13, pp.87-124, 2003. ,
Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Formal Methods for Components and Objects, vol.4111, 2006. ,
The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, vol.3362, 2005. ,
The Algebra of Programming, 1996. ,
A Certified Denotational Abstract Interpreter, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00537810
Program Verification through Characteristic Formulae, Proceedings of the 15 th ACM SIGPLAN International Conference on Functional Programming (ICFP '10), 2010. ,
The Locally Nameless Representation, Journal of Automated Reasoning, vol.49, issue.3, 2011. ,
Soundness and Completeness of an Axiom System for Program Verification, SIAM J. Comput, vol.7, pp.70-90, 1978. ,
Types as Abstract Interpretations, Proceedings of the 24 th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages -POPL '97, 1997. ,
Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, Proceedings of the 4 th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '77), 1977. ,
Higher-Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection and PER Analysis of Functional Languages), Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL94), 1994. ,
Modular Static Program Analysis, Compiler Construction, vol.2304, pp.159-179, 2002. ,
Unification-Based Pointer Analysis with Directional Assignments, Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI '00), 2000. ,
A Type System for Higher-Order Modules, Proceedings of the 30 th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '03), 2003. ,
Pushdown Control-Flow Analysis of Higher-Order Programs, 2010. ,
Compositional Recurrence Analysis, Proceedings of the 15 th Conference on Formal Methods in Computer-Aided Design (FMCAD '15), 2015. ,
Why3 Ð Where Programs Meet Provers, Programming Languages and Systems, vol.7792, 2013. ,
Assigning Meanings to Programs, Program Verification, 1993. ,
A New Approach to Abstract Syntax Involving Binders, Proceedings. 14 th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999. ,
CertiKOS: A Certified Kernel for Secure Cloud Computing, Proceedings of the Second Asia-Pacific Workshop on Systems -APSys '11, 2011. ,
Set-Based Analysis of ML Programs, ACM SIGPLAN Lisp Pointers VII, vol.3, 1994. ,
An Axiomatic Basis for Computer Programming, Commun. ACM, vol.12, pp.576-580, 1969. ,
Descriptive and Relative Completeness of Logics for Higher-Order Functions, Automata, Languages and Programming, 2006. ,
Abstracting Abstract Machines, Proceedings of the 15 th ACM SIGPLAN international conference on Functional programming -ICFP '10, 2010. ,
Collecting Interpretations of Expressions, ACM Transactions on Programming Languages and Systems, vol.13, issue.2, 1991. ,
A Relational Shape Abstract Domain, NASA Formal Methods (LNCS, vol.10227, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01648681
A Relational Approach to Interprocedural Shape Analysis, Static Analysis, vol.3148, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00786335
Complexity of Flow Analysis, Inductive Assertion Synthesis and a Language Due to Dijkstra, 21 st Annual Symposium on Foundations of Computer Science (sfcs, 1980. ,
Data Flow Analysis of Applicative Programs Using Minimal Function Graphs, Proceedings of the 13 th ACM SIGACT-SIGPLAN symposium on Principles of programming languages -POPL '86, 1986. ,
Natural Semantics, STACS 87, 1987. ,
URL : https://hal.archives-ouvertes.fr/inria-00075953
A Relational Framework for Higher-Order Shape Analysis, Proceedings of the 19 th ACM SIGPLAN International Conference on Functional Programming, 2014. ,
Compositional Recurrence Analysis Revisited, Proceedings of the 38 th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017. ,
2009. seL4: Formal Verification of an OS Kernel, Proceedings of the ACM SIGOPS 22 nd symposium on Operating systems principles -SOSP '09 ,
URL : https://hal.archives-ouvertes.fr/hal-01582299
Semantical Analysis of Intuitionistic Logic I, Formal Systems and Recursive Functions, pp.71685-71694, 1965. ,
CakeML: A Verified Implementation of ML, Proceedings of the 41 st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14), 2014. ,
A Modular Module System, Journal of Functional Programming, vol.10, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00073825
Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant, Conference record of the 33 rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages -POPL'06, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00000963
Reasoning About Java Programs with Aliasing and Frame Conditions, Theorem Proving in Higher Order Logics, vol.3603, 2005. ,
Framing the Frame Problem, Dependable Software Systems Engineering. 193?203, 2015. ,
, Control-Flow Analysis of Functional Programs, Comput. Surveys, vol.44, pp.1-33, 2012.
A Calculational Approach to Control-Flow Analysis by Abstract Interpretation, Static Analysis, 2008. ,
Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation, Proceedings of the 14 th ACM SIGPLAN international conference on Functional programming -ICFP '09, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00328154
Hanne Riis Nielson, and Chris Hankin, 1999. ,
, Nominal Techniques. ACM SIGLOG News, vol.3, issue.1, 2016.
Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings 17 th Annual IEEE Symposium on Logic in Computer Science, 2002. ,
Liquid Types, Proceedings of the 29 th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '08), 2008. ,
The Semantics of Scheme Control-Flow Analysis, Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '91), 1991. ,
Extensional Equivalence and Singleton Types, ACM Transactions on Computational Logic, vol.7, issue.4, pp.676-722, 2006. ,
General Bindings and Alpha-Equivalence in Nominal Isabelle, Logical Methods in Computer Science, vol.8, issue.2, 2012. ,
The Information in Intuitionistic Logic, Synthese, vol.167, pp.251-270, 2008. ,
Refinement Types for Haskell, Proceedings of the 19 th ACM SIGPLAN International Conference on Functional Programming -ICFP '14, 2014. ,
Refinement Reflection: Complete Verification with SMT, Proceedings of the ACM on Programming Languages 2, POPL, p.31, 2017. ,