skip to main content
10.1145/1159842.1159849acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
Article

Extended static checking for haskell

Published: 17 September 2006 Publication History

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.

References

[1]
Lennart Augustsson. Cayenne - language with dependent types. In ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pages 239--250, New York, NY, USA, 1998. ACM Press.
[2]
Thomas Ball and Sriram K. Rajamani. The SLAMproject: debugging system software via static analysis. In POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 1--3, New York, NY, USA, 2002. ACM Press.
[3]
Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. CASSIS, LNCS 3362, 2004.
[4]
Koen Claessen and John Hughes. Specification-based testing with QuickCheck, volume Fun of Programming of Cornerstones of Computing, chapter 2, pages 17--40. Palgrave, March 2003.
[5]
David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365--473, 2005.
[6]
Peter Dybjer, Qiao Haiyan, and Makoto Takeyama. Verifying Haskell programs by combining testing and proving. In Proceedings of Third International Conference on Quality Software, pages 272--279. IEEE Press, 2003.
[7]
Robert Bruce Findler and Matthias Felleisen. Contracts for higherorder functions. In ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pages 48--59, New York, NY, USA, 2002. ACM Press.
[8]
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pages 234--245, New York, NY, USA, 2002. ACM Press.
[9]
Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 193--205, New York, NY, USA, 2001. ACM Press.
[10]
Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Counterexample-guided control. Automata, Languages and Programming: 30th International Colloquium, (ICALP03), 2719:886--902, 2003.
[11]
Ralf Hinze, Johan Jeuring, and Andres Löh. Typed contracts for functional programming. In FLOPS '06: Functional and Logic Programming: 8th International Symposium, pages 208--225, 2006.
[12]
Kohei Honda and Nobuko Yoshida. A compositional logic for polymorphic higher-order functions. In PPDP '04: Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 191--202, New York, NY, USA, 2004. ACM Press.
[13]
James Hook, Mark Jones, Richard Kieburtz, John Matthews, Peter White, Thomas Hallgren, and Iavor Diatchki. Programatica. http://www.cse.ogi.edu/PacSoft/projects/programatica/bodynew.htm, 2005.
[14]
K. Rustan M. Leino and Greg Nelson. An extended static checker for Modular-3. In CC '98: Proceedings of the 7th International Conference on Compiler Construction, pages 302--305, London, UK, 1998. Springer-Verlag.
[15]
Neil Mitchell and Colin Runciman. Unfailing Haskell: A static checker for pattern matching. In TFP '05: The 6th Symposium on Trends in Functional Programming, pages 313--328, 2005.
[16]
Andrew Moran and David Sands. Improvement in a lazy context: an operational theory for call-by-need. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 43--56, New York, NY, USA, 1999. ACM Press.
[17]
Simon L. Peyton Jones. Compiling Haskell by program transformation: A report from the trenches. In Proc European Symposium on Programming (ESOP), pages 18--44, 1996.
[18]
Tim Sheard. Languages of the future. In OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pages 116--119, New York, NY, USA, 2004. ACM Press.
[19]
The GHC Team. The Glasgow Haskell Compiler User's Guide. www.haskell.org/ghc/documentation.html, 1998.
[20]
Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In POPL '99: Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages, pages 214--227, New York, NY, USA, 1999. ACM Press.
[21]
Dana N. Xu. Extended static checking for Haskell - technical report. http://www.cl.cam.ac.uk/users/nx200/research/escH-tr.ps, 2006.

Cited By

View all
  • (2019)Lazy counterfactual symbolic executionProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314618(411-424)Online publication date: 8-Jun-2019
  • (2018)Verifying Fail-Free Declarative ProgramsProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236957(1-13)Online publication date: 3-Sep-2018
  • (2015)GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and lazinessACM SIGPLAN Notices10.1145/2858949.278474850:9(424-436)Online publication date: 29-Aug-2015
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell
September 2006
131 pages
ISBN:1595934898
DOI:10.1145/1159842
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 September 2006

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. counterexample guided unrolling
  2. pre/postcondition
  3. symbolic simplification

Qualifiers

  • Article

Conference

ICFP06
Sponsor:

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)6
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2019)Lazy counterfactual symbolic executionProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314618(411-424)Online publication date: 8-Jun-2019
  • (2018)Verifying Fail-Free Declarative ProgramsProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236957(1-13)Online publication date: 3-Sep-2018
  • (2015)GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and lazinessACM SIGPLAN Notices10.1145/2858949.278474850:9(424-436)Online publication date: 29-Aug-2015
  • (2015)GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and lazinessProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784748(424-436)Online publication date: 29-Aug-2015
  • (2012)Hybrid contract checking via symbolic simplificationProceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation10.1145/2103746.2103767(107-116)Online publication date: 23-Jan-2012
  • (2012)The Design of a Practical Proof Checker for a Lazy Functional LanguageProceedings of the 2012 Conference on Trends in Functional Programming - Volume 782910.1007/978-3-642-40447-4_8(117-132)Online publication date: 12-Jun-2012
  • (2012)Contracts and specifications for functional logic programmingProceedings of the 14th international conference on Practical Aspects of Declarative Languages10.1007/978-3-642-27694-1_4(33-47)Online publication date: 23-Jan-2012
  • (2012)Integrated program verification tools in educationSoftware: Practice and Experience10.1002/spe.214343:4(403-418)Online publication date: 23-Jul-2012
  • (2011)PestProceedings of the 1st Workshop on Developing Tools as Plug-ins10.1145/1984708.1984711(5-8)Online publication date: 28-May-2011
  • (2011)Refinement types for secure implementationsACM Transactions on Programming Languages and Systems10.1145/1890028.189003133:2(1-45)Online publication date: 7-Feb-2011
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media