research-article

Language-based verification will change the world

Authors:

Stephanie WeirichAuthors Info & Claims

FoSER '10: Proceedings of the FSE/SDP workshop on Future of software engineering research

Pages 343 - 348

https://doi.org/10.1145/1882362.1882432

Published: 07 November 2010 Publication History

Abstract

We argue that lightweight, language-based verification is poised to enter mainstream industrial use, where it will have a major impact on software quality and reliability. We explain how language-based approaches based on so-called dependent types are already being adopted in functional programming languages, and why such methods will be successful for mainstream use, where traditional formal methods have failed.

References

[1]

The 7th IEEE/ACM International Conference on Autonomic Computing and Communications, Washington, D.C., 2010.

[2]

J. Andrews. General Test Result Checking with Log File Analysis. IEEE Transactions on Software Engineering, 29(7), July 2003.

Digital Library

[3]

D. Aspinall and J. Sevcík. Formalising Java's Data Race Free Guarantee. In K. Schneider and J. Brandt, editors, 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pages 22--37, 2007.

Digital Library

[4]

M. Barnett, B-Y. Chang, R. DeLine, B. Jacobs, and R. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In F. de Boer, M. Bonsangue, S. Graf, and W. de Roever, editors, Proceedings of the 21st International Symposium on Formal Methods for Components and Objects, number 4111 in Lecture Notes in Computer Science, pages 364--387. Springer-Verlag, 2008.

Digital Library

[5]

C. Barrett, M. Deters, A. Oliveras, and A. Stump. Design and Results of the 3rd Annual Satisfiability Modulo Theories competition (SMT-COMP 2007). International Journal of Artificial Intelligence Tools, 17(4):569--606, 2008.

[6]

L. Burdy, Y. Cheon, D.R. Cok, M.D. Ernst, J.R. Kiniry, G.T. Leavens, K.R.M. Leino, and E. Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT), 7(3):212--232, 2005.

Digital Library

[7]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 1999.

Digital Library

[8]

P. Cousot. The Verification Grand Challenge and Abstract Interpretation. In B. Meyer and J. Woodcock, editors, Verified Software: Theories, Tools, Experiments, Lecture Notes in Computer Science, pages 227--240. Springer, 2007.

Digital Library

[9]

E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

Digital Library

[10]

C. Flanagan. Hybrid Type Checking. In G. Morrisett and S. Peyton Jones, editors, Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 245--256, 2006.

Digital Library

[11]

S. Gulwani, S. Srivastava, and R. Venkatesan. Program analysis as constraint solving. In PLDI '08: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, pages 281--292. ACM, 2008.

Digital Library

[12]

M. Jorde, S. Elbaum, and M. Dwyer. Increasing Test Granularity by Aggregating Unit Tests. 23rd IEEE/ACM International Conference on Automated Software Engineering, 2008, pages 9--18, 2008.

Digital Library

[13]

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207--220. ACM, 2009.

Digital Library

[14]

G. Klein and T. Nipkow. Verified Bytecode Verifiers. Theoretical Computer Science, 298(3):583--626, 2003.

Digital Library

[15]

D. Le Berre and L Simon, editors. Special Issue on the SAT 2005 Competitions and Evaluations, volume 2, 2006.

[16]

X. Leroy. Formal Certification of a Compiler Back-end, or: Programming a Compiler with a Proof Assistant. In S. Peyton Jones, editor, Proceedings of the 32nd ACM Symposium on Principles of Programming Languages, pages 42--54, 2006.

Digital Library

[17]

J. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Toward a Verified Relational Database Management System. In J. Palsberg, editor, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 237-248, 2010.

Digital Library

[18]

C. March é, C. Paulin-Mohring, and X. Urbain. The Krakatoa Tool for Certification of JAVA/JAVACARD Programs Annotated in JML. Journal of Logic and Algebraic Programming, 58(1-2):89--106, 2004.

[19]

C. McBride. Epigram: Practical programming with dependent types. In V. Vene and T. Uustalu, editors, Advanced Functional Programming, 5th International School, AFP 2004, Tartu, Estonia, August 14-21, 2004, Revised Lectures, volume 3622 of Lecture Notes in Computer Science, pages 130--170. Springer, 2004.

[20]

T. Mens and T. Tourwe. A survey of software refactoring. IEEE Transactions on software engineering, 30(2):126--139, 2004.

Digital Library

[21]

B. Meyer. Eifiel*: A language and environment for software engineering. Journal of Systems and Software, 8(3):199--246, 1988.

Digital Library

[22]

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent Types for Imperative Programs. In ICFP '08: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, pages 229--240. ACM, 2008.

Digital Library

[23]

U. Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers University of Technology, 2007.

[24]

S. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple unification-based type inference for GADTs. In J. Reppy and J. Lawall, editors, International Conference on Functional Programming (ICFP), pages 50--61, 2006.

Digital Library

[25]

B. Pierce. Types and Programming Languages. The MIT Press, 2002.

Digital Library

[26]

A. Stump, Vilhelm Sjöberg, and S. Weirich. Termination Casts: a Flexible Approach to Termination with General Recursion. In A. Bove, E. Komendantskaya, and M. Niqui, editors, Workshop on Partiality and Recursion in Interactive Theorem Provers, 2010.

[27]

T. Terauchi. Checking race freedom via linear programming. SIGPLAN Not., 43(6):1--10, 2008.

Digital Library

[28]

H. Xi. Dependent ML An approach to Practical Programming with Dependent Types. J. Funct. Program., 17(2):215--286, 2007.

Digital Library

[29]

J. Yang, P. Twohey, D. Engler, and M. Musuvathi. Using model checking to find serious file system errors. ACM Trans. Comput. Syst., 24(4):393--423, 2006.

Digital Library

Cited By

Yoshiura NSugiyama K(2020)Packet Reachability Verification in OpenFlow NetworksProceedings of the 2020 9th International Conference on Software and Computer Applications10.1145/3384544.3384573(227-231)Online publication date: 18-Feb-2020
https://dl.acm.org/doi/10.1145/3384544.3384573
Figueroa IGarcía BLeger PCamarão CSulzmann M(2018)Towards progressive program verification in DafnyProceedings of the XXII Brazilian Symposium on Programming Languages10.1145/3264637.3264649(90-97)Online publication date: 20-Sep-2018
https://dl.acm.org/doi/10.1145/3264637.3264649
Date HYoshiura N(2016)Computational Verification of Network Programs for Several OpenFlow Switches in CoqComputational Science and Its Applications – ICCSA 201610.1007/978-3-319-42108-7_17(223-238)Online publication date: 12-Jul-2016
https://doi.org/10.1007/978-3-319-42108-7_17
Show More Cited By

Index Terms

Language-based verification will change the world
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Verified programming in Guru
PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verification

Operational Type Theory (OpTT) is a type theory allowing possibly diverging programs while retaining decidability of type checking and a consistent logic. This is done by distinguishing proofs and (program) terms, as well as formulas and types. The ...
Dependently typed programming with singletons
Haskell '12

Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas ...
Dependently typed programming with singletons
Haskell '12: Proceedings of the 2012 Haskell Symposium

Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FoSER '10: Proceedings of the FSE/SDP workshop on Future of software engineering research

November 2010

460 pages

ISBN:9781450304276

DOI:10.1145/1882362

General Chair:
Gruia-Catalin Roman
Washington University in St. Louis, USA
,
Program Chair:
Kevin Sullivan
University of Virginia, USA

Copyright © 2010 ACM.

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

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 November 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SIGSOFT/FSE'10

Sponsor:

SIGSOFT

SIGSOFT/FSE'10: 18th ACM SIGSOFT Symposium on the Foundations of Software Engineering

November 7 - 8, 2010

New Mexico, Santa Fe, USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
229
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yoshiura NSugiyama K(2020)Packet Reachability Verification in OpenFlow NetworksProceedings of the 2020 9th International Conference on Software and Computer Applications10.1145/3384544.3384573(227-231)Online publication date: 18-Feb-2020
https://dl.acm.org/doi/10.1145/3384544.3384573
Figueroa IGarcía BLeger PCamarão CSulzmann M(2018)Towards progressive program verification in DafnyProceedings of the XXII Brazilian Symposium on Programming Languages10.1145/3264637.3264649(90-97)Online publication date: 20-Sep-2018
https://dl.acm.org/doi/10.1145/3264637.3264649
Date HYoshiura N(2016)Computational Verification of Network Programs for Several OpenFlow Switches in CoqComputational Science and Its Applications – ICCSA 201610.1007/978-3-319-42108-7_17(223-238)Online publication date: 12-Jul-2016
https://doi.org/10.1007/978-3-319-42108-7_17
Tanter ÉTabareau N(2015)Gradual certified programming in coqACM SIGPLAN Notices10.1145/2936313.281671051:2(26-40)Online publication date: 21-Oct-2015
https://dl.acm.org/doi/10.1145/2936313.2816710
Tanter ÉTabareau NSerrano M(2015)Gradual certified programming in coqProceedings of the 11th Symposium on Dynamic Languages10.1145/2816707.2816710(26-40)Online publication date: 21-Oct-2015
https://dl.acm.org/doi/10.1145/2816707.2816710
Schiller TErnst M(2012)Reducing the barriers to writing verified specificationsACM SIGPLAN Notices10.1145/2398857.238462447:10(95-112)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384624
Schiller TErnst MLeavens GDwyer M(2012)Reducing the barriers to writing verified specificationsProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384624(95-112)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384624

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents