Linear ranking for linear lasso programs

DOI10.1007/978-3-319-02444-8_26MaRDI QIDQ5166700zbMATH OpenOpenAlexFDO

Authors 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)

Abstract: The general setting of this work is the constraint-based synthesis of termination arguments. We consider a restricted class of programs called lasso programs. The termination argument for a lasso program is a pair of a ranking function and an invariant. We present the---to the best of our knowledge---first method to synthesize termination arguments for lasso programs that uses linear arithmetic. We prove a completeness theorem. The completeness theorem establishes that, even though we use only linear (as opposed to non-linear) constraint solving, we are able to compute termination arguments in several interesting cases. The key to our method lies in a constraint transformation that replaces a disjunction by a sum.

Recommendations

• Ranking Templates for Linear Loops
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• A new look at the automatic synthesis of linear ranking functions
• Synthesis for Polynomial Lasso Programs

Cited in

(10)

• Termination of single-path polynomial loop programs
• Automated program verification
• Ranking functions for linear-constraint loops
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• Proving termination of programs with bitvector arithmetic by symbolic execution
• Automatically proving termination and memory safety for programs with pointer arithmetic
• When is a formula a loop invariant?
• Combining model checking and data-flow analysis
• Synthesizing ranking functions for loop programs via SVM
• Commutativity for concurrent program termination proofs

This page was built for publication: Linear ranking for linear lasso programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5166700)