Abstract
lart – llvm abstraction and refinement tool – originates from the divine model-checker [5, 7], in which it was employed as an abstraction toolchain for the llvm interpreter. In this contribution, we present a stand-alone tool that does not need a verification backend but performs the verification natively. The core idea is to instrument abstract semantics directly into the program and compile it into a native binary that performs program analysis. This approach provides a performance gain of native execution over the interpreted analysis and allows compiler optimizations to be employed on abstracted code, further extending the analysis efficiency. Compilation-based abstraction introduces new challenges solved by lart, like domain interaction of concrete and abstract values simulation of nondeterministic runtime or constraint propagation.
This work has been partially supported by Red Hat, Inc.
Henrich Lauko: Jury member representing lart at sv-comp 2022.
Chapter PDF
Similar content being viewed by others
Keywords
References
Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis, Citeseer (1994)
Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS. Springer (2022)
Beyer, D.: Verifiers and validators of the 11th Intl. Competition on Software Verification (SV-COMP 2022). Zenodo (2022). https://doi.org/10.5281/zenodo.5959149
Holzmann, G., Najm, E., Serhrouchni, A.: Spin model checking: An introduction. STTT 2, 321–327 (03 2000). https://doi.org/10.1007/s100090050039
Lauko, H., Ročkai, P., Barnat, J.: Symbolic computation via program transformation. Theoretical Aspects of Computing – ICTAC 2018 (2018). https://doi.org/10.1007/978-3-030-02508-3_17
Poeplau, S., Francillon, A.: Symbolic execution with SymCC: Don’t interpret, compile! In: 29th USENIX Security Symposium (USENIX Security 20). pp. 181–198. USENIX Association (Aug 2020), https://www.usenix.org/conference/usenixsecurity20/presentation/poeplau
Ročkai, P., Štill, V., Černá, I., Barnat, J.: DiVM: Model Checking with LLVM and Graph Memory. Journal of Systems and Software 143, 1–13 (2018). https://doi.org/10.1016/j.jss.2018.04.026
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Lauko, H., Ročkai, P. (2022). LART: Compiled Abstract Execution. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. https://doi.org/10.1007/978-3-030-99527-0_31
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99526-3
Online ISBN: 978-3-030-99527-0
eBook Packages: Computer ScienceComputer Science (R0)