Verification, Model Checking, and Abstract Interpretation

DOI10.1007/11609773MaRDI QIDQ5898607zbMATH OpenOpenAlexFDO

Authors Joxan Jaffar, Andrew E. Santosa, Rǎzvan Voicu

Publication date 12 February 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11609773

Mathematics Subject Classification ID

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

Recommendations

• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
• Leaping Loops in the Presence of Abstraction
• Abstractions from proofs
• Abstract Interpretation as Automated Deduction
• Model Checking Recursive Programs with Exact Predicate Abstraction

Cited in

(5)

• Solving constrained Horn clauses using dependence-disjoint expansions
• Abstract domains for reordering CLP(RLin) programs
• Temporal verification of programs via first-order fixpoint logic
• An overview of the HFL model checking project
• Not all bugs are created equal, but robust reachability can tell the difference

Describes a project that uses

Uses Software

• KRAKATOA
• PVS

This page was built for publication: Verification, Model Checking, and Abstract Interpretation

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