Symbolic Game Semantics for Model Checking Program Families

Aleksandar Dimovski

doi:10.1007/978-3-319-32582-8_2

Symbolic Game Semantics for Model Checking Program Families

Aleksandar Dimovski

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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.

Original language	English
Title of host publication	Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings
Editors	Dragan Bosnacki, Anton Wijs
Number of pages	19
Volume	9641
Publisher	Springer VS
Publication date	8 Apr 2016
Edition	Lecture Notes in Computer Science
Pages	19-37
ISBN (Electronic)	978-3-319-32581-1
DOIs	https://doi.org/10.1007/978-3-319-32582-8_2
Publication status	Published - 8 Apr 2016
Event	Model 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 2016 → 8 Apr 2016 http://www.spin2016.info/

Conference

Conference	Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016,
Location	Eindhoven, The Netherlands
Country/Territory	Netherlands
City	Eindhoven
Period	07/04/2016 → 08/04/2016
Internet address	http://www.spin2016.info/

Series	Lecture Notes in Computer Science
Volume	9641
ISSN	0302-9743

Keywords

Algorithmic Game Semantics
Symbolic Representation
Program Families
Model Checking Algorithms

Access to Document

10.1007/978-3-319-32582-8_2

SPIN_2016_paper_11Accepted author manuscript, 505 KB

Cite this

Dimovski, A. (2016). Symbolic Game Semantics for Model Checking Program Families. In D. Bosnacki, & A. Wijs (Eds.), Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings (Lecture Notes in Computer Science ed., Vol. 9641, pp. 19-37). Springer VS. https://doi.org/10.1007/978-3-319-32582-8_2

Dimovski, Aleksandar. / Symbolic Game Semantics for Model Checking Program Families. Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. editor / Dragan Bosnacki ; Anton Wijs. Vol. 9641 Lecture Notes in Computer Science. ed. Springer VS, 2016. pp. 19-37 (Lecture Notes in Computer Science, Vol. 9641).

@inproceedings{e2b3a912d2da44bab118ccc889f9192d,

title = "Symbolic Game Semantics for Model Checking Program Families",

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.",

keywords = "Algorithmic Game Semantics, Symbolic Representation, Program Families, Model Checking Algorithms, Algorithmic Game Semantics, Symbolic Representation, Program Families, Model Checking Algorithms",

author = "Aleksandar Dimovski",

year = "2016",

month = apr,

day = "8",

doi = "10.1007/978-3-319-32582-8_2",

language = "English",

volume = "9641",

series = "Lecture Notes in Computer Science",

publisher = "Springer VS",

pages = "19--37",

editor = "Dragan Bosnacki and Anton Wijs",

booktitle = "Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings",

edition = "Lecture Notes in Computer Science",

note = "Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016,, SPIN ; Conference date: 07-04-2016 Through 08-04-2016",

url = "http://www.spin2016.info/",

}

Dimovski, A 2016, Symbolic Game Semantics for Model Checking Program Families. in D Bosnacki & A Wijs (eds), Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Lecture Notes in Computer Science edn, vol. 9641, Springer VS, Lecture Notes in Computer Science, vol. 9641, pp. 19-37, Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Eindhoven, Netherlands, 07/04/2016. https://doi.org/10.1007/978-3-319-32582-8_2

Symbolic Game Semantics for Model Checking Program Families. / Dimovski, Aleksandar.
Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. ed. / Dragan Bosnacki; Anton Wijs. Vol. 9641 Lecture Notes in Computer Science. ed. Springer VS, 2016. p. 19-37 (Lecture Notes in Computer Science, Vol. 9641).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Symbolic Game Semantics for Model Checking Program Families

AU - Dimovski, Aleksandar

PY - 2016/4/8

Y1 - 2016/4/8

N2 - 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.

AB - 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.

KW - Algorithmic Game Semantics

KW - Symbolic Representation

KW - Program Families

KW - Model Checking Algorithms

KW - Algorithmic Game Semantics

KW - Symbolic Representation

KW - Program Families

KW - Model Checking Algorithms

UR - http://dx.doi.org/10.1007/978-3-319-32582-8_2

U2 - 10.1007/978-3-319-32582-8_2

DO - 10.1007/978-3-319-32582-8_2

M3 - Article in proceedings

VL - 9641

T3 - Lecture Notes in Computer Science

SP - 19

EP - 37

BT - Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings

A2 - Bosnacki, Dragan

A2 - Wijs, Anton

PB - Springer VS

T2 - Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016,

Y2 - 7 April 2016 through 8 April 2016

ER -

Dimovski A. Symbolic Game Semantics for Model Checking Program Families. In Bosnacki D, Wijs A, editors, Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Lecture Notes in Computer Science ed. Vol. 9641. Springer VS. 2016. p. 19-37. (Lecture Notes in Computer Science, Vol. 9641). doi: 10.1007/978-3-319-32582-8_2

Symbolic Game Semantics for Model Checking Program Families

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this