On theorem prover-based testing

DOI10.1007/S00165-012-0222-YMaRDI QIDQ470025zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Achim D. Brucker, Burkhart Wolff

Publication date 11 November 2014

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-012-0222-y

zbMATH Keywords

theorem provingtest sequencetest case generationdomain partitioningHOL-TestGen

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing
• Tactic program-based testing and bounded verification in Isabelle/HOL
• Smart test data generators via logic programming
• Smart testing of functional programs in Isabelle
• Formal Approaches to Software Testing

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 4219104 (Why is no real title available?)
• scientific article; zbMATH DE number 1543300 (Why is no real title available?)
• scientific article; zbMATH DE number 3421895 (Why is no real title available?)
• A Compiled Implementation of Normalization by Evaluation
• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• An introduction to mathematical logic and type theory: To truth through proof.
• Error Sensitive Test Cases Analysis (ESTCA)
• Formal Approaches to Software Testing
• Hoare logic for Java in Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Notions of computation and monads
• Operating system verification---an overview
• Path Feasibility Analysis for String-Manipulating Programs
• Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing
• Testing can be formal, too
• Winskel is (almost) right: Towards a mechanized semantics textbook

Cited in

(13)

• Monadic Sequence Testing and Explicit Test-Refinements
• Tactic program-based testing and bounded verification in Isabelle/HOL
• Foundational property-based testing
• Test-data generation for control coverage by proof
• Smart testing of functional programs in Isabelle
• Formal Approaches to Software Testing
• On Sample-Based Testers
• Some Theory Concerning Certification of Mathematical Subroutines by Black Box Testing
• Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• Testing-based formal verification for theorems and its application in software specification verification
• Formal Approaches to Software Testing
• Integrating testing and interactive theorem proving

Describes a project that uses

Uses Software

• IMP++
• Isabelle/HOL
• Haskell
• ETPS
• TorX
• GATeL
• Korat
• Pex
• QuickCheck
• Java PathFinder
• Flyspeck
• SpecExplorer
• JPF-SE
• HOL-TestGen

This page was built for publication: On theorem prover-based testing

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