About: Model checking concurrent software using automated deduction of object ownership patterns     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Projekt, within Data Space : linked.opendata.cz:8890 associated with source document(s)

AttributesValues
rdf:type
rdfs:seeAlso
Description
  • Due to state space explosion, verification of concurrent software using model checking is a notoriously hard task. Correctness of concurrent software relies on adherence to certain synchronization rules established by the developers but not explicitly expressed in the program code. Such rules often describe object ownership which relates objects with rules of how to access them in the concurrent environment (e.g., a data structure is owned by a lock). On the one hand, this information might extremely useful for verification of concurrent software. On the other hand, except in very specific cases, it is unrealistic to expect developers to provide it in a form amenable to automated reasoning. In this project, we will design a method for automated deduction of object ownership patterns. Further, we will extend current on-the-fly partial-order-reduction techniques to use this information for more efficient pruning of the search space during the subsequent model checking. We will also develop a prototype implementation. (en)
  • Verifikace vícevláknového softwaru model checkingem je těžký problém, zejména kvůli explozi stavového prostoru. Správnost takového softwaru závisí na dodržení jistých synchronizačních pravidel navržených vývojáři, ale nezachycených v samotném kódu programu. Taková pravidla často popisují object ownership, který přiřazuje objektům pravidla přístupu k nim ve vícevláknovém prostředí (např. datová struktura je vlastněna zámkem). Na jedné straně by znalost této informace mohla být extrémně užitečná při verifikaci vícevláknového softwaru. Na straně druhé se mimo velmi specifické případy nedá realisticky očekávat, že vývojáři tuto informaci zachytí ve formě vhodné k automatickému zpracování. V tomto projektu navrhneme metodu pro automatickou extrakci object ownership vzorů. Dále rozšíříme stávající techniky on-the-fly partial-order-reduction o využití této informace k efektivnějšímu ořezání stavového prostoru během následného model checkingu. Součástí projektu je i prototypová implementace.
Title
  • Model checking concurrent software using automated deduction of object ownership patterns (en)
  • Model checking paralelního software s využitím automatické dedukce object ownership vzorů
skos:notation
  • GPP202/12/P180
http://linked.open...avai/cep/aktivita
http://linked.open...kovaStatniPodpora
http://linked.open...ep/celkoveNaklady
http://linked.open...datumDodatniDoRIV
http://linked.open...i/cep/druhSouteze
http://linked.open...ep/duvernostUdaju
http://linked.open.../cep/fazeProjektu
http://linked.open...ai/cep/hlavniObor
http://linked.open...hodnoceniProjektu
http://linked.open...vai/cep/kategorie
http://linked.open.../cep/klicovaSlova
  • Model checking Program verification Object ownership (en)
http://linked.open...neniPrubehuReseni
  • At the request of the applicant or GACR (not registered in the GACR system) (en)
  • Na žádost žadatele nebo GAČR (není v systému GAČR evidováno) (cs)
http://linked.open...ep/partnetrHlavni
http://linked.open...inujicichPrijemcu
http://linked.open...cep/pocetPrijemcu
http://linked.open...ocetSpoluPrijemcu
http://linked.open.../pocetVysledkuRIV
http://linked.open...enychVysledkuVRIV
http://linked.open...lneniVMinulemRoce
http://linked.open.../prideleniPodpory
http://linked.open...iciPoslednihoRoku
http://linked.open...atUdajeProjZameru
http://linked.open.../vavai/cep/soutez
http://linked.open...usZobrazovaneFaze
http://linked.open...ai/cep/typPojektu
http://linked.open...ep/ukonceniReseni
http://linked.open...ep/zahajeniReseni
http://linked.open...jektu+dodavatelem
  • Tento tříletý projekt skončil po prvním roce z důvodů ukončení pracovního poměru řešitele. Šlo o rozšíření technik verifikace vícevláknového software. Článek vedoucí k navrhovanému výzkumu řešitel publikoval se zahraničními spoluautory na prestižní konferenci CAV (2012). Jeho další publikace dokládají, že pokračuje ve výzkumu na špičkové úrovni. (cs)
  • This three-year project finished after the first year due to the end of the work contract of the grant holder. It dealt with extending the techniques used in verification of concurrent software. A paper leading to the suggested research was published by the holder with foreign co-authors at the prestigious conference CAV (2012). Further publications show continuing of his research at top level. (en)
http://linked.open...tniCyklusProjektu
is http://linked.open...vavai/riv/projekt of
is http://linked.open...vavai/cep/projekt of
Faceted Search & Find service v1.16.121 as of Mar 31 2025


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data]
OpenLink Virtuoso version 07.20.3240 as of Mar 31 2025, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 44 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2025 OpenLink Software