A new look at the automatic synthesis of linear ranking functions

DOI10.1016/j.ic.2012.03.003zbMath1251.68073OpenAlexW2094997043MaRDI 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 analysistermination analysiscomputer-aided verification

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

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

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

This page was built for publication: A new look at the automatic synthesis of linear ranking functions