Proving termination of nonlinear command sequences

DOI10.1007/s00165-012-0252-5zbMath1298.68164MaRDI QIDQ470005

Byron Cook, Zvonimir Rakamarić, Alan J. Hu, Domagoj Babić

Publication date: 11 November 2014

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-012-0252-5

zbMATH Keywords

divergence testing; nonlinear assignments; program termination; well-foundedness provers

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

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

Related Items

Polynomial interrupt timed automata: verification and expressiveness

Uses Software

• Maple
• AProVE
• CiME

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Factoring polynomials with rational coefficients
• Variance analyses from invariance analyses
• Arithmetic Strengthening for Shape Analysis
• A semantic basis for the termination analysis of logic programs
• The size-change principle for program termination
• Computer Aided Verification
• An axiomatic basis for computer programming
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Automata, Languages and Programming
• Programs with Lists Are Counter Automata
• Static Analysis
• CONCUR 2005 – Concurrency Theory
• Verification, Model Checking, and Abstract Interpretation