Program verification with interacting analysis plugins

DOI10.1007/S00165-007-0029-4MaRDI QIDQ2642983zbMATH OpenOpenAlexFDO

Authors 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

AbstractionOpen productPluginsSoftware verification

Mathematics Subject Classification ID

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

Recommendations

• Verification of Java programs with interacting analysis plugins
• Integrated approach to analysis and verification of imperative programs
• scientific article; zbMATH DE number 176727
• scientific article; zbMATH DE number 7364137
• scientific article; zbMATH DE number 4024753

Cites work

• Abstract interpretation and application to logic programs
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Combinations of abstract domains for logic programming: Open product and generic pattern construction
• Computer Aided Verification
• Computer Science Logic
• Constructive versions of Tarski's fixed point theorems
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 1614700 (Why is no real title available?)
• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1254648 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1744961 (Why is no real title available?)
• scientific article; zbMATH DE number 2102703 (Why is no real title available?)
• Languages that Capture Complexity Classes
• Lazy abstraction
• 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
• Static Analysis
• Static Analysis
• Symbolic model checking: \(10^{20}\) states and beyond
• Verification of Java programs with interacting analysis plugins
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• Verification of Java programs with interacting analysis plugins
• Quality engineering: leveraging heterogeneous information (invited talk)
• Relevance heuristics for program analysis
• A framework for combining analysis and verification
• Abstract Interpretation Plugins for Type Systems

Describes a project that uses

Uses Software

• SIMPLIFY
• MONA
• SPIN
• Bebop
• Cyclone

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2642983)