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

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

Added section on Matita

File size: 4.1 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\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
67financial support of the Future and Emerging Technologies (FET) programme within
68the Seventh Framework Programme for Research of the European Commission, under
69FET-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}
105We 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
107The 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
109This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level.
110Untrusted 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}
Note: See TracBrowser for help on using the repository browser.