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

@incollection{butler:divakar:2009,
year={2009},
isbn={978-3-642-03546-3},
booktitle={Contemporary Computing},
volume={40},
series={Communications in Computer and Information Science},
doi={10.1007/978-3-642-03547-0_59},
title={Verification of Liveness Properties in Distributed Systems},
url={https://doi.org/10.1007/978-3-642-03547-0_59},
publisher={Springer Berlin Heidelberg},
keywords={Formal Methods; Distributed Systems; Event-B; Liveness Properties},
author={Yadav, Divakar and Butler, Michael},
pages={625-636},
language={English}
}

@book{abrial:2010,
 author = {Abrial, Jean-Raymond},
 title = {Modeling in Event-B: System and Software Engineering},
 year = {2010},
 isbn = {0521895561, 9780521895569},
 edition = {1st},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
} 

@article{lamport:1994,
 author = {Lamport, Leslie},
 title = {The Temporal Logic of Actions},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {May 1994},
 volume = {16},
 number = {3},
 month = may,
 year = {1994},
 issn = {0164-0925},
 pages = {872--923},
 numpages = {52},
 url = {http://doi.acm.org/10.1145/177492.177726},
 doi = {10.1145/177492.177726},
 acmid = {177726},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concurrent programming, liveness properties, safety properties},
} 

@INPROCEEDINGS{Wolper81,
author={Wolper, Pierre},
booktitle={Foundations of Computer Science},
title={Temporal logic can be more expressive},
year=1981,
pages={340-348},
}

@article{SistlaVardiWolper87,
author={Sistla, Prasad and Vardi, Moshe Y. and Wolper, Pierre},
title={The complementation problem for {B}\"uchi automata with applications to temporal logic},
journal={Theoretical Computer Science},
volume=49,
year=1987,
pages={217-237},
}

@inproceedings{KestenPnueli95,
author={Kesten, Yonit and Pnueli, Amir}, 
title={{A complete proof system for QPTL}},
booktitle={LICS},
month=jun,
year= 1995,
}

@article{preoteasa:2014afp,
  author =   {Preoteasa, Viorel},
  title =    {Formalization of Refinement Calculus for Reactive Systems},
  journal =  {Archive of Formal Proofs},
  month =    Jun,
  year =     2014,
  note =     {\url{http://isa-afp.org/entries/RefinementReactive.shtml}, Formal proof development, {\em Review pending.}},
  ISSN =     {2150-914x}
}

@article{preoteasa:tripakis:2014tr,
author="Preoteasa, Viorel and Tripakis, Stavros",
title="Refinement Calculus of Reactive Systems",
year="2014",
month="Jun",
archivePrefix = "arXiv",
eprint        = "1406.6035",
primaryClass  = "abs",
note = {\url{http://arxiv.org/abs/1406.6035}},
institution={Aalto}
}

@incollection{back:butler:1995,
year={1995},
isbn={978-3-540-60117-3},
booktitle={Mathematics of Program Construction},
volume={947},
series={Lecture Notes in Computer Science},
editor={M\"oller, Bernhard},
doi={10.1007/3-540-60117-1_8},
title={Exploring summation and product operators in the refinement calculus},
url={https://doi.org/10.1007/3-540-60117-1_8},
publisher={Springer Berlin Heidelberg},
author={Back, Ralph-Johan and Butler, Michael},
pages={128-158}
}

@article{back:xu:1998,
year={1998},
issn={0001-5903},
journal={Acta Informatica},
volume={35},
number={2},
doi={10.1007/s002360050116},
title={Refinement of fair action systems},
url={https://doi.org/10.1007/s002360050116},
publisher={Springer-Verlag},
author={Back, Ralph-Johan and Xu, Qiwen},
pages={131-165},
language={English}
}

@incollection{back:1990,
year={1990},
isbn={978-3-540-52559-2},
booktitle={Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness},
doi={10.1007/3-540-52559-9_61},
title={{Refinement calculus, part II: Parallel and reactive programs}},
url={https://doi.org/10.1007/3-540-52559-9_61},
publisher={Springer},
keywords={Stepwise refinement; weakest preconditions; total correctness; parallel programs; reactive programs; refinement mappings; parallel composition; hiding; stuttering; action systems; fairness; simulation},
author={Back, Ralph-Johan},
pages={67-93}
}

@incollection{back:wright:1994,
year={1994},
isbn={978-3-540-58329-5},
booktitle={CONCUR '94: Concurrency Theory},
volume={836},
series={Lecture Notes in Computer Science},
editor={Jonsson, Bengt and Parrow, Joachim},
doi={10.1007/BFb0015020},
title={Trace refinement of action systems},
url={https://doi.org/10.1007/BFb0015020},
publisher={Springer Berlin Heidelberg},
author={Back, Ralph-Johan and Wright, Joakim},
pages={367-384}
}

@article{AlurHenzingerFMSD99,
title={Reactive Modules},
author={Alur, Rajeev and Henzinger, Thomas A.},
journal={Formal Methods in System Design},
volume=15,
pages={7-48},
year=1999,
}

@book{BroyStolen01,
 author = {Broy, Manfred and St{\o}len, Ketil},
 title = {Specification and development of interactive systems: focus on streams, interfaces, and refinement},
 year = {2001},
 publisher = {Springer},
 }

@book{Dill87,
 author = {Dill, David L.},
 title = {Trace theory for automatic hierarchical verification of speed-independent circuits},
 year = {1987},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
 }

@ARTICLE{LynchTuttle89,
    author = {Lynch, Nancy A. and Tuttle, Mark R.},
    title = {An introduction to input/output automata},
    journal = {CWI Quarterly},
    year = {1989},
    volume = {2},
    pages = {219--246}
}

@inproceedings{AlfaroHenzingerFSE01,
author={de Alfaro, Luca and Henzinger, Thomas A.},
title={Interface Automata},
booktitle={Foundations of Software Engineering (FSE)},
publisher={ACM Press},
year=2001,
}

@book{dill:1989,
 author = {Dill, David L.},
 title = {Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits},
 year = {1989},
 isbn = {0-262-04101-4},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
} 

@INPROCEEDINGS{pnueli:1977,
author={Pnueli, Amir},
booktitle={Foundations of Computer Science, 1977., 18th Annual Symposium on},
title={The temporal logic of programs},
year={1977},
month={Oct},
pages={46-57},
keywords={Clocks;Logic;Operating systems;Power system modeling;Programming profession;Real time systems;Reasoning about programs;Safety;Stress;System recovery},
doi={10.1109/SFCS.1977.32},
ISSN={0272-5428},}

@article{preoteasa:2013,
title = "Refinement algebra with dual operator ",
journal = "Science of Computer Programming ",
volume = "92, Part B",
number = "0",
pages = "179 - 210",
year = "2014",
issn = "0167-6423",
doi = "https://doi.org/10.1016/j.scico.2013.07.002",
url = "http://www.sciencedirect.com/science/article/pii/S0167642313001597",
author = "Viorel Preoteasa",
keywords = "Algebra of programming",
keywords = "Refinement algebra",
keywords = "Refinement calculus",
keywords = "Data refinement",
keywords = "Hoare logic "
}

@article{tripakis:2011,
 author = {Tripakis, Stavros and Lickly, Ben and Henzinger, Thomas A. and Lee, Edward A.},
 title = {A Theory of Synchronous Relational Interfaces},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {July 2011},
 volume = {33},
 number = {4},
 month = jul,
 year = {2011},
 issn = {0164-0925},
 pages = {14:1--14:41},
 articleno = {14},
 numpages = {41},
 url = {http://doi.acm.org/10.1145/1985342.1985345},
 doi = {10.1145/1985342.1985345},
 acmid = {1985345},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Compositionality, interfaces, refinement, substitutability},
} 

@article{desharnais:moller:struth:2011,
  author    = {Desharnais, Jules and
               M{\"o}ller, Bernhard and
               Struth, Georg},
  title     = {Algebraic Notions of Termination},
  journal   = {Logical Methods in Computer Science},
  volume    = {7},
  number    = {1},
  year      = {2011},
  ee        = {https://doi.org/10.2168/LMCS-7(1:1)2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{moller:struth:2006,
title = "Algebras of modal operators and partial correctness",
journal = "Theoretical Computer Science",
volume = "351",
number = "2",
pages = "221 - 239",
year = "2006",
issn = "0304-3975",
doi = "10.1016/j.tcs.2005.09.069",
url = "http://www.sciencedirect.com/science/article/pii/S0304397505006195",
author = "M{\"o}ller, Bernhard and Struth, Georg",
keywords = "Semirings",
keywords = "Kleene algebra",
keywords = "Modal operators",
keywords = "Partial correctness",
keywords = "Hoare logic"
}


@article{preoteasa:back:2012,
year={2012},
issn={0934-5043},
journal={Formal Aspects of Computing},
volume={24},
issue={1},
doi={10.1007/s00165-011-0195-2},
title={Invariant diagrams with data refinement},
url={https://doi.org/10.1007/s00165-011-0195-2},
publisher={Springer-Verlag},
keywords={Invariant based programming; Data refinement; Mechanical verification; Graph marking},
author={Preoteasa, Viorel and Back, Ralph-Johan},
pages={67-95},
language={English}
}


@article{kozen:1994,
title = "A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events",
journal = "Information and Computation",
volume = "110",
number = "2",
pages = "366 - 390",
year = "1994",
note = "",
issn = "0890-5401",
doi = "10.1006/inco.1994.1037",
url = "http://www.sciencedirect.com/science/article/pii/S0890540184710376",
author = "Kozen, D."
}


@article{apt:plotkin:1986,
 author = {Apt, K. R. and Plotkin, G. D.},
 title = {Countable nondeterminism and random assignment},
 journal = {J. ACM},
 issue_date = {Oct. 1986},
 volume = {33},
 number = {4},
 month = aug,
 year = {1986},
 issn = {0004-5411},
 pages = {724--767},
 numpages = {44},
 url = {http://doi.acm.org/10.1145/6490.6494},
 doi = {10.1145/6490.6494},
 acmid = {6494},
 publisher = {ACM},
 address = {New York, NY, USA},
} 



@PhdThesis{solin:thesis, 
  author = {Solin, Kim},
  title = {Abstract Algebra of Program Refinement}, 
  school = {Turku Centre for Computer Science},
  month = {Dec},
  year = {2007},
}

@book{dijkstra:1990,
 author = {Dijkstra, Edsger W. and Scholten, Carel S.},
 title = {Predicate calculus and program semantics},
 year = {1990},
 isbn = {0-387-96957-8},
 publisher = {Springer-Verlag New York, Inc.},
 address = {New York, NY, USA},
} 

@incollection{meinicke:2006,
year={2006},
isbn={978-3-540-35631-8},
booktitle={Mathematics of Program Construction},
volume={4014},
series={Lecture Notes in Computer Science},
editor={Uustalu, Tarmo},
title={Continuous Action System Refinement},
publisher={Springer Berlin Heidelberg},
author={Meinicke, Larissa and Hayes, Ian J.},
pages={316-337}
}

@inproceedings{charpentier:2000,
 author = {Charpentier, Michel and Chandy, K. Mani},
 title = {Reasoning about Composition Using Property Transformers and Their Conjugates},
 booktitle = {Proceedings of the International Conference IFIP on Theoretical Computer Science, 
         Exploring New Frontiers of Theoretical Informatics},
 series = {TCS '00},
 year = {2000},
 isbn = {3-540-67823-9},
 pages = {580--595},
 numpages = {16},
 acmid = {723336},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 

@article{solin:2012,
year={2012},
issn={0039-3215},
journal={Studia Logica},
volume={100},
issue={3},
doi={10.1007/s11225-012-9416-9},
title={Dual Choice and Iteration in an Abstract Algebra of Action},
url={https://doi.org/10.1007/s11225-012-9416-9},
publisher={Springer Netherlands},
keywords={Logic of action; Abstract algebra; Nondeterministic choice; Program refinement},
author={Solin, Kim},
pages={607-630},
language={English}
}

@article{preoteasa:2011a,
  author    = {Viorel Preoteasa},
  title     = {Algebra of Monotonic Boolean Transformers},
  journal   = {Archive of Formal Proofs},
  volume    = {2011},
  year      = {2011},
  url       = {http://isa-afp.org/entries/MonoBoolTranAlgebra.shtml},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection {preoteasa:2011,
   author = {Preoteasa, Viorel},
   affiliation = {Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5 A, 20520 Turku, Finland},
   title = {Algebra of Monotonic Boolean Transformers},
   booktitle = {Formal Methods, Foundations and Applications},
   series = {Lecture Notes in Computer Science},
   editor = {Simao, Adenilso and Morgan, Carroll},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-25031-6},
   keyword = {Computer Science},
   pages = {140-155},
   volume = {7021},
   url = {https://doi.org/10.1007/978-3-642-25032-3\_10},
   note = {10.1007/978-3-642-25032-3\_10},
   year = {2011}
}

@incollection {solin:2006,
   author = {Solin, Kim},
   affiliation = {Turku Centre for Computer Science, Lemminkäinengatan 14 A, FIN-20520 Åbo, Finland},
   title = {On Two Dually Nondeterministic Refinement Algebras},
   booktitle = {Relations and Kleene Algebra in Computer Science},
   series = {Lecture Notes in Computer Science},
   editor = {Schmidt, Renate},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-540-37873-0},
   keyword = {Computer Science},
   pages = {373-387},
   volume = {4136},
   url = {https://doi.org/10.1007/11828563\_25},
   note = {10.1007/11828563\_25},
   year = {2006}
}

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

@incollection{preoteasa:back:2010a,
  author =       {Preoteasa, Viorel and Back, Ralph-Johan},
  title =        {Semantics and Data Refinement of Invariant Based Programs },
  booktitle =    {The 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},
  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 =    {The 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},
 }


@incollection{Harel:1989:DRS:101969.101990,
 author = {Harel, David and Pnueli, Amir},
 title = {On the Development of Reactive Systems},
 booktitle = {Logics and Models of Concurrent Systems},
 editor = {Apt, Krzysztof R.},
 year = {1985},
 pages = {477--498},
} 



