Symbolic Game Semantics for Model Checking Program Families

Aleksandar Dimovski

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

Abstrakt

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

Fingeraftryk

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

Citationsformater