Inter-program properties

Andrei Voronkov, Iman Narasamdya

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Abstract

    We develop foundations for proving properties relating two programs. Our formalization is based on a suitably adapted notion of program invariant for a single program. First, we give an abstract formulation of the theory of program invariants based on the notion of assertion function: a function that assigns assertions to program points. Then, we develop this abstract notion further so that it can be used to prove properties between two programs. We describe an application of the theory to proving program properties in translation validation. © 2009 Springer.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    PublisherSpringer Nature
    Pages343-359
    Number of pages16
    Volume5673
    ISBN (Print)3642032362, 9783642032363
    DOIs
    Publication statusPublished - 2009
    Event16th International Symposium on Static Analysis, SAS 2009 - Los Angeles, CA
    Duration: 1 Jul 2009 → …
    http://dblp.uni-trier.de/db/conf/sas/sas2009.html#VoronkovN09http://dblp.uni-trier.de/rec/bibtex/conf/sas/VoronkovN09.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/sas/VoronkovN09

    Publication series

    NameLecture Notes in Computer Science

    Conference

    Conference16th International Symposium on Static Analysis, SAS 2009
    CityLos Angeles, CA
    Period1/07/09 → …
    Internet address

    Keywords

    • Assertion function
    • Invariant
    • Translation validation

    Fingerprint

    Dive into the research topics of 'Inter-program properties'. Together they form a unique fingerprint.

    Cite this