Extending DIVINE with Symbolic Verification Using SMT
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Extending DIVINE with Symbolic Verification Using SMT
Original language description
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.
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-02177S" target="_blank" >GA18-02177S: Abstraction and Other Techniques in Semi-Symbolic Program Verification</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2019
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
Tools and Algorithms for the Construction and Analysis of Systems
ISBN
9783030175016
ISSN
0302-9743
e-ISSN
—
Number of pages
5
Pages from-to
204-208
Publisher name
Springer International Publishing
Place of publication
Cham
Event location
Praha
Event date
Jan 1, 2019
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000681183400014