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

Randomized algorithms (68W20) 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)

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)

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

Describes a project that uses

Uses Software

• QuickCheck
• PVS
• Coq

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)