Proving termination of nonlinear command sequences

DOI10.1007/s00165-012-0252-5zbMath1298.68164OpenAlexW1997553387MaRDI 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 testingnonlinear assignmentsprogram terminationwell-foundedness provers

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

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

This page was built for publication: Proving termination of nonlinear command sequences