Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement
In counterexample-guided abstraction refinement, a predicate refinement scheme is said to be complete for a given theory if it is guaranteed to eventually find predicates sufficient to prove the property, when such exist. However, existing complete methods require deciding if a proof of the counterexample’s spuriousness exists in some finite language of predicates. Such an exact finite-language-restricted predicate search is quite hard for many theories used in practice and incurs a heavy overhead. We address the issue by showing that the language restriction can be relaxed so that the refinement process is restricted to infer proofs from some finite language. We show how a proof-based refinement algorithm can be made to satisfy the relaxed requirement and be complete by restricting only the theory-level reasoning in SMT to emit restricted partial interpolants.
Thu 16 AprDisplayed time zone: Azores change
10:30 - 12:30
|A Semantics for Propositions as Sessions
|Composite Replicated Data Types
|Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement