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”

Function Summarization Modulo Theories

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F18%3A10385478" target="_blank" >RIV/00216208:11320/18:10385478 - isvavai.cz</a>

  • Result on the web

    <a href="https://doi.org/10.29007/d3bt" target="_blank" >https://doi.org/10.29007/d3bt</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.29007/d3bt" target="_blank" >10.29007/d3bt</a>

Alternative languages

  • Result language

    angličtina

  • Original language name

    Function Summarization Modulo Theories

  • Original language description

    SMT-based program verification can achieve high precision using bit-precise models or combinations of different theories. Often such approaches suffer from problems related to scalability due to the complexity of the underlying decision procedures. Precision is traded for performance by increasing the abstraction level of the model. As the level of abstraction increases, missing important details of the program model becomes problematic. In this paper we address this problem with an incremental verification approach that alternates precision of the program modules on demand. The idea is to model a program using the lightest possible (i.e., less expensive) theories that suffice to verify the desired property. To this end, we employ safe over-approximations for the program based on both function summaries and light-weight SMT theories. If during verification it turns out that the precision is too low, our approach lazily strengthens all affected summaries or the theory through an iterative refinement procedure. The resulting summarization framework provides a natural and light-weight approach for carrying information between different theories. An experimental evaluation with a bounded model checker for C on a wide range of benchmarks demonstrates that our approach scales well, often effortlessly solving instances where the state-of-the-art model checker CBMC runs out of time or memory.

  • Czech name

  • Czech description

Classification

  • Type

    D - Article in proceedings

  • CEP classification

  • OECD FORD branch

    10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Result continuities

  • Project

    <a href="/en/project/GA18-17403S" target="_blank" >GA18-17403S: Automated Incremental Verification and Debugging of Concurrent Systems</a><br>

  • Continuities

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Others

  • Publication year

    2018

  • Confidentiality

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

Data specific for result type

  • Article name in the collection

    LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning

  • ISBN

  • ISSN

    2398-7340

  • e-ISSN

    neuvedeno

  • Number of pages

    20

  • Pages from-to

    56-75

  • Publisher name

    EasyChair

  • Place of publication

    Neuveden

  • Event location

    Awassa, Ethiopia

  • Event date

    Nov 17, 2018

  • Type of event by nationality

    WRD - Celosvětová akce

  • UT code for WoS article