Changeset 3603


Ignore:
Timestamp:
Mar 6, 2017, 12:37:34 PM (10 months ago)
Author:
mulligan
Message:

added abstract from fopara as a base to work from

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.tex

    r3602 r3603  
    2626\usepackage{amsfonts}
    2727\usepackage{amsmath}
     28\usepackage{amssymb}
    2829\usepackage[british]{babel}
     30\usepackage{color}
     31\usepackage{fancybox}
     32\usepackage{fancyvrb}
    2933\usepackage{graphicx}
    30 \usepackage[colorlinks]{hyperref}
     34\usepackage[colorlinks,
     35            bookmarks,bookmarksopen,bookmarksdepth=2]{hyperref}
     36\usepackage{hyphenat}
     37\usepackage[utf8x]{inputenc}
     38\usepackage{listings}
     39\usepackage{mdwlist}
    3140\usepackage{microtype}
     41\usepackage{stmaryrd}
     42\usepackage{url}
     43
     44\usepackage{tikz}
     45\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes}
    3246
    3347\smartqed
     
    3751the Seventh Framework Programme for Research of the European Commission, under
    3852FET-Open grant number: 243881}}
    39 \subtitle{The verified lifting of concrete complexity annotations}
     53\subtitle{Verified lifting of concrete complexity annotations through a realistic C compiler}
    4054\journalname{Journal of Automated Reasoning}
    4155\titlerunning{Certified Complexity}
    4256\date{Received: date / Accepted: date}
    4357\author{Jaap Boender \and Brian Campbell \and Dominic P. Mulligan \and Claudio {Sacerdoti Coen}}
     58\authorrunning{Boender, Campbell, Mulligan, and Sacerdoti Coen}
    4459\institute{Jaap Boender \at
    4560              Faculty of Science and Technology,\\
     
    7186
    7287\begin{abstract}
     88We provide an overview of the FET-Open Project CerCo (`Certified Complexity').
     89Our 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.
     90The 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.
     91This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level.
     92Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code.
    7393\keywords{Verified compilation \and Complexity analysis \and CerCo (`Certified Complexity')}
    7494\end{abstract}
Note: See TracChangeset for help on using the changeset viewer.