SAT-based termination analysis using monotonicity constraints over the integers

DOI10.1017/S1471068411000147zbMath1222.68071arXiv1107.5980OpenAlexW2018610026MaRDI QIDQ3087439

Jürgen Giesl, Carsten Fuhs, Michael Codish, Igor Gonopolskiy, Amir M. Ben-Amram

Publication date: 16 August 2011

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1107.5980

zbMATH Keywords

SAT encodingmonotonicity constraintstermination analysis

Mathematics Subject Classification ID

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

Related Items (1)

Analyzing Innermost Runtime Complexity Through Tuple Interpretations

Uses Software

• Sat4j

Cites Work

• Proving Termination of Integer Term Rewriting

This page was built for publication: SAT-based termination analysis using monotonicity constraints over the integers