Towards Complete Reasoning about Axiomatic Specifications
DOI10.1007/978-3-642-18275-4_20zbMATH Open1317.68117OpenAlexW3136909257MaRDI QIDQ3075488FDOQ3075488
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
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
Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)
Cites Work
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Towards Complete Reasoning about Axiomatic Specifications
- On Local Reasoning in Verification
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- Counterexample-guided focus
- Automated Deduction – CADE-20
- Automated reasoning in some local exensions of ordered structures
- Verification, Model Checking, and Abstract Interpretation
- Locality Results for Certain Extensions of Theories with Bridging Functions
- Verification, Model Checking, and Abstract Interpretation
- Incremental Instance Generation in Local Reasoning
- Decision procedures for algebraic data types with abstractions
- Automated Reasoning
- Applications of hierarchical reasoning in the verification of complex systems
Cited In (13)
- Title not available (Why is that?)
- Term Rewriting and Applications
- Adding decision procedures to SMT solvers using axioms with triggers
- Defining behaviorizeable relations to enable inference in semi-automatic program synthesis
- Decidability of verification of safety properties of spatial families of linear hybrid automata
- Refutation-based synthesis in SMT
- On invariant synthesis for parametric systems
- A complete axiomatization of a theory with feature and arity constraints
- A sound and complete axiomatization of embedded cross dependencies
- Reasoning about algebraic data types with abstractions
- A complete axiomatic semantics of spawning
- Towards Complete Reasoning about Axiomatic Specifications
- What's decidable about program verification modulo axioms?
Uses Software
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)
