@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/B75H1-4XYHXFB-B/2/27ba4be3ad580ef9b5a8b4a20a42d8ca",
author = "Viorel Preoteasa and Ralph-Johan Back",
keywords = "Invariant based programming",
keywords = "Data refinement",
keywords = "Mechanical verification"
}

@inproceedings{nipkow:2002,
 author = {Tobias Nipkow},
 title = {Hoare Logics for Recursive Procedures and Unbounded Nondeterminism},
 booktitle = {CSL '02: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic},
 year = {2002},
 isbn = {3-540-44240-5},
 pages = {103--119},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }


@article{schorr:waite:1967,
 author = {H. Schorr and W. M. Waite},
 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 = {Donald E. Knuth},
 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},
 }

@techreport{back:preoteasa:2008,
author="Ralph-Johan Back and Viorel Preoteasa",
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}"
}

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

@INPROCEEDINGS{Back83:invariants,
  author = {Ralph-Johan Back},
  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 = {Ralph-Johan Back},
  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},
}

@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{back:vonwright:2000,
 author = {Back, R. J. and von Wright, J.},
 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},
 }

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

@article {back-81a,
    AUTHOR = {Back, R. J.},
     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{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{back-1980,
  title = {Correctness preserving program refinements: proof theory and applications},
  publisher = {Mathematisch Centrum},
  year = {1980},
  author = {Back, R. J.},
  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, R. J.},
  title = {On the correctness of refinement in program development},
  school = {Department of Computer Science, University of Helsinki},
  year = {1978},
  type = {{PhD} thesis},
}

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