Zobrazeno 1 - 10
of 33
pro vyhledávání: '"Petr Ročkai"'
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:
Petr Ročkai, Jiří Barnat
Publikováno v:
International Journal on Software Tools for Technology Transfer. 24:493-510
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::20776c4acd54f9bcbbc944af45a2e3a2
https://doi.org/10.1007/s10009-022-00659-x
https://doi.org/10.1007/s10009-022-00659-x
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
Autor:
Petr Ročkai
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030549930
FM Workshops (1)
FM Workshops (1)
In this paper, we report on our effort to design a fast, concurrent-safe hash table and implement it in C++, correctly. It is especially the latter that is the focus of this paper: concurrent data structures are notoriously hard to implement, and C++
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5594532d506f540b98dbb622f6cfda0d
https://doi.org/10.1007/978-3-030-54994-7_5
https://doi.org/10.1007/978-3-030-54994-7_5
Autor:
Zuzana Baranová, Petr Ročkai
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030549930
FM Workshops (1)
FM Workshops (1)
Building software packages from source is a complex and highly technical process. For this reason, most software comes with build instructions which have both a human-readable and an executable component. The latter in turn requires substantial infra
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::18245057c18733d0888aca6fb3b8c480
https://doi.org/10.1007/978-3-030-54994-7_4
https://doi.org/10.1007/978-3-030-54994-7_4
Autor:
Jiří Barnat, Petr Ročkai
Publikováno v:
Formal Methods for Industrial Critical Systems ISBN: 9783030270070
FMICS
FMICS
In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level inf
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f2a6a586aeb3b57acb3623fecf2125d3
https://doi.org/10.1007/978-3-030-27008-7_8
https://doi.org/10.1007/978-3-030-27008-7_8
Publikováno v:
Software Engineering and Formal Methods ISBN: 9783030304454
SEFM
SEFM
In this paper, we describe DiOS, a lightweight model operating system which can be used to execute programs that make use of POSIX APIs. Such executions are fully reproducible: running the same program with the same inputs twice will result in two ex
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6387f6cd30f24ed2324f334b85428737
https://doi.org/10.1007/978-3-030-30446-1_18
https://doi.org/10.1007/978-3-030-30446-1_18
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