Abstraction for falsification

DOI10.1007/11513988_8MaRDI QIDQ5716599zbMATH OpenOpenAlexFDO

Authors Thomas Ball, Orna Kupferman, Greta Yorsh

Publication date 10 January 2006

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

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstraction and abstraction refinement
• Formal Methods at the Crossroads. From Panacea to Foundational Support
• Abstraction as the key for invariant verification
• Bug Hunting with False Negatives
• Abstract and model check while you prove

Cited in

(12)

• An abstraction-refinement framework for trigger querying
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• On algebra of program correctness and incorrectness
• Association of under-approximation techniques for generating tests from models
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Bug Hunting with False Negatives
• Falsifying safety properties through games on over-approximating models
• Model Checking Software
• Better Under-Approximation of Programs by Hiding Variables
• Doomed program points
• Low-level reachability analysis based on formal logic
• Model checking as program verification by abstract interpretation

This page was built for publication: Abstraction for falsification

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