About: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures Goto Sponge NotDistinct Permalink

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

Attributes	Values
rdf:type	http://linked.opendata.cz/ontology/domain/vavai/Projekt
rdfs:seeAlso	http://www.isvav.cz/projectDetail.do?rowId=GA14-11384S
Description	The project targets formal verification of infinite-state software systems. In particular, it aims at improving the degree of automation, scalability, and generality of the current approaches to formal verification of programs handling unbounded data structures, such as collections or dynamic linked data structures based on pointers, possibly storing data from unbounded domains, and/or using unbounded or parametric concurrency. As for concurrent programs, the stress will be on programs using modern synchronization means such as lockless data structures or transactional memories. To handle such programs, the project focuses on extending the current and developing new symbolic verification approaches based on automata and/or logics. When working on the project, members of the project teams will build on their deep and mutually complementary expertise with abstract regular model checking, tree and forest automata, separation logic and symbolic memory graphs, predicate abstraction over primitive data and collections, and thread modular verification of concurrent programs. (en) Projekt směřuje do oblasti formální verifikace nekonečně stavových softwarových systémů. Konkrétně se soustředí na zvýšení automatizace, škálovatelnosti a obecnosti současných metod formální verifikace programů s neomezenými datovými strukturami, jako jsou ukazatelové struktury a kolekce, obsahujícími data z případně neomezených domén a/nebo používající neomezený či parametrický paralelismus. V případě paralelních programů bude kladen důraz zejména na programy používající moderní synchronizační prostředky, jako jsou bezzámkové struktury či transakční paměti. S cílem umožnit verifikaci takových programů se projekt zaměřuje na rozvoj stávajících a návrh nových metod symbolické verifikace založených na využití automatů a logik. Při řešení projektu budou řešitelé konkrétně vycházet ze svých hlubokých a vzájemně se doplňujících zkušeností s abstraktním regulárním model checkingem, automaty nad stromy a lesy, separační logikou a symbolickými grafy paměti, predikátovou abstrakcí pro data a kolekce a vláknově modulární verifikací paralelních programů.
Title	Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures (en) Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí
skos:notation	GA14-11384S
http://linked.open...avai/cep/aktivita	Standard projects
http://linked.open...kovaStatniPodpora	http://linked.opendata.cz/resource/domain/vavai/projekt/GA14-11384S/celkovaStatniPodpora
http://linked.open...ep/celkoveNaklady	http://linked.opendata.cz/resource/domain/vavai/projekt/GA14-11384S/celkoveNaklady
http://linked.open...datumDodatniDoRIV	2015-04-23 (xsd:date)
http://linked.open...i/cep/druhSouteze	VS - Veřejná soutěž ve výzkumu a vývoji
http://linked.open...ep/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open.../cep/fazeProjektu	100791972
http://linked.open...ai/cep/hlavniObor	JC - Počítačový hardware a software
http://linked.open...vai/cep/kategorie	ZV - Základní výzkum
http://linked.open.../cep/klicovaSlova	formal verification, symbolic verification, infinite-state systems, theory of automata, logic, dynamic linked data structures, collections, parametric systems, concurrency (en)
http://linked.open...ep/partnetrHlavni	Fakulta informačních technologií
http://linked.open...inujicichPrijemcu	0 (xsd:int)
http://linked.open...cep/pocetPrijemcu	1 (xsd:int)
http://linked.open...ocetSpoluPrijemcu	1 (xsd:int)
http://linked.open.../pocetVysledkuRIV	14 (xsd:int)
http://linked.open...enychVysledkuVRIV	14 (xsd:int)
http://linked.open...lneniVMinulemRoce	2014-04-18 (xsd:date)
http://linked.open.../prideleniPodpory	http://linked.opendata.cz/resource/domain/vavai/cep/prideleniPodpory/14-11384S
http://linked.open...iciPoslednihoRoku	2015
http://linked.open...atUdajeProjZameru	2015
http://linked.open.../vavai/cep/soutez	SGA0201400001
http://linked.open...usZobrazovaneFaze	DRRVB
http://linked.open...ai/cep/typPojektu	P - Projekt výzkumu a vývoje financovaný ze státního rozpočtu
http://linked.open...ep/ukonceniReseni	2016-12-31 (xsd:date)
http://linked.open...ep/zahajeniReseni	2014-01-01 (xsd:date)
http://linked.open...tniCyklusProjektu	ZB
http://linked.open.../cep/klicoveSlovo	formal verification collections dynamic linked data structures infinite-state systems logic parametric systems symbolic verification theory of automata
is http://linked.open...vavai/riv/projekt of	HADES (Hazard Detection System) Block Me If You Can! Context-Sensitive Parameterized Verification A Decision Procedure For The WSkS Logic On Interpolants and Variable Assignments WeVerca: Web Applications Verification for PHP CPAlien: Shape Analyzer for CPAChecker Compositional Entailment Checking for a Fragment of Separation Logic Data-flow Analysis of Programs with Associative Arrays Deciding Entailments in Inductive Separation Logic with Tree Automata Predicate Abstraction in Program Verification: Survey and Current Trends Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution) Mediating for reduction (on minimizing alternating Buchi automata) SLIDE: Separation Logic with Inductive Definitions SPEN - A Solver for Separation Logic Entailments
is http://linked.open...vavai/cep/projekt of	http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA14-11384S/2014/orjk%3A11320 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA14-11384S/2014/orjk%3A26230 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA14-11384S/2015/orjk%3A11320 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA14-11384S/2015/orjk%3A26230 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA14-11384S/2016/orjk%3A11320 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA14-11384S/2016/orjk%3A26230

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 114 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software