Indexed predicate discovery for unbounded system verification

DOI10.1007/978-3-540-27813-9_11MaRDI QIDQ5312894zbMATH OpenOpenAlexFDO

Authors Shuvendu K. Lahiri, Randal E. Bryant

Publication date 25 August 2005

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

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

Mathematics Subject Classification ID

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

Recommendations

• Predicate abstraction with indexed predicates
• Verification, Model Checking, and Abstract Interpretation
• Experience with predicate abstraction
• Counter-example based predicate discovery in predicate abstraction
• A symbolic approach to predicate abstraction.

Cited in

(15)

• Approximated parameterized verification of infinite-state processes with global conditions
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Specification and verification of concurrent programs through refinements
• Predicate abstraction for program verification
• Model checking parameterized systems
• Abstraction Refinement for Quantified Array Assertions
• Verifying Reference Counting Implementations
• Counter-example based predicate discovery in predicate abstraction
• An extension of lazy abstraction with interpolation for programs with arrays
• Multi-parameterised compositional verification of safety properties
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Handling Parameterized Systems with Non-atomic Global Conditions
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Monotonic Abstraction in Action
• Verification, Model Checking, and Abstract Interpretation

Describes a project that uses

Uses Software

• Cadence SMV

This page was built for publication: Indexed predicate discovery for unbounded system verification

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