Type-level Property Based Testing

TL;DR

This paper introduces an automated framework that integrates property-based testing, dependently typed models, and type checking to verify software correctness at compile time, bridging the gap between model checking and type checking.

Contribution

It presents a novel approach combining PBT, ISMs, and dependent types to model systems, verify implementation correctness, and test model-specification alignment.

Findings

Type checker verifies implementation behavior against specifications

Framework models systems and protocols using dependent types and ISMs

Enables testing of model semantics against implementation

Abstract

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.