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 

piccolo14dice (Unpublished)
Author(s) Mauro Piccolo, Claudio Sacerdoti Coen and Paolo Tranquilli
Title« The labelling approach to precise resource analysis on the source code, revisited »
NoteAccepted for presentation in DICE 2014
Abstract
The labelling approach is a technique to lift cost models for non-functional properties of programs from the object code to the source. It allows to perform precise resource analysis of programs directly on the source code, reconciling functional and non functional analysis. The labelling approach is based on the preservation of the structure of the high level program in every intermediate language used by the compiler. In order to prove the cost model correct, the semantics of programs is described with a labelled transition system that makes the program structure observable. The original version of the labelling approach does not simply scale to function calls and it may not work properly with source instructions that have several predecessors. In the talk we will present an improved version that take cares of both limitations and that is more modular. Most of the results presented have being mechanised in the interactive theorem prover Matita.

BibTeX code

@unpublished{piccolo14dice,
  abstract = {The labelling approach is a technique to lift cost models for
              non-functional properties of programs from the object code to the
              source. It allows to perform precise resource analysis of programs
              directly on the source code, reconciling functional and non
              functional analysis. The labelling approach is based on the
              preservation of the structure of the high level program in every
              intermediate language used by the compiler. In order to prove the
              cost model correct, the semantics of programs is described with a
              labelled transition system that makes the program structure
              observable. The original version of the labelling approach does
              not simply scale to function calls and it may not work properly
              with source instructions that have several predecessors. In the
              talk we will present an improved version that take cares of both
              limitations and that is more modular. Most of the results
              presented have being mechanised in the interactive theorem prover
              Matita.},
  title = {The labelling approach to precise resource analysis on the source
           code, revisited},
  author = {Piccolo, Mauro and Sacerdoti Coen, Claudio and Tranquilli, Paolo},
  note = {Accepted for presentation in DICE 2014},
  year = {2014},
}


 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!