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)

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

Describes a project that uses

Uses Software

• QuickCheck
• FocalTest
• Haskell
• ML
• Isabelle

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)