@InCollection{Leino:Dafny:MOD2008,
  author =    {K. Rustan M. Leino},
  title =     {Specification and verification of object-oriented software},
  booktitle = {Engineering Methods and Tools for Software Safety and Security},
  pages =     {231-266},
  publisher = {IOS Press},
  year =      {2009},
  editor =    {Manfred Broy and Wassiou Sitou and Tony Hoare},
  volume =    {22},
  series =    {NATO Science for Peace and Security Series D: Information and Communication Security},
  note =      {Summer School Marktoberdorf 2008 lecture notes},
}

@InCollection{LeinoSchulte:MOD2006,
  author =    {K. Rustan M. Leino and Wolfram Schulte},
  title =     {A verifying compiler for a multi-threaded object-oriented language},
  booktitle = {Software Safety and Security},
  pages =     {351-416},
  publisher = {IOS Press},
  year =      {2007},
  editor =    {Manfred Broy and Johannes Gr{\"u}nbauer and Tony Hoare},
  volume =    {9},
  series =    {NATO Science for Peace and Security Series D: Information and Communication Security},
  note =      {Summer School Marktoberdorf 2006 lecture notes},
}

@techreport{ESC:rr,
  author = "David L. Detlefs and K. Rustan M. Leino and Greg Nelson
                  and James B. Saxe",
  title = "Extended static checking",
  institution = "Compaq Systems Research Center",
  month = dec,
  year = 1998,
  type = "Research Report",
  number = 159
}

@Article{Simplify:tome,
  author = "David Detlefs and Greg Nelson and James B. Saxe",
  title = "Simplify: a theorem prover for program checking",
  journal = JACM,
  volume = 52,
  number = 3,
  month = may,
  year = 2005,
  pages = "365-473",
}

@InProceedings{Doomed:FM2009,
  author =       {Jochen Hoenicke and K. Rustan M. Leino and Andreas
                  Podelski and Martin Sch{\"a}f and Thomas Wies},
  title =        {It's Doomed; We Can Prove It},
  booktitle =    {FM 2009: Formal Methods, Second World Congress},
  editor =       {Ana Cavalcanti and Dennis Dams},
  volume =       5850,
  series =       lncs,
  publisher =    {Springer},
  month =        nov,
  year =         2009,
  pages =        {338-353},
}

@InProceedings{Regis-Gianas:Pottier:MPC2008,
  author =       {Yann R{\'e}gis-Gianas and Fran{\c{c}}ois Pottier},
  title =        {A {Hoare} Logic for Call-by-Value Functional Programs},
  booktitle =    {Mathematics of Program Construction, 9th International Conference},
  editor =       {Philippe Audebaud and Christine Paulin-Mohring},
  volume =       {5133},
  series =       lncs,
  publisher =    {Springer},
  month =        jul,
  year =         {2008},
  pages =        {305-335},
}

@InProceedings{ZeeKuncakRinard:PLDI2008,
  author =       {Karen Zee and Viktor Kuncak and Martin C. Rinard},
  title =        {Full functional verification of linked data structures},
  booktitle =    {Proceedings of the ACM SIGPLAN 2008 Conference on
                  Programming Language Design and Implementation},
  editor =       {Rajiv Gupta and Saman P. Amarasinghe},
  year =         {2008},
  month =        jun,
  publisher =    {ACM},
  pages =        {349-361},
}

@InProceedings{VCC:TPHOLs,
  author =       {Ernie Cohen and Markus Dahlweid and Mark
                  A. Hillebrand and Dirk Leinenbach and Micha{\l}
                  Moskal and Thomas Santen and Wolfram Schulte and
                  Stephan Tobies},
  title =        {{VCC}: A Practical System for Verifying Concurrent {C}},
  booktitle =    {Theorem Proving in Higher Order Logics, 22nd
                  International Conference, TPHOLs 2009},
  editor =       {Stefan Berghofer and Tobias Nipkow and Christian
                  Urban and Makarius Wenzel},
  volume =       {5674},
  series =       lncs,
  publisher =    {Springer},
  year =         {2009},
  month =        aug,
  pages =        {23-42},
}

@InProceedings{seL4:SOSP2009,
  author =       {Gerwin Klein and Kevin Elphinstone and Gernot Heiser
                  and June Andronick and David Cock and Philip Derrin
                  and Dhammika Elkaduwe and Kai Engelhardt and Rafal
                  Kolanski and Michael Norrish and Thomas Sewell and
                  Harvey Tuch and Simon Winwood},
  title =        {{seL4}: formal verification of an {OS} kernel},
  booktitle =    {Proceedings of the 22nd ACM Symposium on Operating
                  Systems Principles 2009, SOSP 2009},
  editor =       {Jeanna Neefe Matthews and Thomas E. Anderson},
  publisher =    {ACM},
  month =        oct,
  year =         {2009},
  pages =        {207-220},
}

@book{Meyer:OOP,
  author = "Bertrand Meyer",
  title = "Object-oriented Software Construction",
  publisher = "Prentice-Hall International",
  series = "Series in Computer Science",
  year = 1988
}

@InProceedings{SpecSharp:Overview,
  author =   {Mike Barnett and K. Rustan M. Leino and Wolfram Schulte},
  title =    {The {Spec\#} Programming System: An Overview},
  booktitle = {{CASSIS 2004}, Construction and Analysis of Safe,
               Secure and Interoperable Smart devices},
  editor = "Gilles Barthe and Lilian Burdy and Marieke Huisman and
                  Jean-Louis Lanet and Traian Muntean",
  series = lncs,
  volume = 3362,
  publisher = "Springer",
  year = 2005,
  pages = "49-69"
}

@InProceedings{Kassios:FM2006,
  author = "Ioannis T. Kassios",
  title = "Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions",
  booktitle = "FM 2006: Formal Methods, 14th International Symposium on Formal Methods",
  editor = "Jayadev Misra and Tobias Nipkow and Emil Sekerinski",
  series = lncs,
  volume = 4085,
  publisher = "Springer",
  month = aug,
  year = 2006,
  pages = "268-283",
}

@InProceedings{Boogie:Architecture,
  author = "Mike Barnett and Bor-Yuh Evan Chang and Robert DeLine and
                  Bart Jacobs and K. Rustan M. Leino",
  title = "{B}oogie: A Modular Reusable Verifier for Object-Oriented Programs",
  booktitle = "Formal Methods for Components and Objects:  4th
                  International Symposium, FMCO 2005",
  editor = "de Boer, Frank S. and Marcello M. Bonsangue and
                  Susanne Graf and de Roever, Willem-Paul",
  series = lncs,
  volume = 4111,
  publisher = "Springer",
  month = sep,
  year = 2006,
  pages = "364-387"
}

@Misc{Leino:Boogie2-RefMan,
  author = {K. Rustan M. Leino},
  title = {This is {B}oogie 2},
  howpublished = {Manuscript KRML 178},
  year = 2008,
  note = "Available at \url{http://research.microsoft.com/~leino/papers.html}",
}

@inproceedings{deMouraBjorner:Z3:overview,
  author    = "de Moura, Leonardo and Nikolaj Bj{\o}rner",
  title     = {{Z3}: An efficient {SMT} solver},
  booktitle = {Tools and Algorithms for the Construction and
                  Analysis of Systems, 14th International Conference,
                  TACAS 2008},
  editor    = {C. R. Ramakrishnan and Jakob Rehof},
  series    = lncs,
  volume    = 4963,
  publisher = {Springer},
  month     = mar # "--" # apr,
  year      = 2008,
  pages     = {337-340},
}

@InProceedings{Gonthier:CAV2006,
  author =    {Georges Gonthier},
  title =     {Verifying the safety of a practical concurrent
               garbage collector},
  booktitle = {Computer Aided Verification, 8th International Conference, CAV '96},
  editor =    {Rajeev Alur and Thomas A. Henzinger},
  volume =    {1102},
  series =    lncs,
  publisher = {Springer},
  month =     jul # "--" # aug,
  year =      {1996},
  pages =     {462-465},
}

@Article{CLIncStack,
  author =    {William R. Bevier and Hunt, Jr., Warren A. and
                  J Strother Moore and William D. Young},
  title =     {Special issue on system verification},
  journal =   {Journal of Automated Reasoning},
  volume =    {5},
  number =    {4},
  month =     dec,
  year =      {1989},
  pages =     {409-530},
}

@InProceedings{ParkinsonBierman:POPL2005,
  author =       {Matthew J. Parkinson and Gavin M. Bierman},
  title =        {Separation logic and abstraction},
  booktitle =    {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium
                  on Principles of Programming Languages, POPL 2005},
  publisher =    {ACM},
  month =        jan,
  year =         {2005},
  pages =        {247-258},
}

@InProceedings{Weide:VSTTE2008,
  author =       {Bruce W. Weide and Murali Sitaraman and Heather
                  K. Harton and Bruce Adcock and Paolo Bucci and
                  Derek Bronish and Wayne D. Heym and Jason
                  Kirschenbaum and David Frazier},
  title =        {Incremental Benchmarks for Software Verification Tools and Techniques},
  booktitle =    {Verified Software: Theories, Tools, Experiments,
                  Second International Conference, VSTTE 2008},
  editor =       {Natarajan Shankar and Jim Woodcock},
  volume =       {5295},
  series =       lncs,
  publisher =    {Springer},
  month =        oct,
  year =         {2008},
  pages =        {84-98},
}

@Article{SchorrWaite:CACM1967,
  author =       {H. Schorr and W. M. Waite},
  title =        {An Efficient Machine-Independent Procedure for
                  Garbage Collection in Various List Structures},
  journal =      cacm,
  volume =       {10},
  number =       {8},
  month =        aug,
  year =         {1967},
  pages =        {501-506},
}

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

@inproceedings{Boyland:SAS2003,
  author =      {John Boyland},
  title =       {Checking Interference with Fractional Permissions},
  booktitle =   "Static Analysis, 10th International Symposium, SAS 2003",
  editor =      {Radhia Cousot},
  series =      lncs,
  volume =      2694,
  publisher =   "Springer",
  year =        2003,
  pages =       {55-72}
}

@InProceedings{Reynolds:SepLogic,
  author =       {John C. Reynolds},
  title =        {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle =    {17th IEEE Symposium on Logic in Computer Science (LICS 2002)},
  publisher =    {IEEE Computer Society},
  year =         {2002},
  month =        jul,
  pages =        {55-74},
}

@InProceedings{Clarke-Drossopoulou02,
  author =	 {Dave Clarke and Sophia Drossopoulou},
  title =	 {Ownership, encapsulation and the disjointness of
                  type and effect},
  booktitle =	 {Proceedings of the 2002 ACM SIGPLAN Conference on
                  Object-Oriented Programming Systems, Languages and
                  Applications, OOPSLA 2002},
  publisher = {ACM},
  Month =	 nov,
  Year =	 2002,
  pages =	 {292--310},
}

@InProceedings{FAP:OOPSLA1998,
  author =       {Dave Clarke and John Potter and James Noble},
  title =        {Ownership Types for Flexible Alias Protection},
  booktitle =    {Proceedings of the 1998 ACM SIGPLAN Conference on
                  Object-Oriented Programming Systems, Languages \&
                  Applications (OOPSLA '98)},
  publisher =    {ACM},
  month =        oct,
  year =         {1998},
  pages =        {48-64},
}

@Article{LeinoNelson:tome,
  author = "K. Rustan M. Leino and Greg Nelson",
  title = "Data abstraction and information hiding",
  journal = toplas,
  month = sep,
  year = 2002,
  volume = 24,
  number = 5,
  pages = "491-553"
}

@PhdThesis{Darvas:thesis,
  author =       {{\'A}d{\'a}m P{\'e}ter Darvas},
  title =        {Reasoning About Data Abstraction in Contract Languages},
  school =       {ETH Zurich},
  year =         {2009},
  note =         {Diss. ETH No. 18622},
}

@InProceedings{SmansEtAl:VeriCool,
  author =       {Jan Smans and Bart Jacobs and Frank Piessens and Wolfram Schulte},
  title =        {Automatic Verifier for {J}ava-Like Programs Based on Dynamic Frames},
  booktitle =    {Fundamental Approaches to Software Engineering, 11th
                  International Conference, FASE 2008},
  editor =       {Jos{\'e} Luiz Fiadeiro and Paola Inverardi},
  volume =       {4961},
  series =       lncs,
  publisher =    {Springer},
  month =        mar # "--" # apr,
  year =         {2008},
  pages =        {261-275},
}

@inproceedings{Why:Platform,
  author    = {Jean-Christophe Filli{\^a}tre and Claude March{\'e}},
  title     = {The {Why}/{Krakatoa}/{Caduceus} Platform for Deductive Program Verification},
  booktitle =    {Computer Aided Verification, 19th International Conference, CAV 2007},
  editor =       {Werner Damm and Holger Hermanns},
  volume =       {4590},
  series =       lncs,
  publisher =    {Springer},
  month =        jul,
  year =         {2007},
  pages     = {173--177}
}

@InProceedings{BarrettTinelli:CVC3,
  author =       {Clark Barrett and Cesare Tinelli},
  title =        {{CVC3}},
  booktitle =    {Computer Aided Verification, 19th International Conference, CAV 2007},
  editor =       {Werner Damm and Holger Hermanns},
  volume =       {4590},
  series =       lncs,
  publisher =    {Springer},
  month =        jul,
  year =         {2007},
  pages =        {298-302},
}

@InProceedings{HubertMarche:SchorrWaite,
  author =       {Thierry Hubert and Claude March{\'e}},
  title =        {A case study of {C} source code verification: the
                  {S}chorr-{W}aite algorithm},
  booktitle =    {Third IEEE International Conference on Software
                  Engineering and Formal Methods (SEFM 2005)},
  editor =       {Bernhard K. Aichernig and Bernhard Beckert},
  publisher =    {IEEE Computer Society },
  month =        sep,
  year =         {2005},
  pages =        {190-199},
}

@Article{BroyPepper:SchorrWaite,
  author =       {Manfred Broy and Peter Pepper},
  title =        {Combining Algebraic and Algorithmic Reasoning: An
                  Approach to the {S}chorr-{W}aite Algorithm},
  journal =      toplas,
  volume =       {4},
  number =       {3},
  month =        jul,
  year =         {1982},
  pages =        {362-381},
}

@Article{MehtaNipkow:SchorrWaite,
  author =       {Farhad Mehta and Tobias Nipkow},
  title =        {Proving pointer programs in higher-order logic},
  journal =      {Information and Computation},
  year =         {2005},
  volume =       {199},
  number =       {1--2},
  pages =        {200-227},
  month =        may # "--" # jun,
}

@InProceedings{Abrial:SchorrWaite,
  author =       {Jean-Raymond Abrial},
  title =        {Event Based Sequential Program Development:
                  Application to Constructing a Pointer Program},
  booktitle =    {FME 2003: Formal Methods, International Symposium of
                  Formal Methods Europe},
  editor =       {Keijiro Araki and Stefania Gnesi and Dino Mandrioli},
  volume =       {2805},
  series =       lncs,
  publisher =    {Springer},
  month =        sep,
  year =         {2003},
  pages =        {51-74},
}

@InCollection{Bubel:SchorrWaite,
  author =       {Richard Bubel},
  title =        {The Schorr-Waite-Algorithm},
  booktitle =    {Verification of Object-Oriented Software: The {KeY} Approach},
  crossref =     {KeY:book},
  chapter =      {15},
}

@InProceedings{BanerjeeEtAl:RegionLogic,
  author =    {Anindya Banerjee and David A. Naumann and Stan Rosenberg},
  title =     {Regional Logic for Local Reasoning about Global Invariants},
  booktitle = {ECOOP 2008 --- Object-Oriented Programming, 22nd European Conference},
  editor =    {Jan Vitek},
  series =    lncs,
  volume =    5142,
  publisher = {Springer},
  month =     jul,
  year =      2008,
  pages =     {387-411},
}

@Book{Abrial:BBook,
  author = "J.-R. Abrial",
  title = "The {B}-Book: Assigning Programs to Meanings",
  publisher = "Cambridge University Press",
  year = 1996
}

@Book{Abrial:EventB:book,
  author =       {Jean-Raymond Abrial},
  title =        {Modeling in {Event-B}: System and Software Engineering},
  publisher =    {Cambridge University Press},
  year =         {2010},
}

@Article{MisraCook:Orc,
  author =       {Jayadev Misra and William R. Cook},
  title =        {Computation Orchestration: A Basis for Wide-Area Computing},
  journal =      {Software and Systems Modeling},
  year =         {2007},
  volume =       6,
  number =       1,
  pages =        {83-110},
  month =        mar,
}

@Book{Jackson:Alloy:book,
  author =       {Daniel Jackson},
  title =        {Software Abstractions: Logic, Language, and Analysis},
  publisher =    {MIT Press},
  year =         {2006},
}

@InProceedings{JacksonEtAl:Formula,
  author =       {Ethan K. Jackson and Dirk Seifert and Markus
                  Dahlweid and Thomas Santen and Nikolaj Bj{\o}rner
                  and Wolfram Schulte},
  title =        {Specifying and Composing Non-functional Requirements
                  in Model-Based Development},
  booktitle =    {Proceedings of the 8th International Conference on
                  Software Composition},
  pages =        {72-89},
  year =         {2009},
  editor =       {Alexandre Bergel and Johan Fabry},
  series =       lncs,
  volume =       {5634},
  month =        jul,
  publisher =    {Springer},
}

@InProceedings{HarelEtAl:PlayInPlayOut,
  author =       {David Harel and Hillel Kugler and Rami Marelly and
                  Amir Pnueli},
  title =        {Smart {P}lay-out of Behavioral Requirements},
  booktitle =    {Formal Methods in Computer-Aided Design, 4th
                  International Conference, FMCAD 2002},
  pages =        {378-398},
  year =         {2002},
  editor =       {Mark Aagaard and John W. O'Leary},
  volume =       {2517},
  series =       lncs,
  month =        nov,
  publisher =    {Springer},
}

@Article{Smith:KIDS-overview,
  author = "Douglas R. Smith",
  title = "{KIDS}: A Semi-Automatic Program Development System",
  journal = {IEEE Transactions on Software Engineering },
  volume = 16,
  number = 9,
  month = sep,
  year = 1990,
  pages = "1024-1043",
}

@article{Hoare:DataRepresentations,
  author = "C. A. R. Hoare",
  title = "Proof of correctness of data representations",
  journal = acta,
  volume = 1,
  number = 4,
  year = 1972,
  pages = "271-281"
}

@InProceedings{Abrial:FM-in-practice,
  author =       {Jean-Raymond Abrial},
  title =        {Formal methods in industry: achievements, problems, future},
  booktitle =    {28th International Conference on Software Engineering (ICSE 2006)},
  editor =       {Leon J. Osterweil and H. Dieter Rombach and Mary Lou Soffa},
  month =        may,
  year =         {2006},
  publisher =    {ACM},
  pages =        {761-768},
}

@InProceedings{MartinEtAl:AsynchMIPS,
  author =       {Alain J. Martin and Andrew Lines and Rajit Manohar
                  and Mika Nystr{\"o}m and Paul I. P{\'e}nzes and
                  Robert Southworth and Uri Cummings},
  title =        {The Design of an Asynchronous MIPS R3000 Microprocessor},
  booktitle =    {17th Conference on Advanced Research in VLSI (ARVLSI '97}},
  month =        sep,
  year =         {1997},
  publisher =    {IEEE Computer Society},
  pages =        {164-181},
}

@InProceedings{BallEtAll:ScalableChecking,
  author =       {Thomas Ball and Brian Hackett and Shuvendu K. Lahiri
                  and Shaz Qadeer and Julien Vanegue},
  title =        {Towards Scalable Modular Checking of User-Defined Properties},
  booktitle =    {Verified Software: Theories, Tools, Experiments,
                  (VSTTE 2010)},
  editor =       {Gary T. Leavens and Peter O'Hearn and Sriram K. Rajamani},
  volume =       {6217},
  series =       lncs,
  publisher =    {Springer},
  month =        aug,
  year =         {2010},
  pages =        {1-24},
}

@InProceedings{RegisGianasPottier:FunctionalHoare,
  author =       {Yann R{\'e}gis-Gianas and Fran{\,c}ois Pottier},
  title =        {A {H}oare Logic for Call-by-Value Functional Programs},
  booktitle =    {Mathematics of Program Construction, 9th International Conference, MPC 2008},
  pages =        {305-335},
  year =         {2008},
  editor =       {Philippe Audebaud and Christine Paulin-Mohring},
  volume =       {5133},
  series =       lncs,
  month =        jul,
  publisher =    {Springer},
}

@InProceedings{VeanesEtAl:SpecExplorer,
  author =       {Margus Veanes and Colin Campbell and Wolfgang
                  Grieskamp and Wolfram Schulte and Nikolai Tillmann
                  and Lev Nachmanson},
  title =        {Model-Based Testing of Object-Oriented Reactive
                  Systems with {Spec} {Explorer}},
  booktitle =    {Formal Methods and Testing},
  pages =        {39-76},
  year =         {2008},
  editor =       {Robert M. Hierons and Jonathan P. Bowen and Mark Harman},
  volume =       {4949},
  series =       lncs,
  publisher =    {Springer},
}

@book{Dijkstra:Discipline,
  author = "Edsger W. Dijkstra",
  title = "A Discipline of Programming",
  publisher = "Prentice Hall",
  address = "Englewood Cliffs, NJ",
  year = 1976
}

@InProceedings{LeinoMueller:ESOP2009,
  author =    {K. Rustan M. Leino and Peter M{\"u}ller},
  title =     {A Basis for Verifying Multi-threaded Programs},
  booktitle = {Programming Languages and Systems, 18th European
                  Symposium on Programming, ESOP 2009},
  editor =    {Giuseppe Castagna},
  volume =    {5502},
  series =    lncs,
  publisher = {Springer},
  month =     mar,
  year =      2009,
  pages =     {378-393},
}

@InProceedings{LeinoRuemmer:Boogie2,
  author =       {K. Rustan M. Leino and Philipp R{\"u}mmer},
  title =        {A Polymorphic Intermediate Verification Language:
                  Design and Logical Encoding},
  booktitle =    {Tools and Algorithms for the Construction and
                  Analysis of Systems, 16th International Conference,
                  TACAS 2010},
  editor =       {Javier Esparza and Rupak Majumdar},
  series =       lncs,
  volume =       6015,
  publisher =    {Springer},
  month =        mar,
  year =         2010,
  pages =        {312-327},
}

@book{LiskovGuttag:book,
  author = "Barbara Liskov and John Guttag",
  title = "Abstraction and Specification in Program Development",
  publisher = "MIT Press",
  series = "MIT Electrical Engineering and Computer Science Series",
  year = 1986
}

@TechReport{DahlEtAl:Simula67,
  author =       {Ole-Johan Dahl and Bj{\o}rn Myhrhaug and Kristen Nygaard},
  title =        {Common Base Language},
  institution =  {Norwegian Computing Center},
  type =         {Publication},
  number =       {S-22},
  month =        oct,
  year =         1970,
}

@inproceedings{LeinoMueller:ModelFields,
  author    = {K. Rustan M. Leino and
               Peter M{\"u}ller},
  title     = {A Verification Methodology for Model Fields},
  booktitle = "Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006",
  editor = "Peter Sestoft",
  series = lncs,
  volume = 3924,
  publisher = "Springer",
  month = mar,
  year = 2006,
  pages = {115-130},
}

@InProceedings{CarterEtAl:UsingPerfectDeveloper,
  author =       {Gareth Carter and Rosemary Monahan and Joseph M. Morris},
  title =        {Software Refinement with {P}erfect {D}eveloper},
  booktitle =    {Third IEEE International Conference on Software
                  Engineering and Formal Methods (SEFM 2005)},
  pages =        {363-373},
  editor =       {Bernhard K. Aichernig and Bernhard Beckert},
  month =        sep,
  year =         {2005},
  publisher =    {IEEE Computer Society},
}

@InProceedings{Abrial:SchorrWaite,
  author =       {Jean-Raymond Abrial},
  title =        {Event Based Sequential Program Development:
                  Application to Constructing a Pointer Program},
  booktitle =    {FME 2003: Formal Methods, International Symposium of
                  Formal Methods Europe},
  editor =       {Keijiro Araki and Stefania Gnesi and Dino Mandrioli},
  volume =       {2805},
  series =       lncs,
  publisher =    {Springer},
  month =        sep,
  year =         {2003},
  pages =        {51-74},
}

@article{Barnett-etal04,
  author    = {Mike Barnett and Robert DeLine and Manuel F{\"a}hndrich and
               K. Rustan M. Leino and Wolfram Schulte},
  title     = {Verification of Object-Oriented Programs with Invariants},
  journal   = {Journal of Object Technology},
  volume    = 3,
  number    = 6,
  year      = 2004,
  pages     = {27-56},
}

@InProceedings{SmansEtAl:ImplicitDynamicFrames,
  author = 	 {Jan Smans and Bart Jacobs and Frank Piessens},
  title = 	 {Implicit Dynamic Frames: Combining Dynamic Frames
                  and Separation Logic},
  booktitle =	 {ECOOP 2009 --- Object-Oriented Programming, 23rd
                  European Conference},
  editor =	 {Sophia Drossopoulou},
  volume =	 {5653},
  series =	 lncs,
  publisher =	 {Springer},
  month =	 jul,
  year =	 {2009},
  pages =	 {148-172},
}

@inproceedings{GriesPrins:Encapsulation,
  author = "David Gries and Jan Prins",
  title = "A New Notion of Encapsulation",
  booktitle = "Proceedings of the {ACM} {SIGPLAN} 85
               Symposium on Language Issues in Programming Environments",
  publisher = "ACM",
  series = "SIGPLAN Notices 20",
  number = 7,
  month = jul,
  year = 1985,
  pages = "131-139"
}

@InProceedings{YangHawblitzel:Verve,
  author =       {Jean Yang and Chris Hawblitzel},
  title =        {Safe to the last instruction: automated verification of a type-safe operating system},
  booktitle =    {Proceedings of the 2010 ACM SIGPLAN Conference on
                  Programming Language Design and Implementation, PLDI
                  2010},
  editor =       {Benjamin G. Zorn and Alexander Aiken},
  month =        jun,
  year =         {2010},
  publisher =    {ACM},
  pages =        {99-110},
}

@Book{BoyerMoore:book,
  author =       {Robert S. Boyer and J Strother Moore},
  title =        {A Computational Logic},
  publisher =    {Academic Press},
  series =       {ACM Monograph Series},
  year =         {1979},
}

@article{HoareWirth:Pascal,
  author = "C. A. R. Hoare and N. Wirth",
  title = "An axiomatic definition of the programming language {PASCAL}",
  journal = acta,
  volume = 2,
  number = 4,
  year = 1973,
  pages = "335-355"
}

@article{Hoare:AxiomaticBasis,
  author    = "C. A. R. Hoare",
  title     = "An axiomatic basis for computer programming",
  journal   = cacm,
  volume    = 12,
  number    = 10,
  year      = 1969,
  month     = oct,
  pages     = "576--580,583"
}

@InProceedings{LeinoMoskal:vacid0-notYetConfirmed,
  author =       {K. Rustan M. Leino and Micha{\l} Moskal},
  title =        {{VACID-0}: {V}erification of {A}mple {C}orrectness
                  of {I}nvariants of {D}ata-structures, Edition 0},
  booktitle =    {VS-Tools & Experiments},
  year =         2010,
  editor =       {Rajeev Joshi and Tiziana Margaria and Peter
                  M{\"u}ller and David Naumann and Hongseok Yang},
  series =       {VSTTE 2010 Workshop Proceedings},
  publisher =    {ETH Zurich Technical Report 676},
  month =        aug,
}

@InCollection{Chalice:tutorial,
  author =    {K. Rustan M. Leino and Peter M{\"u}ller and Jan Smans},
  title =     {Verification of Concurrent Programs with {C}halice},
  booktitle = {Foundations of Security Analysis and Design {V}: {FOSAD} 2007/2008/2009 Tutorial Lectures},
  editor =    {Alessandro Aldini and Gilles Barthe and Roberto Gorrieri},
  volume =    {5705},
  series =    lncs,
  publisher = {Springer},
  year =      {2009},
  pages =     {195-222}
}

@inproceedings{LeinoMuellerSmans10,
  author =    {K. Rustan M. Leino and Peter M{\"u}ller and Jan Smans},
  title =     {Deadlock-Free Channels and Locks},
  booktitle = {Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010},
  editor =    {Andrew D. Gordon},
  volume =    {6012},
  series =    lncs,
  publisher = {Springer},
  month =     mar,
  year =      {2010},
  pages =     {407-426}
}

@Book{BundyEtAl:Rippling,
  author =    {Alan Bundy and David Basin and Dieter Hutter and Andrew Ireland},
  title =     {Rippling: Meta-level Guidance for Mathematical Reasoning},
  publisher = {Cambridge University Press},
  volume =    {56},
  series =    {Cambridge Tracts in Theoretical Computer Science},
  year =      {2005},
}

@book{Gries:Science,
  author = "David Gries",
  title = "The Science of Programming",
  publisher = "Springer-Verlag",
  series = "Texts and Monographs in Computer Science",
  year = 1981
}

@Book{DijkstraFeijen:Book,
  author = "Edsger W. Dijkstra and W. H. J. Feijen",
  title = "A Method of Programming",
  publisher = "Addison-Wesley",
  month = jul,
  year = 1988,
}

@book{Kaldewaij:Programming,
  author    = "Anne Kaldewaij",
  title     = "Programming: The Derivation of Algorithms",
  publisher = "Prentice-Hall International",
  year      = 1990,
  series    = "Series in Computer Science",
}

@InProceedings{LeinoMonahan:VSTTE2010,
  author =       {K. Rustan M. Leino and Rosemary Monahan},
  title =        {Dafny Meets the Verification Benchmarks Challenge},
  booktitle =    {Verified Software: Theories, Tools, Experiments,
                  Third International Conference, VSTTE 2010},
  pages =        {112-126},
  year =         {2010},
  editor =       {Gary T. Leavens and Peter W. O'Hearn and Sriram K. Rajamani},
  volume =       {6217},
  series =       lncs,
  month =        aug,
  publisher =    {Springer},
}

@InProceedings{VSComp2010:report,
  author =       {Vladimir Klebanov and Peter M{\"u}ller and Natarajan Shankar and
                  Gary T. Leavens and Valentin W{\"u}stholz and Eyad Alkassar and
                  Rob Arthan and Derek Bronish and Rod Chapman and Ernie Cohen and
                  Mark Hillebrand and Bart Jacobs and K. Rustan M. Leino and
                  Rosemary Monahan and Frank Piessens and Nadia Polikarpova and
                  Tom Ridge and Jan Smans and Stephan Tobies and Thomas Tuerk and
                  Mattias Ulbrich and Benjamin Wei{\ss}},
  title =        {The 1st Verified Software Competition: Experience Report},
  booktitle =    {FM 2011: Formal Methods --- 17th International
                  Symposium on Formal Methods},
  pages =        {154-168},
  year =         {2011},
  editor =       {Michael Butler and Wolfram Schulte},
  volume =       {6664},
  series =       lncs,
  month =        jun,
  publisher =    {Springer},
}

@InProceedings{Leino:Dafny:LPAR16,
  author =       {K. Rustan M. Leino},
  title =        {Dafny: An Automatic Program Verifier for Functional Correctness},
  booktitle =    {LPAR-16},
  year =         {2010},
  volume =       {6355},
  series =       lncs,
  publisher =    {Springer},
  month =        apr,
  editor =       {Edmund M. Clarke and Andrei Voronkov},
  pages =        {348-370},
}

@book{BackVonWright:Book,
  author = "Ralph-Johan Back and von Wright, Joakim",
  title = "Refinement Calculus: A Systematic Introduction",
  series = "Graduate Texts in Computer Science",
  publisher = "Springer-Verlag",
  year = 1998
}

@Article{BalzerCheathamGreen:1990s,
  author = 	 {Robert Balzer and {Cheatham, Jr.}, Thomas E. and Cordell Green},
  title = 	 {Software Technology in the 1990's: Using a New Paradigm},
  journal = 	 {IEEE Computer},
  year = 	 {1983},
  volume =	 {16},
  number =	 {11},
  pages =	 {39-45 },
  month =	 nov,
}

@InProceedings{Zloof:QBE,
  author = 	 {Mosh{\'e} M. Zloof},
  title = 	 {Query by Example},
  booktitle =	 {American Federation of Information Processing
                  Societies: 1975 National Computer Conference},
  pages =	 {431-438},
  year =	 {1975},
  month =	 may,
  publisher =	 {AFIPS Press },
}

@InProceedings{HarrisGulwani:PLDI2011,
  author = 	 {William R. Harris and Sumit Gulwani},
  title = 	 {Spreadsheet table transformations from examples},
  booktitle =	 {Proceedings of the 32nd ACM SIGPLAN Conference on
                  Programming Language Design and Implementation, PLDI
                  2011},
  pages =	 {317-328},
  year =	 {2011},
  editor =	 {Mary W. Hall and David A. Padua},
  month =	 jun,
  publisher =	 {ACM},
}

@Article{Smith:KIDS-overview,
  author = "Douglas R. Smith",
  title = "{KIDS}: A Semi-Automatic Program Development System",
  journal = {IEEE Transactions on Software Engineering },
  volume = 16,
  number = 9,
  month = sep,
  year = 1990,
  pages = "1024-1043",
}

@Article{RodinToolset,
  author =       {Jean-Raymond Abrial and Michael Butler and Stefan
                  Hallerstede and Thai Son Hoang and Farhad Mehta and
                  Laurent Voisin},
  title =        {Rodin: An Open Toolset for Modelling and Reasoning in {Event-B}},
  journal =      {International Journal on Software Tools for Technology Transfer},
  year =         {2010},
  month =        apr,
}

@Article{Summers:LISP-from-examples,
  author = 	 {Phillip D. Summers},
  title = 	 {A Methodology for {LISP} Program Construction from Examples},
  journal = 	 jacm,
  year = 	 {1977},
  volume =	 {24},
  number =	 {1},
  pages =	 {161-175},
  month =	 jan,
}

@InProceedings{Pex:overview,
  author = 	 {Nikolai Tillmann and de Halleux, Jonathan},
  title = 	 {Pex---White Box Test Generation for {.NET}},
  booktitle =	 {Tests and Proofs, Second International Conference, TAP 2008},
  pages =	 {134-153},
  year =	 {2008},
  editor =	 {Bernhard Beckert and Reiner H{\"a}hnle},
  series =	 lncs,
  volume =	 {4966},
  month =	 apr,
  publisher =	 {Springer},
}

@InProceedings{GodefroidKlarlundSen:DART,
  author = 	 {Patrice Godefroid and Nils Klarlund and Koushik Sen},
  title = 	 {{DART}: directed automated random testing},
  booktitle =	 {Proceedings of the ACM SIGPLAN 2005 Conference on
                  Programming Language Design and Implementation},
  pages =	 {213-223},
  year =	 {2005},
  editor =	 {Vivek Sarkar and Mary W. Hall},
  month =	 jun,
  publisher =	 {ACM},
}

@PhdThesis{Monahan:thesis,
  author = 	 {Rosemary Monahan},
  title = 	 {Data Refinement in Object-Oriented Verification},
  school = 	 {Dublin City University},
  year = 	 {2010},
}

@InProceedings{Denali:pldi2002,
  author = 	 {Rajeev Joshi and Greg Nelson and Keith H. Randall},
  title = 	 {Denali: A Goal-directed Superoptimizer},
  booktitle =	 {Proceedings of the 2002 ACM SIGPLAN Conference on
                  Programming Language Design and Implementation
                  (PLDI)},
  pages =	 {304-314},
  year =	 {2002},
  month =	 jun,
  publisher =	 {ACM},
}
@Book{SETL,
  author =       {J. T. Schwartz and R. B. K. Dewar and E. Dubinsky and E. Schonberg},
  title =        {Programming with Sets: An Introduction to {SETL}},
  series =       {Texts and Monographs in Computer Science},
  publisher =    {Springer},
  year =         {1986},
}

@InProceedings{KuncakEtAl:PLDI2010,
  author = 	 {Viktor Kuncak and Mika{\"e}l Mayer and Ruzica Piskac
                  and Philippe Suter},
  title = 	 {Complete functional synthesis},
  booktitle =	 {Proceedings of the 2010 ACM SIGPLAN Conference on
                  Programming Language Design and Implementation, PLDI
                  2010},
  pages =	 {316-329},
  year =	 {2010},
  editor =	 {Benjamin G. Zorn and Alexander Aiken},
  month =	 jun,
  publisher =	 {ACM},
}

@Article{JML:ToolSuite:STTT,
  author = 	 {Lilian Burdy and Yoonsik Cheon and David R. Cok and 
                   Michael D. Ernst and Joeseph R. 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},
  volume =       7,
  number =       3,
  publisher =    {Springer},
  month =        jun,
  year = 	 2005,
  pages =        {212-232},
}

@InProceedings{Green:ProblemSolving,
  author =       {Cordell Green},
  title =        {Application of Theorem Proving to Problem Solving},
  booktitle =    {Proceedings of the 1st International Joint Conference on Artificial Intelligence},
  editor =       {Donald E. Walker and Lewis M. Norton},
  pages =        {219-240},
  year =         {1969},
  month =        may,
  publisher =    {William Kaufmann},
}

@Article{MannaWaldinger:CACM1971,
  author =       {Zohar Manna and Richard J. Waldinger},
  title =        {Towards automatic program synthesis},
  journal =      cacm,
  year =         {1971},
  volume =       {14},
  number =       {3},
  pages =        {151-165},
  month =        mar,
}

@Article{RichWaters:ProgAppren,
  author =       {Charles Rich and Richard C. Waters},
  title =        {The {P}rogrammer's {A}pprentice: A Research Overview},
  journal =      {IEEE Computer},
  year =         {1988},
  volume =       {21},
  number =       {11},
  pages =        {10-25},
  month =        nov,
}

@InProceedings{Green:PSI,
  author =       {Cordell Green},
  title =        {The Design of the {PSI} Program Synthesis System},
  booktitle =    {Proceedings of the 2nd International Conference on Software Engineering},
  pages =        {4-18},
  year =         {1976},
  month =        oct,
  publisher =    {IEEE Computer Society},
}

@Article{SpecSharp:Retrospective:CACM,
  author = 	 {Mike Barnett and Manuel F{\"a}hndrich and
                  K. Rustan M. Leino and Peter M{\"u}ller and
                  Wolfram Schulte and Herman Venter},
  title = 	 {Specification and Verification: The {Spec\#} Experience},
  journal = 	 cacm,
  volume =	 {54},
  number =	 {6},
  pages =	 {81-91},
  month =	 jun,
  year = 	 2011,
}

@article{Filipovic:SepLogicRefinement,
  author = {Ivana Filipovi{\'c} and Peter O'Hearn and
            Noah Torp-Smith and Hongseok Yang},
  title     = {Blaming the client: on data refinement in the presence of pointers},
  journal   = {Formal Aspects of Computing},
  volume    = {22},
  number    = {5},
  month     = sep,
  year      = {2010},
  pages     = {547-583},
}

@inproceedings{Grandy:JavaRefinement,
  author = {Grandy, Holger and Stenzel, Kurt and Reif, Wolfgang},
  title = {A refinement method for {J}ava programs},
  booktitle = {Formal Methods for Open Object-Based Distributed Systems, 9th IFIP WG 6.1 International Conference, FMOODS 2007},
  editor = {Marcello M. Bonsangue and Einar Broch Johnsen},
  series = lncs,
  number = {4468},
  month = jun,
  year = {2007},
  publisher = {Springer},
  pages = {221--235},
} 

@InCollection{KoenigLeino:MOD2011,
  author =    {Jason Koenig and K. Rustan M. Leino},
  title =     {Getting Started with {D}afny: A Guide},
  booktitle = {Software Safety and Security:  Tools for Analysis and Verification},
  pages =     {152-181},
  publisher = {IOS Press},
  year =      {2012},
  editor =    {Tobias Nipkow and Orna Grumberg and Benedikt Hauptmann},
  volume =    {33},
  series =    {NATO Science for Peace and Security Series D: Information and Communication Security},
  note =      {Summer School Marktoberdorf 2011 lecture notes},
}

@InProceedings{VonWright:ExtendingWindowInference,
  author = 	 {von Wright, Joakim},
  title = 	 {Extending Window Inference},
  booktitle =	 {Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98},
  pages =	 {17-32},
  year =	 {1998},
  editor =	 {Jim Grundy and Malcolm C. Newey},
  volume =	 {1479},
  series =	 lncs,
  publisher =	 {Springer},
}

@InProceedings{BauerWenzel:IsarExperience,
  author = 	 {Gertrud Bauer and Markus Wenzel},
  title = 	 {Calculational reasoning revisited: an {I}sabelle/{I}sar experience},
  booktitle =	 {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001},
  pages =	 {75-90},
  year =	 {2001},
  editor =	 {Richard J. Boulton and Paul B. Jackson},
  volume =	 {2152},
  series =	 lncs,
  month =	 sep,
  publisher =	 {Springer},
}

@InProceedings{Leino:induction,
  author = 	 {K. Rustan M. Leino},
  title = 	 {Automating Induction with an {SMT} Solver},
  booktitle =	 {Verification, Model Checking, and Abstract Interpretation --- 13th International Conference, VMCAI 2012},
  pages =	 {315-331},
  year =	 {2012},
  editor =	 {Viktor Kuncak and Andrey Rybalchenko},
  volume =	 {7148},
  series =	 lncs,
  month =	 jan,
  publisher =	 {Springer},
}

@InProceedings{LGLM:BVD,
  author = 	 {Le Goues, Claire and K. Rustan M. Leino and Micha{\l} Moskal},
  title = 	 {The {B}oogie {V}erification {D}ebugger (Tool Paper)},
  booktitle =	 {Software Engineering and Formal Methods --- 9th International Conference, SEFM 2011},
  pages =	 {407-414},
  year =	 {2011},
  editor =	 {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
  volume =	 {7041},
  series =	 lncs,
  month =	 nov,
  publisher =	 {Springer},
}

@InProceedings{Filliatre:2lines,
  author = 	 {Jean-Christophe Filli{\^a}tre},
  title = 	 {Verifying two lines of {C} with {Why3}: an exercise in
                  program verification},
  booktitle =	 {Verified Software: Theories, Tools, Experiments ---
                  4th International Conference, VSTTE 2012},
  pages =	 {83-97},
  year =	 {2012},
  editor =	 {Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski},
  volume =	 {7152},
  series =	 lncs,
  month =	 jan,
  publisher =	 {Springer},
}

@InCollection{LeinoMoskal:UsableProgramVerification,
  author = 	 {K. Rustan M. Leino and Micha{\l} Moskal},
  title = 	 {Usable Auto-Active Verification},
  booktitle = 	 {UV10 (Usable Verification) workshop},
  year =	 {2010},
  editor =	 {Tom Ball and Lenore Zuck and N. Shankar},
  month =	 nov,
  publisher =	 {\url{http://fm.csl.sri.com/UV10/}},
}

@InProceedings{LeinoMonahan:Comprehensions,
  author =    {K. Rustan M. Leino and Rosemary Monahan},
  title =     {Reasoning about Comprehensions with First-Order {SMT} Solvers},
  booktitle = {Proceedings of the 2009 ACM Symposium on Applied Computing (SAC)},
  editor =    {Sung Y. Shin and Sascha Ossowski},
  publisher = {ACM},
  month =     mar,
  year =      2009,
  pages =     {615-622},
}

@TechReport{VeriFast:TR,
  author =       {Bart Jacobs and Frank Piessens},
  title =        {The {VeriFast} program verifier},
  institution =  {Department of Computer Science, Katholieke Universiteit Leuven},
  year =         {2008},
  number =       {CW-520},
  month =        aug,
}

@book{DijkstraScholten:book,
  author = "Edsger W. Dijkstra and Carel S. Scholten",
  title = "Predicate Calculus and Program Semantics",
  publisher = "Springer-Verlag",
  series = "Texts and Monographs in Computer Science",
  year = 1990
}

@Book{KeY:book,
   author    = {Bernhard Beckert and Reiner H{\"a}hnle and Peter H. Schmitt},
   title     = {Verification of Object-Oriented Software: The {KeY} Approach},
   volume    = 4334,
   series    = lnai,
   publisher = {Springer},
   year      = 2007,
}

@Book{Coq:book,
  author =	 {Yves Bertot and Pierre Cast{\'e}ran},
  title = 	 {Interactive Theorem Proving and Program Development --- {C}oq'{A}rt: The Calculus of Inductive Constructions},
  publisher = 	 {Springer},
  year = 	 {2004},
  series =	 {Texts in Theoretical Computer Science},
}

@Book{ACL2:book,
  author =	 {Matt Kaufmann and Panagiotis Manolios and J Strother Moore},
  title = 	 {Computer-Aided Reasoning: An Approach},
  publisher = 	 {Kluwer Academic Publishers},
  year = 	 {2000},
}

@InProceedings{Coq:Coinduction,
  author = 	 {Eduardo Gim{\'e}nez},
  title = 	 {An Application of Co-inductive Types in {Coq}: Verification of the Alternating Bit Protocol},
  booktitle =    {Types for Proofs and Programs, International Workshop TYPES'95},
  pages =	 {135-152},
  year =	 {1996},
  editor =	 {Stefano Berardi and Mario Coppo},
  volume =	 1158,
  series =	 lncs,
  publisher =	 {Springer},
}

@InCollection{JacobsRutten:IntroductionCoalgebra,
  author = 	 {Bart Jacobs and Jan Rutten},
  title = 	 {An Introduction to (Co)Algebra and (Co)Induction},
  booktitle = 	 {Advanced Topics in Bisimulation and Coinduction},
  editor =	 {Davide Sangiorgi and Jan Rutten},
  series =	 {Cambridge Tracts in Theoretical Computer Science},
  number =	 {52},
  publisher =	 {Cambridge University Press},
  month =	 oct,
  year =	 {2011},
  pages =	 {38-99},
}

@InProceedings{SonnexEtAl:Zeno,
  author = 	 {William Sonnex and Sophia Drossopoulou and Susan Eisenbach},
  title = 	 {Zeno: An Automated Prover for Properties of Recursive
                  Data Structures},
  booktitle =	 {Tools and Algorithms for the Construction and Analysis of
                  Systems --- 18th International Conference, TACAS 2012},
  editor =	 {Cormac Flanagan and Barbara K{\"o}nig},
  volume =	 {7214},
  series =	 lncs,
  year =	 {2012},
  month =	 mar # "--" # apr,
  publisher =	 {Springer},
  pages =	 {407-421},
}

@InProceedings{JohanssonEtAl:IPT2010,
  author = 	 {Moa Johansson and Lucas Dixon and Alan Bundy},
  title = 	 {Case-Analysis for {R}ippling and Inductive Proof},
  booktitle =	 {Interactive Theorem Proving, First International Conference, ITP 2010},
  editor =	 {Matt Kaufmann and Lawrence C. Paulson},
  volume =	 {6172},
  series =	 lncs,
  publisher =	 {Springer},
  month =	 jul,
  year =	 {2010},
  pages =	 {291-306},
}

@Article{HatcliffEtAl:BISL,
  author = 	 {John Hatcliff and Gary T. Leavens and
                  K. Rustan M. Leino and Peter M{\"u}ller and Matthew Parkinson},
  title = 	 {Behavioral interface specification languages},
  journal = 	 {ACM Computing Surveys},
  volume =	 {44},
  number =	 {3},
  note =	 {Article 16},
  month =	 jun,
  year = 	 {2012},
}

@InProceedings{BoehmeNipkow:Sledgehammer,
  author = 	 {Sascha B{\"o}hme and Tobias Nipkow},
  title = 	 {Sledgehammer: {J}udgement {D}ay},
  booktitle =	 {Automated Reasoning, 5th International Joint Conference, IJCAR 2010},
  editor =	 {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
  year =	 {2010},
  pages =	 {107-121},
  volume =	 {6173},
  series =	 lncs,
  month =	 jul,
  publisher =	 {Springer},
}

@InProceedings{Dafny:LASER2011,
  author = 	 {Luke Herbert and K. Rustan M. Leino and Jose Quaresma},
  title = 	 {Using {Dafny}, an Automatic Program Verifier},
  booktitle =	 {Tools for Practical Software Verification, {LASER}, International Summer School 2011},
  editor =	 {Bertrand Meyer and Martin Nordio},
  volume =	 {7682},
  series =	 lncs,
  year =	 {2012},
  pages =	 {156-181},
  publisher =	 {Springer},
}

@Article{Leroy:CompCert:CACM,
  author = 	 {Xavier Leroy},
  title = 	 {Formal verification of a realistic compiler},
  journal = 	 cacm,
  volume =	 {52},
  number =	 {7},
  year = 	 {2009},
  pages =	 {107-115},
}

@InProceedings{Leino:ITP2013,
  author = 	 {K. Rustan M. Leino},
  title = 	 {Automating Theorem Proving with {SMT}},
  booktitle =	 {Interactive Theorem Proving --- 4th International Conference, ITP 2013},
  year =	 {2013},
  editor =	 {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
  volume =	 {7998},
  series =	 lncs,
  pages =	 {2-16},
  month =	 jul,
  publisher =	 {Springer},
}

@techreport{Nelson:thesis,
  author = "Charles Gregory Nelson",
  title = "Techniques for Program Verification",
  institution = "Xerox PARC",
  month = jun,
  year = 1981,
  number = "CSL-81-10",
  note = "The author's PhD thesis"
}

@InProceedings{LernerMillsteinChambers:VerifiedOptimizations,
  author = 	 {Sorin Lerner and Todd Millstein and Craig Chambers},
  title = 	 {Automatically proving the correctness of compiler optimizations},
  booktitle =	 {Proceedings of the ACM SIGPLAN 2003 Conference on
                  Programming Language Design and Implementation 2003},
  year =	 {2003},
  editor =	 {Ron Cytron and Rajiv Gupta},
  pages =	 {220-231},
  month =	 jun,
  publisher =	 {ACM},
}

@InProceedings{BoyerHunt:ACL2,
  author =       {Robert S. Boyer and Hunt, Jr., Warren A.},
  title =        {Function Memoization and Unique Object Representation for {ACL2} Functions},
  booktitle =    {Proceedings of the Sixth International Workshop on
                  the ACL2 Theorem Prover and its Applications, ACL2 2006},
  editor =       {Panagiotis Manolios and Matthew Wilding},
  month =        aug,
  year =         {2006},
  pages =        {81--89},
  publisher =    {ACM},
}

@inproceedings{LeinoWuestholz:DafnyIDE,
  author    = {K. Rustan M. Leino and
               Valentin W{\"{u}}stholz},
  title     = {The {D}afny Integrated Development Environment},
  booktitle = {Proceedings 1st Workshop on Formal Integrated Development Environment,
               {F-IDE} 2014},
  month     = apr,
  year      = {2014},
  pages     = {3--15},
  editor    = {Catherine Dubois and
               Dimitra Giannakopoulou and
               Dominique M{\'{e}}ry},
  series    = {{EPTCS}},
  volume    = {149},
}

@inproceedings{BarnettLeino:Weakest,
 author = {Mike Barnett and K. Rustan M. Leino},
 title = {Weakest-precondition of unstructured programs},
 booktitle = {Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on
                  Program Analysis For Software Tools and Engineering,
                  PASTE'05},
 editor = {Michael D. Ernst and Thomas P. Jensen},
 month = sep,
 year = {2005},
 pages = {82-87},
 publisher = {ACM},
}