Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification

DOI10.1007/978-3-319-41135-4_7zbMath1348.68222OpenAlexW2480689304MaRDI QIDQ2827442

Shaoying Liu

Publication date: 19 October 2016

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

Full work available at URL: https://doi.org/10.1007/978-3-319-41135-4_7

Mathematics Subject Classification ID

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

Uses Software

• ACL2
• Coq
• Isabelle
• PVS
• Yices
• z3
• TestEra
• QuickChick

Cites Work

• Specification and verification challenges for sequential object-oriented programs
• Model-Based Mutation Testing of Reactive Systems
• ACL2s: “The ACL2 Sedan”
• Foundational Property-Based Testing
• The New Quickcheck for Isabelle
• Theory and Applications of Satisfiability Testing
• Formal Approaches to Software Testing
• Unnamed Item
• Unnamed Item

This page was built for publication: Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification