Extending DIVINE with Symbolic Verification Using SMT

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F19%3A00107528" target="_blank" >RIV/00216224:14330/19:00107528 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-17502-3_14" target="_blank" >https://doi.org/10.1007/978-3-030-17502-3_14</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-17502-3_14" target="_blank" >10.1007/978-3-030-17502-3_14</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Extending DIVINE with Symbolic Verification Using SMT

Popis výsledku v původním jazyce

DIVINE is an LLVM-based verification tool focusing on the analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for the representation of input data.

Název v anglickém jazyce

Extending DIVINE with Symbolic Verification Using SMT

Popis výsledku anglicky

DIVINE is an LLVM-based verification tool focusing on the analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for the representation of input data.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/GA18-02177S" target="_blank" >GA18-02177S: Abstrakce a jiné techniky v semi-symbolické verifikaci programů</a><br>

Návaznosti

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

Rok uplatnění

2019

Kód důvěrnosti údajů

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

Název statě ve sborníku

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

9783030175016

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

5

Strana od-do

204-208

Název nakladatele

Springer International Publishing

Místo vydání

Cham

Místo konání akce

Praha

Datum konání akce

1. 1. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000681183400014