Type-level Property Based Testing

We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Proper...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-07
Main Authors: Thomas Ekström Hansen, Brady, Edwin
Format: Article
Language:English
Subjects:
Semantics
Specifications
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.
ISSN:2331-8422
DOI:10.48550/arxiv.2407.12726