Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

amadio14fopara (In proceedings)
Author(s) Roberto M. Amadio, Nicholas Ayache, François Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark and Paolo Tranquilli
Title« Certified Complexity (CerCo) »
InFoundational and Practical Aspects of Resource Analysis - Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013, Revised Selected Papers
SeriesLecture Notes in Computer Science
Editor(s) Ugo Dal Lago and Ricardo Peña
Volume8552
Page(s)1--18
Year2013
PublisherSpringer
Abstract
This paper provides an overview of the FET-Open Project CerCo (`Certified Complexity'). The project's main achievement is the de- velopment of a technique for performing static analyses of non-functional properties of programs (time, space) at the source level, without loss of accuracy and with a small, trusted code base. The main software component developed is a certified compiler producing cost annotations. The compiler translates source code to object code and produces an instrumented copy of the source code. This instrumentation exposes at the source level¦and tracks precisely¦the actual (non-asymptotic) computational cost of the input program. Untrusted invariant generators and trusted theorem provers are then used to compute and certify the parametric execution time of the code.

BibTeX code

@inproceedings{amadio14fopara,
  volume = {8552},
  author = {Roberto M. Amadio and Nicholas Ayache and Fran{\c{c}}ois Bobot and
            Jaap Boender and Brian Campbell and Ilias Garnier and Antoine Madet
            and James McKinna and Dominic P. Mulligan and Mauro Piccolo and
            Randy Pollack and Yann R{\'{e}}gis{-}Gianas and Claudio Sacerdoti
            Coen and Ian Stark and Paolo Tranquilli},
  series = {Lecture Notes in Computer Science},
  booktitle = {Foundational and Practical Aspects of Resource Analysis - Third
               International Workshop, {FOPARA} 2013, Bertinoro, Italy, August
               29-31, 2013, Revised Selected Papers},
  editor = {Ugo Dal Lago and Ricardo Pe{\~{n}}a},
  abstract = {This paper provides an overview of the FET-Open Project CerCo
              (`Certified Complexity'). The project's main achievement is the
              de- velopment of a technique for performing static analyses of
              non-functional properties of programs (time, space) at the source
              level, without loss of accuracy and with a small, trusted code
              base. The main software component developed is a certified
              compiler producing cost annotations. The compiler translates
              source code to object code and produces an instrumented copy of
              the source code. This instrumentation exposes at the source
              level|and tracks precisely|the actual (non-asymptotic)
              computational cost of the input program. Untrusted invariant
              generators and trusted theorem provers are then used to compute
              and certify the parametric execution time of the code.},
  title = {Certified Complexity (CerCo)},
  publisher = {Springer},
  pages = {1--18},
  year = {2013},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!