Decision Procedures for Automating Termination Proofs

DOI10.1007/978-3-642-18275-4_26zbMath1317.68034MaRDI QIDQ3075496

Thomas Wies, Ruzica Piskac

Publication date: 15 February 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-18275-4_26

Mathematics Subject Classification ID

03B70: Logic in computer science

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

Uses Software

• ACL2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Simple LPO constraint solving methods
• Automating the Knuth Bendix ordering
• Ensuring termination by typability
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Linear Arithmetic with Stars
• Ordered Sets in the Calculus of Data Structures
• Incremental Instance Generation in Local Reasoning
• Proving termination with multiset orderings
• Simplification by Cooperating Decision Procedures
• Term Rewriting and All That
• The size-change principle for program termination
• Decision procedures for algebraic data types with abstractions
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Decision Procedures for Multisets with Cardinality Constraints
• On Local Reasoning in Verification
• Theorem Proving in Higher Order Logics
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation