Automated termination in model-checking modulo theories

DOI10.1142/S012905411340008XMaRDI QIDQ2841996zbMATH OpenFDO

Authors Alessandro Carioni, Silvio Ghilardi, Silvio Ranise

Publication date 30 July 2013

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1142/S012905411340008X

zbMATH Keywords

infinite state model checkingsatisfiability modulo theorieswell-quasi-orderings

Mathematics Subject Classification ID

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

Recommendations

• Automated Termination in Model Checking Modulo Theories
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Ensuring completeness of symbolic verification methods for infinite-state systems
• Computer Science Logic
• Goal-directed invariant synthesis for model checking modulo theories

Cites work

• Ordering by Divisibility in Abstract Algebras
• Verifying lossy channel systems has nonprimitive recursive complexity.
• Verifying programs with unreliable channels

Cited in

(4)

• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Automated Termination in Model Checking Modulo Theories
• Termination Modulo Combinations of Equational Theories
• scientific article; zbMATH DE number 2086510 (Why is no real title available?)

This page was built for publication: Automated termination in model-checking modulo theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2841996)