On the linear ranking problem for simple floating-point loops

DOI10.1007/978-3-662-53413-7_15MaRDI QIDQ1664396zbMATH OpenOpenAlexFDO

Authors Fonenantsoa Maurica, Frédéric Mesnard, Étienne Payet

Publication date 27 August 2018

Full work available at URL https://hal.univ-reunion.fr/hal-01451688/file/sas16.pdf

zbMATH Keywords

termination analysisfloating-point numberslinear ranking functions

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• On the \textsc{Linear Ranking} problem for integer linear-constraint loops
• Ranking functions for linear-constraint loops
• The hardness of finding linear ranking functions for lasso programs
• Computer Aided Verification
• A new look at the automatic synthesis of linear ranking functions

Cited in

(7)

• On the \textsc{Linear Ranking} problem for integer linear-constraint loops
• Termination of floating-point computations
• Unrestricted termination and non-termination arguments for bit-vector programs
• The hardness of finding linear ranking functions for lasso programs
• Model checking linear dynamical systems under floating-point rounding
• Synthesizing ranking functions for loop programs via SVM
• Ranking Templates for Linear Loops

This page was built for publication: On the linear ranking problem for simple floating-point loops

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