An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method

We present a novel approach to optimize scope-bounded checking programs using a relational constraint solver. Given a program and its correctness specification, the traditional approach translates a bounded code segment of the entire program into a declarative formula and uses a constraint solver to search for any correctness violations. Scalability is a key issue with such approaches since for non-trivial programs the formulas are complex and represent a heavy workload that can choke the solvers. Our insight is that bounded code segments, which can be viewed as a set of (possible) execution paths, naturally lend to incremental checking through a partitioning of the set, where each partition represents a sub-set of paths. The partitions can be checked independently, and thus the problem of scope-bounded checking for the given program reduces to several sub-problems, where each sub-problem requires the constraint solver to check a less complex formula, thereby likely reducing the solver...

• Type: Conference
• Year: 2009
• Where: FM
• Authors: Danhua Shao, Sarfraz Khurshid, Dewayne E. Perry
• Keywords: Constraint Solver, FM 2009, Natural Language Processing, Relational Constraint Solver, Scope-bounded Checking