Locality Results for Certain Extensions of Theories with Bridging Functions

DOI10.1007/978-3-642-02959-2_5zbMath1250.03022OpenAlexW1556480840MaRDI QIDQ5191097

Viorica Sofronie-Stokkermans

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_5

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Related Items

Modular Termination and Combinability for Superposition Modulo Counter Arithmetic, A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited, Reasoning about algebraic data types with abstractions, A Rewriting Approach to the Combination of Data Structures with Bridging Theories, Quantitative separation logic and programs with lists, Unnamed Item, Towards Complete Reasoning about Axiomatic Specifications, Politeness and combination methods for theories with bridging functions, Polite combination of algebraic datatypes, Politeness for the theory of algebraic datatypes

Uses Software

• H-PILoT

Cites Work

• Unnamed Item
• Easy intruder deduction problems with homomorphisms
• A rewriting approach to satisfiability procedures.
• Modular proof systems for partial functions with Evans equality
• Decision procedures for term algebras with integer constraints
• Rewrite-Based Decision Procedures
• An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• Challenges in the Automated Verification of Security Protocols
• Reasoning About Recursively Defined Data Structures
• Verification: Theory and Practice
• Automated Deduction – CADE-20
• On Local Reasoning in Verification
• Polynomial-time computation via local inference relations