1 | \begin{filecontents*}{example.eps} |
---|
2 | %!PS-Adobe-3.0 EPSF-3.0 |
---|
3 | %%BoundingBox: 19 19 221 221 |
---|
4 | %%CreationDate: Mon Sep 29 1997 |
---|
5 | %%Creator: programmed by hand (JK) |
---|
6 | %%EndComments |
---|
7 | gsave |
---|
8 | newpath |
---|
9 | 20 20 moveto |
---|
10 | 20 220 lineto |
---|
11 | 220 220 lineto |
---|
12 | 220 20 lineto |
---|
13 | closepath |
---|
14 | 2 setlinewidth |
---|
15 | gsave |
---|
16 | .4 setgray fill |
---|
17 | grestore |
---|
18 | stroke |
---|
19 | grestore |
---|
20 | \end{filecontents*} |
---|
21 | |
---|
22 | \RequirePackage{fix-cm} |
---|
23 | |
---|
24 | \documentclass[smallextended]{svjour3} |
---|
25 | |
---|
26 | \usepackage{amsfonts} |
---|
27 | \usepackage{amsmath} |
---|
28 | \usepackage{amssymb} |
---|
29 | \usepackage[british]{babel} |
---|
30 | \usepackage{color} |
---|
31 | \usepackage{fancybox} |
---|
32 | \usepackage{fancyvrb} |
---|
33 | \usepackage{graphicx} |
---|
34 | \usepackage[colorlinks, |
---|
35 | bookmarks,bookmarksopen,bookmarksdepth=2]{hyperref} |
---|
36 | \usepackage{hyphenat} |
---|
37 | \usepackage[utf8x]{inputenc} |
---|
38 | \usepackage{listings} |
---|
39 | \usepackage{mdwlist} |
---|
40 | \usepackage{microtype} |
---|
41 | \usepackage{stmaryrd} |
---|
42 | \usepackage{url} |
---|
43 | |
---|
44 | \usepackage{tikz} |
---|
45 | \usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes} |
---|
46 | |
---|
47 | \lstset{language=C,basicstyle=\tt,basewidth=.5em,lineskip=-1.5pt} |
---|
48 | \def\lstlanguagefiles{lst-grafite.tex} |
---|
49 | |
---|
50 | \newlength{\mylength} |
---|
51 | \newenvironment{frametxt}% |
---|
52 | {\setlength{\fboxsep}{5pt} |
---|
53 | \setlength{\mylength}{\linewidth}% |
---|
54 | \addtolength{\mylength}{-2\fboxsep}% |
---|
55 | \addtolength{\mylength}{-2\fboxrule}% |
---|
56 | \Sbox |
---|
57 | \minipage{\mylength}% |
---|
58 | \setlength{\abovedisplayskip}{0pt}% |
---|
59 | \setlength{\belowdisplayskip}{0pt}% |
---|
60 | }% |
---|
61 | {\endminipage\endSbox |
---|
62 | \[\fbox{\TheSbox}\]} |
---|
63 | |
---|
64 | \smartqed |
---|
65 | |
---|
66 | \title{CerCo: Certified Complexity\thanks{The project CerCo acknowledges the |
---|
67 | financial support of the Future and Emerging Technologies (FET) programme within |
---|
68 | the Seventh Framework Programme for Research of the European Commission, under |
---|
69 | FET-Open grant number: 243881}} |
---|
70 | \subtitle{Verified lifting of concrete complexity annotations through a realistic C compiler} |
---|
71 | \journalname{Journal of Automated Reasoning} |
---|
72 | \titlerunning{Certified Complexity} |
---|
73 | \date{Received: date / Accepted: date} |
---|
74 | \author{Jaap Boender \and Brian Campbell \and Dominic P. Mulligan \and Claudio Sacerdoti~Coen} % who else? |
---|
75 | \authorrunning{Boender, Campbell, Mulligan, and Sacerdoti~Coen} |
---|
76 | \institute{Jaap Boender \at |
---|
77 | Faculty of Science and Technology,\\ |
---|
78 | Middlesex University London,\\ |
---|
79 | United Kingdom.\\ |
---|
80 | \email{J.Boender@mdx.ac.uk} |
---|
81 | \and |
---|
82 | Brian Campbell \at |
---|
83 | Department of Informatics,\\ |
---|
84 | University of Edinburgh,\\ |
---|
85 | United Kingdom.\\ |
---|
86 | \email{Brian.Campbell@ed.ac.uk} |
---|
87 | \and |
---|
88 | Dominic P. Mulligan \at |
---|
89 | Computer Laboratory,\\ |
---|
90 | University of Cambridge, \\ |
---|
91 | United Kingdom.\\ |
---|
92 | \email{Dominic.Mulligan@cl.cam.ac.uk} |
---|
93 | \and |
---|
94 | Claudio Sacerdoti~Coen \at |
---|
95 | Dipartimento di Informatica---Scienza e Ingegneria (DISI),\\ |
---|
96 | University of Bologna,\\ |
---|
97 | Italy.\\ |
---|
98 | \email{Claudio.SacerdotiCoen@unibo.it}} |
---|
99 | |
---|
100 | \begin{document} |
---|
101 | |
---|
102 | \maketitle |
---|
103 | |
---|
104 | \begin{abstract} |
---|
105 | 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. |
---|
106 | |
---|
107 | The core component is a C compiler, verified in the Matita theorem prover, that produces an instrumented copy of the source code in addition to generating object code. |
---|
108 | |
---|
109 | This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level. |
---|
110 | Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code. |
---|
111 | \keywords{Verified compilation \and Complexity analysis \and CerCo (`Certified Complexity')} |
---|
112 | \end{abstract} |
---|
113 | |
---|
114 | \include{introduction} |
---|
115 | \include{architecture} |
---|
116 | \include{proof} |
---|
117 | \include{development} |
---|
118 | \include{framac} |
---|
119 | \include{conclusions} |
---|
120 | |
---|
121 | \begin{acknowledgements} |
---|
122 | \end{acknowledgements} |
---|
123 | |
---|
124 | \bibliographystyle{spmpsci} |
---|
125 | \bibliography{cerco} |
---|
126 | |
---|
127 | \end{document} |
---|