Predicate abstraction in a program logic calculus
DOI10.1016/J.SCICO.2010.06.008zbMATH Open1221.68066OpenAlexW2142528518MaRDI QIDQ549686FDOQ549686
Authors: Benjamin Weiß 
Publication date: 18 July 2011
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.scico.2010.06.008
Recommendations
abstract interpretationformal methodstheorem provingsoftware verificationpredicate abstractioninvariant generation
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Simplify: a theorem prover for program checking
- Static Analysis
- Title not available (Why is that?)
- Title not available (Why is that?)
- An axiomatic basis for computer programming
- Abstract interpretation and application to logic programs
- Symbolic execution and program testing
- Predicate abstraction for software verification
- Dynamic Logic with Non-rigid Functions
- Title not available (Why is that?)
- Predicate Abstraction in a Program Logic Calculus
- Logical Interpretation: Static Program Analysis Using Theorem Proving
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- Programming Languages and Systems
Cited In (17)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Set abstraction - an extension of all solutions predicate in logic programming language
- Combining Predicate Abstraction with Fixpoint Approximations
- Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Necessary and Sufficient Preconditions via Eager Abstraction
- Constraint-Based Invariant Inference over Predicate Abstraction
- Predicate abstraction with minimum predicates
- Predicate Abstraction with Under-approximation Refinement
- Tools and Algorithms for the Construction and Analysis of Systems
- Collecting Semantics under Predicate Abstraction in the K Framework
- Partial-predicate logic in computer science
- Programming by predicates: a formal model for interactive synthesis
- Predicate Abstraction in a Program Logic Calculus
- Predicate abstraction with indexed predicates
Uses Software
This page was built for publication: Predicate abstraction in a program logic calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q549686)
