source: Papers/fopara2013/fopara13.bib @ 3435

@TechReport{survey,
 author = {W. W\"ogerer},
 title = {A Survey of Static Program Analysis Techniques},
 institution = {Technische Universit\"at Wien},
 year = {2005}
}


@article{cerco,
  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
                  B. Campbell and D. Mulligan and R. Pollack and
                  Y. R{\'e}gis-Gianas and C. Sacerdoti Coen and I.
                  Stark},
  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
                  Brian Campbell and Dominic Mulligan and Randy Pollack and
                  Yann R{\'e}gis-Gianas and Claudio Sacerdoti Coen and Ian
                  Stark},
  title     = {Certified Complexity},
  journal   = {Procedia Computer Science},
  volume    = 7,
  year      = 2011,
  pages     = {175--177},
  doi       = {10.1016/j.procs.2011.09.054},
  note      = {Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11)}
}

@incollection{labelling,
year={2012},
isbn={978-3-642-32468-0},
booktitle={Formal Methods for Industrial Critical Systems},
volume={7437},
series={LNCS},
editor={Stoelinga, Mariëlle and Pinger, Ralf},
doi={10.1007/978-3-642-32469-7_3},
title={Certifying and Reasoning on Cost Annotations in {C} Programs},
url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
publisher={Springer Berlin Heidelberg},
author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann},
pages={32-46}
}

@incollection{labelling2,
year={2012},
isbn={978-3-642-32494-9},
booktitle={Foundational and Practical Aspects of Resource Analysis},
volume={7177},
series={LNCS},
editor={Peña, Ricardo and Eekelen, Marko and Shkaravska, Olha},
doi={10.1007/978-3-642-32495-6_5},
title={Certifying and Reasoning on Cost Annotations of Functional Programs},
url={http://dx.doi.org/10.1007/978-3-642-32495-6_5},
publisher={Springer Berlin Heidelberg},
author={Amadio, RobertoM. and R\'egis-Gianas, Yann},
pages={72-89},
note={Extended version to appear in Higher Order and Symbolic Computation, 2013}
}

@article{compcert,
  author = {Xavier Leroy},
  title = {Formal verification of a realistic compiler},
  journal = {Communications of the ACM},
  year = 2009,
  volume = 52,
  number = 7,
  pages = {107--115},
  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
  pubkind = {journal-int-mono},
  abstract = {This paper reports on the development and formal verification (proof
of semantic preservation) of CompCert, a compiler from Clight (a
large subset of the C programming language) to PowerPC assembly code,
using the Coq proof assistant both for programming the compiler and
for proving its correctness.  Such a verified compiler is useful in
the context of critical software and its formal verification: the
verification of the compiler guarantees that the safety properties
proved on the source code hold for the executable compiled code as
well.}
}

@Manual{framac,
title = {Frama-{C} user manual},
author = {L. Correnson and P. Cuoq and F. Kirchner and V. Prevosto and A. Puccetti and J. Signoles and
B. Yakobowski},
organization = {CEA-LIST, Software Safety Laboratory, Saclay, F-91191},
note = {\url{http://frama-c.com/}}
}

@Unpublished{paolo,
 author = {Paolo Tranquilli},
 title = {Indexed Labels for Loop Iteration Dependent Costs},
 note = {to appear in EPTCS, proceedings of QAPL 2013},
 month = jan,
 year = {2013},
 url = {http://www.cs.unibo.it/~tranquil/content/docs/indlabels.pdf}
}

@INPROCEEDINGS{separation,
    author = {John C. Reynolds},
    title = {Intuitionistic Reasoning about Shared Mutable Data Structure},
    booktitle = {Millennial Perspectives in Computer Science},
    year = {2000},
    pages = {303--321},
    publisher = {Palgrave}
}

@inproceedings{lustre,
  author    = {Paul Caspi and
               Daniel Pilaud and
               Nicolas Halbwachs and
               John Plaice},
  title     = {Lustre: A Declarative Language for Programming Synchronous
               Systems},
  booktitle = {POPL},
  year      = {1987},
  pages     = {178-188},
  ee        = {http://doi.acm.org/10.1145/41625.41641},
  crossref  = {DBLP:conf/popl/1987},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/popl/1987,
  title     = {Conference Record of the Fourteenth Annual ACM Symposium
               on Principles of Programming Languages, Munich, Germany,
               January 21-23, 1987},
  booktitle = {POPL},
  publisher = {ACM Press},
  year      = {1987},
  isbn      = {0-89791-215-2},
  ee        = {http://dl.acm.org/citation.cfm?id=41625},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
  
@inproceedings{correctness,
  author    = {Mulligan, Dominic P.  and
               Sacerdoti Coen, Claudio},
  title     = {On the Correctness of an Optimising Assembler for the Intel
               MCS-51 Microprocessor},
  booktitle = {CPP},
  year      = {2012},
  pages     = {43-59},
  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6_7},
  crossref  = {DBLP:conf/cpp/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cpp/2012,
  editor    = {Chris Hawblitzel and
               Dale Miller},
  title     = {Certified Programs and Proofs - Second International Conference,
               CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
  booktitle = {CPP},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7679},
  year      = {2012},
  isbn      = {978-3-642-35307-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{proartis,
    title = {PROARTIS: Probabilistically Analysable Real-Time Systems},
    journal = {Transactions on Embedded Computing Systems},
    year = {2012},
    publisher = {ACM},
    author = {Francisco Cazorla and Eduardo Qui{\~n}ones and Tullio Vardanega and Liliana Cucu and Benoit Triquet and Guillem Bernat and Emery Berger and Jaume Abella and Franck Wartel and Michael Houston and Luca Santinelli and Leonidas Kosmidis and Code Lo and Dorin Maxim}
}

@inproceedings{embounded,
  author    = {Kevin Hammond and
               Roy Dyckhoff and
               Christian Ferdinand and
               Reinhold Heckmann and
               Martin Hofmann and
               Steffen Jost and
               Hans-Wolfgang Loidl and
               Greg Michaelson and
               Robert F. Pointon and
               Norman Scaife and
               Jocelyn S{\'e}rot and
               Andy Wallace},
  title     = {{The Embounded Project (Project Start Paper)}},
  booktitle = {TFP},
  year      = {2005},
  pages     = {195--210},
  crossref  = {TFP2005},
}

@proceedings{TFP2005,
  title     = {Revised Selected Papers from the Sixth Symposium on Trends
               in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
               September 2005},
  booktitle = {Trends in Functional Programming},
  publisher = {Intellect, UK/The University of Chicago Press, USA},
  series    = {Trends in Functional Programming},
  volume    = {6},
  year      = {2007},
  isbn      = {978-1-84150-176-5},
}

@inproceedings{matita,
  author    = {Andrea Asperti and
               Wilmer Ricciotti and
               Claudio Sacerdoti Coen and
               Enrico Tassi},
  title     = {The Matita Interactive Theorem Prover},
  booktitle = {CADE},
  year      = {2011},
  pages     = {64-69},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_7},
  crossref  = {DBLP:conf/cade/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2011,
  title     = {Automated Deduction - CADE-23 - 23rd International Conference
               on Automated Deduction, Wroclaw, Poland, July 31 - August
               5, 2011. Proceedings},
  booktitle = {CADE},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6803},
  year      = {2011},
  isbn      = {978-3-642-22437-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{typeffects,
  author    = {Jean-Pierre Talpin and
               Pierre Jouvelot},
  title     = {The Type and Effect Discipline},
  journal   = {Inf. Comput.},
  volume    = {111},
  number    = {2},
  year      = {1994},
  pages     = {245-296},
  ee        = {http://dx.doi.org/10.1006/inco.1994.1046},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{stateart,
  author    = {Reinhard Wilhelm and
               Jakob Engblom and
               Andreas Ermedahl and
               Niklas Holsti and
               Stephan Thesing and
               David B. Whalley and
               Guillem Bernat and
               Christian Ferdinand and
               Reinhold Heckmann and
               Tulika Mitra and
               Frank Mueller and
               Isabelle Puaut and
               Peter P. Puschner and
               Jan Staschulat and
               Per Stenstr{\"o}m},
  title     = {The worst-case execution-time problem - overview of methods
               and survey of tools},
  journal   = {ACM Trans. Embedded Comput. Syst.},
  volume    = {7},
  number    = {3},
  year      = {2008},
  ee        = {http://doi.acm.org/10.1145/1347375.1347389},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{bobot,
  year={2012},
  isbn={978-3-642-34280-6},
  booktitle={Formal Methods and Software Engineering},
  volume={7635},
  series={Lecture Notes in Computer Science},
  editor={Aoki, Toshiaki and Taguchi, Kenji},
  doi={10.1007/978-3-642-34281-3_14},
  title={Separation Predicates: A Taste of Separation Logic in First-Order Logic},
  url={http://dx.doi.org/10.1007/978-3-642-34281-3_14},
  publisher={Springer Berlin Heidelberg},
  author={Bobot, François and Filliâtre, Jean-Christophe},
  pages={167-181}
}