Predicate Abstraction in a Program Logic Calculus

DOI10.1007/978-3-642-00255-7_10zbMath1211.68257OpenAlexW2162713269MaRDI QIDQ3605465

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

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

Related Items (4)

Precise quantitative information flow analysis -- a symbolic approach ⋮ Predicate abstraction in a program logic calculus ⋮ Interleaving Symbolic Execution and Partial Evaluation ⋮ Abstract Interpretation of Symbolic Execution with Explicit State Updates

Uses Software

• JML
• SIMPLIFY
• Boogie

Cites Work

• Unnamed Item
• Unnamed Item
• Simplify: a theorem prover for program checking
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Dynamic Logic with Non-rigid Functions
• Predicate abstraction for software verification
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Programming Languages and Systems
• An axiomatic basis for computer programming

This page was built for publication: Predicate Abstraction in a Program Logic Calculus