Test-data generation for control coverage by proof

DOI10.1007/s00165-013-0279-2zbMath1342.68206OpenAlexW1970908606MaRDI QIDQ736805

Ana Cavalcanti, Colin O'Halloran, Steve F. King, J. C. P. Woodcock

Publication date: 5 August 2016

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

Full work available at URL: https://doi.org/10.1007/s00165-013-0279-2

zbMATH Keywords

invariantssemanticsUTPcontrol coverage

Mathematics Subject Classification ID

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

Uses Software

• Isabelle/HOL
• PVS
• Daikon
• ProofPower
• ClawZ
• Z
• ZRC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mechanical reasoning about families of UTP theories
• On theorem prover-based testing
• A process algebraic framework for specification and validation of real-time systems
• Testing algebraic data types and processes: A unifying theory
• ZRC -- A refinement calculus for \(Z\)
• Isabelle/HOL. A proof assistant for higher-order logic
• The Daikon system for dynamic detection of likely invariants
• The B-Book
• Automatically generating test data from a Boolean specification
• Pointers and Records in the Unifying Theories of Programming
• Formal Approaches to Software Testing

This page was built for publication: Test-data generation for control coverage by proof