Extracting Zing Models from C Source Code

Autor:	Tomas Matousek, Filip Zavoral
Rok vydání:	2007
Předmět:	Model checking Focus (computing) Source code Kernel (image processing) Programming language Computer science media_common.quotation_subject Synchronization (computer science) computer.software_genre Representation (mathematics) computer Extractor media_common
Zdroj:	Lecture Notes in Computer Science ISBN: 9783540695066 SOFSEM (1)
DOI:	10.1007/978-3-540-69507-3_78
Popis:	In the paper, we propose an approach to an automatic extraction of verification models for the C language source code. We primarily focus on the representation of pointers and arrays, which make the extraction from the C language specific. We provide an implementation of the model extractor as a part of our broader effort to develop a verifier of Windows kernel drivers based on the Zing model checker. To demonstrate the feasibility of our approach, we give examples of the extraction results on a practical synchronization problem.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::aac1da43183278646987516e89e3ef0c https://doi.org/10.1007/978-3-540-69507-3_78 Zobrazit plný text záznamu