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

@incollection{citeulike:6082910, abstract = {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.}, author = {Shao, Danhua and Khurshid, Sarfraz and Perry, Dewayne}, citeulike-article-id = {6082910}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-05089-3_48}, citeulike-linkout-1 = {http://www.springerlink.com/content/t1072l3j76m35311}, doi = {10.1007/978-3-642-05089-3_48}, journal = {FM 2009: Formal Methods}, keywords = {2009, alloy, bounded\_verification, lightweight\_formal\_method, novel\_approach}, pages = {757--772}, posted-at = {2009-11-07 13:27:18}, priority = {4}, title = {An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method}, url = {http://dx.doi.org/10.1007/978-3-642-05089-3_48}, year = {2009} }

TY - CHAP ID - citeulike:6082910 L3 - citeulike-article-id:6082910 N2 - 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. JF - FM 2009: Formal Methods EP - 772 TI - An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method SP - 757 KW - 2009 KW - alloy KW - bounded_verification KW - lightweight_formal_method KW - novel_approach AU - Shao, Danhua AU - Khurshid, Sarfraz AU - Perry, Dewayne PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-05089-3_48 ER -