From testing to formal verification in Haskell

Hafidi, Mustafa (2020). From testing to formal verification in Haskell. Thesis (Master thesis), E.T.S. de Ingenieros Informáticos (UPM).

Description

Title: From testing to formal verification in Haskell
Author/s:
  • Hafidi, Mustafa
Contributor/s:
  • Vazou, Niki
  • Darulova, Eva
  • Majumdar, Rupak
  • Carro, Manuel
Item Type: Thesis (Master thesis)
Masters title: Ingeniería del Software
Date: July 2020
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Otro
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (379kB) | Preview

Abstract

Haskell’s expressive type-system saves developers from writing several categories of bugs. Yet, even though it allows them to encode complicated invariants statically, logic related errors can still escape to the type system. Typical testing mechanisms are still offered to ensure higher levels of quality of pieces of software written in Haskell. In particular, the testing framework QuickCheck6 enables a type-based property testing, where the programmer encodes invariants as properties, and the library generates (appropriate) test data to cover them. It is a known issue that the effectiveness of any testing mechanism is sensitive to the nature of the test cases and formal verification is preferred whenever applicable. LiquidHaskell allows enhancements to the Haskell’s type-system with refinement types in order for developers to encode type-based invariants and automatically prove their satisfiability using an SMT solver. Typically, trivial properties are easily proved by LiquidHaskell, whereas other times the developer needs to manually provide inductive hypotheses, additional lemmas, or use equational reasoning to complete the proof. In this thesis work we study the ”manual” proofs in LiquidHaskell. We formally prove QuickCheck properties of a real-world library and study a way to automate a major part of the manual work. We introduce a proof generator written in Template Haskell21 that, given a boolean property (QuickCheck test), automatically generates the corresponding proof to formally verify the property in LiquidHaskell. We noticed that many of the manual proofs involve induction and case splitting, thus, we integrated into the proof generator two heuristics that help in those cases in a similar style to the tactics in Coq 4 proofs.

More information

Item ID: 63616
DC Identifier: http://oa.upm.es/63616/
OAI Identifier: oai:oa.upm.es:63616
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 07 Sep 2020 09:26
Last Modified: 07 Sep 2020 09:26
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM