• DocumentCode
    3141587
  • Title

    Formal reasoning about runtime code update

  • Author

    Charlton, Nathaniel ; Horsfall, Ben ; Reus, Bernhard

  • Author_Institution
    Sch. of Inf., Univ. of Sussex, Brighton, UK
  • fYear
    2011
  • fDate
    11-16 April 2011
  • Firstpage
    134
  • Lastpage
    138
  • Abstract
    We show how dynamic software updates can be modelled using a “higher order store” programming language where procedures can be written to the heap. We then show how such updates can be proved correct with a Hoare-calculus that allows for keeping track of behavioural specifications of such stored procedures.
  • Keywords
    programming languages; software engineering; Hoare-calculus; behavioural specification; dynamic software update; formal reasoning; programming language; runtime code update; Calculus; Computer crashes; Loading; Runtime; Semantics; Servers; Software;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Data Engineering Workshops (ICDEW), 2011 IEEE 27th International Conference on
  • Conference_Location
    Hannover
  • Print_ISBN
    978-1-4244-9195-7
  • Electronic_ISBN
    978-1-4244-9194-0
  • Type

    conf

  • DOI
    10.1109/ICDEW.2011.5767624
  • Filename
    5767624
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3141587