Foundational property-based testing

DOI10.1007/978-3-319-22102-1_22MaRDI QIDQ2945645zbMATH OpenOpenAlexFDO

Authors Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce

Publication date 14 September 2015

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01162898/file/main.pdf

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Randomized algorithms (68W20)

Recommendations

• Towards substructural property-based testing
• Beginner's luck: a language for property-based generators
• Functional Testing in the Focal Environment
• Do judge a test by its cover. Combining combinatorial and property-based testing
• Tests and proofs for custom data generators

Cites work

• A first step in the design of a formally verified constraint-based testing tool: FocalTest
• A new look at generalized rewriting in type theory
• An introduction to small scale reflection in Coq
• On theorem prover-based testing
• Producing certified functional code from inductive specifications
• Smart testing of functional programs in Isabelle
• Testing noninterference, quickly
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• Theoretical Aspects of Computing - ICTAC 2004
• Turning Inductive into Equational Specifications

Cited in

(14)

• Tests and proofs for custom data generators
• Automated proof of Bell-LaPadula security properties
• From LCF to Isabelle/HOL
• QuickChick
• Tests and Proofs for Enumerative Combinatorics
• Testing-based formal verification for theorems and its application in software specification verification
• A first step in the design of a formally verified constraint-based testing tool: FocalTest
• αCheck: A mechanized metatheory model checker
• Erasure-Resilient Property Testing
• Parameterized property testing of functions
• Functional Testing in the Focal Environment
• Tuning as convex optimisation: a polynomial tuner for multi-parametric combinatorial samplers
• Towards substructural property-based testing
• Two applications of logic programming to Coq

Describes a project that uses

Uses Software

• Coq
• PVS
• QuickCheck

This page was built for publication: Foundational property-based testing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945645)