Abstract
To (dis)prove termination of C programs, AProVE uses symbolic execution to transform the program’s LLVM code into an integer transition system, which is then analyzed by several backends. The transformation steps in AProVE and the tools in the backend only produce sub-proofs in their domains. Hence, we now developed new techniques to automatically combine the essence of these proofs. If non-termination is proved, then they yield an overall witness, which identifies a non-terminating path in the original C program.
funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - 235950644 (Project GI 274/6-2)
Chapter PDF
Similar content being viewed by others
References
AProVE: https://github.com/aprove-developers/aprove-releases/releases
AProVE Website: https://aprove.informatik.rwth-aachen.de/
Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS ’22. LNCS (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
Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV ’11. pp. 184–190. LNCS 6806 (2011), https://doi.org/10.1007/978-3-642-22110-1_16
Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: Temporal property verification. In: Proc. TACAS ’16. pp. 387–393. LNCS 9636 (2016), https://doi.org/10.1007/978-3-662-49674-9_22
Clang: https://clang.llvm.org
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proc. TACAS ’08. pp. 337–340. LNCS 4963 (2008), https://doi.org/10.1007/978-3-540-78800-3_24
Dutertre, B., de Moura, L.: System Description: Yices 1.0 (2006), https://yices.csl.sri.com/papers/yices-smtcomp06.pdf
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Proc. SAT ’03. pp. 502–518. LNCS 2919 (2003), https://doi.org/10.1007/978-3-540-24605-3_37
Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. In: Proc. FMCAD ’19. pp. 221–230 (2019), https://doi.org/10.23919/FMCAD.2019.8894271
Heizmann, M., Dietsch, D., Leike, J., Musa, B., Podelski, A.: Ultimate Automizer with array interpolation. In: Proc. TACAS ’15. pp. 455–457. LNCS 9035 (2015), https://doi.org/10.1007/978-3-662-46681-0_43
Hensel, J., Emrich, F., Frohn, F., Ströder, T., Giesl, J.: AProVE: Proving and disproving termination of memory-manipulating C programs (competition contribution). In: Proc. TACAS ’17. pp. 350–354. LNCS 10206 (2017), https://doi.org/10.1007/978-3-662-54580-5_21
Hensel, J., Giesl, J., Frohn, F., Ströder, T.: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution. Journal of Logical and Algebraic Methods in Programming 97, 105–130 (2018), https://doi.org/10.1016/j.jlamp.2018.02.004
Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proc. CGO ’04. pp. 75–88 (2004), https://doi.org/10.1109/CGO.2004.1281665
Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P., Aschermann, C.: Automatically proving termination and memory safety for programs with pointer arithmetic. J. of Aut. Reasoning 58(1), 33–65 (2017), https://doi.org/10.1007/s10817-016-9389-x
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
Hensel, J., Mensendiek, C., Giesl, J. (2022). AProVE: Non-Termination Witnesses for C Programs. 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_21
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_21
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)