
@techreport{detlefs-1998,
author       = "D. L. Detlefs and K. R. M. Leino and G. Nelson and J. B. Saxe",
title        = {{Extended Static Checking}},
institution  = "Digital Equipment Corporation Systems Research Center",
year         = "1998"
}

@inproceedings{floyd-1967,
author       = "R. W. Floyd",
title        = {{Assigning Meanings to Programs}},
booktitle    = "Proc. Amer. Math. Soc. Symposium in Applied Mathematics",
year         = "1967"
}

@article{hoare-1969,
author       = "C. A. R. Hoare",
title        = {An Axiomatic Basis for Computer Programming},
journal      = "Communications of the ACM",
volume       = "12",
number       = "10",
year         = "1969",
month        = "Oct",
pages        = "576--580"
}

@book{dijkstra-1976,
author = "E. W. Dijkstra",
title = "A Discipline of Programming",
publisher="Prentice-Hall",
year=1976}

@book{gries-1981,
author = "D. Gries",
title = "The Science of Programming",
publisher="Springer-Verlag", 
year=1981}

@inproceedings{necula-2002,
author       = "G. C. Necula and S. McPeak and S. P. Rahul and W. Weimer",
title        = {{CIL: Intermediate Language and Tools for Analysis and
               Transformation of C Programs}},
booktitle    = "Proc. of Conference on Compiler Design",
year         = "2002"
}

@article{weiser-1984,
author       = "M. Weiser",
title        = {Program Slicing},
journal      = "IEEE Transactions on Software Engineering",
volume       = "10",
number       = "4",
month        = "Jul",
year         = "1984"
}

@book{cgp99,
author="E. Clarke and O. Grumberg and D. Peled",
title={{Model Checking}},
year=1999,
publisher="The MIT Press"}

@inproceedings{ks93,
 author = "N. Klarlund and M. Schwartzbach",
 title = {Graph types},
 booktitle = {Principles of Programming Languages},
 year = {1993},
 pages = {196--205},
 publisher = {ACM Press}
 }

@book{sr02,
title={Proof and System-Reliability},
editor={H. Schwichtenberg and R. Steinbr\"{u}ggen},
year=2002,
publisher="Kluwer",
note={NATO Advanced Study Institute},
address="Marktoberdorf, Germany"}

@inproceedings{MehtaN-CADE03,
author={F. Mehta and T. Nipkow},
title={{Proving Pointer Programs in Higher-Order Logic}},
booktitle="19th International Conference on Automated Deduction",
editor="F. Baader",
year=2003,
publisher="Springer-Verlag",
series="LNCS",
volume={2741},
pages={121--135}}

@inbook{nipkow02,
title={{Hoare Logics in Isabelle/HOL}},
chapter=11,
pages={341--367},
author="T. Nipkow",
crossref="sr02"}

@booklet{nist02,
title={{The Economic Impacts of Inadequate Infrastructure for Software Testing}},
author={{Research Triangle Institute}},
note={{Sponsored by the Department of Commerce's National Institute of Standards and Technology}},
year=2002}

@booklet{pitac05,
title={{Report to the President on Cyber Security: a Crisis of Prioritization}},
author={{President's Information Technology Advisory Committee}},
note={{Available at \url{http://www.nitrd.gov/pitac/reports/20050301_cybersecurity/cybersecurity.pdf}}},
year=2005}


@article{cg01,
author={M. Chechik and J. Gannon},
title={{Automatic Analysis of Consistency between Requirements and Designs}},
journal={IEEE Transactions on Software Engineering},
volume={27},
year={2001}
}

@article{cook78,
author={S. Cook},
title={{Soundness and Completeness of an Axiom System for Program Verification}},
journal={SIAM Journal on Computing},
volume={7},
year={1978}
}

@book{hkt00,
author={D. Harel and D. Kozen and J. Tiuryn},
title={{Dynamic Logic}},
year=2000,
publisher={MIT Press}}

@phdthesis{leino95,
author= {K. R. M. Leino},
title={{Toward Reliable Modular Programs}},
school={California Institute of Technology}, 
year=1995,
note="Available as Technical Report Caltech CS-TR-95-03"}

@article{nelson89,
author={Nelson, G.},
title={A Generalization of Dijkstra's Calculus},
journal={ACM Transactions on Programming Languages and Systems},
volume={11},
year={1989}
}

@inproceedings{engler02,
author={Ashcraft, K. and Engler, D.},
title={Using programmer-written compiler extensions to catch security holes},
booktitle={IEEE Symposium on Security and Privacy},
year={2002}
}

@article{leino02,
author={C. Flanagan and K. Leino and M. Lillibridge and G. Nelson and J. Saxe and R. Stata},
title={{Extended Static Checking for Java}},
journal={SIGPLAN Notices},
volume={37},
year={2002}
}

@inproceedings{jackson+03,
author="I. Shlyakhter and R. Seater and D. Jackson and M. Sridharan and M. Taghdiri",
title={{Debugging Overconstrained Declarative Models Using Unsatisfiable Cores}},
booktitle="18th IEEE International Conference on Automated Software Engineering",
year=2003,
note="received best paper award"} 

@inproceedings{nelson90,
title={{Some generalizations and applications of Dijkstra's guarded commands}},
author="G. Nelson",
booktitle="Programming and Mathematical Method",
editor="M. Broy",
series="NATO ASI Series. Series F: Computer and Systesms Sciences",
volume=88,
publisher="Springer-Verlag",
year=1990}

@article{wassermanblum97,
title={{Software Reliability via Run-Time Result-Checking}},
author="H. Wasserman and M. Blum",
journal={{Journal of the ACM}},
volume=44,
number=6,
pages="826--849",
year=1997,
month=nov}

@article{ZPG+04,
author={L.~Zuck and A.~Pnueli and B.~Goldberg and C.~Barrett and Y.~Fang and Y.~Hu},
title={{Translation and Run-Time Validation of Loop Transformations}},
journal={Journal of Formal Methods in System Design},
year = {2004},
note={To appear, preliminary version in {\em ENTCS}, 70(4), 2002}
}

@inproceedings{pnueli+98,
author="A. Pnueli and M. Siegel and E. Singerman",
title={{Translation Validation}},
editor="B. Steffen",
booktitle="Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
year=1998, 
volume=1384,
series="LNCS",
publisher="Springer-Verlag",
pages="151--166"}

@inproceedings{velevbryant99,
author="M. Velev and R. Bryant", 
title={{Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions}},
booktitle="Correct Hardware Design and Verification Methods",
Publisher="Springer-Verlag",
Series="Lecture Notes in Computer Science",
volume="1703",
pages="37--53",
year=1999,
editor="L. Pierre and T. Kropf"}

@inproceedings{pnueli+99,
author="A. Pnueli and Y. Rodeh and O. Shtrichman and M. Siegel",
title={{Deciding Equality Formulas by Small Domains Instantiations}},
booktitle="Proceedings of the 11th International Computer-Aided Verification Conference",
volume="1633",
series="Lecture Notes in Computer Science",
publisher="Springer-Verlag",
pages="455--469",
year=1999}

@inproceedings{ bornat00proving,
    author = "Richard Bornat",
    title = {{Proving Pointer Programs in Hoare Logic}},
    booktitle = "Mathematics of Program Construction",
    pages = "102-126",
    year = "2000"}


@inproceedings{ohearn+04,
 author = {P. O'Hearn and H. Yang and J. Reynolds},
 title = {{Separation and Information Hiding}},
 booktitle = {Proceedings of the 31st ACM Symposium on Principles of Programming Languages},
 year = {2004},
 pages = {268--280},
 publisher = {ACM Press}}


@inproceedings{jacobs+02,
author="B. Jacobs and J. Kiniry and M. Warnier",
title={{Java Program Verification Challenges}},
editor="F. de Boer and M. Bonsangue and S. Graf and W.-P. de Roever",
booktitle="Formal Methods for Components and Objects",
year=2002,
publisher="Springer",
series="LNCS",
number="2852",
pages="202--219"}

@inproceedings{lahiri+04,
author="S. Lahiri and R. Bryant and A. Goel and M. Talupur",
title={{Revisiting Positive Equality}},
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year=2004,
volume=2988,
series="LNCS",
publisher="Springer-Verlag",
pages="1-15"}


@inproceedings{pnueli+01,
author="A. Pnueli and Y. Rodeh and O. Strichman",
title="Range allocation for equivalence logic",
booktitle="21st Conference on Foundations of Software Technology and Theoretical Computer Science",
volume=2245,
series="LNCS",
publisher="Springer-Verlag",
year=2001,
pages="317--333"}


@inproceedings{xie+05,
title={{Scalable Error Detection using Boolean Satisfiability}},
author="Y. Xie and A. Aiken",
booktitle="Proceedings of the 32nd ACM Symposium on Principles of Programming Languages",
editor="M. Abadi",
year=2005}

@inproceedings{flanagan+05,
title={{Dynamic Partial-Order Reduction for Model Checking Software}},
author="C. Flanagan and P. Godefroid",
booktitle="Proceedings of the 32nd ACM Symposium on Principles of Programming Languages",
editor="M. Abadi",
year=2005}

@article{krakatoa04,
author="C. March{\'{e}} and C. Paulin-Mohring and X. Urbain",
title={{The Krakatoa Tool for Certification of JAVA/JAVACARD Programs Annotated in JML}},
journal="Journal of Logic and Algebraic Programming",
volume=58,
number="1-2",
pages="89-106",
year=2004}

@inproceedings{sagiv99,
    author = "S. Sagiv and T. Reps and R. Wilhelm",
    title = {{Parametric Shape Analysis via 3-Valued Logic}},
    booktitle = "Symposium on Principles of Programming Languages",
    pages = "105--118",
    year = "1999"}

@article{KeY2005, 
  author        = {W. Ahrendt and T. Baar and 
                   B. Beckert and R. Bubel and 
                   M. Giese and R. H\"ahnle and 
                   W. Menzel and W. Mostowski and 
                   A. Roth and S. Schlager and 
                   P. Schmitt}, 
  title         = {The {KeY} Tool}, 
  journal       = {Software and System Modeling},   
  volume        = {4},
  pages         = {32-54},
  year          = {2005}, 
  publisher     = {Springer}
}

@article{wangmusser97,
 author = {C. Wang and D. Musser},
 title = {{Dynamic Verification of C++ Generic Algorithms}},
 journal = {IEEE Transactions on Software Engineering},
 volume = {23},
 number = {5},
 year = {1997},
 pages = {314--323},
 publisher = {IEEE Press}}

@inproceedings{mcpeaknecula05,
author = {S. McPeak and G. Necula},
title = {{Data Structure Specifications via Local Equality Axioms}},
booktitle = {17th International Conference on Computer-Aided Verification},
year = 2005,
pages={476--490},
publisher="Springer",
editor="K. Etessami and S. Rajamani"}

@inproceedings{NieuwenhuisOliveras05,
author = {R. Nieuwenhuis and A. Oliveras},
title = {{DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic}},
booktitle = {17th International Conference on Computer-Aided Verification},
year = 2005,
publisher="Springer",
editor="K. Etessami and S. Rajamani"}

@inproceedings{zhu+05,
author = "D. Zhu and H. Xi",
title = {{Safe Programming with Pointers through Stateful Views}},
booktitle = "Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages",
publisher = "Springer",
year = "2005",
pages = "83--97"}

@inproceedings{lahiri+05,
author = {S. Lahiri and T. Ball and B. Cook},
title = {{Predicate Abstraction via Symbolic Decision Procedures}},
booktitle = {17th International Conference on Computer-Aided Verification},
year = 2005,
publisher="Springer",
pages="24--38",
editor="K. Etessami and S. Rajamani"}

@inproceedings{leroy06,
author="X. Leroy",
title={{Formal Certification of a Compiler Back-end, or: Programming a Compiler with a Proof Assistant}},
booktitle="Proceedings of the 32nd ACM Symposium on Principles of Programming Languages",
editor="S. Peyton Jones",
year=2006}

@inproceedings{leroy06b,
author="X. Leroy and S. Blazy and Z. Dargaye",
title={{Formal Verification of a C Compiler Front-end}},
booktitle="Proceedings of Formal Methods",
editor="J. Misra and T. Nipkow",
year=2006}

@article{gonthier,
title={{A computer-checked proof of the Four-Colour Theorem}},
author="G. Gonthier",
note="Unpublished manuscript, available from Gonthier's website"}

@inproceedings{boogie06,
title = {{Boogie: A Modular Reusable Verifier for Object-Oriented Programs}},
author = "M. Barnett and B.-Y. Chang and R. DeLine and B. Jacobs and K. Leino",
booktitle="Fourth International Symposium on Formal Methods for Components and Objects (FMCO'05), Post-Proceedings",
editor="F. de Boer and M. Bonsangue and S. Graf and W.-P. de Roever",
year = 2006}

@inproceedings{Lahiri+06,
  author    = {S. Lahiri and
               R. Nieuwenhuis and
               A. Oliveras},
  title     = {{SMT Techniques for Fast Predicate Abstraction}},
  booktitle = {18th International Conference on Computer-Aided Verification},
  publisher="Springer-Verlag",
  year      = {2006},
  pages     = {424-437}}

@inproceedings{BFG+05,
  author    = "C. Barrett and Y. Fang and B. Goldberg and Y. Hu and A. Pnueli and L. Zuck",
  title     = "{TVOC}: A Translation Validator for Optimizing Compilers",
  booktitle = "Proceedings of the $17^{th}$ International Conference on Computer Aided Verification (CAV '05)",
  series    = "Lecture Notes in Computer Science",
  volume    = 3576,
  publisher = "Springer-Verlag",
  editor    = "K. Etessami and S. Rajamani",
  pages     = "291--295",
  year      = 2005
}

@article{ball+06,
author="T. Ball and E. Bounimova and B. Cook and V. Levin and J. Lichtenberg and C. McGarvery and B. Ondrusek and S. Rajamani and A. Ustuner",
title={{Thorough Static Analysis of Device Drivers}},
journal={ACM SIGOPS Operating Systems Review},
volume=40,
number=4,
year=2006,
pages="73--85"}