Abstract
We show how to formalise a constraint-based data flow analysis in the specification language of the Coq proof assistant. This involves defining a dependent type of lattices together with a library of lattice functors for modular construction of complex abstract domains. Constraints are expressed in an intermediate representation that allows for both efficient constraint resolution and correctness proof of the analysis with respect to an operational semantics. The proof of existence of a correct, minimal solution to the constraints is constructive which means that the extraction mechanism of Coq provides a provably correct data flow analyser in ocaml. The library of lattices together with the intermediate representation of constraints are defined in an analysis-independent fashion that provides a basis for a generic framework for proving and extracting static analysers in Coq.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Barthe, G., Dufay, G., Huisman, M., de Sousa, S.M.: Jakarta: A Toolset for Reasoning about JavaCard. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol. 2140, p. 2. Springer, Heidelberg (2001)
Barthe, G., Dufay, G., Jakubiec, L., Serpette, B.P., de Sousa, S.M.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 302. Springer, Heidelberg (2001)
Bertot, Y.: Formalizing a JVML Verifier for Initialization in a Theorem Prover. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 14. Springer, Heidelberg (2001)
Casset, L., Burdy, L., Requet, A.: Formal Development of an embedded verifier for Java Card Byte Code. In: Proc. of IEEE Int. Conference on Dependable Systems & Networks, DSN (2002)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixpoints. In: Proc. of 4th ACM Symposium on Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
Coglio, A., Goldberg, A., Qian, Z.: Towards a Provably-Correct Implementation of the JVM Bytecode Verifier. In: Proc. OOPSLA 1998 Workshop on Formal Underpinnings of Java (1998)
Denney, E.: The synthesis of a Java Card tokenisation algorithm. In: Proc. of 16th Int. Conf. on Automated Software Engineering (ASE 2001), pp. 43–50. IEEE Press, Los Alamitos (2001)
Genet, T., Jensen, T., Kodati, V., Pichardie, D.: A Java Card CAP converter in PVS. In: Proc. of 2nd International Workshop on Compiler Optimization Meets Compiler Verification, COCV 2003 (2003)
Hansen, R.R.: Flow Logic for Carmel. Technical Report SECSAFE-IMM-001, Danish Technical University (2002)
Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science 298(3), 583–626 (2002)
Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: Proc. of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pp. 220–231. ACM Press, New York (2003)
Marlet, R.: Syntax of the JCVM language to be studied in the SecSafe project. Technical Report SECSAFE-TL-005, Trusted Logic SA (May 2001)
Monniaux, D.: Réalisation mécanisée d’interpréteurs abstraits. Rapport de DEA, Université Paris VII (1998) (in French)
Nielson, H.R., Nielson, F.: Flow Logics for Constraint Based Analysis. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 109–127. Springer, Heidelberg (1998)
Okasaki, C., Gill, A.: Fast mergeable integer maps. In: Workshop on ML, pp. 77–86 (1998)
Prost, F.: Interprétation de l’analyse statique en théorie des types. PhD thesis, École normale supérieure de Lyon (1999) (in French)
Siveroni, I.: Operational semantics of the Java Card Virtual Machine. J. Logic and Automated Reasoning (2004) (to appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cachera, D., Jensen, T., Pichardie, D., Rusu, V. (2004). Extracting a Data Flow Analyser in Constructive Logic. In: Schmidt, D. (eds) Programming Languages and Systems. ESOP 2004. Lecture Notes in Computer Science, vol 2986. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24725-8_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-24725-8_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21313-0
Online ISBN: 978-3-540-24725-8
eBook Packages: Springer Book Archive