Linear Ranking for Linear Lasso Programs

DOI10.1007/978-3-319-02444-8_26zbMath1410.68086arXiv1401.5347OpenAlexW1542502949MaRDI QIDQ5166700

Matthias Heizmann, Jochen Hoenicke, Jan Leike, Andreas Podelski

Publication date: 8 July 2014

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Related Items

Automatically proving termination and memory safety for programs with pointer arithmetic, Combining Model Checking and Data-Flow Analysis, Termination of Single-Path Polynomial Loop Programs, Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution, Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution, When Is a Formula a Loop Invariant?, Automated Program Verification, Synthesizing ranking functions for loop programs via SVM, Ranking Functions for Linear-Constraint Loops