Model Checking via Gamma-CFA Export

@inproceedings{Might:2007:ModelChecking, abstract = {We present and discuss techniques for performing and improving the model-checking of higher-order, functional programs based upon abstract interpretation [4]. We use continuation-passing-style conversion to produce an abstractable state machine, and then utilize abstract garbage collection and abstract counting [9] to indirectly prune false branches in the abstract state-to-state transition graph. In the process, we generalize abstract garbage collection to conditional garbage collection; that is, we collect values which an ordinary reaching-based collector would have deemed live when it is provable that such values will never be referenced. In addition, we enhance abstract counting, and then exploit it to more precisely evaluate conditions in the abstract.}, author = {Might, Matthew and Chambers, Benjamin and Shivers, Olin}, booktitle = {Verification, Model Checking, and Abstract Interpretation}, citeulike-article-id = {4915352}, citeulike-linkout-0 = {http://matt.might.net/}, citeulike-linkout-1 = {http://dx.doi.org/10.1007/978-3-540-69738-1_4}, doi = {10.1007/978-3-540-69738-1_4}, keywords = {abstract-garbage-collection, abstract-interpretation, gamma-cfa, model-checking}, location = {Nice, France}, month = {January}, pages = {59--73}, posted-at = {2009-06-20 06:43:41}, priority = {0}, title = {Model Checking via {Gamma-CFA}}, url = {http://dx.doi.org/10.1007/978-3-540-69738-1_4}, year = {2007} }

TY - CONF ID - Might:2007:ModelChecking L3 - citeulike-article-id:4915352 N2 - We present and discuss techniques for performing and improving the model-checking of higher-order, functional programs based upon abstract interpretation [4]. We use continuation-passing-style conversion to produce an abstractable state machine, and then utilize abstract garbage collection and abstract counting [9] to indirectly prune false branches in the abstract state-to-state transition graph. In the process, we generalize abstract garbage collection to conditional garbage collection; that is, we collect values which an ordinary reaching-based collector would have deemed live when it is provable that such values will never be referenced. In addition, we enhance abstract counting, and then exploit it to more precisely evaluate conditions in the abstract. CY - Nice, France EP - 73 TI - Model Checking via {Gamma-CFA} T2 - Verification, Model Checking, and Abstract Interpretation SP - 59 KW - abstract-garbage-collection KW - abstract-interpretation KW - gamma-cfa KW - model-checking AU - Might, Matthew AU - Chambers, Benjamin AU - Shivers, Olin PY - 2007/01// UR - http://dx.doi.org/10.1007/978-3-540-69738-1_4 ER -