| Attributes | Values |
|---|
| rdf:type
| |
| Description
| - We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case stud
- We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case stud (en)
- Článek se zabývá verifikací programů pracujících s dynamickými datovými strukturami. Každý uzel může obsahovat několik ukazatelů na následující uzly a datovou hodnotu z konečné množiny datových hodnot. Kontrolujeme zakázané manipulace s nulovými a nedefinovanými ukazateli, a dále i tvarové vlastnosti (shape properties) datové struktury. Pro specifikaci těchto vlastností používáme fragment first-order logiky nad grafy. Zakázané stavy popsané v této logice lze automaticky převést do C programu, který je přidán na konec verifikovaného programu. Tímto převedeme problem kontroly datové struktury na problem dosažitelnosti dané řádky v programu. Konfigurace programu, které jsou orientovanými grafy kódujeme jako rozšířené stromové automaty, a příkazy programu jako stromové převodníky. Poté můžeme využít metodu abstract regular tree model checking pro automatickou verifikaci těchto programů. Kompletní metoda byla implementována v prototy (cs)
|
| Title
| - Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
- Verifikace komplexních dynamických datových struktur za použitím abstraktního regulárního stromového model checkingu (cs)
- Abstract Regular Tree Model Checking of Complex Dynamic Data Structures (en)
|
| skos:prefLabel
| - Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
- Verifikace komplexních dynamických datových struktur za použitím abstraktního regulárního stromového model checkingu (cs)
- Abstract Regular Tree Model Checking of Complex Dynamic Data Structures (en)
|
| skos:notation
| - RIV/00216305:26230/06:PU66952!RIV07-GA0-26230___
|
| http://linked.open.../vavai/riv/strany
| |
| http://linked.open...avai/riv/aktivita
| |
| http://linked.open...avai/riv/aktivity
| - P(GA102/04/0780), P(GD102/05/H050), P(GP102/03/D211)
|
| http://linked.open...vai/riv/dodaniDat
| |
| http://linked.open...aciTvurceVysledku
| |
| http://linked.open.../riv/druhVysledku
| |
| http://linked.open...iv/duvernostUdaju
| |
| http://linked.open...titaPredkladatele
| |
| http://linked.open...dnocenehoVysledku
| |
| http://linked.open...ai/riv/idVysledku
| - RIV/00216305:26230/06:PU66952
|
| http://linked.open...riv/jazykVysledku
| |
| http://linked.open.../riv/klicovaSlova
| - Formal verification, symbolic verification, shape analysis, dynamic data structures, tree automata.<br> (en)
|
| http://linked.open.../riv/klicoveSlovo
| |
| http://linked.open...ontrolniKodProRIV
| |
| http://linked.open...v/mistoKonaniAkce
| |
| http://linked.open...i/riv/mistoVydani
| |
| http://linked.open...i/riv/nazevZdroje
| |
| http://linked.open...in/vavai/riv/obor
| |
| http://linked.open...ichTvurcuVysledku
| |
| http://linked.open...cetTvurcuVysledku
| |
| http://linked.open...vavai/riv/projekt
| |
| http://linked.open...UplatneniVysledku
| |
| http://linked.open...iv/tvurceVysledku
| - Vojnar, Tomáš
- Habermehl, Peter
- Rogalewicz, Adam
- Bouajjani, Ahmed
|
| http://linked.open...vavai/riv/typAkce
| |
| http://linked.open.../riv/zahajeniAkce
| |
| number of pages
| |
| http://purl.org/ne...btex#hasPublisher
| |
| https://schema.org/isbn
| |
| http://localhost/t...ganizacniJednotka
| |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)