Extended Static Checking for Haskell Export

@inproceedings{citeulike:2394381, abstract = {Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and to systems that are guarded by runtime checks. Extended static checking can reduce these costs by helping to detect bugs at compile-time, where possible. Extended static checking has been applied to objectoriented languages, like Java and C\#, but it has not been applied to a lazy functional language, like Haskell. In this paper, we describe an extended static checking tool for Haskell, named ESC/Haskell, that is based on symbolic computation and assisted by a few novel strategies. One novelty is our use of Haskell as the specification language itself for pre/post conditions. Any Haskell function (including recursive and higher order functions) can be used in our specification which allows sophisticated properties to be expressed. To perform automatic verification, we rely on a novel technique based on symbolic computation that is augmented by counter-example guided unrolling. This technique can automate our verification process and be efficiently implemented.}, address = {New York, NY, USA}, author = {Xu, Dana N.}, booktitle = {Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell}, citeulike-article-id = {2394381}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1159842.1159849}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1159842.1159849}, doi = {10.1145/1159842.1159849}, isbn = {1595934898}, keywords = {haskell, static-checking, verification}, pages = {48--59}, posted-at = {2008-02-18 13:57:23}, priority = {2}, publisher = {ACM}, title = {Extended Static Checking for Haskell}, url = {http://dx.doi.org/10.1145/1159842.1159849}, year = {2006} }

TY - CONF ID - citeulike:2394381 L3 - citeulike-article-id:2394381 N2 - Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and to systems that are guarded by runtime checks. Extended static checking can reduce these costs by helping to detect bugs at compile-time, where possible. Extended static checking has been applied to objectoriented languages, like Java and C#, but it has not been applied to a lazy functional language, like Haskell. In this paper, we describe an extended static checking tool for Haskell, named ESC/Haskell, that is based on symbolic computation and assisted by a few novel strategies. One novelty is our use of Haskell as the specification language itself for pre/post conditions. Any Haskell function (including recursive and higher order functions) can be used in our specification which allows sophisticated properties to be expressed. To perform automatic verification, we rely on a novel technique based on symbolic computation that is augmented by counter-example guided unrolling. This technique can automate our verification process and be efficiently implemented. SN - 1595934898 AD - New York, NY, USA EP - 59 TI - Extended Static Checking for Haskell PB - ACM T2 - Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell SP - 48 KW - haskell KW - static-checking KW - verification AU - Xu, Dana PY - 2006/// UR - http://dx.doi.org/10.1145/1159842.1159849 ER -