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!
cited_by
cites
container_end_page
container_issue
container_start_page
container_title arXiv.org
container_volume
creator Thomas Ekström Hansen
Brady, Edwin
description 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.
doi_str_mv 10.48550/arxiv.2407.12726
format article
fullrecord <record><control><sourceid>proquest</sourceid><recordid>TN_cdi_proquest_journals_3082397312</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>3082397312</sourcerecordid><originalsourceid>FETCH-LOGICAL-a522-70ecd16e2d49da271838f13d34948074b88bd0d0b209ba13a443b9398578b02f3</originalsourceid><addsrcrecordid>eNotzc1qAjEUQOEgFCrWB-hupOtMb-5NJjdLlf6B0C5mL0mTKcrgTBOV-vYV2tXZnU-IewW1ZmPg0eef3blGDbZWaLGZiCkSKcka8VbMS9kDADYWjaGpWLSXMck-nVNffeRhTPl4qVa-pFi1qRx3h687cdP5vqT5f2eifX5q169y8_7ytl5upDeI0kL6jKpJGLWLHq1i4k5RJO00g9WBOUSIEBBc8Iq81hQcOTaWA2BHM_Hwtx3z8H260tv9cMqHq7glYCRnSSH9Ahb9Pho</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>3082397312</pqid></control><display><type>article</type><title>Type-level Property Based Testing</title><source>ProQuest - Publicly Available Content Database</source><creator>Thomas Ekström Hansen ; Brady, Edwin</creator><creatorcontrib>Thomas Ekström Hansen ; Brady, Edwin</creatorcontrib><description>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.</description><identifier>EISSN: 2331-8422</identifier><identifier>DOI: 10.48550/arxiv.2407.12726</identifier><language>eng</language><publisher>Ithaca: Cornell University Library, arXiv.org</publisher><subject>Semantics ; Specifications</subject><ispartof>arXiv.org, 2024-07</ispartof><rights>2024. This work is published under http://creativecommons.org/licenses/by-nc-nd/4.0/ (the “License”). Notwithstanding the ProQuest Terms and Conditions, you may use this content in accordance with the terms of the License.</rights><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://www.proquest.com/docview/3082397312?pq-origsite=primo$$EHTML$$P50$$Gproquest$$Hfree_for_read</linktohtml><link.rule.ids>780,784,25752,27924,37011,44589</link.rule.ids></links><search><creatorcontrib>Thomas Ekström Hansen</creatorcontrib><creatorcontrib>Brady, Edwin</creatorcontrib><title>Type-level Property Based Testing</title><title>arXiv.org</title><description>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.</description><subject>Semantics</subject><subject>Specifications</subject><issn>2331-8422</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2024</creationdate><recordtype>article</recordtype><sourceid>PIMPY</sourceid><recordid>eNotzc1qAjEUQOEgFCrWB-hupOtMb-5NJjdLlf6B0C5mL0mTKcrgTBOV-vYV2tXZnU-IewW1ZmPg0eef3blGDbZWaLGZiCkSKcka8VbMS9kDADYWjaGpWLSXMck-nVNffeRhTPl4qVa-pFi1qRx3h687cdP5vqT5f2eifX5q169y8_7ytl5upDeI0kL6jKpJGLWLHq1i4k5RJO00g9WBOUSIEBBc8Iq81hQcOTaWA2BHM_Hwtx3z8H260tv9cMqHq7glYCRnSSH9Ahb9Pho</recordid><startdate>20240717</startdate><enddate>20240717</enddate><creator>Thomas Ekström Hansen</creator><creator>Brady, Edwin</creator><general>Cornell University Library, arXiv.org</general><scope>8FE</scope><scope>8FG</scope><scope>ABJCF</scope><scope>ABUWG</scope><scope>AFKRA</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>HCIFZ</scope><scope>L6V</scope><scope>M7S</scope><scope>PIMPY</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope><scope>PRINS</scope><scope>PTHSS</scope></search><sort><creationdate>20240717</creationdate><title>Type-level Property Based Testing</title><author>Thomas Ekström Hansen ; Brady, Edwin</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-a522-70ecd16e2d49da271838f13d34948074b88bd0d0b209ba13a443b9398578b02f3</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2024</creationdate><topic>Semantics</topic><topic>Specifications</topic><toplevel>online_resources</toplevel><creatorcontrib>Thomas Ekström Hansen</creatorcontrib><creatorcontrib>Brady, Edwin</creatorcontrib><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>Materials Science &amp; Engineering Collection</collection><collection>ProQuest Central (Alumni)</collection><collection>ProQuest Central</collection><collection>ProQuest Central Essentials</collection><collection>AUTh Library subscriptions: ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central</collection><collection>SciTech Premium Collection (Proquest) (PQ_SDU_P3)</collection><collection>ProQuest Engineering Collection</collection><collection>Engineering Database</collection><collection>ProQuest - Publicly Available Content Database</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><collection>ProQuest Central China</collection><collection>Engineering Collection</collection><jtitle>arXiv.org</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Thomas Ekström Hansen</au><au>Brady, Edwin</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Type-level Property Based Testing</atitle><jtitle>arXiv.org</jtitle><date>2024-07-17</date><risdate>2024</risdate><eissn>2331-8422</eissn><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.</abstract><cop>Ithaca</cop><pub>Cornell University Library, arXiv.org</pub><doi>10.48550/arxiv.2407.12726</doi><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier EISSN: 2331-8422
ispartof arXiv.org, 2024-07
issn 2331-8422
language eng
recordid cdi_proquest_journals_3082397312
source ProQuest - Publicly Available Content Database
subjects Semantics
Specifications
title Type-level Property Based Testing
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-09T09%3A16%3A37IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Type-level%20Property%20Based%20Testing&rft.jtitle=arXiv.org&rft.au=Thomas%20Ekstr%C3%B6m%20Hansen&rft.date=2024-07-17&rft.eissn=2331-8422&rft_id=info:doi/10.48550/arxiv.2407.12726&rft_dat=%3Cproquest%3E3082397312%3C/proquest%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-a522-70ecd16e2d49da271838f13d34948074b88bd0d0b209ba13a443b9398578b02f3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=3082397312&rft_id=info:pmid/&rfr_iscdi=true