Monadic Abstraction

Overview

Given a formula and a set of predicates {P1,...,Pn}, decide for each Pi, whether F and Pi is satisfiable or not.

Applications

• k-induction (in checking mulitple properties)
• Optimization Modulo Theories (for symbolic abstraction)
• Value-flow analysis (in checking mulitple properties)
• etc.? (e.g., as a sub-proceure of other algorithms)

Related Work

• Predicate abstraction
• Symbolic abstraction
• Consequence finding
• Quantifier elimination
• Forgetting
• ...