Hensel, Jera; Giesl, Jürgen; Frohn, Florian; Ströder, Thomas Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution. (English) Zbl 1395.68093 J. Log. Algebr. Methods Program. 97, 105-130 (2018). MSC: 68N30 68Q25 PDFBibTeX XMLCite \textit{J. Hensel} et al., J. Log. Algebr. Methods Program. 97, 105--130 (2018; Zbl 1395.68093) Full Text: DOI
Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius Automatically proving termination and memory safety for programs with pointer arithmetic. (English) Zbl 1409.68077 J. Autom. Reasoning 58, No. 1, 33-65 (2017). MSC: 68N30 68Q42 68Q60 68T15 PDFBibTeX XMLCite \textit{T. Ströder} et al., J. Autom. Reasoning 58, No. 1, 33--65 (2017; Zbl 1409.68077) Full Text: DOI Link
Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René Analyzing program termination and complexity automatically with AProVE. (English) Zbl 1409.68255 J. Autom. Reasoning 58, No. 1, 3-31 (2017). MSC: 68T15 68N15 68Q42 PDFBibTeX XMLCite \textit{J. Giesl} et al., J. Autom. Reasoning 58, No. 1, 3--31 (2017; Zbl 1409.68255) Full Text: DOI