Predicate abstraction in a program logic calculus

DOI10.1016/J.SCICO.2010.06.008MaRDI QIDQ549686zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

abstract interpretationformal methodstheorem provingsoftware verificationpredicate abstractioninvariant generation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Predicate Abstraction in a Program Logic Calculus
• Predicate abstraction with minimum predicates
• Predicate abstraction with indexed predicates
• Predicate abstraction of ANSI-C programs using SAT
• Predicate abstraction for program verification

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 2102703 (Why is no real title available?)
• Abstract interpretation and application to logic programs
• An axiomatic basis for computer programming
• Dynamic Logic with Non-rigid Functions
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Predicate Abstraction in a Program Logic Calculus
• 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
• Static Analysis
• Symbolic execution and program testing

Cited in

(17)

• Tools and Algorithms for the Construction and Analysis of Systems
• Constraint-Based Invariant Inference over Predicate Abstraction
• Programming by predicates: a formal model for interactive synthesis
• Necessary and Sufficient Preconditions via Eager Abstraction
• scientific article; zbMATH DE number 1942465 (Why is no real title available?)
• Partial-predicate logic in computer science
• Predicate Abstraction in a Program Logic Calculus
• scientific article; zbMATH DE number 512961 (Why is no real title available?)
• Combining Predicate Abstraction with Fixpoint Approximations
• Collecting Semantics under Predicate Abstraction in the K Framework
• scientific article; zbMATH DE number 549957 (Why is no real title available?)
• Set abstraction - an extension of all solutions predicate in logic programming language
• Predicate abstraction with minimum predicates
• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate abstraction with indexed predicates
• Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL
• Predicate Abstraction with Under-approximation Refinement

Describes a project that uses

Uses Software

• JML
• SIMPLIFY
• Boogie
• KIV

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)