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 | |
---|
49 | \newlength{\mylength} |
---|
50 | \newenvironment{frametxt}% |
---|
51 | {\setlength{\fboxsep}{5pt} |
---|
52 | \setlength{\mylength}{\linewidth}% |
---|
53 | \addtolength{\mylength}{-2\fboxsep}% |
---|
54 | \addtolength{\mylength}{-2\fboxrule}% |
---|
55 | \Sbox |
---|
56 | \minipage{\mylength}% |
---|
57 | \setlength{\abovedisplayskip}{0pt}% |
---|
58 | \setlength{\belowdisplayskip}{0pt}% |
---|
59 | }% |
---|
60 | {\endminipage\endSbox |
---|
61 | \[\fbox{\TheSbox}\]} |
---|
62 | |
---|
63 | \smartqed |
---|
64 | |
---|
65 | % PROPOSED PAPER STRUCTURE |
---|
66 | |
---|
67 | % Introduction |
---|
68 | % Problem being solved, background, etc. |
---|
69 | % Current state of the art (and problem with it) |
---|
70 | % The `CerCo approach' (tm) |
---|
71 | % Brief Matita overview |
---|
72 | % Map of paper |
---|
73 | |
---|
74 | % CerCo compiler architecture |
---|
75 | % Description of languages |
---|
76 | % Target hardware description |
---|
77 | |
---|
78 | % Compiler proof |
---|
79 | % Structure of proof, and high-level discussion |
---|
80 | % Technical devices: structured traces, labelling, etc. |
---|
81 | % Assembler proof |
---|
82 | % Technical issues in front end (Brian?) |
---|
83 | % Main theorem statement |
---|
84 | |
---|
85 | % FramaC plugin |
---|
86 | % Purpose |
---|
87 | % Description of architecture |
---|
88 | % Case study/worked example (crypto example?) |
---|
89 | |
---|
90 | % Formal development |
---|
91 | % Source code repo link |
---|
92 | % Statistics (number of lines, etc.) |
---|
93 | % Description of remaining axioms --- try and explain them away/make them sound reasonable |
---|
94 | |
---|
95 | % Conclusions |
---|
96 | % Summary |
---|
97 | % Related work |
---|
98 | % Future work |
---|
99 | |
---|
100 | % Bibliography |
---|
101 | |
---|
102 | \title{CerCo: Certified Complexity\thanks{The project CerCo acknowledges the |
---|
103 | financial support of the Future and Emerging Technologies (FET) programme within |
---|
104 | the Seventh Framework Programme for Research of the European Commission, under |
---|
105 | FET-Open grant number: 243881}} |
---|
106 | \subtitle{Verified lifting of concrete complexity annotations through a realistic C compiler} |
---|
107 | \journalname{Journal of Automated Reasoning} |
---|
108 | \titlerunning{Certified Complexity} |
---|
109 | \date{Received: date / Accepted: date} |
---|
110 | \author{Jaap Boender \and Brian Campbell \and Dominic P. Mulligan \and Claudio Sacerdoti~Coen} % who else? |
---|
111 | \authorrunning{Boender, Campbell, Mulligan, and Sacerdoti~Coen} |
---|
112 | \institute{Jaap Boender \at |
---|
113 | Faculty of Science and Technology,\\ |
---|
114 | Middlesex University London,\\ |
---|
115 | United Kingdom.\\ |
---|
116 | \email{J.Boender@mdx.ac.uk} |
---|
117 | \and |
---|
118 | Brian Campbell \at |
---|
119 | Department of Informatics,\\ |
---|
120 | University of Edinburgh,\\ |
---|
121 | United Kingdom.\\ |
---|
122 | \email{Brian.Campbell@ed.ac.uk} |
---|
123 | \and |
---|
124 | Dominic P. Mulligan \at |
---|
125 | Computer Laboratory,\\ |
---|
126 | University of Cambridge, \\ |
---|
127 | United Kingdom.\\ |
---|
128 | \email{Dominic.Mulligan@cl.cam.ac.uk} |
---|
129 | \and |
---|
130 | Claudio Sacerdoti~Coen \at |
---|
131 | Dipartimento di Informatica---Scienza e Ingegneria (DISI),\\ |
---|
132 | University of Bologna,\\ |
---|
133 | Italy.\\ |
---|
134 | \email{Claudio.SacerdotiCoen@unibo.it}} |
---|
135 | |
---|
136 | \begin{document} |
---|
137 | |
---|
138 | \maketitle |
---|
139 | |
---|
140 | \begin{abstract} |
---|
141 | 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. |
---|
142 | |
---|
143 | 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. |
---|
144 | |
---|
145 | This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level. |
---|
146 | Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code. |
---|
147 | \keywords{Verified compilation \and Complexity analysis \and CerCo (`Certified Complexity')} |
---|
148 | \end{abstract} |
---|
149 | |
---|
150 | \include{introduction} |
---|
151 | \include{architecture} |
---|
152 | \include{proof} |
---|
153 | \include{framac} |
---|
154 | \include{conclusions} |
---|
155 | |
---|
156 | \begin{acknowledgements} |
---|
157 | \end{acknowledgements} |
---|
158 | |
---|
159 | \bibliographystyle{spmpsci} |
---|
160 | \bibliography{cerco} |
---|
161 | |
---|
162 | \end{document} |
---|