A new look at the automatic synthesis of linear ranking functions

DOI10.1016/j.ic.2012.03.003zbMath1251.68073MaRDI QIDQ714505

Andrea Pescetti, Fred Mesnard, Enea Zaffanella, Roberto Bagnara

Publication date: 11 October 2012

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2012.03.003

zbMATH Keywords

static analysis; termination analysis; computer-aided verification

Mathematics Subject Classification ID

68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

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

Related Items

Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis, Ranking Functions for Linear-Constraint Loops, Certified abstract cost analysis, Complexity and resource bound analysis of imperative programs using difference constraints, On the Termination of Integer Loops, Termination of Single-Path Polynomial Loop Programs, Proving Termination Through Conditional Termination

Uses Software

• PPL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• Exact join detection for convex polyhedra and other numerical abstractions
• Precise widening operators for convex polyhedra
• Not necessarily closed convex polyhedra and the double description method
• Proving Conditional Termination
• Smoothed analysis of algorithms
• The 3x + 1 Problem and Its Generalizations
• A semantic basis for the termination analysis of logic programs
• Programming as a Discipline of Mathematical Nature
• Recurrence with affine level mappings is P-time decidable for CLP
• On Termination of Binary CLP Programs
• Logic Programming
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation