This file was created with JabRef 1.7.
Encoding: UTF-8

@inproceedings{preoteasa:2011c,
 author = {Preoteasa, Viorel},
 title = {Algebra of Monotonic Boolean Transformers},
 booktitle = {Proceedings of SBMF 2011},
 series          = {Lecture Notes in Computer Science},
 editors = {Simao, A. and Morgan, C.},
 year = {2011},
 pages = {140--155},
 publisher = {Springer-Verlag},
 address = {Berlin Heidelberg},
} 

@article {meinicke:solin:2010,
   author = {Meinicke, Larissa and Solin, Kim},
   affiliation = {Åbo Akademi Åbo Finland},
   title = {Refinement algebra for probabilistic programs},
   journal = {Formal Aspects of Computing},
   publisher = {Springer London},
   issn = {0934-5043},
   keyword = {Computer Science},
   pages = {3-31},
   volume = {22},
   issue = {1},
   url = {https://doi.org/10.1007/s00165-009-0111-1},
   note = {10.1007/s00165-009-0111-1},
   year = {2010}
}

@article{solin:vonwright:2009,
 author = {Solin, Kim and von Wright, Joakim},
 title = {Enabledness and termination in refinement algebra},
 journal = {Sci. Comput. Program.},
 volume = {74},
 issue = {8},
 month = {June},
 year = {2009},
 issn = {0167-6423},
 pages = {654--668},
 numpages = {15},
 url = {http://portal.acm.org/citation.cfm?id=1537316.1537540},
 doi = {10.1016/j.scico.2007.11.004},
 acmid = {1537540},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Action systems, Enabledness, Refinement algebra, Termination},
} 

@inproceedings{vonwright:2002,
 author = {von Wright, Joakim},
 title = {From Kleene Algebra to Refinement Algebra},
 booktitle = {Proceedings of the 6th International Conference on Mathematics of Program Construction},
 series = {MPC '02},
 year = {2002},
 isbn = {3-540-43857-2},
 pages = {233--262},
 numpages = {30},
 url = {http://portal.acm.org/citation.cfm?id=648086.747317},
 acmid = {747317},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 



@proceedings{2005gabbay2,
  editor    = {N. Art{\"e}mov, Sergei  and
               Barringer, Howard  and
                Garcez, Artur S. d'Avila and
                Lamb,  Lu\'{\i}s C.and
               Woods, John},
  title     = {We Will Show Them! Essays in Honour of Dov Gabbay, Volume
               Two},
  booktitle = {We Will Show Them! (2)},
  publisher = {College Publications},
  year      = {2005},
  isbn      = {1-904987-26-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{preoteasa:back:2009,
title = "Data Refinement of Invariant Based Programs",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "259",
number = "",
pages = "143 - 163",
year = "2009",
note = "Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009)",
issn = "1571-0661",
doi = "DOI: 10.1016/j.entcs.2009.12.022",
url = "http://www.sciencedirect.com/science/article/pii/S1571066109005040",
author = "Preoteasa, Viorel and Back, Ralph-Johan",
keywords = "Invariant based programming",
keywords = "Data refinement",
keywords = "Mechanical verification"
}


@article{kozen:1997,
 author = {Kozen, Dexter},
 title = {Kleene algebra with tests},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {19},
 issue = {3},
 month = {May},
 year = {1997},
 issn = {0164-0925},
 pages = {427--443},
 numpages = {17},
 url = {http://doi.acm.org/10.1145/256167.256195},
 doi = {http://doi.acm.org/10.1145/256167.256195},
 acmid = {256195},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Kleene algebra, dynamic logic, specification},
} 

@article{vonwright:2004,
 author = {von Wright, Joakim},
 title = {Towards a refinement algebra},
 journal = {Sci. Comput. Program.},
 volume = {51},
 issue = {1-2},
 month = {May},
 year = {2004},
 issn = {0167-6423},
 pages = {23--45},
 numpages = {23},
 url = {http://portal.acm.org/citation.cfm?id=1007972.1007975},
 doi = {10.1016/j.scico.2003.09.002},
 acmid = {1007975},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Kleene algebra, iteration, predicate transformers, refinement},
} 

@PhdThesis{preoteasa:thesis, 
  author = {Preoteasa, Viorel},
  title = {Program Variables -- The Core of Mechanical Reasoning about Imperative Programs}, 
  school = {Turku Centre for Computer Science},
  month = {Nov},
  year = {2006},
}

@article{preoteasa:2009,
title = "Frame rule for mutually recursive procedures manipulating pointers",
journal = "Theoretical Computer Science",
volume = "410",
number = "42",
pages = "4216 - 4233",
year = "2009",
note = "",
issn = "0304-3975",
doi = "DOI: 10.1016/j.tcs.2009.05.016",
url = "http://www.sciencedirect.com/science/article/pii/S0304397509003752",
author = "Preoteasa, Viorel",
keywords = "Predicate transformer semantics",
keywords = "Mechanical verification of programs",
keywords = "Mutually recursive procedures",
keywords = "Pointers",
keywords = "Separation logic",
keywords = "Frame rule"
}

@incollection {guerreiro:82,
   author = {Guerreiro, Pedro},
   title = {Another characterization of weakest preconditions},
   booktitle = {International Symposium on Programming},
   series = {Lecture Notes in Computer Science},
   editor = {Dezani-Ciancaglini, Mariangiola and Montanari, Ugo},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {},
   pages = {164-177},
   volume = {137},
   url = {https://doi.org/10.1007/3-540-11494-7\_12},
   note = {10.1007/3-540-11494-7\_12},
   year = {1982}
}

@inproceedings{back:vonwright:1989,
 author = {Back, Ralph-Johan and von Wright, Joakim},
 title = {A Lattice-theoretical Basis for a Specification Language},
 booktitle = {Proceedings of the International Conference on Mathematics of Program Construction, 375th Anniversary of the Groningen University},
 year = {1989},
 isbn = {3-540-51305-1},
 pages = {139--156},
 numpages = {18},
 url = {http://portal.acm.org/citation.cfm?id=648081.746973},
 acmid = {746973},
 publisher = {Springer-Verlag},
 address = {London, UK},
}

@article{back:vonwright:1990,
 author = {Back, Ralph-Johan and von Wright, Joakim},
 title = {Duality in specification languages: a lattice-theoretical approach},
 journal = {Acta Inf.},
 volume = {27},
 issue = {7},
 month = {July},
 year = {1990},
 issn = {0001-5903},
 pages = {583--625},
 numpages = {43},
 url = {http://portal.acm.org/citation.cfm?id=87660.87661},
 acmid = {87661},
 publisher = {Springer-Verlag New York, Inc.},
 address = {Secaucus, NJ, USA},
} 

@inproceedings{pnueli:2005,
  author    = {Pnueli, Amir},
  title     = {Verification of Procedural Programs},
  booktitle = {We Will Show Them!  Essays in Honour of Dov Gabbay, Volume Two},
  year      = {2005},
  pages     = {543-590},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{back:preoteasa:2011,
   author = {Back, Ralph-Johan and Preoteasa, Viorel},
   title = {Semantics and Proof Rules of Invariant Based Programs},
   booktitle = {Proc. of 26th Symposium On Applied Computing - Software Verification and Testing Track},
   publisher = {ACM},
   month = {March},
   year = {2011},
}

@article{preoteasa:back:2009,
author = {Preoteasa, Viorel and Back, Ralph-Johan},
title = {Data Refinement of Invariant Based Programs},
pdf = {marking-refine2009-final.pdf},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {259},
pages = {143 - 163},
year = {2009},
note = {Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009)},
issn = {1571-0661},
doi = {DOI: 10.1016/j.entcs.2009.12.022},
url = {http://www.sciencedirect.com/science/article/B75H1-4XYHXFB-B/2/27ba4be3ad580ef9b5a8b4a20a42d8ca},
keywords = {Invariant based programming},
keywords = {Data refinement},
keywords = {Mechanical verification},
abstract = {
Invariant based programming is an approach where we start to construct a program by first identifying the basic situations
(pre- and postconditions as well as invariants) that could arise during the execution of the algorithm. These situations are
identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow
of control in the program. Data refinement is a technique of building correct programs working on concrete data structures
as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant
based programs and we apply it the the construction of the classical Deutsch-Schorr-Waite graph marking algorithm. Our
results are formalized and mechanically proved in the Isabelle/HOL theorem prover.
},
}

@incollection{preoteasa:back:2010a,
  author =       {Preoteasa, Viorel and Back, Ralph-Johan},
  title =        {Semantics and Data Refinement of Invariant Based Programs },
  booktitle =    {Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {http://isa-afp.org/entries/DataRefinementIBP.shtml},
  month =        May,
  year =         2010,
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}

@incollection{preoteasa:back:2010b,
  author =       {Preoteasa, Viorel and Back, Ralph-Johan},
  title =        {Verification of the {D}eutsch-{S}chorr-{W}aite Graph Marking Algorithm using Data Refinement},
  booktitle =    {Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {http://isa-afp.org/entries/GraphMarkingIBP.shtml},
  month =        May,
  year =         2010,
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}

@article{aBack08,
	Author = {Back, Ralph-Johan},
	Date-Added = {2008-07-05 14:58:33 +0300},
	Date-Modified = {2008-08-05 17:58:06 +0300},
	Journal = {Formal Aspects of Computing},
	Owner = {ralph-johanback},
	Timestamp = {2007.11.20},
	Title = {Invariant Based Programming: Basic approach and Teaching Experience},
	Year = {2008},
	Bdsk-File-1 = { }}

@inproceedings{pBaErMy07,
	Author = {Back, Ralph-Johan and Eriksson, Johannes and Myreen, Magnus},
	Booktitle = {The International Conference on Tests And Proofs (TAP)},
	Date-Modified = {2008-08-05 18:30:14 +0300},
	Owner = {ralph-johanback},
	Timestamp = {2007.01.28},
	Title = {Testing and Verifying Invariant Based Programs in the {SOCOS} Environment},
	Year = {2007}}

@inproceedings{inpBaErMy06a,
	Author = {Back, Ralph-Johan and Eriksson, Johannes and Myreen, Magnus},
	Booktitle = {Teaching Formal Methods: Practice and Experience},
	Date-Added = {2008-07-05 14:56:28 +0300},
	Date-Modified = {2008-07-05 14:56:28 +0300},
	Editor = {Boca, P. and Bowen, J. P. and Duce, D. A.},
	File = {inpBaErMy06a.pdf:http\://crest.abo.fi/publications/public/2006/inpBaErMy06a.pdf:PDF},
	Month = {Dec},
	Publisher = {BCS},
	Series = {Electronic Workshops in Computing (eWiC)},
	Title = {Verifying Invariant Based Programs in the {SOCOS} Environment},
	Year = {2006},
	Bdsk-File-1 = { }}



@article{mehta:nipkow:2003,
    author={Mehta, F. and Nipkow, T.},
    title={Proving Pointer Programs in Higher-Order Logic},
    journal={Information and Computation},
    year=2005,
    volume=199,
    pages={200-227}
}

@article{schorr:waite:1967,
 author = {Schorr, H. and Waite, W. M.},
 title = {An efficient machine-independent procedure for garbage collection in various list structures},
 journal = {Commun. ACM},
 volume = {10},
 number = {8},
 year = {1967},
 issn = {0001-0782},
 pages = {501--506},
 doi = {http://doi.acm.org/10.1145/363534.363554},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@book{knuth:1997,
 author = {Knuth, D. E.},
 title = {The art of computer programming, volume 1 (3rd ed.): fundamental algorithms},
 year = {1997},
 isbn = {0-201-89683-4},
 publisher = {Addison Wesley Longman Publishing Co., Inc.},
 address = {Redwood City, CA, USA},
 }

@article{back:vonwright:2000,
 author = {Back, Ralph-Johan and von Wright, Joakim},
 title = {Encoding, Decoding and Data Refinement},
 journal = {Formal Aspects of Computing},
 volume = {12},
 issue = {5},
 year = {2000},
 issn = {0001-0782},
 pages = {313--349},
 doi = {10.1007/s001650070008},
 publisher = {Springer},
 }

@techreport
{back:preoteasa:2008,
author="Back, Ralph-Johan and Preoteasa, Viorel",
title="Semantics and Proof Rules of Invariant Based Programs",
language="none",
number="903",
year="2008",
month="Jul",
address="",
note="",
keywords="Invariant based programming. Semantics. Hoare proof rules. Completeness",
series="",
organisation="",
ISBN="978-952-12-2111-8",
institution="{TUCS}"
}

@book{abrial:1996,
 author = {Abrial, Jean-Raymond},
 title = {The B-book: assigning programs to meanings},
 year = {1996},
 isbn = {0-521-49619-5},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@book{deroever:1999,
 author = {DeRoever, W. and Engelhardt, K.},
 title = {Data Refinement: Model-Oriented Proof Methods and Their Comparison},
 year = {1999},
 isbn = {0521641705},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@inproceedings{Abrial:2003,
  author    = {Abrial, J.-R.},
  title     = {Event Based Sequential Program Development: Application
               to Constructing a Pointer Program},
  booktitle = {FME},
  year      = {2003},
  pages     = {51-74},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2805{\&}spage=51},
  crossref  = {DBLP:conf/fm/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/fm/2003,
  editor    = {Araki, Keijiro and
               Gnesi, Stefania and
               Mandrioli, Dino},
  title     = {FME 2003: Formal Methods, International Symposium of Formal
               Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings},
  booktitle = {FME},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2805},
  year      = {2003},
  isbn      = {3-540-40828-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{harrison-98,
        crossref        = "hol98",
        author          = "Harrison, J.",
        title           = "Formalizing {D}ijkstra",
        pages           = "171--188"}

@PROCEEDINGS{hol98,
        editor          = "Grundy, J. and Newey, M.",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           11th International Conference, TPHOLs'98",
        series          = "Lecture Notes in Computer Science",
        volume          = 1497,
        address         = "Canberra, Australia",
        date            = "September/October 1998",
        year            = 1998,
        publisher       = "Springer-Verlag"}

@article {igarashi-london-luckham-73,
    AUTHOR = {Igarashi, S. and London, R.L. and Luckham, D.C.},
     TITLE = {Automatic program verification. {I}. {A} logical basis and its
              implementation},
   JOURNAL = {Acta Informat.},
    VOLUME = {4},
      YEAR = {1974/75},
    NUMBER = {2},
     PAGES = {145--182},
   MRCLASS = {68A05},
  MRNUMBER = {MR0468284 (57 \#8121)},
MRREVIEWER = {Andrea Maggiolo-Schettini},
}


@PhdThesis{schirmer:phd, 
author = {Schirmer, N.},
title = {Verification of Sequential Imperative Programs in {I}sabelle/{HOL}}, 
school = {Technische Universit\"at M\"unchen},
 year = {2006}, }

@inproceedings{schirmer:2005,
author={Schirmer, N},
title={A Verification Environment for Sequential Imperative Programs in {I}sabelle/{HOL}},
booktitle="Logic for Programming, Artificial Intelligence, and Reasoning",
editor="F. Baader and A. Voronkov",
year=2005,
publisher={Springer},
series={LNAI},
volume=3452,
pages={398--414}}



@incollection {back-80,
    AUTHOR = {Back, Ralph-Johan},
     TITLE = {Semantics of unbounded nondeterminism},
 BOOKTITLE = {Automata, languages and programming (Proc. Seventh Internat.
              Colloq., Noordwijkerhout, 1980)},
    SERIES = {Lecture Notes in Comput. Sci.},
    VOLUME = {85},
     PAGES = {51--63},
 PUBLISHER = {Springer},
   ADDRESS = {Berlin},
      YEAR = {1980},
   MRCLASS = {68F05 (68B10)},
  MRNUMBER = {MR588992 (81j:68084)},
}

@TECHREPORT{Back-87,
  author = {Back, Ralph-Johan},
  title = {Procedural abstraction in the refinement calculus. Reports on computer science and mathematics},
  institution = {\AA bo Akademi},
  year = {1987},
  number = {55},
  url = {http://www.tucs.fi/Publications/Search/search.php},
}



@article {back-81,
    AUTHOR = {Back, Ralph-Johan},
     TITLE = {Proving total correctness of nondeterministic programs in
              infinitary logic},
   JOURNAL = {Acta Inform.},
  FJOURNAL = {Acta Informatica},
    VOLUME = {15},
      YEAR = {1981},
    NUMBER = {3},
     PAGES = {233--249},
      ISSN = {0001-5903},
     CODEN = {AINFA2},
   MRCLASS = {68B10 (03C75)},
  MRNUMBER = {MR625163 (82h:68010)},
}

@article {back-81a,
    AUTHOR = {Back, Ralph-Johan},
     TITLE = {On correct refinement of programs},
   JOURNAL = {J. Comput. System Sci.},
  FJOURNAL = {Journal of Computer and System Sciences},
    VOLUME = {23},
      YEAR = {1981},
    NUMBER = {1},
     PAGES = {49--68},
      ISSN = {0022-0000},
     CODEN = {JCSSBM},
   MRCLASS = {68B10},
  MRNUMBER = {MR636180 (83c:68013)},
}

@article {back-88,
    AUTHOR = {Back, Ralph-Johan},
     TITLE = {A calculus of refinements for program derivations},
   JOURNAL = {Acta Inform.},
  FJOURNAL = {Acta Informatica},
    VOLUME = {25},
      YEAR = {1988},
    NUMBER = {6},
     PAGES = {593--624},
      ISSN = {0001-5903},
     CODEN = {AINFA2},
   MRCLASS = {68Q60 (03B70)},
  MRNUMBER = {MR963274 (90c:68049)},
MRREVIEWER = {Alexey P. Stolboushkin},
}

@article {back-vonwright-92,
    AUTHOR = {Back, Ralph-Johan and von Wright, Joakim},
     TITLE = {Duality in specification languages: a lattice-theoretical approach},
   JOURNAL = {Acta Inform.},
  FJOURNAL = {Acta Informatica},
    VOLUME = {27},
      YEAR = {1990},
    NUMBER = {7},
     PAGES = {583--625},
      ISSN = {0001-5903},
     CODEN = {AINFA2},
   MRCLASS = {68Q60},
  MRNUMBER = {MR1073002 (91m:68118)},
MRREVIEWER = {A. V. An{\={\i}}s{\={\i}}mov},
}

@incollection {back-vonwright-93,
    AUTHOR = {Back, Ralph-Johan and von Wright, Joakim},
     TITLE = {Predicate transformers and higher order logic},
 BOOKTITLE = {Semantics: foundations and applications (Beekbergen, 1992)},
    SERIES = {Lecture Notes in Comput. Sci.},
    VOLUME = {666},
     PAGES = {1--20},
 PUBLISHER = {Springer},
   ADDRESS = {Berlin},
      YEAR = {1993},
   MRCLASS = {68Q60 (03B15 03B70)},
  MRNUMBER = {MR1255982 (94k:68129)},
}

================================================

@book{johnstone-87,
 author = {Johnstone, P.T.},
 title = {Notes on logic and set theory},
 year = {1987},
 isbn = {0-521-33502-7},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@TECHREPORT{preoteasa-05,
  author = {Preoteasa, V.},
  title = {Mutually recursive procedures},
  institution = {TUCS - Turku Centre for Computer Science},
  year = {2005},
  number = {???},
  month = {October},
  url = {http://www.tucs.fi/Publications/Search/search.php},
}

@TECHREPORT{preoteasa-06-b-tr,
  author = {Preoteasa, V.},
  title = {Mechanical Verification of Mutually Recursive Procedures for Parsing Expressions using Separation Logic},
  institution = {TUCS - Turku Centre for Computer Science},
  year = {2006},
  number = {771},
  month = {May},
  url = {http://www.tucs.fi/Publications/Search/search.php},
}

@inproceedings{preoteasa-06-a,
  author = {Preoteasa, V.},
  title = {Mechanical Verification of Recursive Procedures Manipulating Pointers using Separation Logic},
  booktitle = {FM 2006: Formal Methods},
  editor = {Misra, J. and Nipkow, T. and Sekerinski, E.},
  month = {August},
  year = {2006},
  location = {Hamilton, Canada},
  publisher = {Springer-Verlag},
  series={LNCS},
  volume=4085,
  pages={508--523},
}

@article{nipkow-98,author={Nipkow, T.},
title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
journal={Formal Aspects of Computing},
volume=10,
pages={171--186},
year=1998}

@article{hoare:1972,
 author = {Hoare, C. A. R.},
 title = {Proof of correctness of data representations},
 journal = {Acta Informatica},
 year = {1972},
 volume = {1},
 number = {4},
 month = dec,
 publisher = {Springer-Verlag New York, Inc.},
 address = {New York, NY, USA},
 }


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

@inproceedings{ohearn-reynolds-yang-01,
 author = {O'Hearn, P.W. and Reynolds, J.C. and Yang, H.},
 title = {Local Reasoning about Programs that Alter Data Structures},
 booktitle = {CSL '01: Proceedings of the 15th International Workshop on Computer Science Logic.},
 year = {2001},
 series = {Lecture Notes In Computer Science},
 volume = {2142},
 isbn = {3-540-42554-3},
 pages = {1--19},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@article{hehner-79,
 author = {Hehner, E. C. R.},
 title = {do considered od: A contribution to the programming calculus},
 journal = {Acta Informatica},
 volume = {11},
 number = {4},
 year = {1979},
 pages = {287--304},
 doi = {http://doi.acm.org/10.1007/BF00289091},
 publisher = {Springer},
 address = {Berlin / Heidelberg},
 }


@INPROCEEDINGS{inpBack06a,
  author = {Back, Ralph-Johan},
  title = {Invariant Based Programming Revisited},
  booktitle = {Petri Nets 2006, 27th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency},
  year = {2006},
  editor = {Donatelli, S. and Thiagarajan, P.S.},
  volume = {4024},
  series = {Lecture Notes in Computer Science},
  pages = {1 - 18},
  month = {Jun},
  publisher = {Springer Verlag},
}

@INPROCEEDINGS{reynolds:78,
  author = {Reynolds, J. C.},
  title = {Programming with Transition Diagrams},
  booktitle = {Programming Methodology},
  year = {1978},
  editor = {Gries, D.},
  publisher = {Springer Verlag, Berlin},
}

@article{vanemden-79,
 author = {Van Emden, M. H.},
 title = {Programming with Verification Conditions},
 journal = {IEEE Trans. Softw. Eng.},
 volume = {5},
 number = {2},
 year = {1979},
 issn = {0098-5589},
 pages = {148--159},
 doi = {https://doi.org/10.1109/TSE.1979.234171},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
 }

@INPROCEEDINGS{Back83:invariants,
  author = {Back, Ralph-Johan},
  title = {Invariant Based Programs and Their Correctness},
  booktitle = {Automatic Program Construction Techniques },
  year = {1983},
  editor = {Biermann, W. and Guiho, G and Kodratoff, Y},
  pages = {223--242},
  publisher = {MacMillan Publishing Company},
  pdf = {http://crest.abo.fi/publications/public/1983/InvariantBasedProgramsAndTheirCorrectnessP.pdf},
  project = {methods verification},
}


@INPROCEEDINGS{Back80:invariants,
  author = {Back, Ralph-Johan},
  title = {Semantic Correctness of Invariant Based Programs},
  booktitle = {International Workshop on Program Construction},
  year = {1980},
  address = {Chateau de Bonas, France},
  pdf = {http://crest.abo.fi/publications/public/1980/SemanticCorrectnessOfInvariantBasedProgramsP.pdf},
  project = {methods verification},
}

@INPROCEEDINGS{Back80:exceptions,
  author = {Back, Ralph-Johan},
  title = {Exception Handling with Multi-exit Statements},
  booktitle = {6th Fachtagung Programmiersprachen und Programmentwicklungen},
  year = {1980},
  editor = {H. J. Hoffmann},
  volume = {25},
  series = {Informatik Fachberichte},
  pages = {71-82},
  address = {Darmstadt},
  publisher = {Springer-Verlag},
  pdf = {http://crest.abo.fi/publications/public/1980/ExceptionHandlingWithMulti-ExitStatementsP.pdf},
  project = {methods verification},
}



@inproceedings{yang-ohearn-02,
 author = {Yang, H. and O'Hearn, P.W.},
 title = {A Semantic Basis for Local Reasoning},
 booktitle = {FoSSaCS '02: Proceedings of the 5th International Conference on 
              Foundations of Software Science and Computation Structures},
 year = {2002},
 volume = {2303},
 series = {Lecture Notes In Computer Science},
 isbn = {3-540-43366-X},
 pages = {402--416},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@inproceedings{weber-04,
  author    = {Weber, Tjark},
  title     = {Towards Mechanized Program Verification with Separation Logic},
  editor    = {Jerzy Marcinkowski and Andrzej Tarlecki},
  booktitle = {Computer Science Logic~-- 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 2004, Proceedings},
  volume    = {3210},
  series    = {Lecture Notes in Computer Science},
  pages     = {250--264},
  publisher = {Springer},
  month     = sep,
  year      = {2004},
  isbn      = {3-540-23024-6}
}



@article{back-preoteasa-05,
 author = {Back, Ralph-Johan and Preoteasa, Viorel},
 title = {An algebraic treatment of procedure refinement to support mechanical verification},
 journal = {Formal Aspects of Computing},
 year = {2005},
 volume = {17},
 issue = {1},
 month = {May},
 pages = {69 -- 90},
 publisher = {Springer},
 }

@inproceedings{back-vonwright-89a,
 author = {Back, Ralph-Johan and von Wright, Joakim},
 title = {A Lattice-theoretical Basis for a Specification Language},
 booktitle = {Proceedings of the International Conference on Mathematics of Program Construction, 375th Anniversary of the Groningen University},
 year = {1989},
 isbn = {3-540-51305-1},
 pages = {139--156},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@INPROCEEDINGS{cel-wri-02,
  author = {Celiku, Orieta and von Wright, Joakim},
  title = {Theorem Prover Support for Precondition and Correctness Calculation},
  booktitle = {4th International Conference on Formal Engineering Methods},
  year = {2002},
  pages = {299-310},
  crossref = {icfem02},
}

@inproceedings{nipkow-02a,
author={Nipkow, Tobias},
title={Hoare Logics for Recursive Procedures and Unbounded Nondeterminism},
booktitle={Computer Science Logic (CSL 2002)},
editor={J. Bradfield},
publisher={Springer},
series={LNCS},
volume={2471},
pages={103-119},
year=2002}


@article{homeier-martin-03,
 author = {Homeier, P.V. and Martin, D.F.},
 title = {Secure mechanical verification of mutually recursive procedures},
 journal = {Information and Computation},
 volume = {187},
 number = {1},
 year = {2003},
 issn = {0890-5401},
 pages = {1--19},
 doi = {https://doi.org/10.1016/S0890-5401(03)00133-0},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }


@inproceedings{homeier-martin-98,
 author = {Homeier, P.V. and Martin, D.F.},
 title = {Mechanical Verification of Total Correctness through Diversion Verification Conditions},
 booktitle = {Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics},
 year = {1998},
 isbn = {3-540-64987-5},
 pages = {189--206},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }



@BOOK{back-1980,
  title = {Correctness preserving program refinements: proof theory and applications},
  publisher = {Mathematisch Centrum},
  year = {1980},
  author = {Back, Ralph-Johan},
  volume = {131},
  series = {Mathematical Centre Tracts},
  address = {Amsterdam},
  isbn = {90-6196-207-2},
  mrclass = {68B10 (03C75)},
  mrnumber = {83k:68008},
  mrreviewer = {J. Bergstra},
  pages = {iii+118},
}

@PHDTHESIS{back-1978,
  author = {Back, Ralph-Johan},
  title = {On the correctness of refinement in program development},
  school = {Department of Computer Science, University of Helsinki},
  year = {1978},
  type = {{PhD} thesis},
}

@TECHREPORT{back-preoteasa-03,
  author = {Back, R. J. and Preoteasa, V.},
  title = {Reasoning about Recursive Procedures with Parameters},
  institution = {TUCS - Turku Centre for Computer Science},
  year = {2003},
  number = {500},
  month = {January},
  url = {http://www.tucs.fi/Publications/Search/search.php},
}

@INPROCEEDINGS{back-preoteasa-03-2,
  author = {Back, Ralph-Johan and Preoteasa, Viorel},
  title = {Reasoning about recursive procedures with parameters},
  booktitle = {Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding},
  year = {2003},
  pages = {1--7},
  publisher = {ACM Press},
  doi = {http://doi.acm.org/10.1145/976571.976573},
  isbn = {1-58113-800-8},
  location = {Uppsala, Sweden},
}

@ARTICLE{back-wright-02,
  author = {Back, Ralph-Johan and von Wright, Joakim},
  title = {Compositional Action System Refinement},
  journal = {Formal Aspects of Computing},
  year = {2003},
  volume = {15},
  pages = { 103--117 },
  number = {2--3},
  month = {November},
  publisher = {Springer-Verlag },
}

@BOOK{back-wright-98,
  title = {Refinement Calculus. A systematic Introduction},
  publisher = {Springer},
  year = {1998},
  author = {Back, Ralph-Johan and von Wright, Joakim},
}

@INPROCEEDINGS{back-fan-preoteasa-03,
  author = {Back, R. J. and Xiaocong, F. and Preoteasa, V.},
  title = {Reasoning about Pointers in Refinement Calculus},
  booktitle = {Tenth Asia-Pacific Software Engineering Conference Software Engineering Conference},
  year = {2003},
  pages = {425--434},
  month = DEC,
  publisher = {IEEE Computer Society},
}

@INPROCEEDINGS{stump:barrett:dill:2001,
  author = {Stump, A. and Barrett, C.W. and Dill, D.L.},
  title = {A decision Procedure for an Extensinal Theory of Arrays},
  booktitle = {16th Annual IEEE Symposium on Logic in Computer Science},
  year = {2001},
  publisher = {IEEE Computer Society},
}

@inproceedings{doligez:gonthier:1994,
 author = {Doligez, D. and Gonthier, G.},
 title = {Portable, unobtrusive garbage collection for multiprocessor systems},
 booktitle = {POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {1994},
 isbn = {0-89791-636-0},
 pages = {70--83},
 location = {Portland, Oregon, United States},
 doi = {http://doi.acm.org/10.1145/174675.174673},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@book{bauer,	
  author = {Bauer, F.L. and W\"{o}ssner, H.},
  title = {Algorithmic Language and Program Development},
  publisher = {Springer-Verlag},
  year = {1982}
}

@PHDTHESIS{king-69,
  author = {King, J.C.},
  title = {A program verifier},
  school = {Computer Science Department, Carnegie-Mellon University, Pittsburg, Pennsylvania},
  year = {1978},
  type = {{PhD} thesis},
}


@ARTICLE{bijlsma-1989,
  author = {Bijlsma, A. and Matthews, P. A. and Wiltink, J. G.},
  title = {A sharp proof rule for procedures in wp semantics},
  journal = {Acta Inform.},
  year = {1989},
  volume = {26},
  pages = {409--419},
  number = {5},
  coden = {AINFA2},
  fjournal = {Acta Informatica},
  issn = {0001-5903},
  mrclass = {68Q60},
  mrnumber = {90g:68088},
}

@INCOLLECTION{butler-grundy-wright-97,
  author = {Butler, M.J. and Grundy, J. and {L\aa ngbacka}, T. and Ruksenas R. and von~Wright, J.},
  title = {The Refinemen Calculator: Proof Support for Program Verification},
  booktitle = {FMP'97 Formal Methods Pacific},
  publisher = {Springer-Verlag},
  year = {1997},
  series = {Discrete Mathematics and Theoretical Computer Science},
  address = {Wellington, New Zealand},
  month = JUL,
}

@ARTICLE{church-40,
  author = {Church, A.},
  title = {A formulation of the simple theory of types},
  journal = {J. Symbolic logic},
  year = {1940},
  volume = {5},
  pages = {56--68},
  mrclass = {02.0X},
  mrnumber = {1,321d},
  mrreviewer = {H. B. Curry},
}

@BOOK{priestley,
  title = {Introduction to lattices and order},
  publisher = {Cambridge University Press},
  year = {2002},
  author = {Davey, B.A. and Priestley, H.A.},
  address = {New York},
  edition = {Second},
  isbn = {0-521-78451-4},
  mrclass = {06-01 (68Q55)},
  mrnumber = {1 902 334},
  pages = {xii+298},
}

@BOOK{dijkstra-76,
  title = {A discipline of programming},
  publisher = {Prentice-Hall Inc.},
  year = {1976},
  author = {Dijkstra, E.W.},
  address = {Englewood Cliffs, N.J.},
  note = {With a foreword by C. A. R. Hoare, Prentice-Hall Series in Automatic Computation},
  isbn = {0-13-215871-X},
  mrclass = {68A05},
  mrnumber = {58 \#31999},
  mrreviewer = {H. Kilov},
  pages = {xvii+217},
}

@article{wirth-71,
 author = {Wirth, N.},
 title = {Program development by stepwise refinement},
 journal = {Commun. ACM},
 volume = {14},
 number = {4},
 year = {1971},
 issn = {0001-0782},
 pages = {221--227},
 doi = {http://doi.acm.org/10.1145/362575.362577},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@INCOLLECTION{dijkstra-71,
  author = {Dijkstra, E.W.},
  title = {Notes on structured programming},
  editors = {O. Dahl, E.W. Dijkstra, and C.A.R. Hoare},
  booktitle = {Structured Programming},
  publisher = {Academic press},
  year = {1971},
}



@ARTICLE{dijkstra-75,
  author = {Dijkstra, E.W.},
  title = {Guarded commands, nondeterminacy and formal derivation of programs},
  journal = {Comm. ACM},
  year = {1975},
  volume = {18},
  pages = {453--457},
  number = {8},
  mrclass = {68A05},
  mrnumber = {52 \#4688},
  mrreviewer = {John Kam},
}

@BOOK{donahue,
  title = {Complementary definitions of programming language semantics},
  publisher = {Springer-Verlag},
  year = {1976},
  author = {Donahue, J.E.},
  address = {Berlin},
  note = {Lecture Notes in Computer Science, Vol. 42},
  mrclass = {68A05},
  mrnumber = {58 \#3611},
  pages = {iv+172},
}

@article {cook-78, 
AUTHOR = {Cook, S.A.}, 
TITLE = {Soundness and completeness of an axiom system for program verification}, 
JOURNAL = {SIAM J. Comput.}, 
FJOURNAL = {SIAM Journal on Computing}, 
VOLUME = {7}, YEAR = {1978}, 
NUMBER = {1}, 
PAGES = {70--90}, 
ISSN = {1095-7111}, 
MRCLASS = {68A05}, 
MRNUMBER = {MR0495086 (58 \#13843)},
 } 


@INPROCEEDINGS{gordon-88,
  author = {Gordon, M.J.C.},
  title = {Mechanizing Programming Logics in Higher-Order Logic},
  booktitle = {Current Trends in Hardware Verification and Automatic Theorem Proving ({P}roceedings of the Workshop on Hardware Verification)},
  year = {1988},
  editor = {{Birtwistle, G.M.} and {Subrahmanyam, P.A.}},
  pages = {387--439},
  address = {Banff, Canada},
  publisher = {Springer-Verlag, Berlin},
  url = {citeseer.nj.nec.com/gordon88mechanizing.html},
}

@ARTICLE{gries-levin-80,
  author = {Gries, D. and Levin, G.},
  title = {Assignment and Procedure Call Proof Rules},
  journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  year = {1980},
  volume = {2},
  pages = {564--579},
  number = {4},
  doi = {http://doi.acm.org/10.1145/357114.357119},
  issn = {0164-0925},
  publisher = {ACM Press},
}

@ARTICLE{halmos,
  author = {Halmos, P.R.},
  title = {An autobiography of polyadic algebras},
  journal = {Log. J. IGPL},
  year = {2000},
  volume = {8},
  pages = {383--392},
  number = {4},
  fjournal = {Logic Journal of the IGPL. Interest Group in Pure and Applied Logics},
  issn = {1367-0751},
}

@BOOK{kozen,
  title = {Dynamic logic},
  publisher = {MIT Press},
  year = {2000},
  author = {Harel, D. and Kozen, D. and Tiuryn, J.},
  address = {Cambridge, MA},
  isbn = {0-262-08289-6},
  pages = {xvi+459},
}

@ARTICLE{hesselink,
  author = {Hesselink, W.M.},
  title = {Predicate Transformers for Recursive Procedures with Local Variables},
  journal = {Formal Aspect of Computing},
  year = {1999},
  volume = {11},
  pages = {616--336},
}

@inproceedings{hoare-99,
title={A Trace Model for Pointers and Objects},
author={C.A.R. Hoare and H. Jifeng},
pages={1--17},
booktitle={Object Oriented Programming 13th European Conference (ECOOP'99),
	Lecture Notes in Computer Science},
year=1999,
volume=1628,
publisher={Springer-Verlag}
}


@INPROCEEDINGS{bart,
  author = {Jacobs, B.},
  title = {Coalgebraic Reasoning about Classes in Object-Oriented Languages},
  booktitle = {Electronic Notes in Theoretical Computer Science},
  year = {2000},
  editor = {Jacobs, B., and Moss, L. and Reichel, H. and Rutten, J.},
  volume = {11},
  publisher = {Elsevier Science Publishers},
}

@ARTICLE{kleymann-99,
  author = {Kleymann, T.},
  title = {Hoare Logic and Auxiliary Variables},
  journal = {Formal Aspect of Computing},
  year = {1999},
  volume = {11},
  pages = {541--566},
}

@PHDTHESIS{kleymann-98,
  author = {Kleymann, T.},
  title = {Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs},
  school = {Laboratory for Foundations of Computer Science, University of Edinburgh},
  year = {1998},
  type = {{PhD} thesis},
}

@PHDTHESIS{laibinis,
  author = {Laibinis, L.},
  title = {Mechanised Formal Reasoning About Modular Programs},
  school = {Turku Centre for Computer Science},
  year = {2000},
  type = {{PhD} Dissertation},
  month = apr,
}

@PHDTHESIS{leino-95,
  author = {Leino, K.R.M.},
  title = {Toward reliable modular programs},
  school = {California Institute of Technology},
  year = {1995},
  type = {{PhD} Thesis},
  month = jan,
}

@inproceedings{boulton:gordon:gordon:harrison:1992,
 author = {Boulton, R. J. and Gordon, A. and Gordon, M.J.C. and Harrison, J. and Herbert, J. and Van Tassel, J.},
 title = {Experience with Embedding Hardware Description Languages in HOL},
 booktitle = {Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design},
 year = {1992},
 isbn = {0-444-89686-4},
 pages = {129--156},
 publisher = {North-Holland},
 }


@TECHREPORT{detlefs-leino-nelson-saxe-98,
  author = {Detlefs, D.L. and Leino,  K.R.M. and Nelson, G. and Saxe,J.B.},
  title = {Extended static checking},
  institution = {Compaq Systems Research Center, Palo Alto, CA},
  year = {1998},
  number = {159},
  month = dec,
}

@inproceedings{flanagan:leino:al:2002,
 author = {Flanagan, C. and Leino,  K.R.M. and Lillibridge, M. and Nelson, G. and Saxe, J.B. and Stata, R.},
 title = {Extended static checking for Java},
 booktitle = {PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation},
 year = {2002},
 isbn = {1-58113-463-0},
 pages = {234--245},
 location = {Berlin, Germany},
 doi = {http://doi.acm.org/10.1145/512529.512558},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }



@PHDTHESIS{laibinis-00,
  author = {Laibinis, L.},
  title = {Mechanised Formal Reasoning About Modular Programs},
  school = {Turku Centre for Computer Science},
  year = {2000},
  type = {{PhD} Dissertation},
  month = apr,
}

@TECHREPORT{laibinis-wright-2001,
  author = {Laibinis, L. and von Wright, J.},
  title = {Specification Variables: Between the Angel and the Demon},
  institution = {TUCS - Turku Centre for Computer Science},
  year = {2001},
  number = {412},
  month = {June},
}

@BOOK{morgan-94,
  title = {Programming from specifications},
  publisher = {Prentice-Hall International},
  year = {1994},
  author = {Morgan, Carroll},
}

@ARTICLE{morgan-1988,
  author = {Morgan, Carroll},
  title = {The specification statement},
  journal = {ACM Trans. Program. Lang. Syst.},
  year = {1988},
  volume = {10},
  pages = {403--419},
  number = {3},
  doi = {http://doi.acm.org/10.1145/44501.44503},
  issn = {0164-0925},
  publisher = {ACM Press},
}

@ARTICLE{morgan-88,
  author = {Morgan, Carroll},
  title = {Procedures, parameters, and abstraction: separate concerns},
  journal = {Sci. Comput. Programming},
  year = {1988},
  volume = {11},
  pages = {17--27},
  number = {1},
  coden = {SCPGD4},
  fjournal = {Science of Computer Programming},
  issn = {0167-6423},
  mrclass = {68N05},
  mrnumber = {984 085},
}

@INCOLLECTION{morris-90,
  author = {J. M. Morris},
  title = {Programs from specifications},
  booktitle = {Formal development programs and proofs},
  publisher = {Addison-Wesley Longman Publishing Co., Inc.},
  year = {1990},
  pages = {81--115},
  isbn = {0-201-17237-2},
}

@ARTICLE{morris-87,
  author = {Morris, J.M.},
  title = {A theoretical basis for stepwise refinement and the programming calculus},
  journal = {Science of Computer Programming},
  year = {1987},
  volume = {9},
  pages = {287--306},
  number = {3},
  coden = {SCPGD4},
  issn = {0167-6423},
  doi = {https://doi.org/10.1016/0167-6423(87)90011-6},
  publisher = {Elsevier North-Holland, Inc.},
  mrclass = {68N05 (68Q55)},
  mrnumber = {88k:68017},
}

@INPROCEEDINGS{naraschewski-wenzel-98,
  author = {Naraschewski, W. and Wenzel, M.},
  title = {Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic},
  booktitle = {Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics},
  year = {1998},
  pages = {349--366},
  publisher = {Springer-Verlag},
  isbn = {3-540-64987-5},
}

@INPROCEEDINGS{barnett-leino-schulte-04,
  author = {Barnett, M. and Leino, K.R.M. and Schulte, W.},
  title = {The Spec\# programming system: An overview},
  booktitle = {In CASSIS 2004 post-proceedings},
  year = {2004},
}

@ARTICLE{naumann-2001,
  author = {Naumann, D.A.},
  title = {Calculating sharp adaptation rules},
  journal = {Inform. Process. Lett.},
  year = {2001},
  volume = {77},
  pages = {201--208},
  number = {2-4},
  coden = {IFPLAT},
  fjournal = {Information Processing Letters},
  issn = {0020-0190},
  mrclass = {68Q60},
  mrnumber = {2001m:68121},
}

@INPROCEEDINGS{nipkow-02,
  author = {Nipkow, T.},
  title = {Hoare Logics in {Isabelle/HOL}},
  booktitle = {Proof and System-Reliability},
  year = {2002},
  editor = {H. Schwichtenberg and R. Steinbr\"uggen},
  pages = {341-367},
  publisher = {Kluwer},
}

@ARTICLE{olderog-1983,
  author = {Olderog, E.R.},
  title = {On the notion of expressiveness and the rule of adaptation},
  journal = {Theoret. Comput. Sci.},
  year = {1983},
  volume = {24},
  pages = {337--347},
  number = {3},
  coden = {TCSDI},
  fjournal = {Theoretical Computer Science},
  issn = {0304-3975},
  mrclass = {68Q60 (03B70)},
  mrnumber = {85g:68047},
  mrreviewer = {Michael Bauer},
}

@TECHREPORT{PVS:Prelude,
  author = {Owre, S. and Shankar, N.},
  title = {The {PVS} Prelude library},
  institution = {Computer Science Laboratory, {SRI} International},
  year = {2003},
  number = {SRI-CSL-03-01},
  address = {Menlo Park, CA},
  month = {March},
}

@TECHREPORT{PVS:Interpretations,
  author = {Owre, S. and Shankar, N.},
  title = {Theory Interpretations in {PVS}},
  institution = {Computer Science Laboratory, {SRI} International},
  year = {2001},
  number = {SRI-CSL-01-01},
  address = {Menlo Park, CA},
  month = {April},
}

@TECHREPORT{PVS-ADT:TR,
  author = {Owre, S. and Shankar, N.},
  title = {Abstract Datatypes in {PVS}},
  institution = {Computer Science Laboratory, {SRI} International},
  year = {1993},
  number = {{SRI-CSL-93-9R}},
  address = {Menlo Park, {CA}},
  month = {dec},
  note = {Extensively revised June 1997},
  url = {<http://www.csl.sri.com/papers/csl-93-9/>},
}

@TECHREPORT{pvs,
  author = {Owre, S. and Shankar, N. and Rushby, J.M. and Stringer-Clavert, D.W.J.},
  title = {{PVS} Language Reference},
  institution = {Computer Science Laboratory, {SRI} International},
  year = {2001},
  month = {dec},
  publisher = {{SRI} International},
}

@BOOK{reynolds-81,
  title = {The Craft of Programming},
  publisher = {Prentice-Hall Inc.},
  year = {1981},
  author = {Reynolds, J.C.},
  address = {London},
}

@INCOLLECTION{reynolds-81a,
  author = {Reynolds, J.C.},
  title = {The essence of {ALGOL}},
  booktitle = {Algorithmic languages (Amsterdam, 1981)},
  publisher = {North-Holland},
  year = {1981},
  pages = {345--372},
  address = {Amsterdam},
  mrclass = {68B05 (01A65 68-03)},
  mrnumber = {83g:68014},
}

@ARTICLE{staples-00,
  author = {Staples, M.},
  title = {Interfaces for Refining Recursion and Procedures},
  journal = {Formal Aspect of Computing},
  year = {2000},
  volume = {12},
  pages = {372--391},
}

@INCOLLECTION{staples-99,
  author = {Staples, M.},
  title = {Representing {WP} semantics in {I}sabelle/{ZF}},
  booktitle = {Theorem proving in higher order logics (Nice, 1999)},
  publisher = {Springer},
  year = {1999},
  volume = {1690},
  series = {Lecture Notes in Comput. Sci.},
  pages = {239--254},
  address = {Berlin},
  mrclass = {68T15 (03B35 68Q60)},
}

@PHDTHESIS{staples-98,
  author = {Staples, M.},
  title = {A Mechanised Theory of Refinement},
  school = {Computer Laboratory, University of Cambridge},
  year = {1998},
  type = {{PhD} Dissertation},
  month = nov,
}

@ARTICLE{tarski-55,
  author = {Tarski, A.},
  title = {A lattice-theoretical fixpoint theorem and its applications},
  journal = {Pacific J. Math.},
  year = {1955},
  volume = {5},
  pages = {285--309},
  mrclass = {06.0X},
  mrnumber = {17,574d},
  mrreviewer = {B. J{\'o}nsson},
}

@INPROCEEDINGS{oheimb-99,
  author = {von Oheimb, D.},
  title = {Hoare Logic for Mutual Recursion and Local Variables},
  booktitle = {Foundations of Software Technology and Theoretical Computer Science},
  year = {1999},
  editor = {Pandu Rangan, C. and Raman, V. and Ramanujam, R.},
  volume = {1738},
  series = {LNCS},
  pages = {168--180},
  publisher = {Springer},
  crclassification = {D.2.4, D.3.1, F.3.1},
  crgenterms = {Languages, Verification, Theory},
  url = {\url{http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html}},
}

@INCOLLECTION{zhang-munro-harman-hu-02,
  author = {Zhang, X. and Munro, M. and Harman, M. and Hu, L. },
  title = {Weakest Precondition for General Recursive Programs Formalized in Coq},
  booktitle = {Theorem proving in higher order logics (Hampton, 2002)},
  publisher = {Springer},
  year = {2002},
  volume = {2410},
  series = {Lecture Notes in Comput. Sci.},
  pages = {332--347},
  address = {Berlin},
}


@PROCEEDINGS{icfem02,
  title = {4th International Conference on Formal Engineering Methods},
  year = {2002},
  volume = {2495},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  month = OCT,
  booktitle = {4th International Conference on Formal Engineering Methods},
}

@article{martin:curtis:rewitzky:2007,
title = "Modelling angelic and demonic nondeterminism with multirelations",
journal = "Science of Computer Programming",
volume = "65",
number = "2",
pages = "140 - 158",
year = "2007",
note = "Special Issue dedicated to selected papers from the conference of program construction 2004 (MPC 2004)",
issn = "0167-6423",
doi = "DOI: 10.1016/j.scico.2006.01.007",
url = "http://www.sciencedirect.com/science/article/pii/S0167642306002115",
author = "Martin, C. E. and Curtis, S. A and Rewitzky, I."
}

@inproceedings{hoare:moller:struth:wehrman:2009,
 author = {Hoare, C. A. and M\"{o}ller, Bernhard and Struth, Georg and Wehrman, Ian},
 title = {Concurrent Kleene Algebra},
 booktitle = {Proceedings of the 20th International Conference on Concurrency Theory},
 series = {CONCUR 2009},
 year = {2009},
 isbn = {978-3-642-04080-1},
 location = {Bologna, Italy},
 pages = {399--414},
 numpages = {16},
 url = {https://doi.org/10.1007/978-3-642-04081-8_27},
 doi = {https://doi.org/10.1007/978-3-642-04081-8_27},
 acmid = {1611740},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 

@article{dang:hofner:moller:2011,
title = "Algebraic separation logic",
journal = "Journal of Logic and Algebraic Programming",
volume = "80",
number = "6",
pages = "221 - 247",
year = "2011",
note = "Relations and Kleene Algebras in Computer Science",
issn = "1567-8326",
doi = "DOI: 10.1016/j.jlap.2011.04.003",
url = "http://www.sciencedirect.com/science/article/pii/S1567832611000142",
author = {Dang, H.-H. and H\"{o}fner, P and M\"{o}ller, B},
keywords = "Formal semantics",
keywords = "Separation logic",
keywords = "Frame rule",
keywords = "Algebra",
keywords = "Semirings",
keywords = "Quantales"
}

@article{desharnais:moller:struth:2006,
 author = {Desharnais, Jules and M\"{o}ller, Bernhard and Struth, Georg},
 title = {Kleene algebra with domain},
 journal = {ACM Trans. Comput. Logic},
 issue_date = {October 2006},
 volume = {7},
 issue = {4},
 month = {October},
 year = {2006},
 issn = {1529-3785},
 pages = {798--833},
 numpages = {36},
 url = {http://doi.acm.org/10.1145/1183278.1183285},
 doi = {http://doi.acm.org/10.1145/1183278.1183285},
 acmid = {1183285},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Idempotent semiring, Kleene algebra, codomain, domain, equational reasoning, image and preimage operation, program development and analysis, state transition systems},
} 


@BOOK{morgan-90,
  author = {Morgan, Carroll},
  title = {Programming from specifications},
  publisher = {Prentice-Hall, Inc.},
  year = {1990},
  isbn = {0-13-726225-6},
}


@article{hoare-69,
 author = {Hoare, Charles Antony Richard},
 title = {An axiomatic basis for computer programming},
 journal = {Communications of the ACM},
 volume = {12},
 number = {10},
 year = {1969},
 issn = {0001-0782},
 pages = {576--580},
 doi = {http://doi.acm.org/10.1145/363235.363259},
 publisher = {ACM Press}
 }

@inproceedings{paige,
    AUTHOR = {R.F. Paige and J.S. Ostroff and P.J. Brooke},
     TITLE = {Formalising {E}iffel Reference and Expanded Types in {PVS}},
 BOOKTITLE = {Proc. International Workshop on Aliasing, Confinement, and Ownership in Object-Oriented Programming, 
                           Darmstadt, Germany},
      YEAR = {2003},
     month = {July}
}

@incollection {ohearn-reynolds-yang,
    AUTHOR = {P. O'Hearn and J. Reynolds and H. Yang},
     TITLE = {Local reasoning about programs that alter data structures},
 BOOKTITLE = {Computer science logic (Paris, 2001)},
    SERIES = {Lecture Notes in Comput. Sci.},
    VOLUME = {2142},
     PAGES = {1--19},
 PUBLISHER = {Springer},
   ADDRESS = {Berlin},
      YEAR = {2001},
   MRCLASS = {68Q60 (68P05)},
  MRNUMBER = {2003c:68155},
}

@incollection {floyd-67,
    AUTHOR = {Floyd, R.W.},
     TITLE = {Assigning meanings to programs},
 BOOKTITLE = {Proc. Sympos. Appl. Math., Vol. XIX},
     PAGES = {19--32},
 PUBLISHER = {Amer. Math. Soc.},
   ADDRESS = {Providence, R.I.},
      YEAR = {1967},
   MRCLASS = {68.00},
  MRNUMBER = {38 \#4074},
MRREVIEWER = {M. Gross},
}

@inproceedings{meyer-03,
title={Towards Practical Proofs of Class Correctness},
author={B. Meyer},
pages={359--387},
booktitle={ZB 2003: Formal Specification and Development in Z and B,
	Lecture Notes in Computer Science},
year=2003,
volume=2651,
publisher={Springer-Verlag}
}

@Article{bijlsma,
title={Calculating with pointers},
author={A. Bijlsma},
pages={191--205},
journal={Science of Computer Programming},
year=1989,
volume=12
}

@Article{bird-01,
title={Functional Pearl: Unfolding pointer algorithms},
author={R.S. Bird},
pages={347--358},
journal={Journal of Functional Programming},
year=2001,
month={May},
volume=11,
number = 3
}

@BOOK{HOL,
  title = {Introduction to {HOL}},
  publisher = {Cambridge University Press},
  year = {1993},
  editor = {Gordon, M.J.C. and Melham, T.F.},
  address = {Cambridge},
  note = {A theorem proving environment for higher order logic, Appendix B by {R. J. Boulton}},
  isbn = {0-521-44189-7},
  mrclass = {03B35 (03B15 68T15)},
  mrnumber = {94h:03031},
  pages = {xx+471},
}

@TechReport{back-preoteasa-pointer,
  author = 	 "R. J. Back and X. Fan and V. Preoteasa",
  title = 	 "Reasoning about Pointers in Refinement Calculus",
  institution =  "TUCS - Turku Centre for Computer Science",
  year = 	 2003,
  number =	 "543",
  month =	 "June",
  url =		 "http://www.tucs.fi/Publications/Search/search.php"
}


@Article{moller,
title={Towards pointer algebra},
author={M\"{o}ller, B.},
pages={57--90},
journal={Science of Computer Programming},
year=1993,
volume=21,
month={August},
number=1
}

@Article{mason,
title={verification of programs that destructively manipulate data},
author={I. A. Mason},
pages={177--210},
journal={Science of Computer Programming},
year=1988,
volume=10,
month={April},
number=2
}

@inproceedings{bornat,
title={Proving pointer programs in {Hoare} Logic},
author={Bornat, R.},
booktitle={Mathematics of Program Construction},
year=2000,
publisher={Springer-Verlag}
}

@inproceedings{reynolds-00,
title={Intuitionistic reasoning about shared mutable data structure},
author={J. Reynolds},
booktitle={Millenial Perspectives in Computer Science},
year=2000
}

@inproceedings{reynolds-02,
title={Separation Logic: A Logic for Shared Mutable Data Structures },
author={Reynolds, J.},
booktitle={17th Annual IEEE Symposium on Logic in Computer Science},
month={July },
year=2002,
publisher={IEEE}
}

@inproceedings{morris-82,
title={A general axiom of assignment, Assignment and linked data stuctures,
A proof of the {S}chorr-{W}aite algorithm},
author={Morris, J.M.},
editors={M. Broy and G. Schmidt},
booktitle={Theoretical Foundations of Programming Methodology,
Proceedings of the 1981 Marktoberdorf Summer School},
year=1982,
pages={25--51},
publisher={D. Reidel Publishing Company}
}


@inproceedings{ishtiaq-hearn,
 author = {S.S. Ishtiaq and P.W. O'Hearn},
 title = {BI as an assertion language for mutable data structures},
 booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {2001},
 isbn = {1-58113-336-7},
 pages = {14--26},
 location = {London, United Kingdom},
 doi = {http://doi.acm.org/10.1145/360204.375719},
 publisher = {ACM Press},
 }

@inproceedings{calcagno,
title={Semantic analysis of pointer aliasing, allocation and disposal in {H}oare logic},
author={C. Calcagno and S. Ishtiaq and P.W. O'Hearn},
booktitle={ACM-SIGPLAN 2nd International Conference on Principles and practice of Declarative Programming (PPDP 2000)},
month={September},
year=2000,
publisher={ACM Press}
}

@Article{butler,
title={Calculational derivation of pointer algorithms from tree operations},
author={M. Butler},
pages={221--260},
journal={Science of Computer Programming},
year=1999,
volume=33,
number=3,
}

@Article{burstall-72,
title={Some techniques for proving correctness of programs which alter data structures},
author={R. M. Burstall},
pages={23--50},
journal={Machine Intelligence},
year=1972,
volume=7,
publisher={American Elsevier}
}

@article {back-wright-99,
    AUTHOR = {Back, Ralph-Joakim and von Wright, Joakim},
     TITLE = {Reasoning algebraically about loops},
   JOURNAL = {Acta Inform.},
  FJOURNAL = {Acta Informatica},
    VOLUME = {36},
      YEAR = {1999},
    NUMBER = {4},
     PAGES = {295--334},
      ISSN = {0001-5903},
     CODEN = {AINFA2},
   MRCLASS = {68Q60},
  MRNUMBER = {2001d:68146},
}

@article{luckham-suzuki-79,
 author = {D.C. Luckham and N. Suzuki},
 title = {Verification of Array, Record, and Pointer Operations in {P}ascal},
 journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
 volume = {1},
 number = {2},
 year = {1979},
 issn = {0164-0925},
 pages = {226--244},
 doi = {http://doi.acm.org/10.1145/357073.357078},
 publisher = {ACM Press},
 }





