Program verification with interacting analysis plugins

DOI10.1007/s00165-007-0029-4zbMath1125.68073OpenAlexW1972083926MaRDI QIDQ2642983

Nathaniel Charlton

Publication date: 6 September 2007

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-007-0029-4

zbMATH Keywords

Software verificationAbstractionOpen productPlugins

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• SPIN
• SIMPLIFY
• MONA
• Bebop
• Cyclone

Cites Work

• Symbolic model checking: \(10^{20}\) states and beyond
• Constructive versions of Tarski's fixed point theorems
• Combinations of abstract domains for logic programming: Open product and generic pattern construction
• Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic
• Simplify: a theorem prover for program checking
• Languages that Capture Complexity Classes
• Abstract interpretation and application to logic programs
• Lazy abstraction
• Computer Science Logic
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Static Analysis
• Foundations of Software Science and Computation Structures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Program verification with interacting analysis plugins