ITU

Symbolic Game Semantics for Model Checking Program Families

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

View graph of relations

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.
Original languageEnglish
Title of host publicationModel Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings
EditorsDragan Bosnacki, Anton Wijs
Number of pages19
Volume9641
PublisherSpringer VS
Publication date8 Apr 2016
EditionLecture Notes in Computer Science
Pages19-37
ISBN (Electronic)978-3-319-32581-1
DOIs
Publication statusPublished - 8 Apr 2016
EventModel Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, - Eindhoven, The Netherlands, Eindhoven, Netherlands
Duration: 7 Apr 20168 Apr 2016
http://www.spin2016.info/

Conference

ConferenceModel Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016,
LocationEindhoven, The Netherlands
LandNetherlands
ByEindhoven
Periode07/04/201608/04/2016
Internetadresse
SeriesLecture Notes in Computer Science
Volume9641
ISSN0302-9743
Close

    Research areas

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

Downloads

No data available

ID: 80904169