@article{AbadiLamportRefinement,
  author = {Mart\'in Abadi and Leslie Lamport},
  title = {The Existence of Refinement Mappings},
  journal = {Journal of Theoretical Computer Science},
  year = 1991,
  volume = 82,
  number = 2,
  pages = {253--284}
}

@book{BBook,
  author = {Jean-Raymond Abrial},
  title = {The {B-Book}: Assigning Programs to Meanings},
  year = 1996,
  publisher = {Cambridge University Press}
}

@article{ClarksonSchneiderHyperproperties,
  author = {Michael Clarkson and Fred Schneider},
  title = {Hyperproperties},
  journal = {Journal of Computer Security},
  year = 2010,
  volume = 18,
  number = 6,
  pages = {1157--1210}
}

@article{DijkstraConstructive,
  author = {Edsger W.\ Dijkstra},
  title = {A Constructive Approach to the Problem of Program Correctness},
  journal = {BIT},
  year = 1968,
  volume = 8,
  number = 3,
  pages = {174--186}
}

@InProceedings{GoguenMeseguerNonInterference,
  author = {Joseph Goguen and Jos\'{e} Meseguer},
  title = {Security Policies and Security Models},
  booktitle = {Proc.\ {IEEE} Symposium on Security and Privacy},
  year = 1982,
  pages = {11--20}
}

@article{AFP_TLA,
  author = {Gudmund Grov and Stephan Merz},
  title = {A Definitional Encoding of {TLA*} in {Isabelle/HOL}},
  journal = {Archive of Formal Proofs},
  year = 2011,
  note = {\url{http://isa-afp.org/entries/TLA.shtml},
          Formal proof development},
  ISSN = {2150-914x}
}

@article{AFP-Statecharts,
  author  = {Steffen Helke and Florian Kamm\"{u}ller},
  title   = {Formalizing {Statecharts} using Hierarchical Automata},
  journal = {Archive of Formal Proofs},
  year    = 2010,
  note    = {\url{http://isa-afp.org/entries/Statecharts.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{HoareData,
  author = {C.~A.~R.~Hoare},
  title = {Proof of Correctness of Data Representations},
  journal = {Acta Informatica},
  year = 1972,
  volume = 1,
  number = 4,
  pages = {271--281}
}

@book{SystematicVDM,
  author = {Cliff Jones},
  title = {Systematic Software Development using {VDM}},
  year = 1990,
  publisher = {Prentice Hall},
  edition = {Second}
}

@InProceedings{McCulloughSpecificationsMLS,
  author = {Daryl McCullough},
  title = {Specifications for Multi-Level Security and a Hook-Up Property},
  booktitle = {Proc.\ {IEEE} Symposium on Security and Privacy},
  year = 1987,
  pages = {161--166}
}

@Article{McLeanPossibilisticProperties,
  author = {John McLean},
  title = {A General Theory of Composition
           for a Class of ``Possibilistic'' Properties},
  journal = {{IEEE} Transactions on Software Engineering},
  year = 1996,
  volume = 22,
  number = 1,
  pages = {53--67}
}

@techreport{MilnerSimulation,
  author = {Robin Milner},
  title = {An Algebraic Definition of Simulation between Programs},
  institution = {Stanford University},
  year = 1971,
  type = {Technical Report},
  number = {CS-205}
}

@book{RefinementCalculus,
  author = {Carroll Morgan},
  title = {Programming from Specifications},
  year = 1998,
  publisher = {Prentice Hall},
  edition = {Second}
}

@book{ZReference,
  author = {J.~M.~Spivey},
  title = {The {Z} Notation: A Reference Manual},
  year = 1992,
  publisher = {Prentice Hall},
  edition = {Second}
}

@article{WirthRefinement,
  author = {Niklaus Wirth},
  title = {Program Development by Stepwise Refinement},
  journal = {Communications of the ACM},
  year = 1971,
  volume = 14,
  number = 4,
  pages = {221--227}
}

@inproceedings{SmithMarktoberdorf,
  author = {Douglas R.\ Smith},
  title = {Mechanizing the Development of Software},
  booktitle = {Calculational System Design,
               Proc.\ Marktoberdorf Summer School},
  year = 1999,
  editor = {Manfred Broy},
  publisher = {IOS Press}
}

@misc{SpecwareWebSite,
  author = {{Kestrel Institute}},
  title = {{Specware}},
  note = {\url{http://www.specware.org}}
}

@misc{LambertPrivate,
  author = {Lambert Meertens},
  title = {Private communication},
  year = 2012
}
