Abstract
We provide an overview of the FET-Open Project CerCo (‘Certified Complexity’). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of accuracy and a small trusted code base. The core component is a C compiler, verified in Matita, that produces an instrumented copy of the source code in addition to generating object code. This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level. Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code.
The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
AbsInt: aiT WCET analysis tools. http://www.absint.com/ait/
Amadio, R., Asperti, A., Ayache, N., Campbell, B., Mulligan, D.P., Pollack, R., Régis-Gianas, Y., Coen, C.S., Stark, I.: Certified complexity. Procedia Comput. Sci. 7, 175–177 (2011). Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11)
Amadio, R.M., Régis-Gianas, Y.: Certifying and reasoning on cost annotations of functional programs. In: Peña, R., van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2011. LNCS, vol. 7177, pp. 72–89. Springer, Heidelberg (2012). Extended version to appear in Higher Order and Symbolic Computation
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The matita interactive theorem prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64–69. Springer, Heidelberg (2011)
Ayache, N., Amadio, R.M., Régis-Gianas, Y.: Certifying and reasoning on cost annotations in C programs. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 32–46. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-32469-7_3
Bobot, F., Filliâtre, J.-C.: Separation predicates: a taste of separation logic in first-order logic. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 167–181. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-34281-3_14
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: a declarative language for programming synchronous systems. In: POPL, pp. 178–188. ACM Press (1987)
Cazorla, F., Quiñones, E., Vardanega, T., Cucu, L., Triquet, B., Bernat, G., Berger, E., Abella, J., Wartel, F., Houston, M., Santinelli, L., Kosmidis, L., Lo, C., Maxim, D.: Proartis: probabilistically analysable real-time systems. Trans. Embed. Comput. Syst. (2012)
The Certified Complexity (CerCo) project web site. http://cerco.cs.unibo.it
Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B.: Frama-C user manual. CEA-LIST, Software Safety Laboratory, Saclay, F-91191. http://frama-c.com/
Hammond, K., Dyckhoff, R., Ferdinand, C., Heckmann, R., Hofmann, M., Jost, S., Loidl, H.W., Michaelson, G., Pointon, R.F., Scaife, N., Sérot, J., Wallace, A.: The EmBounded project (project start paper). Trends Funct. Program. TFP 6, 195–210 (2005)
Jessie Frama-C plugin. http://krakatoa.lri.fr/
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Mulligan, D.P., Sacerdoti Coen, C.: On the correctness of an optimising assembler for the intel MCS-51 microprocessor. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 43–59. Springer, Heidelberg (2012)
Talpin, J.P., Jouvelot, P.: The type and effect discipline. Inf. Comput. 111(2), 245–296 (1994)
Tranquilli, P.: Indexed labels for loop iteration dependent costs. In: QAPL. EPTCS, vol. 117, pp. 19–23 (2013)
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenström, P.: The worst-case execution-time problem-overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7(3), 1–53 (2008)
Wögerer, W.: A survey of static program analysis techniques. Technical report, Technische Universität Wien (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Amadio, R.M. et al. (2014). Certified Complexity (CerCo). In: Dal Lago, U., Peña, R. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2013. Lecture Notes in Computer Science(), vol 8552. Springer, Cham. https://doi.org/10.1007/978-3-319-12466-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-12466-7_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12465-0
Online ISBN: 978-3-319-12466-7
eBook Packages: Computer ScienceComputer Science (R0)