Predicate abstraction in a program logic calculus

DOI10.1016/j.scico.2010.06.008zbMath1221.68066OpenAlexW2142528518MaRDI QIDQ549686

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

theorem provingformal methodssoftware verificationabstract interpretationpredicate abstractioninvariant generation

Mathematics Subject Classification ID

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

Uses Software

• JML
• SIMPLIFY
• Boogie
• KIV

Cites Work

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

This page was built for publication: Predicate abstraction in a program logic calculus