Inter-program properties

Andrei Voronkov, Iman Narasamdya

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


    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
    Number of pages16
    ISBN (Print)3642032362, 9783642032363
    Publication statusPublished - 2009
    Event16th International Symposium on Static Analysis, SAS 2009 - Los Angeles, CA
    Duration: 1 Jul 2009 → …

    Publication series

    NameLecture Notes in Computer Science


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


    • Assertion function
    • Invariant
    • Translation validation


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

    Cite this