source: Papers/jar-cerco-2017/cerco.tex @ 3613

Last change on this file since 3613 was 3613, checked in by boender, 3 years ago

Cut paper into sections, continued introduction rewrite

File size: 4.9 KB
Line 
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
7gsave
8newpath
9  20 20 moveto
10  20 220 lineto
11  220 220 lineto
12  220 20 lineto
13closepath
142 setlinewidth
15gsave
16  .4 setgray fill
17grestore
18stroke
19grestore
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
103financial support of the Future and Emerging Technologies (FET) programme within
104the Seventh Framework Programme for Research of the European Commission, under
105FET-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}
141We 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
143The 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
145This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level.
146Untrusted 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}
Note: See TracBrowser for help on using the repository browser.