@string{lncs = "LNCS"}

@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},
}

@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{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},
  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 Joseph 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 =	 {VMCAI 2012},
  pages =	 {315-331},
  year =	 {2012},
  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 =  {Dept. of Computer Science, Katholieke Universiteit Leuven},
  year =         {2008},
  number =       {CW-520},
}

@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{Coq:book,
  author =	 {Yves Bertot and Pierre Cast{\'e}ran},
  title = 	 {{C}oq'{A}rt: The Calculus of Inductive Constructions},
  publisher = 	 {Springer},
  year = 	 {2004},
  series =	 {Texts in Theoretical Comp. Sci.},
}

@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},
  series =	 {Cambridge Tracts in Theoretical Comp. Sci.},
  number =	 {52},
  publisher =	 {Cambridge Univ. Press},
  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 =	 {ITP 2013},
  year =	 {2013},
  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},
}

@InProceedings{AutoProof:TACAS2015,
  author = 	 {Julian Tschannen and Carlo A. Furia and Martin Nordio and Nadia Polikarpova},
  title = 	 {{AutoProof}: Auto-Active Functional Verification of Object-Oriented Programs},
  booktitle =	 {Tools and Algorithms for the Construction and
                  Analysis of Systems --- 21st International Conference,
                  TACAS 2015},
  OPTyear = 	 {2015},
  editor =	 {Christel Baier and Cesare Tinelli},
  volume =	 {9035},
  series =	 lncs,
  pages =	 {566-580},
  month =	 apr,
  publisher =	 {Springer},
}

@Article{Doyle:TMS,
  author = 	 {Jon Doyle},
  title = 	 {A Truth Maintenance System},
  journal = 	 {Artificial Intelligence},
  year = 	 {1979},
  month =	 nov,
  volume =	 {12},
  number =	 {3},
  pages =	 {231-272},
}

@InProceedings{LeinoMueller:SpecSharp:Tutorial,
  author =    {K. Rustan M. Leino and Peter M{\"u}ller},
  title =     {Using the {Spec\#} Language, Methodology, and Tools to Write Bug-Free Programs},
  booktitle = {LASER Summer School 2007/2008},
  editor =    {Peter M{\"u}ller},
  series =    lncs,
  volume =    6029,
  year =      2010,
  publisher = {Springer},
  pages =     {91-139},
}

@inproceedings{TFNP-TACAS15,
  author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Nadia Polikarpova},
  title = {{AutoProof}: Auto-active Functional Verification of Object-oriented Programs},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems --- 21st International Conference, TACAS 2015},
  editor = {Christel Baier and Cesare Tinelli},
  series = lncs,
  volume = {9035},
  month = apr,
  year = {2015},
  publisher = {Springer},
  pages = {566-580},
}

@inproceedings{PTFM-FM14,
  author = {Nadia Polikarpova and Julian Tschannen and Carlo A. Furia and Bertrand Meyer},
  title = {Flexible Invariants Through Semantic Collaboration},
  booktitle = {FM 2014},
  series = lncs,
  volume = {8442},
  publisher = {Springer},
  month = may,
  year = {2014},
  pages = {514-530}
}

@InProceedings{VeriFast:Java:tutorial,
  author = 	 {Jan Smans and Bart Jacobs and Frank Piessens},
  title = 	 {{VeriFast} for {J}ava: A Tutorial},
  booktitle =	 {Aliasing in Object-Oriented Programming. Types, Analysis and Verification},
  year =	 {2013},
  editor =	 {Dave Clarke and James Noble and Tobias Wrigstad},
  volume =	 {7850},
  series =	 lncs,
  pages =	 {407-442},
  publisher =	 {Springer},
}

@InProceedings{Traits:ECOOP2003,
  author = 	 {Nathanael Sch{\"a}rli and St{\'e}phane Ducasse and Oscar Nierstrasz and Andrew P. Black},
  title = 	 {Traits: Composable Units of Behaviour},
  booktitle =	 {ECOOP 2003 --- Object-Oriented Programming, 17th European Conference},
  editor =	 {Luca Cardelli},
  series =	 lncs,
  volume =	 {2743},
  pages =	 {248-274},
  month =	 jul,
  year =	 {2003},
  publisher =	 {Springer},
}

@Article{Traits:logic,
  author = 	 {Ferruccio Damiani and Johan Dovland and Einar Broch Johnsen and Ina Schaefer},
  title = 	 {Verifying traits: an incremental proof system for fine-grained reuse},
  journal = 	 {Formal Aspects of Computing},
  volume =	 {26},
  number =	 {4},
  pages =	 {761-793},
  month =	 jul,
  year = 	 {2014},
}

@inproceedings{LeinoPolikarpova:calc,
  author    = {K. Rustan M. Leino and
               Nadia Polikarpova},
  title     = {Verified Calculations},
  booktitle = {VSTTE 2013},
  series = lncs,
  volume = 8164,
  year      = {2014},
  pages     = {170-190},
  publisher = {Springer},
}

@Article{LeinoYessenov:ChaliceRefinement,
  author =       {K. Rustan M. Leino and Kuat Yessenov},
  title =        {Stepwise refinement of heap-manipulating code in {C}halice},
  journal =      {Formal Aspects of Computing},
  year =         {2012},
  volume =       {24},
  number =       {4--6},
  pages =        {519--535},
  month =        jul,
}

@article{Wirth:StepwiseRefinment,
  author    = "N. Wirth",
  title     = "{Program Development by Stepwise Refinement}",
  journal   = cacm,
  volume    = 14,
  year      = 1971,
  pages     = "221-227"
}

@article{Dijkstra:Refinement,
  author = "E. W. Dijkstra",
  title = "A constructive approach to the problem of program correctness",
  journal = "BIT",
  volume = 8,
  year = 1968,
  pages = "174-186"
}

@phdthesis{Back:thesis,
  author    = "R.-J. R. Back",
  title     = "On the Correctness of Refinement Steps in Program Development",
  school    = "University of Helsinki",
  year      = 1978,
  note      = "Report A-1978-4"
}

@article{Morgan:SpecStmt,
  author = "Carroll Morgan",
  title = "The Specification Statement",
  journal = toplas,
  volume = 10,
  number = 3,
  year = 1988,
  month = jul,
  pages = "403-419"
}

@book{Morgan:book,
  author    = "Carroll Morgan",
  title     = "Programming from Specifications",
  publisher = "Prentice-Hall International",
  series = "Series in Computer Science",
  year      = 1990
}

@article{Morris:Refinement,
  author = "Joseph M. Morris",
  title = "A theoretical basis for stepwise refinement and the
    programming calculus",
  journal = scp,
  volume = 9,
  number = 3,
  month = dec,
  year = 1987,
  pages = "287-306"
}

@article{GriesVolpano:Transform,
  author = "David Gries and Dennis Volpano",
  title = "The Transform --- a New Language Construct",
  journal = "Structured Programming",
  volume = 11,
  number = 1,
  year = 1990,
  pages = "1-10"
}

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

@Book{Jones:VDM:book,
  Author = "Cliff B. Jones",
  Title = "Systematic Software Development Using {VDM}",
  Publisher = "Prentice Hall",
  Series = "International Series in Computer Science",
  Address = "Englewood Cliffs, N.J.",
  Edition = "Second",
  Year = 1990
}

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

@Misc{ClearSy:AtelierB,
  author =       {ClearSy},
  title =        {Atelier {B}},
  howpublished = {\url{http://www.atelierb.eu/}},
}

@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},
}

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

@Article{BackSere:ActionSystems,
  author =       {Ralph-Johan Back and Kaisa Sere},
  title =        {Stepwise Refinement of Action Systems},
  journal =      {Structured Programming},
  year =         {1991},
  volume =       {12},
  number =       {1},
  pages =        {17-30},
}

@InProceedings{VCC:overview,
  author =       {Ernie Cohen and Markus Dahlweid and Mark 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},
  month =        aug,
  year =         {2009},
  pages =        {23-42},
}

@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},
}

@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
}

@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},
}

@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"
}

@manual{baudin09acsl,
  title = {{ACSL}: {ANSI}/{ISO} {C} Specification Language, version 1.4},
  author = {Patrick Baudin and Jean-Christophe Filli{\^a}tre and
    Claude March{\'e} and Benjamin Monate and Yannick
      Moy and Virgile Prevosto},
  year = 2009,
  note = {\url{http://frama-c.com/}}
}

@InProceedings{BarnettEtAl:Boogie,
  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"
}

@inproceedings{deMouraBjorner:Z3:overview,
  author    = "de Moura, Leonardo and Nikolaj Bj{\o}rner",
  title     = {{Z3}: An efficient {SMT} solver},
  booktitle = {TACAS 2008},
  series    = lncs,
  volume    = 4963,
  publisher = {Springer},
  month     = mar # "--" # apr,
  year      = 2008,
  pages     = {337-340},
}

@Article{Back-Mikhajlova-vonWright:ClassRefinement,
  author =       {Ralph-Johan Back and Anna Mikhaljova and von Wright, Joakim},
  title =        {Class Refinement as Semantics of Correct Object Substitutability},
  journal =      {Formal Aspects of Computing},
  volume =       {12},
  number =       {1},
  year =         {2000},
  month =        oct,
  pages =        {18-40},
}

@InProceedings{MikhajlovaSekerinski:ClassRefinement,
  author = 	 {Anna Mikhaljova and Emil Sekerinski},
  title = 	 {Class Refinement and Interface Refinement in Object-Oriented Programs},
  booktitle =	 {FME '97: Industrial Applications and Strengthened
    Foundations of Formal Methods, 4th International
      Symposium of Formal Methods Europe},
  editor =	 {John S. Fitzgerald and Cliff B. Jones and Peter Lucas},
  volume =	 {1313 },
  series =	 lncs,
  publisher =	 {Springer},
  month =	 sep,
  year =	 {1997},
  pages =	 {82-101},
}

@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},
}

@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 Robert Gorrieri},
  volume = 	  {5705},
  series = 	  lncs,
  publisher = {Springer},
  year = 	    {2009},
  pages =     {195-222},
}

@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{tafat10foveoos,
  author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
  title = {A Refinement Methodology for Object-Oriented Programs},
  booktitle = {Formal Verification of Object-Oriented Software, Papers
    Presented at the International Conference},
  editor = {Bernhard Beckert and Claude March\'e},
  month = jun,
  year = 2010,
  pages = {143--159},
}

@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},
}

@TechReport{HatcliffEtAl:survey-tr,
  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},
  institution =  {University of Central Florida, School of EECS},
  month =        oct,
  year =         {2010},
  number =       {CS-TR-09-01a},
}

@Article{HatcliffEtAl:survey:journal:tentativeInfo,
  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},
  year = 	 {2012},
  volume =	 {44},
  number =	 {3},
  month =	 may,
}

@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{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},
}

@Misc{Escher,
  author = "{Escher Technologies, Inc.}",
  title = "Getting started with {P}erfect",
  howpublished = "\url{http://www.eschertech.com}",
  year = 2001
}

@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"
}

@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{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},
}

# References supplied by the reviewers.
# Added 12/20/11.

@incollection{Potet:BComposition,
  author = {Potet, Marie and Rouzaud, Yann},
  affiliation = {LSR-IMAG Grenoble France},
  title = {Composition and refinement in the B-method},
  booktitle = {B￿￿98: Recent Advances in the Development and Use of the B Method},
  series = lncs,
  editor = {Bert, Didier},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {978-3-540-64405-7},
  keyword = {Computer Science},
  pages = {46-65},
  volume = {1393},
  url = {http://dx.doi.org/10.1007/BFb0053355},
  note = {10.1007/BFb0053355},
  year = {1998}
}

@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},
} 

@inproceedings{Wehrheim:Subtypes,
  author    = {Heike Wehrheim},
  title     = {Checking Behavioural Subtypes via Refinement},
  booktitle = {FMOODS},
  year      = {2002},
  pages     = {79-93},
  crossref  = {DBLP:conf/fmoods/2002},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Banerjee:ownership,
  author = {Banerjee, Anindya and Naumann, David A.},
  title = {Ownership confinement ensures representation independence for object-oriented programs},
  journal = jacm,
  volume = {52},
  issue = {6},
  month = {November},
  year = {2005},
  issn = {0004-5411},
  pages = {894--960},
  numpages = {67},
  url = {http://doi.acm.org/10.1145/1101821.1101824},
  doi = {http://doi.acm.org/10.1145/1101821.1101824},
  acmid = {1101824},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Alias control, confinement, data refinement, relational parametricity, simulation},
} 

@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,
}

@InProceedings{Heule:FractionsWithoutFractions,
  author = 	 {Stefan Heule and K. Rustan M. Leino and Peter
                  M{\"u}ller and Alexander J. Summers},
  title = 	 {Fractional Permissions without the Fractions},
  booktitle =	 {13th Workshop on Formal Techniques for Java-like
                  Programs, FTfJP 2011},
  year =	 {2011},
  month =	 jul,
}

@incollection{Morgan:Capjunctive,
  author = "Carroll Morgan",
  title = "The Cuppest Capjunctive Capping, and {G}alois",
  editor = "A. W. Roscoe",
  booktitle = "A Classical Mind:  Essays in Honour of C.A.R. Hoare",
  publisher = "Prentice-Hall",
  series = "International Series in Computer Science",
  pages = "317-332",
  year = 1994
}

@Article{Morgan:CompositionalNoninterference,
  author = 	 {Carroll Morgan},
  title = 	 {Compositional noninterference from first principles},
  journal = 	 fac,
  year = 	 {2012},
  volume =	 {24},
  number =	 {1},
  pages =	 {3-26},
}

@article{DenningDenning:Certification,
  author = "Dorothy E. Denning and Peter J. Denning",
  title = "Certification of Programs for Secure Information Flow",
  journal = cacm,
  volume = 20,
  number = 7,
  month = jul,
  year = 1977,
  pages = "504-513"
}

@article{Jones:Interference,
  author = "C. B. Jones",
  title = "Accommodating interference in the formal design of
		  concurrent object-based programs",
  journal = "Formal Methods in System Design",
  volume = 8,
  number = 2,
  pages = "105-122",
  month = mar,
  year = 1996
}

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

@inproceedings{LeuschelButler:FME03,
   author =    {Michael Leuschel and Michael Butler},
   title =     {Pro{B}: A Model Checker for {B}},
   booktitle = {FME 2003: Formal Methods},
   editor =    {Araki, Keijiro and Gnesi, Stefania and Mandrioli, Dino},
   publisher = {Springer},
   series =    lncs,
   number =    {2805},
   year =      2003,
   pages =     {855-874},
}

@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},
}

@Article{LiskovWing94,
  author = "Barbara Liskov and Jeannette M. Wing",
  title = "A Behavioral Notion of Subtyping",
  journal = toplas,
  year = 1994,
  volume = 16,
  number = 6
}

@book{WoodcockDavies:UsingZ,
  title = "Using {Z}: Specification, Refinement, and Proof",
  author = "Jim Woodcock and Jim Davies",
  year = "1996",
  publisher = "Prentice Hall International",
}

@Article{Leavens:ModularOOSpecs,
  author = 	 {Gary T. Leavens},
  title = 	 {Modular Specification and Verification of Object-Oriented Programs},
  journal = 	 {IEEE Software},
  year = 	 {1991},
  volume =	 {8},
  number =	 {4},
  pages =	 {72-80},
}

@InProceedings{ShieldHayes:InvsAndDynConstraints,
  author = 	 {Jamie Shield and Ian J. Hayes},
  title = 	 {Refining Object-Oriented Invariants and Dynamic Constraints},
  booktitle =	 {9th Asia-Pacific Software Engineering Conference (APSEC 2002)},
  pages =	 {52-61},
  year =	 {2002},
  publisher =	 {IEEE Computer Society},
}

@TechReport{Chalice:predicates:TR,
 author = {S. Heule and I. T. Kassios and P. M\"uller and A. J. Summers},
 title = {Verification Condition Generation for Permission Logics with Abstraction Functions},
 institution = {ETH Zurich},
 year = {2012},
 number = {761}
}

@InCollection{KleinEtAl:DataRefinement,
  author =    {Gerwin Klein and Thomas Sewell and Simon Winwood},
  title =     {Refinement in the formal verification of {seL4}},
  booktitle = {Design and Verification of Microprocessor Systems for High-Assurance Applications},
  editor =    {David S. Hardin},
  pages =     {323--339},
  month =     Mar,
  year =      {2010},
  publisher = {Springer},
}

@InProceedings{DharaLeavens:forcing,
  author =       {Krishna Kishore Dhara and Gary T. Leavens},
  title =        {Forcing Behavioral Subtyping through Specification Inheritance},
  booktitle =    {18th International Conference on Software Engineering},
  year =         {1996},
  editor =       {H. Dieter Rombach and T. S. E. Maibaum and Marvin V. Zelkowitz},
  pages =        {258-267},
  month =        mar,
  publisher =    {IEEE Computer Society},
}

@InProceedings{SpiritOfGhostCode,
  author =       {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and Andrei Paskevich},
  title =        {The Spirit of Ghost Code},
  booktitle =    {Computer Aided Verification --- 26th International Conference, CAV 2014},
  year =         {2014},
  editor =       {Armin Biere and Roderick Bloem},
  series =       lncs,
  volume =       {8559},
  pages =        {1-16},
  month =        jul,
  publisher =    {Springer},
}

@InProceedings{Dafny:traits,
  author =       {Reza Ahmadi and K. Rustan M. Leino and Jyrki Nummenmaa},
  title =        {Automatic Verification of {D}afny Programs with Traits},
  booktitle =    {Formal Techniques for {J}ava-like Programs, FTfJP 2015},
  year =         {2015},
  editor =       {Rosemary Monahan},
  publisher =    {ACM},
}

@InProceedings{Dafny:Cloudmake,
  author =       {Maria Christakis and K. Rustan M. Leino and Wolfram Schulte},
  title =        {Formalizing and Verifying a Modern Build Language},
  booktitle =    {FM 2014: Formal Methods --- 19th International Symposium},
  year =         {2014},
  editor =       {Cliff B. Jones and Pekka Pihlajasaari and Jun Sun},
  volume =       {8442},
  series =       lncs,
  pages =        {643-657},
  month =        may,
  publisher =    {Springer},
}

@Misc{Leino:SPLASH2012:keynote,
  author =       {K. Rustan M. Leino},
  title =        {Staged Program Development},
  howpublished = {SPLASH 2012 keynote},
  note =         {InfoQ video, \url{http://www.infoq.com/presentations/Staged-Program-Development}},
  month =        oct,
  year =         {2012},
}

@article{Parnas:secret,
  author = "D. L. Parnas",
  title = "On the criteria to be used in decomposing systems into modules",
  journal = cacm,
  volume = 15,
  number = 12,
  month = dec,
  year = 1972,
  pages = "1053-1058",
  note = "Reprinted as {\tt www.acm.org/classics/may96/}"
}

@InProceedings{KIV:overview,
  author = 	 {Wolfgang Reif},
  title = 	 {The {KIV} System: Systematic Construction of Verified Software},
  booktitle =	 {Automated Deduction --- CADE-11, 11th International Conference
                  on Automated Deduction},
  editor =	 {Deepak Kapur},
  series =	 lncs,
  volume =	 {607},
  publisher =	 {Springer},
  pages =	 {753-757},
  month =	 jun,
  year =	 {1992},
}

@InProceedings{LeinoMoskal:Coinduction,
  author =       {K. Rustan M. Leino and Micha{\l} Moskal},
  title =        {Co-induction Simply --- Automatic Co-inductive Proofs in a Program Verifier},
  booktitle =    {FM 2014},
  series =       lncs,
  volume =       {8442},
  publisher =    {Springer},
  month =        may,
  year =         {2014},
  pages =        {382-398},
}

@Article{Tarski:theorem,
  author = "Alfred Tarski",
  title = "A lattice-theoretical fixpoint theorem and its applications",
  journal = "Pacific Journal of Mathematics",
  year = 1955,
  volume = 5,
  pages = "285-309"
}

@TechReport{KozenSilva:Coinduction,
  author =       {Dexter Kozen and Alexandra Silva},
  title =        {Practical coinduction},
  institution =  {Comp. and Inf. Science, Cornell Univ.},
  year =         {2012},
  number =       {\url{http://hdl.handle.net/1813/30510}},
}

@book{Milner:CCS,
 author = "Robin Milner",
 title = {A  Calculus of Communicating Systems},
 year = {1982},
 publisher = {Springer},
}
 
@Book{NipkowKlein:ConcreteSemantics,
  author =       {Tobias Nipkow and Gerwin Klein},
  title =        {Concrete Semantics with {I}sabelle/{HOL}},
  publisher =    {Springer},
  year =         {2014},
}

@Book{Pierce:SoftwareFoundations,
  author =       {Benjamin C. Pierce and Chris Casinghino and
                  Marco Gaboardi and Michael Greenberg and
                  C{\u{a}}t{\u{a}}lin Hri\c{t}cu and Vilhelm Sj{\"o}berg and
                  Brent Yorgey},
  title =        {Software Foundations},
  publisher =    {\url{http://www.cis.upenn.edu/~bcpierce/sf}},
  year =         {2015},
  edition =      {version 3.2},
  month =        jan,
}

@InProceedings{ClochardEtAl:SemanticsInWhy3,
  author = {Martin Clochard and Jean-Christophe
  Filli\^atre and Claude March\'e and Andrei Paskevich},
  title =        {Formalizing Semantics with an Automatic Program Verifier},
  booktitle =    {VSTTE 2014},
  volume =       {8471},
  series =       lncs,
  publisher =    {Springer},
  month =        jul,
  year =         {2014},
  pages =        {37--51},
}

@Article{LeroyGrall:CoinductiveBigStep,
  author =       {Xavier Leroy and Herv\'e Grall},
  title =        {Coinductive big-step operational semantics},
  journal =      {Information and Computation},
  volume =       {207},
  number =       {2},
  pages =        {284-304},
  month =        feb,
  year =         {2009},
}

@InProceedings{SwamyEtAl:Fstar2011,
  author = 	 {Nikhil Swamy and Juan Chen and C{\'e}dric Fournet and
                  Pierre-Yves Strub and Karthikeyan Bhargavan and Jean Yang},
  title = 	 {Secure distributed programming with value-dependent types},
  booktitle =	 {ICFP 2011},
  publisher =	 {ACM},
  month =	 sep,
  year =	 {2011},
  pages =	 {266-278},
}

@Book{Nipkow-Paulson-Wenzel02,
  author =	 {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title = 	 {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
  publisher = 	 {Springer},
  year = 	 2002,
  volume =	 2283,
  series =	 LNCS,
}

@InProceedings{BoveDybjerNorell:BriefAgda,
  author = 	 {Ana Bove and Peter Dybjer and Ulf Norell},
  title = 	 {A Brief Overview of {A}gda --- A Functional Language with Dependent Types},
  booktitle =	 {TPHOLs 2009},
  series =	 lncs,
  volume =	 {5674},
  publisher =	 {Springer},
  month =	 aug,
  year =	 {2009},
  pages =	 {73-78},
}

@InProceedings{PaulinMohring:InductiveCoq,
  author =       {Christine Paulin-Mohring},
  title =        {Inductive Definitions in the system {C}oq --- Rules and Properties},
  booktitle =    {TLCA '93},
  series =       lncs,
  volume =       {664},
  pages =        {328-345},
  year =         {1993},
  publisher =    {Springer},
}

@TechReport{CamilleriMelham:InductiveRelations,
  author =       {Juanito Camilleri and Tom Melham},
  title =        {Reasoning with Inductively Defined Relations
                  in the {HOL} Theorem Prover},
  institution =  {University of Cambridge Computer Laboratory},
  year =         {1992},
  number =       {265},
  OPTmonth =     aug,
}

@Book{Winskel:FormalSemantics,
  author =       {Glynn Winskel},
  title =        {The Formal Semantics of Programming Languages: An Introduction},
  publisher =    {MIT Press},
  year =         {1993},
}

@inproceedings{Paulson:CADE1994,
  author    = {Lawrence C. Paulson},
  title     = {A Fixedpoint Approach to Implementing (Co)Inductive Definitions},
  booktitle = {CADE-12},
  editor    = {Alan Bundy},
  volume    = {814},
  series    = lncs,
  publisher = {Springer},
  year      = {1994},
  pages     = {148-161},
}

@InProceedings{Harrison:InductiveDefs,
  author =       {John Harrison},
  title =        {Inductive Definitions: Automation and Application},
  booktitle =    {TPHOLs 1995},
  year =         {1995},
  editor =       {E. Thomas Schubert and Phillip J. Windley and Jim Alves-Foss},
  volume =       {971},
  series =       lncs,
  pages =        {200-213},
  publisher =    {Springer},
}

@Article{ManoliosMoore:PartialFunctions,
  author =       {Panagiotis Manolios and J Strother Moore},
  title =        {Partial Functions in {ACL2}},
  journal =      {Journal of Automated Reasoning},
  year =         {2003},
  volume =       {31},
  number =       {2},
  pages =        {107-127},
}

@PhdThesis{Krauss:PhD,
  author =       {Alexander Krauss},
  title =        {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
  school =       {Technische Universit{\"a}t M{\"u}nchen},
  year =         {2009},
}