biblio.bib

@STRING{SV = {Springer}}

@STRING{LNCS = {Lecture Notes in Computer Science}}

@Misc{ESCJava2,
  title =	 {{ESC/Java2}},
  author = {Kiniry, Joseph},
  note =	 {\url{http://kind.ucd.ie/products/opensource/ESCJava2/}}
}

@InProceedings{Kiniry-Cok05,
	author = "David R. Cok and Joseph R. Kiniry",
	title = "{ESC/Java2}: Uniting {ESC/Java} and {JML}: Progress and
	issues in building and using {ESC/Java2}, including
	a case study involving the use of the tool to
	verify portions of an {Internet} voting tally system",
	booktitle = "Construction and Analysis of Safe,
	Secure, and Interoperable Smart Devices (CASSIS 2004)",
	editor = "Gilles Barthe and Lilian Burdy and Marieke Huisman and Jean-Louis Lanet and Traian Muntean",
	year = 2005,
	pages = "108-128",
	series = LNCS,
	publisher = SV,
	URL ={http://dx.doi.org/10.1007/b105030},
	volume = 3362
}

@BOOK{KR88,
  author = {Brian Kernighan and Dennis Ritchie},
  title = {The C Programming Language (2nd Ed.)},
  publisher = {Prentice-Hall},
  year = 1988
}

@ARTICLE{barnett04jot,
  author = {Mike Barnett and Robert DeLine and Manuel F\"ahndrich and K. Rustan M. Leino and Wolfram Schulte},
  title = {Verification of object-oriented programs with invariants},
  journal = {Journal of Object Technology},
  year = 2004,
  volume = 3,
  number = 6,
  pages = {27--56},
  month = JUN
}

@INPROCEEDINGS{leavens00jml,
  author = {Gary T. Leavens and K. Rustan M. Leino and Erik Poll
                 and Clyde Ruby and Bart Jacobs},
  title = {{JML}: notations and tools supporting detailed design in {Java}},
  booktitle = {{OOPSLA} 2000 Companion, Minneapolis, Minnesota},
  pages = {105--106},
  year = 2000
}

@TECHREPORT{leavens00preliminary,
  author = {Gary T. Leavens and Albert L. Baker and Clyde Ruby},
  title = {Preliminary Design of {JML}: {A} Behavioral Interface
           Specification Language for {Java}},
  institution = {Iowa State University},
  number = {98-06i},
  year = 2000
}

@ARTICLE{hatcliff2012behavioral,
	title={Behavioral interface specification languages},
	author={Hatcliff, John and Leavens, Gary T. and Leino, K Rustan M and M{\"u}ller, Peter and Parkinson, Matthew},
	journal={ACM Computing Surveys (CSUR)},
	volume={44},
	NUMBER={3},
	pages={16},
	year={2012},
	publisher={ACM}
}

@TECHREPORT{raghavan00desugaring,
  author = {Arun D. Raghavan and Gary T. Leavens},
  title = {Desugaring {JML} Method Specifications},
  institution = {Iowa State University},
  number = {00-03a},
  year = 2000
}

@INPROCEEDINGS{filliatre04icfem,
  author = {Jean-Christophe Filli{\^a}tre and Claude March{\'e}},
  title = {Multi-Prover Verification of {C} Programs},
  crossref = {icfem04},
  year = {2004},
  pages = {15--29},
  topics = {team},
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz}
}

@INPROCEEDINGS{filliatre07cav,
  author = {Jean-Christophe Filli\^atre and Claude March\'e},
  title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
  Verification},
  topics = {team, lri},
  crossref = {cav07},
  url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf}
}

@INPROCEEDINGS{chalin07icse,
  author = {Patrice Chalin},
  title = {A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler},
  booktitle = {Proceedings of the International Conference on Software Engineering (ICSE'07)},
  pages = {23-33},
  year = 2007,
  address = {Los Alamitos, CA, USA},
  publisher = {IEEE Computer Society}
}

@INPROCEEDINGS{chalin05ftfjp,
  author = {Patrice Chalin},
  title = {Reassessing {JML}'s Logical Foundation},
  booktitle = {Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP'05)},
  year = 2005,
  address = {Glasgow, Scotland},
  month = JUL
}

@TECHREPORT{kiriny07implnotes,
  author = {David R. Cok and Joseph R. Kiniry},
  title = {{ESC/Java2} Implementation Notes},
  year = 2007,
  month = may,
  institution = {University College Dublin},
  note = {\url{http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/Escjava2-ImplementationNotes.pdf}}
}

@INPROCEEDINGS{necula02ccured,
  author = {George C. Necula and Scott McPeak and Westley Weimer},
  title = {{CCured}: Type-Safe Retrofitting of Legacy Code},
  booktitle = {Symposium on Principles of Programming Languages},
  year = {2002},
  pages = {128--139}
}

@INPROCEEDINGS{condit03ccured,
  author = {Jeremy Condit and Matthew Harren and Scott McPeak and George C. Necula and Westley Weimer},
  title = {CCured in the real world},
  booktitle = {PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation},
  year = {2003},
  pages = {232--244}
}

@INPROCEEDINGS{condit07deputy,
  author = {Jeremy Paul Condit and Matthew Thomas Harren and Zachary Ryan Anderson and David Gay and George Necula},
  booktitle = {ESOP '07: Proceedings of the 16th European Symposium on Programming},
  title = {Dependent Types for Low-Level Programming},
  year = {2006},
  month = Oct
}

@MISC{jmlhomepage,
  title = {JML},
  author = { Gary Leavens},
  note = {\url{http://www.eecs.ucf.edu/~leavens/JML/}}
}

@TECHREPORT{moy07ccpp,
  author = {Yannick Moy},
  title = {Union and Cast in Deductive Verification},
  booktitle = {Proceedings of the {C/C++} Verification Workshop},
  year = {2007},
  month = jul,
  institution = {Radboud University Nijmegen},
  number = {ICIS-R07015},
  note = {\url{http://www.lri.fr/~moy/union_and_cast/union_and_cast.pdf}}
}

@MANUAL{standardc99,
  title = {The {ANSI C} standard ({C99})},
  organization = {International Organization for Standardization ({ISO})},
  key = {C99},
  note = {\url{http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf}}
}

@PROCEEDINGS{icfem04,
  title = {Formal Engineering Methods},
  year = 2004,
  booktitle = {6th International Conference on Formal Engineering Methods},
  series = LNCS,
  volume = 3308,
  editor = {Jim Davies and Wolfram Schulte and Mike Barnett},
  address = {Seattle, WA, USA},
  month = NOV,
  publisher = SV
}

@PROCEEDINGS{cav07,
  editor = {Werner Damm and Holger Hermanns},
  title = {Computer Aided Verification},
  booktitle = {19th International Conference on Computer Aided Verification},
  publisher = SV,
  series = LNCS,
  address = {Berlin, Germany},
  month = JUL,
  year = {2007}
}


@book{Morgan94,
 author = {Carroll Morgan},
 title = {Programming from specifications (2nd ed.)},
 year = 1994,
 isbn = {0-13-123274-6},
 publisher = {Prentice Hall International (UK) Ltd.},
 }

@INCOLLECTION{marche07,
  AUTHOR = {Claude March\'e},
  TITLE = {Towards Modular Algebraic Specifications for Pointer Programs: a Case Study},
  BOOKTITLE = {Rewriting, Computation and Proof},
  PAGES = {235--258},
  YEAR = 2007,
  EDITOR = {H. Comon-Lundh and C. Kirchner and H. Kirchner},
  VOLUME = 4600,
  SERIES = LNCS,
  PUBLISHER = {Springer-Verlag}
}

@article{leavens07,
 author = {Gary T. Leavens and K. Rustan M. Leino and Peter M\"uller},
 title = {Specification and verification challenges for sequential object-oriented programs},
 journal = {Form. Asp. Comput.},
 volume = {19},
 number = {2},
 year = {2007},
 issn = {0934-5043},
 pages = {159--189},
 doi = {http://dx.doi.org/10.1007/s00165-007-0026-7},
 publisher = {Springer-Verlag},
 address = {London, UK}
 }

@Misc{Coq,
  title = 	 {{The Coq Proof Assistant}},
  key =          {Coq},
  note = 	 {\url{http://coq.inria.fr/}}
}

@Misc{frama-c,
  title = 	 {{The Frama-C framework for analysis of C code.}},
  key =          {Frama-C},
  note = 	 {\url{http://frama-c.cea.fr/}}
}



@inproceedings{giorgetti06fase,
author = {Giorgetti, A. and Groslambert, J.},
title = {{JAG}: {JML} {A}nnotation {G}eneration for Verifying Temporal Properties},
booktitle = {FASE'2006, Fundamental Approaches to Software Engineering},
series = {LNCS},
volume = 3922,
pages = {373--376},
address = {Vienna, Austria},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/11693017_27},
month = mar,
year = 2006,

}

@Book{abrial96:_b_book,
  author =    {Jean-Raymond Abrial},
  title =        {{The B-Book: Assigning Programs to Meanings}},
  publisher =    {{Cambridge University Press}},
  year =         1996}

@Misc{wikipedia-fo-logic,
  author =    {Wikipedia},
  title =     {First Order Logic},
  howpublished = {\url{http://en.wikipedia.org/wiki/First_order_logic}}}

@Misc{wikipedia-float,
 author =    {Wikipedia},
  title =     {{IEEE 754}},
  howpublished = {\url{http://en.wikipedia.org/wiki/IEEE_754-1985}}}


@Article{float-std,
  author =       {David Stevenson and others},
  title =        {An american national standard: {IEEE} standard for binary floating point arithmetic},
  journal =      {{ACM SIGPLAN} Notices},
  year =         1987,
  volume =    22,
  number =    2,
  pages =     {9-25}}

@Misc{cil,
title={{The C Intermediate Language (CIL) library}},
author={{Berkeley University}},
howpublished={\url{http://manju.cs.berkeley.edu/cil/}}
}


@inproceedings{BoldoFilliatre07,
  author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
  title = {{Formal Verification of Floating-Point Programs}},
  booktitle = {18th IEEE International Symposium on Computer Arithmetic},
  pages = {187-194},
  month = jun,
  year = 2007,
  address = {Montpellier, France},
  topics = {team,lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  abstract = {
  This paper introduces a methodology to perform formal verification
  of floating-point C programs. It extends an existing tool for the
  verification of C programs, Caduceus, with new annotations specific
  to floating-point arithmetic. The Caduceus first-order logic model
  for C programs is extended accordingly. Then verification conditions
  expressing the correctness of the programs are obtained in the usual
  way and can be discharged interactively with the Coq proof
  assistant, using an existing Coq formalization of floating-point
  arithmetic.  This methodology is already implemented and has been
  successfully applied to several short floating-point programs, which
  are presented in this paper.}
}

@techreport{ayad09rr,
  author = {Ali Ayad},
  title = {On formal methods for certifying floating-point {C} programs},
  institution = {INRIA},
  year = 2009,
  note = {\url{http://hal.inria.fr/inria-00383793/fr}}
}

@Misc{ayad09,
  author =    {Ali Ayad and Claude March\'e},
  title =     {Behavioral Properties of Floating-Point Programs},
  howpublished = {Hisseo publications},
  year =      2009,
  note =      {\url{http://hisseo.saclay.inria.fr/ayad09.pdf}},
  url =      {http://hisseo.saclay.inria.fr/ayad09.pdf},
  topics = {team}
}

@inproceedings{ayad10ijcar,
  author = {Ali Ayad and Claude March\'e},
  title = {Multi-Prover Verification of Floating-Point Programs},
  crossref = {ijcar10},
  url = {http://www.lri.fr/~marche/ayad10ijcar.pdf},
  topics = {team},
  type_publi = {icolcomlec}
}

@proceedings{ijcar10,
  title = {International Joint Conference on Automated Reasoning},
  booktitle = {Fifth International Joint Conference on Automated Reasoning},
  year = 2010,
  editor = {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
  address = {Edinburgh, Scotland},
  month = jul,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer}
}


@Misc{boldo09misc,
  author =    {Boldo, Sylvie and Nguyen, Thi Minh Tuyen},
  title =     {Hardware-independent proofs of numerical programs},
  howpublished = {Hisseo publications},
  year =      2009,
  note =      {\url{http://hisseo.saclay.inria.fr/tuyen09.pdf}},
  url =      {http://hisseo.saclay.inria.fr/tuyen09.pdf},
  topics = {team}
}

@inproceedings{boldo10-nfm,
  author = {Sylvie Boldo and Thi Minh Tuyen Nguyen},
  title = {Hardware-independent proofs of numerical programs},
  booktitle = {Proceedings of the Second NASA Formal Methods Symposium},
  year = 2010,
  series = {NASA Conference Publication},
  address = {Washington D.C., USA},
  month = apr,
  topics = {team},
  pages = {14--23},
  editor = {C\'esar Mu\~noz},
  url = {http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf}
}


@InProceedings{Tuch_KN_07,
  author =    {Harvey Tuch and Gerwin Klein and Michael Norrish},
  title =     {Types, Bytes, and Separation Logic},
  booktitle = {Proc.\ 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07)},
  pages =     {97-108},
  year =      2007,
  editor =    {Martin Hofmann and Matthias Felleisen},
  address =   {Nice, France},
  month =     Jan
}

@phdthesis{moy09phd,
  author = {Yannick Moy},
  title = {Automatic Modular Static Safety Checking for C Programs},
  school = {Universit{\'e} Paris-Sud},
  year = 2009,
  month = jan,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport},
  url = {http://www.lri.fr/~marche/moy09phd.pdf}
}



@article{moy10jsc,
  author = {Yannick Moy and Claude March\'e},
  title = {Modular Inference of Subprogram Contracts for Safety Checking},
  journal = {Journal of Symbolic Computation},
  year = 2010,
  topics = {team},
  note = {to appear}
}

@incollection {Cok-2011-OpenJML,
	author = {David R. Cok},
	affiliation = {GrammaTech, Inc., Ithaca, NY 14850, USA},
	title = {{OpenJML: JML for Java 7 by Extending OpenJDK}},
	booktitle = {{NASA Formal Methods}},
	series = {Lecture Notes in Computer Science},
	editor = {Bobaru, Mihaela and Havelund, Klaus and Holzmann, Gerard and Joshi, Rajeev},
	publisher = {Springer Berlin / Heidelberg},
	isbn = {},
	pages = {472-479},
	volume = {6617},
	url = {http://dx.doi.org/10.1007/978-3-642-20398-5\_35},
	note = {10.1007/978-3-642-20398-5\_35},
	year = {2011}
}

@inproceedings{Cok-2014-OpenJML,
	author    = {David R. Cok},
	title     = {{OpenJML: Software verification for Java 7 using JML, OpenJDK,
	and Eclipse}},
	booktitle = {{F-IDE}},
	year      = {2014},
	pages     = {79-92},
	ee        = {http://dx.doi.org/10.4204/EPTCS.149.8},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@MISC{C++-2011,key={C++-2011},
	title={{ISO/IEC 14882:2011 Information technology -- Programming languages -- C++}, \url{https://www.iso.org/standard/50372.html}},
	year={2011}
}

@inproceedings{Liskov:1987:KAD:62138.62141,
	author = {Liskov, Barbara},
	title = {Keynote Address - Data Abstraction and Hierarchy},
	booktitle = {Addendum to the Proceedings on Object-oriented Programming Systems, Languages and Applications (Addendum)},
	series = {OOPSLA '87},
	year = {1987},
	isbn = {0-89791-266-7},
	location = {Orlando, Florida, USA},
	pages = {17--34},
	numpages = {18},
	url = {http://doi.acm.org/10.1145/62138.62141},
	doi = {10.1145/62138.62141},
	acmid = {62141},
	publisher = {ACM},
	address = {New York, NY, USA},
} 

[download]

@article{Liskov:1987:KAD:62139.62141,
	author = {Liskov, Barbara},
	title = {Keynote Address - Data Abstraction and Hierarchy},
	journal = {SIGPLAN Not.},
	issue_date = {May 1988},
	volume = {23},
	number = {5},
	month = jan,
	year = {1987},
	issn = {0362-1340},
	pages = {17--34},
	numpages = {18},
	url = {http://doi.acm.org/10.1145/62139.62141},
	doi = {10.1145/62139.62141},
	acmid = {62141},
	publisher = {ACM},
	address = {New York, NY, USA},
} 



@article{Liskov:1994:BNS:197320.197383,
	author = {Liskov, Barbara H. and Wing, Jeannette M.},
	title = {A Behavioral Notion of Subtyping},
	journal = {ACM Trans. Program. Lang. Syst.},
	issue_date = {Nov. 1994},
	volume = {16},
	number = {6},
	month = nov,
	year = {1994},
	issn = {0164-0925},
	pages = {1811--1841},
	numpages = {31},
	url = {http://doi.acm.org/10.1145/197320.197383},
	doi = {10.1145/197320.197383},
	acmid = {197383},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {Larch, formal specifications, subtyping},
} 


@inproceedings{Weimer:2004:FPR:1028976.1029011,
	author = {Weimer, Westley and Necula, George C.},
	title = {Finding and Preventing Run-time Error Handling Mistakes},
	booktitle = {Proceedings of the 19th Annual ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications},
	series = {OOPSLA '04},
	year = {2004},
	isbn = {1-58113-831-8},
	location = {Vancouver, BC, Canada},
	pages = {419--431},
	numpages = {13},
	url = {http://doi.acm.org/10.1145/1028976.1029011},
	doi = {10.1145/1028976.1029011},
	acmid = {1029011},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {dataflow, destructors, exceptions, finalizers, try-finally},
} 

@TECHREPORT{20.500.11850/153152,
	series = {Technical Report},
	volume = {711},
	author = {Kassios, Ioannis T. and Müller, Peter},
	institution = {ETH, Department of Computer Science},
	year = {2011-01},
	language = {en},
	copyright = {In Copyright - Non-Commercial Use Permitted},
	keywords = {SPEZIFIKATIONEN (SOFTWARE ENGINEERING); VERIFICATION (SOFTWARE ENGINEERING); SPECIFICATIONS (SOFTWARE ENGINEERING); VERIFIKATION (SOFTWARE ENGINEERING)},
	size = {34 p.},
	adress = {Zürich},
	abstract = {Delegation is a very common programming idiom, whereby a task is carried out by a statically unknown part of the program. Delegation enhances the modularity and the extensibility of a program, and, for that reason, is the main ingredient of many important design patterns. Unfortunately, delegation complicates specification and verification: the programmer must either rely on unsuitably weak specifications imposed by behavioral subtyping, or compromise automation by resorting to higherorder logic. In this paper, we present an expressive specification and verification methodology, in which partial correctness reasoning about delegation can be carried out in first order logic, using automated SMT solvers.},
	DOI = {10.3929/ethz-a-006903018},
	title = {Modular Specification and Verification of Delegation with SMT Solvers},
	Note = {.}
}