Abstract
Static analyzers usually return partial results. They can assert that some properties are valid during all possible executions of a program, but generally leave some other properties to be verified by other means. In practice, it is common to combine results from several methods manually to achieve the full verification of a program. In this context, Frama-C is a platform for analyzing C source programs with multiple analyzers. Hence, one analyzer might conclude about properties assumed by another one, in the same environment. We present here the semantical foundations of validity of program properties in such a context. We propose a correct and complete algorithm for combining several partial results into a fully consolidated validity status for each program property. We illustrate how such a framework provides meaningful feedback on partial results.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8) (1975)
Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B.: Frama-C User Manual (October 2011), http://frama-c.com
Elberzhager, F., Münch, J., Nha, V.T.N.: A systematic mapping study on the combination of static and dynamic quality assurance techniques. Information & Software Technology 54(1), 1–15 (2012)
Heintze, N., Jaffar, J., Voicu, R.: A framework for combining analysis and verification. In: POPL 2000 (2000)
Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 382–398. Springer, Heidelberg (2011)
Comar, C., Kanig, J., Moy, Y.: Integrating formal program verification with testing. In: ERTSS 2012 (2012)
Baudin, P., Filliâtre, J.C., Hubert, T., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language (February 2011), http://frama-c.cea.fr/acsl.html
Canet, G., Cuoq, P., Monate, B.: A Value Analysis for C Programs. In: SCAM 2009 (2009)
Correnson, L., Dargaye, Z.: WP Plug-in Manual, version 0.5 (January 2012)
Baudin, P., Correnson, L., Hermann, P.: WP Tutorial, version 0.5. (January 2012)
Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo Automated Theorem Prover, http://alt-ergo.lri.fr
Herms, P., Marché, C., Monate, B.: A Certified Multi-prover Verification Condition Generator. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 2–17. Springer, Heidelberg (2012)
Grall, H.: Deux critères de sécurité pour l’exécution de code mobile. PhD thesis, École Nationale des Ponts et Chaussées (December 2003) (in French)
Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation 207(2) (2009)
Giorgetti, A., Groslambert, J., Julliand, J., Kouchnarenko, O.: Verification of class liveness properties with Java Modeling Language. IET Software 2(6) (2008)
Cuoq, P., Monate, B., Pacalet, A., Prevosto, V., Regehr, J., Yakobowski, B., Yang, X.: Testing Static Analyzers with Randomly Generated Programs. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 120–125. Springer, Heidelberg (2012)
Delahaye, M., Kosmatov, N., Signoles, J.: Towards a common specification language for static and dynamic analyses of C programs (submitted)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Correnson, L., Signoles, J. (2012). Combining Analyses for C Program Verification. In: Stoelinga, M., Pinger, R. (eds) Formal Methods for Industrial Critical Systems. FMICS 2012. Lecture Notes in Computer Science, vol 7437. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32469-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-32469-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32468-0
Online ISBN: 978-3-642-32469-7
eBook Packages: Computer ScienceComputer Science (R0)