Conflict-driven conditional termination

DOI10.1007/978-3-319-21668-3_16zbMATH Open1381.68155OpenAlexW1025122386MaRDI QIDQ1702895FDOQ1702895

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

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

Mathematics Subject Classification ID

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

Cited In (8)

• 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
• Lifting CDCL to template-based abstract domains for program verification

Uses Software

• Apron
• Ultimate Automizer
• AProVE
• FuncTion

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)