Tactic program-based testing and bounded verification in Isabelle/HOL

DOI10.1007/978-3-319-92994-1_6MaRDI QIDQ6039393zbMATH OpenOpenAlexFDO

Authors Chantal Keller

Publication date 5 May 2023

Published in Tests and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-92994-1_6

zbMATH Keywords

interactive theorem provingsymbolic executioncoverage criteriawhite-box testingbounded verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On theorem prover-based testing
• Monadic Sequence Testing and Explicit Test-Refinements
• Smart testing of functional programs in Isabelle
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing

Cited in

(4)

• Smart testing of functional programs in Isabelle
• Logic for Programming, Artificial Intelligence, and Reasoning
• On theorem prover-based testing
• Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing

This page was built for publication: Tactic program-based testing and bounded verification in Isabelle/HOL

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