All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Automata and Logic for Symbolic Verification of Software

Public support

  • Provider

    Ministry of Education, Youth and Sports

  • Programme

    KONTAKT

  • Call for proposals

  • Main participants

  • Contest type

    M2 - International cooperation

  • Contract ID

    10999/2010-32

Alternative language

  • Project name in Czech

    Automaty a logiky v symbolické verifikaci software.

  • Annotation in Czech

    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.

Scientific branches

  • R&D category

    ZV - Basic research

  • CEP classification - main branch

    JC - Computer hardware and software

  • CEP - secondary branch

    IN - Informatics

  • CEP - another secondary branch

  • OECD FORD - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)

    10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)<br>20206 - Computer hardware and architecture

Completed project evaluation

  • Provider evaluation

    U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)

  • Project results evaluation

    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.

Solution timeline

  • Realization period - beginning

    Jan 1, 2010

  • Realization period - end

    Jan 31, 2011

  • Project status

    U - Finished project

  • Latest support payment

    Mar 25, 2011

Data delivery to CEP

  • Confidentiality

    S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

  • Data delivery code

    CEP12-MSM-ME-U/01:1

  • Data delivery date

    Jul 12, 2012

Finance

  • Total approved costs

    121 thou. CZK

  • Public financial support

    121 thou. CZK

  • Other public sources

    0 thou. CZK

  • Non public and foreign sources

    0 thou. CZK