| Attributes | Values |
|---|
| rdf:type
| |
| Description
| - Tento článek zkoumá možnosti dvou pokročilých automatických prostředků (jmenovitě TVLA a PALE) pro verifikaci systémů pracujících s <i>neomezenými</i> dynamickými datovými strukturami. Uvažujeme verifikaci procedur pracujících s binárními seřazenýmistromy, kde chceme zverifikovat základní požadavky správnosti ukazatelových operací (dereference přes null atd.) a dále i požadavek úplné uspořádanosti zmíněných stromů, tj. všechny uzly levého podstromu uzlu <i>n</i> jsou menší než <i>n </i>a a všechny uzly pravého podstromu uzlu <i>n</i> jsou větší než <i>n </i>(čili nezkoumáme jen vztah uzlu a jeho následníků). Abychom byli schopni zverifikovat tuto vlastnost v TVLA, představíme nový instrumentační predikát, který je schopen tuto vlastnost u příslušné procedury zverifikovat. (cs)
- This paper investigates capabilities of two advanced state-of-the-art tools-namely Pale and TVLA-for automated formal verification of programs manipulating <i>unbounded </i>dynamic data structures. We consider verification of operations dealing with binary search trees over which we want to verify the basic correctness of pointer manipulations (no null pointer dereferences, etc.) as well as the sortedness requirement of binary search trees. Unlike in other works, we want to verify the <i>full </i>sorteddness requirement, i.e. that all nodes in the left subtree of a node <i>n </i>are smaller than <i>n</i>, and all nodes in the right subtree of <i>n </i>are bigger than <i>n </i>(and not just the relation between a node and its direct subnodes). For the needs of verifying this property in the TVLA tool, we provide a new kind of instrumentation predicate that allows one to handle such a property.
- This paper investigates capabilities of two advanced state-of-the-art tools-namely Pale and TVLA-for automated formal verification of programs manipulating <i>unbounded </i>dynamic data structures. We consider verification of operations dealing with binary search trees over which we want to verify the basic correctness of pointer manipulations (no null pointer dereferences, etc.) as well as the sortedness requirement of binary search trees. Unlike in other works, we want to verify the <i>full </i>sorteddness requirement, i.e. that all nodes in the left subtree of a node <i>n </i>are smaller than <i>n</i>, and all nodes in the right subtree of <i>n </i>are bigger than <i>n </i>(and not just the relation between a node and its direct subnodes). For the needs of verifying this property in the TVLA tool, we provide a new kind of instrumentation predicate that allows one to handle such a property. (en)
|
| Title
| - Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools
- Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools (en)
- Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools (cs)
|
| skos:prefLabel
| - Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools
- Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools (en)
- Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools (cs)
|
| skos:notation
| - RIV/00216305:26230/05:PU55729!RIV06-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(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/05:PU55729
|
| http://linked.open...riv/jazykVysledku
| |
| http://linked.open.../riv/klicovaSlova
| - automated formal verification, TVLA, PALE, full sortedness, insertBST (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
| - Proceedings of 8th International Conference ISIM'05 Information System Implementation and Modeling
|
| 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áš
- Erlebach, Pavel
|
| 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
| |
| is http://linked.open...avai/riv/vysledek
of | |
![[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)