Non-termination Checking for Imperative Programs

DOI10.1007/978-3-540-79124-9_11MaRDI QIDQ5458816zbMATH OpenOpenAlexFDO

Authors Helga Velroyen, Philipp Rümmer

Publication date 24 April 2008

Published in Tests and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-79124-9_11

Mathematics Subject Classification ID

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

Recommendations

• Proving non-termination
• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• A practical analysis of non-termination in large logic programs
• Non-termination Analysis of Logic Programs Using Types
• Syntax-guided termination analysis

Cited in

(10)

• Convergence: integrating termination and abort-freedom
• Discovering non-terminating inputs for multi-path polynomial programs
• Extended Nested Dual System Groups, Revisited
• Proving non-termination
• Proving termination through conditional termination
• A dynamic logic with traces and coinduction
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• simpA: an agent-oriented approach for programming concurrent applications on top of Java
• Local Nontermination Detection for Parallel C++ Programs
• Multiphase-linear ranking functions and their relation to recurrent sets

This page was built for publication: Non-termination Checking for Imperative Programs

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