Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs

DOI10.1007/978-3-662-46669-8_8zbMath1335.68050arXiv1410.5089OpenAlexW2161089445MaRDI QIDQ2802436

No author found.

Publication date: 26 April 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1410.5089

zbMATH Keywords

terminationnon-terminationbit-vector ranking functionsfloating-point ranking functionslexicographic ranking functions

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution ⋮ Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution ⋮ \textsc{Synbit}: synthesizing bidirectional programs using unidirectional sketches

This page was built for publication: Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs