Smart testing of functional programs in Isabelle

DOI10.1007/978-3-642-28717-6_14MaRDI QIDQ2891447zbMATH OpenOpenAlexFDO

Authors Lukas Bulwahn

Publication date 15 June 2012

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28717-6_14

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Smart test data generators via logic programming
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• On theorem prover-based testing
• Tactic program-based testing and bounded verification in Isabelle/HOL
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder

Cited in

(12)

• Sound and complete concolic testing for higher-order functions
• From LCF to Isabelle/HOL
• Foundational property-based testing
• Automatically generating counterexamples to naive free theorems
• αCheck: A mechanized metatheory model checker
• On theorem prover-based testing
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• Quick specifications for the busy programmer
• Automatic Testing of Higher Order Functions
• Formal Approaches to Software Testing
• Tactic program-based testing and bounded verification in Isabelle/HOL
• Integrating testing and interactive theorem proving

Describes a project that uses

Uses Software

• Haskell
• QuickCheck
• Isabelle
• ML
• FocalTest

This page was built for publication: Smart testing of functional programs in Isabelle

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