Dynamic symbolic execution is an effective technique for fuzzing programs with application to software verification as well if the search terminates during symbolic execution. However, the state space explosion problem often prevents the symbolic search from exploring the entire state space. As static analysis operates on the whole program rather than single execution paths, it can cut out parts of the program that are irrelevant for verifying a property. In this paper, we explore how slicing can be used before dynamic symbolic execution for analyzing assertion reachability in Java programs. We report on our first experience using state-of-the-art open-source Java slicers on the SV-COMP Java benchmark before applying GDart, a dynamic symbolic execution engine for Java. Currently, this experiment has not been successful, as the slicers are not mature enough to reliably produce correct slices of a task in the SV-COMP benchmark. However, in a few examples, the approach delivered promising results that motivate the future development of slicers for Java.
Deductive verification provides a proof that, under the provided pre-conditions, each terminating execution of a given function satisfies the stated post-conditions. In general, pre- and post-conditions are expressed in a logical specification language and typically rely on theories including abstract definitions, axioms and lemmas. As they are written by humans, errors may be introduced into specifications. Some errors can be detected when the proof fails, but sometimes, they remain unnoticed due to misleading proofs: most of the program may become dead code under the provided pre-conditions, or the proof may succeed because of inconsistencies in hypotheses and axioms. In this tool paper, we explore how to detect such unwanted situations by using deductive verification techniques and describe the smoke test mechanism in Frama-C/WP, a popular deductive verifier for C code. We show that, while the intuitive idea is simple, making it practical requires optimizations to scale up, and report on experiments with critical industrial code. Although our method is based on proof techniques, it is not complete and is similar to testing. In the end, can we ever be sure that our programs are proved well enough?
Often, testing is part of software quality assurance, in which testers may use automatic tools to generate test cases. To avoid redundant work, the tools may consider collateral coverage, i.e., use that a test case generated for a particular test goal, e.g., a branch, may cover further goals. We present a novel approach to use collateral coverage during test-case generation with software model checkers that apply counterexample-guided abstraction refinement. For every test goal, those model checkers perform a reachability analysis, which we plan to support with previous test inputs. More concretely, we use a feasibility annotation to map already covered goals to their test inputs. Whenever the reachability analysis detects a syntactical path to an uncovered test goal, we select a test input from the feasibility annotation that is likely a (partial) input for the path and use this input as a potential guide to check whether the path is semantically feasible. So far, we have integrated our approach into and evaluated it on the Test-Comp tasks. Compared to the original approach, our approach performs similar or better. In total, we increase the achieved branch coverage by 2
While the theory and practice of runtime monitoring are overall well developed, in embedded systems, runtime monitoring is not as common as one would expect. Especially small-scale embedded systems, which are found in many household devices, are often somewhat safety-critical and could benefit from the possibility to detect software or hardware defects that cannot be uncovered with verification alone. While monitoring frameworks such as RTLola and Copilot are available to address this problem, employing them leads to a gap between verification and runtime monitoring by these frameworks having specialized specification languages for monitoring, and what can be expressed in them is incomparable to the capabilities of the temporal logics traditionally employed in formal verification. This paper discusses how (linear) temporal logic runtime monitoring for small-scale embedded systems can be made more efficient and attractive to the embedded systems practitioner. This includes identifying why monitoring for traditional temporal logics is somewhat inefficient in software, how this problem can be addressed in a low-cost way, and how runtime monitors can become a more useful component of an embedded system. By providing a way to translate a specification to monitor code that also tracks the reason for a specification violation, the overall approach discussed in the paper makes spending developer time on writing a relatively precise specification of a system to build attractive, which also helps paving the way to make formal verification for small-scale embedded systems more common.
We present Affinitree, a compositional framework for analyzing Deep Neural Networks (DNNs) based on three elementary principles: (1) symbolic execution, (2) infeasible path elimination, and (3) abstraction. The combination of these principles allows one to elegantly solve a number of interesting analysis and verification tasks, like traditional verification problems with pre- and post-conditions, model explanations in terms of semantically equivalent decision trees, concolic execution for slice-oriented testing, and visual verification of two-dimensional slices. The paper illustrates the flexibility of Affinitree over three different use cases covering fairness evaluation, adversarial examples, and counterfactuals. Affinitree is available as a modular open source library for replication, experimentation, and extension.
