How Test Generation Helps Software Specification and Deductive Verification in Frama-C
Abstract
This paper describes an incremental methodology of deductive verification assisted by test generation and illustrates its benefits
by a set of frequent verification scenarios.
We present StaDy, a new integration of the concolic test generator PathCrawler within the software analysis platform FramaC.
This new plugin treats a complete formal specification of a C program
during test generation and provides the validation engineer with a helpful feedback
at all stages of the specification and verification tasks.
Origin : Files produced by the author(s)
Loading...