About: Automata and Logic for Symbolic Verification of Software

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

About: Automata and Logic for Symbolic Verification of Software 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=MEB021023
Description	The scientific goal of the proposed project is to significantly advance the state of the art in the area of symbolic logic-based and automata-based verification methods for infinite-state software, namely to increase the scalability of these approaches and to broaden the area of their applicability. To achieve this goal we plan to further improve the various individual logic-based as well as automata-based techniques, but also invest a significant amount of research into approaches combining advantages of both automata as well as logics. In the research, we will in particular concentrate on verification of programs with unbounded integers, (parametrised-size) arrays, and complex dynamic linked data structures. (en) Vědeckým cílem projektu je významně přispět ke zlepšení obecnosti a škálovatelnosti současných symbolických metod verifikace nekonečně stavových programů založených na využití logik a/nebo automatů. Za tím účelem budou jednak zkoumány možnosti zlepšení jednotlivých přístupů založených na logikách nebo automatech, velká pozornost však bude věnována také možnostem kombinace výhod obou těchto přístupů. Výzkum se přitom soustředí zejména na verifikaci programů s neomezenými celočíselnými proměnnými, poli a/nebo dynamickými datovými strukturami založenými na ukazatelích.
Title	Automata and Logic for Symbolic Verification of Software (en) Automaty a logiky v symbolické verifikaci software.
skos:notation	MEB021023
http://linked.open...avai/cep/aktivita	KONTAKT
http://linked.open...kovaStatniPodpora	http://linked.opendata.cz/resource/domain/vavai/projekt/MEB021023/celkovaStatniPodpora
http://linked.open...ep/celkoveNaklady	http://linked.opendata.cz/resource/domain/vavai/projekt/MEB021023/celkoveNaklady
http://linked.open...datumDodatniDoRIV	2012-07-12 (xsd:date)
http://linked.open...i/cep/druhSouteze	M2 - Mezinárodní spolupráce podle uzavřených smluv o dvoustranné mezinárodní spolupráci ve VaV
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	91775302
http://linked.open...ai/cep/hlavniObor	JC - Počítačový hardware a software
http://linked.open...hodnoceniProjektu	U - Uspěl podle zadání, tj. byly splněny cíle a jeho předpokládané výsledky uvedené ve smlouvě / rozhodnutí o poskytnutí podpory
http://linked.open...vai/cep/kategorie	ZV - Základní výzkum
http://linked.open.../cep/klicovaSlova	formal verification; infinite-state systems; symbolic representations; automata; logics (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	0 (xsd:int)
http://linked.open.../pocetVysledkuRIV	4 (xsd:int)
http://linked.open...enychVysledkuVRIV	4 (xsd:int)
http://linked.open...lneniVMinulemRoce	2011-03-25 (xsd:date)
http://linked.open.../prideleniPodpory	http://linked.opendata.cz/resource/domain/vavai/cep/prideleniPodpory/10999%2F2010-32
http://linked.open...iciPoslednihoRoku	2011
http://linked.open...atUdajeProjZameru	2012
http://linked.open...usZobrazovaneFaze	DUU
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	2011-01-31 (xsd:date)
http://linked.open.../cep/vedlejsiObor	IN - Informatika
http://linked.open...ep/zahajeniReseni	2010-01-01 (xsd:date)
http://linked.open...jektu+dodavatelem	The project targeted basic research in the area of verification of infinite state-space systems. The results are an original method for verification of dynamic memory manipulations and methods for checking properties of counter automata. (en) Projekt se zabýval základním výzkumem v oblasti verifikace nekonečně stavových systémů. Výsledkem je nová technika pro verifikaci práce s dynamickou pamětí a nové techniky pro ověřování vlastností čítačových automatů. (cs)
http://linked.open...tniCyklusProjektu	ZKU
http://linked.open.../cep/klicoveSlovo	formal verification infinite-state systems automata symbolic representations
is http://linked.open...vavai/riv/projekt of	Forest Automata for Verification of Heap Manipulation Abstract Regular (Tree) Model Checking Forester: A Tool for Verification of Programs with Pointers Fast Acceleration of Ultimately Periodic Relations
is http://linked.open...vavai/cep/projekt of	http://linked.opendata.cz/resource/domain/vavai/cep/ucast/MEB021023/2010/orjk%3A26230 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/MEB021023/2011/orjk%3A26230 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/MEB021023/2012/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, 46 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software