Changeset 3605


Ignore:
Timestamp:
Mar 6, 2017, 12:46:20 PM (6 months ago)
Author:
mulligan
Message:

bib file

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

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

    r3599 r3605  
     1@TechReport{survey,
     2 author = {W. W\"ogerer},
     3 title = {A Survey of Static Program Analysis Techniques},
     4 institution = {Technische Universit\"at Wien},
     5 year = {2005}
     6}
     7
     8
     9@article{cerco,
     10  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
     11                  B. Campbell and D. P. Mulligan and R. Pollack and
     12                  Y. R{\'e}gis-Gianas and C. Sacerdoti Coen and I.
     13                  Stark},
     14  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
     15                  Brian Campbell and Dominic P. Mulligan and Randy Pollack and
     16                  Yann R{\'e}gis-Gianas and Claudio Sacerdoti Coen and Ian
     17                  Stark},
     18  title     = {Certified Complexity},
     19  journal   = {Procedia Computer Science},
     20  volume    = 7,
     21  year      = 2011,
     22  pages     = {175--177},
     23  doi       = {10.1016/j.procs.2011.09.054},
     24  note      = {Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11)}
     25}
     26
     27@incollection{labelling,
     28year={2012},
     29isbn={978-3-642-32468-0},
     30booktitle={Formal Methods for Industrial Critical Systems},
     31volume={7437},
     32series={LNCS},
     33doi={10.1007/978-3-642-32469-7_3},
     34title={Certifying and Reasoning on Cost Annotations in {C} Programs},
     35url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
     36author={Ayache, Nicolas and Amadio, Roberto and R\'egis-Gianas, Yann},
     37pages={32--46},
     38publisher={Springer Berlin Heidelberg}
     39}
     40
     41@incollection{labelling2,
     42year={2012},
     43booktitle={Foundational and Practical Aspects of Resource Analysis},
     44volume={7177},
     45series={LNCS},
     46doi={10.1007/978-3-642-32495-6_5},
     47title={Certifying and Reasoning on Cost Annotations of Functional Programs},
     48author={Amadio, Roberto and R\'egis-Gianas, Yann},
     49pages={72--89},
     50note={Extended version to appear in Higher Order and Symbolic Computation},
     51publisher={Springer Berlin Heidelberg}
     52}
     53
     54@article{compcert,
     55  author = {Xavier Leroy},
     56  title = {Formal verification of a realistic compiler},
     57  journal = {Communications of the ACM},
     58  year = 2009,
     59  volume = 52,
     60  number = 7,
     61  pages = {107--115},
     62  urlthatwewillskip = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
     63  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
     64  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
     65  pubkind = {journal-int-mono},
     66  abstract = {This paper reports on the development and formal verification (proof
     67of semantic preservation) of CompCert, a compiler from Clight (a
     68large subset of the C programming language) to PowerPC assembly code,
     69using the Coq proof assistant both for programming the compiler and
     70for proving its correctness.  Such a verified compiler is useful in
     71the context of critical software and its formal verification: the
     72verification of the compiler guarantees that the safety properties
     73proved on the source code hold for the executable compiled code as
     74well.}
     75}
     76
     77@Manual{framac,
     78title = {Frama-{C} user manual},
     79author = {L. Correnson and P. Cuoq and F. Kirchner and V. Prevosto and A. Puccetti and J. Signoles and
     80B. Yakobowski},
     81organization = {CEA-LIST, Software Safety Laboratory, Saclay, F-91191},
     82note = {\url{http://frama-c.com/}}
     83}
     84
     85@inproceedings{paolo,
     86 author = {Paolo Tranquilli},
     87 title = {Indexed Labels for Loop Iteration Dependent Costs},
     88 booktitle = {QAPL},
     89 series = {EPTCS},
     90 volume = {117},
     91 doi = {10.4204/EPTCS.117.2},
     92 year = {2013},
     93 pages = {19--23}
     94}
     95
     96@INPROCEEDINGS{separation,
     97    author = {John C. Reynolds},
     98    title = {Intuitionistic Reasoning about Shared Mutable Data Structure},
     99    booktitle = {Millennial Perspectives in Computer Science},
     100    year = {2000},
     101    pages = {303--321},
     102    publisher = {Palgrave}
     103}
     104
     105@inproceedings{lustre,
     106  author    = {Paul Caspi and
     107               Daniel Pilaud and
     108               Nicolas Halbwachs and
     109               John Plaice},
     110  title     = {Lustre: A Declarative Language for Programming Synchronous
     111               Systems},
     112  booktitle = {POPL},
     113  year      = {1987},
     114  pages     = {178-188},
     115  ee        = {http://doi.acm.org/10.1145/41625.41641},
     116  crossref  = {DBLP:conf/popl/1987},
     117  bibsource = {DBLP, http://dblp.uni-trier.de}
     118}
     119@proceedings{DBLP:conf/popl/1987,
     120  title     = {Conference Record of the Fourteenth Annual ACM Symposium
     121               on Principles of Programming Languages, Munich, Germany,
     122               January 21-23, 1987},
     123  booktitle = {POPL},
     124  publisher = {ACM Press},
     125  year      = {1987},
     126  isbn      = {0-89791-215-2},
     127  ee        = {http://dl.acm.org/citation.cfm?id=41625},
     128  bibsource = {DBLP, http://dblp.uni-trier.de}
     129}
     130 
     131@inproceedings{correctness,
     132  author    = {Mulligan, Dominic P.  and
     133               Sacerdoti Coen, Claudio},
     134  title     = {On the Correctness of an Optimising Assembler for the {Intel
     135               MCS-51} Microprocessor},
     136  booktitle = {CPP},
     137  year      = {2012},
     138  pages     = {43--59},
     139  doi       = {10.1007/978-3-642-35308-6_7}
     140}
     141@proceedings{DBLP:conf/cpp/2012,
     142  editor    = {Chris Hawblitzel and
     143               Dale Miller},
     144  title     = {Certified Programs and Proofs - Second International Conference,
     145               CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
     146  booktitle = {CPP},
     147  publisher = {Springer},
     148  series    = {LNCS},
     149  volume    = {7679},
     150  year      = {2012},
     151  isbn      = {978-3-642-35307-9},
     152  ee        = {http://dx.doi.org/10.1007/978-3-642-35308-6},
     153  bibsource = {DBLP, http://dblp.uni-trier.de}
     154}
     155
     156@article{proartis,
     157    title = {PROARTIS: Probabilistically Analysable Real-Time Systems},
     158    journal = {Transactions on Embedded Computing Systems},
     159    year = {2012},
     160    publisher = {ACM},
     161    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}
     162}
     163
     164@inproceedings{embounded,
     165  author    = {Kevin Hammond and
     166               Roy Dyckhoff and
     167               Christian Ferdinand and
     168               Reinhold Heckmann and
     169               Martin Hofmann and
     170               Steffen Jost and
     171               Hans-Wolfgang Loidl and
     172               Greg Michaelson and
     173               Robert F. Pointon and
     174               Norman Scaife and
     175               Jocelyn S{\'e}rot and
     176               Andy Wallace},
     177  title     = {{The {EmBounded} Project (Project Start Paper)}},
     178  booktitle = {TFP},
     179  year      = {2005},
     180  pages     = {195--210},
     181  crossref  = {TFP2005},
     182}
     183
     184@proceedings{TFP2005,
     185  title     = {Revised Selected Papers from the Sixth Symposium on Trends
     186               in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24
     187               September 2005},
     188  booktitle = {Trends in Functional Programming},
     189  series    = {Trends in Functional Programming},
     190  volume    = {6},
     191  year      = {2007},
     192  isbn      = {978-1-84150-176-5},
     193}
     194
     195@inproceedings{matita,
     196  author    = {Andrea Asperti and
     197               Wilmer Ricciotti and
     198               Claudio Sacerdoti Coen and
     199               Enrico Tassi},
     200  title     = {The {Matita} Interactive Theorem Prover},
     201  booktitle = {CADE},
     202  year      = {2011},
     203  pages     = {64-69},
     204  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_7},
     205  crossref  = {DBLP:conf/cade/2011},
     206  bibsource = {DBLP, http://dblp.uni-trier.de}
     207}
     208@proceedings{DBLP:conf/cade/2011,
     209  title     = {Automated Deduction - CADE-23 - 23rd International Conference
     210               on Automated Deduction, Wroclaw, Poland, July 31 - August
     211               5, 2011. Proceedings},
     212  booktitle = {CADE},
     213  publisher = {Springer},
     214  series    = {LNCS},
     215  volume    = {6803},
     216  year      = {2011},
     217  isbn      = {978-3-642-22437-9},
     218  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6},
     219  bibsource = {DBLP, http://dblp.uni-trier.de}
     220}
     221
     222@article{typeffects,
     223  author    = {Jean-Pierre Talpin and
     224               Pierre Jouvelot},
     225  title     = {The Type and Effect Discipline},
     226  journal   = {Inf. Comput.},
     227  volume    = {111},
     228  number    = {2},
     229  year      = {1994},
     230  pages     = {245-296},
     231  ee        = {http://dx.doi.org/10.1006/inco.1994.1046},
     232  bibsource = {DBLP, http://dblp.uni-trier.de}
     233}
     234
     235@article{stateart,
     236  author    = {Reinhard Wilhelm and
     237               Jakob Engblom and
     238               Andreas Ermedahl and
     239               Niklas Holsti and
     240               Stephan Thesing and
     241               David B. Whalley and
     242               Guillem Bernat and
     243               Christian Ferdinand and
     244               Reinhold Heckmann and
     245               Tulika Mitra and
     246               Frank Mueller and
     247               Isabelle Puaut and
     248               Peter P. Puschner and
     249               Jan Staschulat and
     250               Per Stenstr{\"o}m},
     251  title     = {The worst-case execution-time problem---overview of methods
     252               and survey of tools},
     253  journal   = {ACM Trans. Embedded Comput. Syst.},
     254  volume    = {7},
     255  number    = {3},
     256  year      = {2008},
     257  ee        = {http://doi.acm.org/10.1145/1347375.1347389},
     258  bibsource = {DBLP, http://dblp.uni-trier.de}
     259}
     260
     261@inproceedings{bobot,
     262  year={2012},
     263  booktitle={Formal Methods and Software Engineering},
     264  volume={7635},
     265  series={Lecture Notes in Computer Science},
     266  doi={10.1007/978-3-642-34281-3_14},
     267  title={Separation Predicates: A Taste of Separation Logic in First-Order Logic},
     268  url={http://dx.doi.org/10.1007/978-3-642-34281-3_14},
     269  author={Bobot, François and Filliâtre, Jean-Christophe},
     270  pages={167-181}
     271}
     272
     273@misc
     274{ absint,
     275  url = {http://www.absint.com/ait/},
     276  author = {{AbsInt}},
     277  title = {{aiT WCET} analysis tools}
     278}
     279
     280@misc
     281{ cerco-website,
     282  url = {http://cerco.cs.unibo.it},
     283  title = {The {Certified Complexity} ({CerCo}) project web site},
     284  key = {cerco}
     285}
     286
     287@misc
     288{ jessie,
     289  url = {http://krakatoa.lri.fr/},
     290  title = {Jessie {Frama-C} plugin},
     291  key = {jessie}
     292}
  • Papers/jar-cerco-2017/cerco.tex

    r3604 r3605  
    7171\titlerunning{Certified Complexity}
    7272\date{Received: date / Accepted: date}
    73 \author{Jaap Boender \and Brian Campbell \and Dominic P. Mulligan \and Claudio {Sacerdoti Coen}}
     73\author{Jaap Boender \and Brian Campbell \and Dominic P. Mulligan \and Claudio {Sacerdoti Coen}} % who else?
    7474\authorrunning{Boender, Campbell, Mulligan, and Sacerdoti Coen}
    7575\institute{Jaap Boender \at
     
    566566\end{acknowledgements}
    567567
    568 %\bibliographystyle{spbasic}      % basic style, author-year citations
    569 \bibliography{cerco}   % name your BibTeX data base
     568\bibliographystyle{spbasic}
     569\bibliography{cerco}
    570570
    571571\end{document}
Note: See TracChangeset for help on using the changeset viewer.