Synthesizing ranking functions for loop programs via SVM

DOI10.1016/j.tcs.2022.07.002OpenAlexW4285097223MaRDI QIDQ2084940

Yi Li, Xie Li, Xuechao Sun, Yong Li, Andrea Turrini, Li-jun Zhang

Publication date: 14 October 2022

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2022.07.002

zbMATH Keywords

program analysisterminationsupport vector machinemulti-phase ranking functionnested ranking function

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• z3
• CPAchecker
• iRankFinder

Cites Work

• Unnamed Item
• Unnamed Item
• Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
• Some efficient solutions to the affine scheduling problem. I: One- dimensional time
• Support-vector networks
• On multiphase-linear ranking functions
• Termination of polynomial loops
• Geometric nontermination arguments
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Linear Ranking for Linear Lasso Programs
• Ranking Templates for Linear Loops
• Ranking Functions for Linear-Constraint Loops
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Automata, Languages and Programming
• On Computable Numbers, with an Application to the Entscheidungsproblem
• On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
• Verification, Model Checking, and Abstract Interpretation