Certified Complexity (CerCo)

被引：19

作者：

Amadio, Roberto M. ^{[4
]}

Ayache, Nicolas ^{[3
,4
]}

Bobot, Francois ^{[3
,4
]}

Boender, Jaap P. ^{[1
]}

Campbell, Brian ^{[2
]}

Garnier, Ilias ^{[3
]}

Madet, Antoine ^{[4
]}

McKinna, James ^{[3
]}

Mulligan, Dominic P. ^{[1
]}

Piccolo, Mauro ^{[1
]}

Pollack, Randy ^{[2
]}

Regis-Gianas, Yann ^{[4
]}

Coen, Claudio Sacerdoti ^{[1
]}

Stark, Ian ^{[2
]}

Tranquilli, Paolo ^{[1
]}

机构：

[1] Univ Bologna, Dipartimento Informat Sci & Ingn, Bologna, Italy

[2] Univ Edinburgh, Sch Informat, LFCS, Edinburgh, Midlothian, Scotland

[3] INRIA, Paris, France

[4] Univ Paris, Paris, France

来源：

FOUNDATIONAL AND PRACTICAL ASPECTS OF RESOURCE ANALYSIS, FOPARA 2013 | 2014年 / 8552卷

关键词：

D O I：

10.1007/978-3-319-12466-7_1

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：1 / 18

页数：18

共 15 条

[1]

Amadio R. M., 2012, LNCS, V7177, P72

[2] Certified Complexity [J].

Armadio, R. ;

Asperti, A. ;

Ayache, N. ;

Campbell, B. ;

Mulligan, D. ;

Pollack, R. ;

Regis-Gianas, Y. ;

Coen, C. Sacerdoti ;

Stark, I. .

PROCEEDINGS OF THE 2ND EUROPEAN FUTURE TECHNOLOGIES CONFERENCE AND EXHIBITION 2011 (FET 11), 2011, 7 :175-177

[3]

Asperti A, 2011, LECT NOTES ARTIF INT, V6803, P64, DOI 10.1007/978-3-642-22438-6_7

[4]

Ayache N, 2012, LECT NOTES COMPUT SC, V7437, P32, DOI 10.1007/978-3-642-32469-7_3

[5]

Bobot Francois., 2012, Formal Methods and Software Engineering, volume 7635 of Lecture Notes in Computer Science, V7635, P167

[6]

Caspi P., 1987, Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, P178, DOI 10.1145/41625.41641

[7]

Cazorla F., 2012, T EMBED COMPUT SYST

[8]

Correnson L., Frama-c user manual

[9]

Hammond K., 2005, TRENDS FUNCTIONAL PR, V6, P195

[10] Formal Verification of a Realistic Compiler [J].

Leroy, Xavier .

COMMUNICATIONS OF THE ACM, 2009, 52 (07) :107-115

← 1 2 →