Discovering non-terminating inputs for multi-path polynomial programs
From MaRDI portal
Publication:2341594
DOI10.1007/s11424-014-2145-6zbMath1327.68080MaRDI QIDQ2341594
Naijun Zhan, Jiang Liu, Ming Xu, Heng-Jun Zhao
Publication date: 27 April 2015
Published in: Journal of Systems Science and Complexity (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s11424-014-2145-6
68W30: Symbolic computation and algebraic computation
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Recent advances in program verification through computer algebra
- Symbolic decision procedure for termination of linear programs
- Termination of linear programs with nonlinear constraints
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- An algorithm for isolating the real solutions of semi-algebraic systems
- Symbolic termination analysis of solvable loops
- Computing polynomial program invariants
- Generating all polynomial invariants in simple loops
- Finding positively invariant sets of a class of nonlinear loops via curve fitting
- TERMINATION ANALYSIS OF LINEAR LOOPS
- Proving non-termination
- Non-linear loop invariant generation using Gröbner bases
- Proving Conditional Termination
- Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
- Alternation for Termination
- Membership in polynomial ideals over Q is exponential space complete
- Computer Aided Verification
- Reasoning Algebraically About P-Solvable Loops
- Non-termination Checking for Imperative Programs
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Termination of Integer Linear Programs
- Verification, Model Checking, and Abstract Interpretation
