An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method
| Autor: | Dewayne E. Perry, Sarfraz Khurshid, Danhua Shao |
|---|---|
| Rok vydání: | 2009 |
| Předmět: | |
| Zdroj: | FM 2009: Formal Methods ISBN: 9783642050886 FM |
| DOI: | 10.1007/978-3-642-05089-3_48 |
| Popis: | 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's overall workload. Experimental results show that our approach provides significant speed-ups over the traditional approach. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|