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

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