Automatically generating counterexamples to naive free theorems

DOI10.1007/978-3-642-12251-4_14MaRDI QIDQ3558338zbMATH OpenOpenAlexFDO

Authors Daniel Seidel, Janis Voigtländer

Publication date 4 May 2010

Published in Functional and Logic Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Instrumenting a weakest precondition calculus for counterexample generation
• Smart testing of functional programs in Isabelle
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Generating counterexamples for structural inductions by exploiting nonstandard models
• Smart test data generators via logic programming

Cited in

(4)

• Safe typing of functional logic programs with opaque patterns and local bindings
• scientific article; zbMATH DE number 2090301 (Why is no real title available?)
• A liberal type system for functional logic programs
• Refined typing to localize the impact of forced strictness on free theorems

Describes a project that uses

Uses Software

• QuickCheck

This page was built for publication: Automatically generating counterexamples to naive free theorems

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