Agent-based Code-Block Verification (Master's Thesis)
Master's Thesis on agent-based block verification. The overarching goal is the creation of a conceptual framework for creation of an agent-based, potentially distributed and block-wise verification approach.
A full software verification is distributed into multiple interacting block-wise verifications: Each block-wise verification is represented by a block summary.
A block summary of a block B is a relation between input- and output-values of that block B. Input-output relations are computed with CPAchecker's predicate analysis.
At the end of this milestone, it should be possible to use agent-based, block-wise verification in CPAchecker on a single machine. This is the minimum baseline for this milestone.
It is expected that blocks are configurable and block nesting is possible.
Depending on the chosen focus, execution should be possible in a distributed setting and/or the scheduling mechanism should be configurable. If block-wise verification results are made persistent, reuse of partial results could be explored. Optimizations may be interesting, as well.
An examplary use of this technique and an extensive evaluation on sv-benchmarks should be conducted to show the effect of this technique.
Example use cases: Multi-threaded and distributed verification, incremental verification, continuous verification, multi-property verification etc.