Conflict-driven conditional termination

DOI10.1007/978-3-319-21668-3_16MaRDI QIDQ1702895zbMATH OpenOpenAlexFDO

Authors Vijay D'Silva, C. Urban

Publication date 1 March 2018

Full work available at URL https://doi.org/10.1007/978-3-319-21668-3_16

Mathematics Subject Classification ID

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

Recommendations

• Abstract conflict driven learning
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Proving termination through conditional termination
• SAT-based termination analysis using monotonicity constraints over the integers
• Deciding conditional termination

Cited in

(8)

• Lifting CDCL to template-based abstract domains for program verification
• Reflections on termination of linear loops
• Specifying termination in CSP
• Proving termination through conditional termination
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Abstract conflict driven learning
• Abstract interpretation as automated deduction
• Inference of ranking functions for proving temporal properties by abstract interpretation

Describes a project that uses

Uses Software

• FuncTion
• AProVE
• Ultimate Automizer
• Apron

This page was built for publication: Conflict-driven conditional termination

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