@STRING{fac = "Formal Aspects of Computing"}
@STRING{amai = "Annals of Mathematics and Artificial Intelligence"}
@STRING{jsl = "Journal of Symbolic Logic"}
@STRING{jsc = "Journal of Symbolic Computation"}
@STRING{jlc = "Journal of Logic and Computation"}
@STRING{jlp = "Journal of Logic Programming"}
@STRING{jar = "Journal of Automated Reasoning"}
@STRING{sl = "Studia Logica"}
@STRING{ipl = "Information Processing Letters"}
@STRING{tcs = "Theoretical Computer Science"}
@STRING{lnm = "Lecture Notes in Mathematics"}
@STRING{lncs = "LNCS"}
@STRING{lnai = "LNCS"}
@STRING{spv = "Springer-Verlag"}
@STRING{cacm = "Communications of the {ACM}"}
@STRING{jacm = "Journal of the {ACM}"}
@STRING{sc = "Soft Computing---A Fusion of Foundations, Methodologies
		  and Applications"}

@inproceedings{DDP99,
author =     "Satyaki Das and David L. Dill and Seungjoon Park",
title =      "Experience with Predicate Abstraction",
Editors=     "Nicolas Halbwachs and Doron Peled",		  
booktitle=   {11th International Conference on Computer-Aided Verification},
year      =  {1999},
month =      "July",
Note =       "Trento, Italy",
publisher=   "Springer-Verlag"
}

@inproceedings{DD2002,
author = "Satyaki Das and David L. Dill",
title = "Counter-Example Based Predicate Discovery in Predicate Abstraction",
booktitle = "Formal Methods in Computer-Aided Design",
year = "2002",
month = "November",
publisher = "Springer-Verlag",
location = "Portland, Oregon"
}

@inproceedings{DD2001,
author = "Satyaki Das and David L. Dill",
title = "Successive Approximation of Abstract Transition Relations",
booktitle = "Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science",
year = "2001",
note = "June 2001, Boston, USA"}

@inproceedings{ graf97construction,
    author = "{S. Graf} and {H. Sa{\"{\i}}di}",
    title = "Construction of Abstract State Graphs with {PVS}",
    booktitle = "Proc. 9th {INternational} Conference on Computer Aided Verification ({CAV}'97)",
    volume = "1254",
    publisher = "Springer Verlag",
    editor = "O. Grumberg",
    pages = "72--83",
    year = "1997",
    url = "citeseer.ist.psu.edu/graf97construction.html" }

@article{ hoare69,
 author = {C. A. R. Hoare},
 title = {An axiomatic basis for computer programming},
 journal = {Commun. ACM},
 volume = {12},
 number = {10},
 year = {1969},
 issn = {0001-0782},
 pages = {576--580},
 doi = {http://doi.acm.org/10.1145/363235.363259},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@inproceedings{ henzinger02popl,
  title = "{Lazy abstraction}",
  author = "Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Gregoire Sutre",
  booktitle = {Proceedings of the 29th Annual Symposium on Principles of Programming Languages (POPL), ACM Press, 2002, pp. 58-70} ,
  year = 2002,
}

@manual{PVS:tutorial,
	TITLE = {PVS Tutorial},
	AUTHOR = {N. Shankar and S. Owre and J. M. Rushby},
	MONTH = feb,
	YEAR = 1993,
	ORGANIZATION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Also appears in Tutorial Notes, {\em Formal Methods Europe
		'93: Industrial-Strength Formal Methods}, pages 357--406,
		Odense, Denmark, April 1993}
}

@inproceedings{cksy2005,
  AUTHOR    = { Clarke, Edmund
                and Kroening, Daniel
                and Sharygina, Natasha
                and Yorav, Karen },
  TITLE     = {{ SATABS: SAT-based Predicate Abstraction for ANSI-C }},
  BOOKTITLE = { Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005) },
  YEAR      = { 2005 },
  PUBLISHER = { Springer Verlag },
  PAGES     = { 570--574 },
  ISBN      = { 3-540-25333-5 },
  SERIES    = { Lecture Notes in Computer Science },
  VOLUME    = { 3440 },
}

@article{Dijkstra72,
  author  = {Edsger W. Dijkstra},
  title   = {{The Humble Programmer}},
  journal = CACM,
  year    = 1972,
  volume  = {15},
  number  = {10},
  pages   = {859-866},
  month   = {October},
  topics  = {Programming/Software Engineering}
}


@inproceedings{CousotCousot77-1,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {{Abstract interpretation: a unified lattice model for static 
                analysis of programs by construction or approximation of 
                fixpoints}},
   pages =     {238--252},
   booktitle = {Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT 
                Symposium on Principles of Programming Languages},
   address =   {Los Angeles, California},
   publisher = {ACM Press, New York, NY},
   year =      1977,
}

@article{Meyer92,
 author = {Bertrand Meyer},
 title = {{Applying "Design by Contract"}},
 journal = {Computer},
 volume = {25},
 number = {10},
 year = {1992},
 issn = {0018-9162},
 pages = {40--51},
 doi = {http://dx.doi.org/10.1109/2.161279},
 publisher = {IEEE Computer Society Press},
 address = {Los Alamitos, CA, USA},
 }

@BOOK{Gries81,
  AUTHOR = {D. Gries},
  TITLE = {{The Science of Programming}},
  PUBLISHER = spv,
  YEAR = 1981
}

@BOOK{Hussmann97,
  author =       "Heinrich Hu{\ss{}}mann",
  title =        "Formal Foundations for Software Engineering Methods",
  volume =       "1322",
  publisher =    spv,
  year =         "1997",
  ISBN_ISSN =         "3-540-63613-7",
  series =       lncs
}

@InProceedings{DFS04-IJCAR,
    Author       = "Denney, E. and Fischer, B. and Schumann, J.",
    Year         = "2004",
    Title        = "{Using Automated Theorem Provers to Certify Auto-generated
                    Aerospace Software}",
    Editor       = "Rusinowitch, M. and Basin, D.",
    BookTitle    = "{Proceedings of the 2nd International Joint Conference on
                    Automated Reasoning}",
    Place        = "Cork, Ireland",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "3097",
    Pages        = "198-212",
    Comment      = "TPTPRef,TPTPCite"
}

@unpublished{FilliatreOwreRuessShankar:CAV2001,
    AUTHOR = {Jean-Christophe Filli\^{a}tre and Sam Owre and Harald Rue\ss and {N.} Shankar},
    TITLE = {{ICS:} Integrated Canonizer and Solver},
    NOTE = {To be presented at {CAV'2001}},
    YEAR = {2001},
    URL = {http://www.csl.sri.com/papers/cav01/}
}

@Book{Schumann00,
  author =	 {Johann M. P. Schumann},
  title = 	 {Automated Theorem Proving in Software Engineering},
  publisher =    {Springer},
  year = 	 {2000},
  isbn_issn =    {3-540-67989-8}
}

@MISC{Spin:manual,
AUTHOR="Bell Labs",
INSTITUTION="Bell Labs",
TITLE={{Basic Spin Manual}},
ABSTRACT="Spin is a tool for analyzing the logical consistency of concurrent systems, specifically of data communication protocols. The system is described in a modeling language called Promela. The language allows for the dynamic creation of concurrent processes. Communication via message channels can be defined to be synchronous (i.e., rendezvous), or asynchronous (i.e., buffered).",
URL="http://cm.bell-labs.com/cm/cs/what/spin/Man/Manual.html",
NOTE={{Available at http://cm.bell-labs.com/cm/cs/what/spin/Man/Manual.html}},
ENTRYBY=xiaotaow
}

@inproceedings{512963,
 author = {Norihisa Suzuki and Kiyoshi Ishihata},
 title = {Implementation of an array bound checker},
 booktitle = {POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages},
 year = {1977},
 pages = {132--143},
 location = {Los Angeles, California},
 doi = {http://doi.acm.org/10.1145/512950.512963},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }
 
@phdthesis{SatyakiThesis,
author = "Satyaki Das",
title = "Predicate Abstraction",
school = "Stanford University",
month="December",
year=2003
}

@inproceedings{FlanaganQadeer02,
 author = {Cormac Flanagan and Shaz Qadeer},
 title = {Predicate abstraction for software verification},
 booktitle = {POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {2002},
 isbn = {1-58113-450-9},
 pages = {191--202},
 location = {Portland, Oregon},
 doi = {http://doi.acm.org/10.1145/503272.503291},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@BOOK{beck00:_progr_embrac_chang,
  AUTHOR = {Kent Beck},
  TITLE = {eXtreme Programming eXplained, Embrace Change},
  PUBLISHER = {Addison Wesley},
  YEAR = 2000
}

@BOOK{Eckel_00,
  author = { Bruce Eckel },
  publisher = { Prentice-Hall },
  title = { Thinking in Java 2 },
  year = { 2000 },
      URL = { http://64.78.49.204/TIJ-2nd-edition.zip },
  ISBN = { 0-13-027363-5 }
}

@BOOK{Nissanke99,
  author = { Nimal Nissanke },
  publisher = { Springer },
  title = { Formal Specification: Techniques and Applications },
  year = { 1999 },
  ISBN = { 1852330023 }
}

@incollection{Cousot81-1,
   author =    {Cousot, P{.}},
   title =     {Semantic Foundations of Program Analysis},
   pages =     {303--342},
   editor =    {Muchnick, S.S{.} and Jones, N.D{.}},
   chapter =   10,
   booktitle = {Program Flow Analysis: Theory and Applications},
   publisher = {Prentice-Hall, Inc{.}, Englewood Cliffs, New Jersey},
   year =      1981,
}

@Article{BPR-STTT03,
  author =	 {Tom Ball and Andreas Podelski and Sriram
                  K. Rajamani},
  title =	 {Boolean and Cartesian Abstraction for Model Checking
                  {C} Programs},
  journal =	 {International Journal on Software Tools for
                  Technology Transfer (STTT), Special Section on
                  TACAS'01},
  year =	 2003,
  note =	 {To appear.}
}

@BOOK{AptOlderog91,
  AUTHOR = {K. R. Apt and E.-R. Olderog},
  TITLE = {Verification of sequential and concurrent programs},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1991
}

@article{BurdyEtAl04,
  author = 	 {Lilian Burdy and Yoonsik Cheon and David Cok and 
                   Michael Ernst and Joe Kiniry and Gary T. Leavens and 
                   K. Rustan M. Leino and Erik Poll},
  title = 	 {An overview of {JML} tools and applications},
  journal = 	 {International Journal on Software Tools for Technology Transfer (STTT)},
  year = 	 {2004},
  publisher =    {Springer-Verlag},
  note =    {To appear},
}

@book{Loveland78,
   address=	{Amsterdam},
   author=	{Loveland, Donald W.},
   key=		{Loveland},
   origin=	{jjf},
   publisher=	{North-Holland Publishing Co.},
   subject=	{R},
   title=	{Automated Theorem Proving: A Logical Basis},
   year=	{1978}
}

@article{wiftTutorial,
    AUTHOR = {Judy Crow and Sam Owre and John Rushby and Natarajan Shankar and and Mandayam Srivas},
    TITLE = {{A} Tutorial Introduction to {PVS}},
    YEAR = {1995},
    MONTH = {April},
    ADDRESS = {Boca Raton, Florida},
    URL = {http://www.csl.sri.com/papers/wift-tutorial/},
    BOOKTITLE = {Workshop on Industrial-Strength Formal Specification Techniques}
}

@ARTICLE{badsoftware,
    TITLE = "Why software is so bad", 
    AUTHOR = "Charles C.\ Mann", 
    JOURNAL = "Technology Review (http:\-/\-/www\-.technologyreview\-.com\-/)", 
    YEAR = 2002,
    VOLUME = "July\-/ August 2002", 
    NOTE = "pp. 33--38",
    URL = {{http://academic.bowdoin.edu/courses/s05/csci260/readings/whysoftwarebad.html}}
}

@inproceedings{Holzmann02b,
   author = {G.J. Holzmann},
   title = {Static source code checking for user-defined properties},
   journal = {Proc. IDPT 2002},
   address = {Pasadena, CA, USA},
   year = {2002},
   month = {June},
}

@PHDTHESIS{Filliatre99,
  AUTHOR = {J.-C. Filli\^atre},
  TITLE = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
  TYPE = {Th{\`e}se de Doctorat},
  SCHOOL = {Universit\'e Paris-Sud},
  YEAR = 1999,
  MONTH = {July},
  URL = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz},
  ABSTRACT = {Nous Ä‚L tudions le problème de la certification de programmes mÄ‚Lžlant
  traits impÄ‚L ratifs et fonctionnels dans le cadre de la thÄ‚L orie des
  types.

  La thÄ‚L orie des types constitue un puissant langage de spÄ‚L cification,
  naturellement adaptÄ‚L  Ă  la preuve de programmes purement
  fonctionnels.  Pour y certifier Ä‚L galement des programmes impÄ‚L ratifs,
  nous commençons par exprimer leur sÄ‚L mantique de manière purement
  fonctionnelle. Cette traduction repose sur une analyse statique des
  effets de bord des programmes, et sur l'utilisation de la notion de
  monade, notion que nous raffinons en l'associant Ă  la notion d'effet
  de manière gÄ‚L nÄ‚L rale.  Nous montrons que cette traduction est
  sÄ‚L mantiquement correcte.

  Puis, Ă  partir d'un programme annotÄ‚L , nous construisons une preuve
  de sa spÄ‚L cification, traduite de manière fonctionnelle. Cette preuve
  est bâtie sur la traduction fonctionnelle prÄ‚L cÄ‚L demment
  introduite. Elle est presque toujours incomplète, les parties
  manquantes Ä‚L tant autant d'obligations de preuve qui seront laissÄ‚L es
  Ă  la charge de l'utilisateur.  Nous montrons que la validitÄ‚L  de ces
  obligations entraĂL ne la correction totale du programme.

  Nous avons implantÄ‚L  notre travail dans l'assistant de preuve
  Coq, avec lequel il est dès Ă  prÄ‚L sent distribuÄ‚L . Cette
  implantation se prÄ‚L sente sous la forme d'une tactique prenant en
  argument un programme annotÄ‚L  et engendrant les obligations de
  preuve.  Plusieurs algorithmes non triviaux ont Ä‚L tÄ‚L  certifiÄ‚L s Ă 
  l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de
  Knuth-Morris-Pratt).}
}

@Article{FisherRabin74,
  author = 	 {Fisher, M. J. and Rabin, M. O.},
  title = 	 {Superexponential complexity of Presburger's arithmetic},
  journal = 	 {SIAM-AMS Proceedings},
  year = 	 1974,
  volume =	 7,
  pages =	 {27-41}
} 

@inproceedings{boogieOverview,
    AUTHOR = {{Mike Barnett, K. Rustan M. Leino, and Wolfram Schultei}}
    TITLE = {{The Spec# programming system:  An overview}},
    YEAR = {2004},
    URL = {http://research.microsoft.com/specsharp/papers/krml136.pdf} 
    BOOKTITLE = {CASSIS}
    PUBLISHER = spv
}