Zobrazeno 1 - 10
of 12
pro vyhledávání: '"Henrich Lauko"'
Publikováno v:
Applied Sciences, Vol 10, Iss 21, p 7853 (2020)
Data type abstraction plays a crucial role in software verification. In this paper, we introduce a domain for abstracting strings in the C programming language, where strings are managed as null-terminated arrays of characters. The new domain M-Strin
Externí odkaz:
https://doaj.org/article/c9434aff104c4086b2194398fdfb9cc0
Publikováno v:
ACM Transactions on Software Engineering and Methodology. 31:1-27
Most C and C++ programs use dynamically allocated memory (often known as a heap) to store and organize their data. In practice, it can be useful to compare addresses of different heap objects, for instance, to store them in a binary search tree or a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f50a5760b5b467301d7d8e519385c11f
https://doi.org/10.1145/3508363
https://doi.org/10.1145/3508363
Autor:
Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko
Publikováno v:
Computer Aided Verification ISBN: 9783031131875
Spot is a C++17 library for LTL and $$\omega $$ ω -automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to su
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3a1228d6feac1ee58f07fcae262b8634
https://doi.org/10.1007/978-3-031-13188-2_9
https://doi.org/10.1007/978-3-031-13188-2_9
Autor:
Henrich Lauko, Petr Ročkai
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995263
lart–llvmabstraction and refinement tool – originates from thedivinemodel-checker [5, 7], in which it was employed as an abstraction toolchain for thellvminterpreter. In this contribution, we present a stand-alone tool that does not need a verifi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::95298369bc04dfae9d5240b35c79951a
https://doi.org/10.1007/978-3-030-99527-0_31
https://doi.org/10.1007/978-3-030-99527-0_31
Publikováno v:
QRS
In this paper, we present a combination of existing and new tools that together make it possible to apply formal verification methods to programs in the form of x86_64 machine code. Our approach first uses a decompilation tool (remill) to extract low
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::24ad4726de474a38f92769ed9ff6de63
https://doi.org/10.1109/qrs51102.2020.00044
https://doi.org/10.1109/qrs51102.2020.00044
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030175016
TACAS (3)
TACAS (3)
DIVINE is an LLVM-based verification tool focusing on 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
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::08c4905f60a1e99c2fbdcffd33c33391
https://doi.org/10.1007/978-3-030-17502-3_14
https://doi.org/10.1007/978-3-030-17502-3_14
Publikováno v:
Model Checking Software ISBN: 9783030309220
SPIN
SPIN
Automatic abstraction is a powerful software verification technique. In this paper, we elaborate an abstract domain for C strings, that is, null-terminated arrays of characters. We describe the abstract semantics of basic string operations and prove
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0d4171c01f673b9a9f926deb5ff75339
http://hdl.handle.net/10278/3721099
http://hdl.handle.net/10278/3721099
Publikováno v:
Theoretical Aspects of Computing – ICTAC 2018 ISBN: 9783030025076
ICTAC
ICTAC
Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practic
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::72d4114bfcf9107f82a4fe4f87f5738d
https://doi.org/10.1007/978-3-030-02508-3_17
https://doi.org/10.1007/978-3-030-02508-3_17
Autor:
Vladimír Štill, Henrich Lauko, Tadeáš Kučera, Jan Mrázek, Katarína Kejstová, Jiří Barnat, Zuzana Baranová, Petr Ročkai
Publikováno v:
Automated Technology for Verification and Analysis ISBN: 9783319681665
ATVA
ATVA
The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a se
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e38caa8939551ac15fd3bf342d5a7982
https://doi.org/10.1007/978-3-319-68167-2_14
https://doi.org/10.1007/978-3-319-68167-2_14
Publikováno v:
Model Checking Software ISBN: 9783319325811
SPIN
SPIN
We present SymDIVINE: a tool for bit-precise model checking of parallel C and C++ programs. It builds upon LLVM compiler infrastructure, hence, it uses LLVM IR as an input formalism. Internally, SymDIVINE extends the standard explicit-state state spa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::49611876a95754f2e321566b71001ac9
https://doi.org/10.1007/978-3-319-32582-8_14
https://doi.org/10.1007/978-3-319-32582-8_14