Symbolic Game Semantics for Model Checking Program Families

Aleksandar Dimovski

    Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

    Abstract

    Program families can produce a (potentially huge) number of related programs from a common code base. Many such programs are safety critical. However, most verification techniques are designed to work on the level of single programs, and thus are too costly to apply to the entire program family. In this paper, we propose an efficient game semantics based approach for verifying open program families, i.e. program families with free (undefined) identifiers. We use symbolic representation of algorithmic game semantics, where concrete values are replaced with symbolic ones. In this way, we can compactly represent program families with infinite integers as so-called (finite-state) featured symbolic automata. Specifically designed model checking algorithms are then employed to verify safety of all programs from a family at once and pinpoint those programs that are unsafe (respectively, safe). We present a prototype tool implementing this approach, and we illustrate it with several examples.
    OriginalsprogEngelsk
    TitelModel Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings
    RedaktørerDragan Bosnacki, Anton Wijs
    Antal sider19
    Vol/bind9641
    ForlagSpringer VS
    Publikationsdato8 apr. 2016
    UdgaveLecture Notes in Computer Science
    Sider19-37
    ISBN (Elektronisk)978-3-319-32581-1
    DOI
    StatusUdgivet - 8 apr. 2016
    BegivenhedModel Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, - Eindhoven, The Netherlands, Eindhoven, Holland
    Varighed: 7 apr. 20168 apr. 2016
    http://www.spin2016.info/

    Konference

    KonferenceModel Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016,
    LokationEindhoven, The Netherlands
    Land/OmrådeHolland
    ByEindhoven
    Periode07/04/201608/04/2016
    Internetadresse
    NavnLecture Notes in Computer Science
    Vol/bind9641
    ISSN0302-9743

    Emneord

    • Algorithmic Game Semantics
    • Symbolic Representation
    • Program Families
    • Model Checking Algorithms

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Symbolic Game Semantics for Model Checking Program Families'. Sammen danner de et unikt fingeraftryk.

    Citationsformater