Language-based verification will change the world

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. Categories and Subject Descriptors D.3.2 [Programming Languages]: Applicative (functional) languages; F.3.1 [Logics and Meanings of Programs]: Mechanical verification; F.4.1 [Mathematical Logic]: Mechanical theorem proving General Terms Languages, Verification Keywords Language-Based Verification, Dependently Typed Programming

• Type: Journal
• Year: 2010
• Where: SIGSOFT
• Authors: Tim Sheard, Aaron Stump, Stephanie Weirich
• Keywords: Keywords Language-Based Verification, Language-based Verification, Programming Languages, SIGSOFT 2010, Software Engineering