Towards Complete Reasoning about Axiomatic Specifications

DOI10.1007/978-3-642-18275-4_20MaRDI QIDQ3075488zbMATHOpenAlexFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 3938560
• An axiomatic approach to structuring specifications
• Term Rewriting and Applications
• scientific article; zbMATH DE number 3890711
• Completeness of Proof Systems for Equational Specifications
• A complete axiomatization of a theory with feature and arity constraints
• An extended framework for specifying and reasoning about proof systems
• scientific article; zbMATH DE number 3880082
• Axiomatizing schemes and their behaviors

Cites work

• Applications of hierarchical reasoning in the verification of complex systems
• Automated Deduction – CADE-20
• Automated Reasoning
• Automated reasoning in some local exensions of ordered structures
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Computer Aided Verification
• Counterexample-guided focus
• Decision procedures for algebraic data types with abstractions
• Incremental Instance Generation in Local Reasoning
• Locality Results for Certain Extensions of Theories with Bridging Functions
• On Local Reasoning in Verification
• Towards Complete Reasoning about Axiomatic Specifications
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(13)

• scientific article; zbMATH DE number 7318985 (Why is no real title available?)
• Reasoning about algebraic data types with abstractions
• Adding decision procedures to SMT solvers using axioms with triggers
• A complete axiomatization of a theory with feature and arity constraints
• Refutation-based synthesis in SMT
• A sound and complete axiomatization of embedded cross dependencies
• What's decidable about program verification modulo axioms?
• On invariant synthesis for parametric systems
• A complete axiomatic semantics of spawning
• Towards Complete Reasoning about Axiomatic Specifications
• Term Rewriting and Applications
• Defining behaviorizeable relations to enable inference in semi-automatic program synthesis
• Decidability of verification of safety properties of spatial families of linear hybrid automata

Describes a project that uses

Uses Software

• VCC

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075488)