Towards Complete Reasoning about Axiomatic Specifications

DOI10.1007/978-3-642-18275-4_20zbMath1317.68117OpenAlexW3136909257MaRDI QIDQ3075488

Swen Jacobs, Viktor Kuncak

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_20

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (7)

Adding decision procedures to SMT solvers using axioms with triggers ⋮ Reasoning about algebraic data types with abstractions ⋮ Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata ⋮ Defining behaviorizeable relations to enable inference in semi-automatic program synthesis ⋮ Refutation-based synthesis in SMT ⋮ Towards Complete Reasoning about Axiomatic Specifications ⋮ On invariant synthesis for parametric systems

Uses Software

• VCC

Cites Work

• Unnamed Item
• Applications of Hierarchical Reasoning in the Verification of Complex Systems
• Towards Complete Reasoning about Axiomatic Specifications
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Incremental Instance Generation in Local Reasoning
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Decision procedures for algebraic data types with abstractions
• Counterexample-guided focus
• Automated Reasoning
• Automated Deduction – CADE-20
• On Local Reasoning in Verification
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Towards Complete Reasoning about Axiomatic Specifications