Predicate Abstraction in a Program Logic Calculus

DOI10.1007/978-3-642-00255-7_10MaRDI QIDQ3605465zbMATH OpenOpenAlexFDO

Authors Benjamin Weiß

Publication date 24 February 2009

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-00255-7_10

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Predicate abstraction in a program logic calculus
• Predicate abstraction of rewrite theories
• scientific article; zbMATH DE number 194642
• Predicate abstraction for program verification
• scientific article; zbMATH DE number 549957
• Predicate Abstraction via Symbolic Decision Procedures
• Computer Aided Verification
• Predicate Abstraction of Programs with Non-linear Computation
• Abstract interpretation and application to logic programs

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 2102703 (Why is no real title available?)
• An axiomatic basis for computer programming
• Dynamic Logic with Non-rigid Functions
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Predicate abstraction for software verification
• Programming Languages and Systems
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Simplify: a theorem prover for program checking

Cited in

(18)

• scientific article; zbMATH DE number 1942465 (Why is no real title available?)
• scientific article; zbMATH DE number 512961 (Why is no real title available?)
• 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
• Predicate abstraction in a program logic calculus
• Precise quantitative information flow analysis -- a symbolic approach
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• scientific article; zbMATH DE number 549957 (Why is no real title available?)
• Necessary and Sufficient Preconditions via Eager Abstraction
• Constraint-Based Invariant Inference over Predicate Abstraction
• 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
• Interleaving symbolic execution and partial evaluation
• Programming by predicates: a formal model for interactive synthesis
• Predicate abstraction with indexed predicates

Describes a project that uses

Uses Software

• Boogie
• SIMPLIFY
• JML

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 Q3605465)