We present a new fuzzing technique for multithreaded C# programs running on the .NET platform. It is built upon the .NET Profiling library, supported by CLR (Common Language Runtime) on Windows, and uses configurable strategies for the fuzzing process. During execution of the subject program, the fuzzing algorithm controls thread scheduling and preemption through suspending and resuming threads at specific code locations that we call stop points. For the purpose of driving the fuzzing process, we have designed a hybrid systematic-random strategy that gradually finds yet unexplored thread schedules. Results of experiments with programs from the SCT benchmark collection show that our tool is able to find errors triggered by specific thread interleavings, and within practical time limits.
Hyperproperties are properties of systems that relate more than one trace, which are common in information-flow, concurrency, symmetry, diagnosability, etc. Several temporal logics for hyperproperties have been proposed—like HyperLTL and HyperCTL* where traces are compared synchronously—and recently extended for comparing traces asynchronously. However, all these temporal hyperlogics are for infinite traces, in spite of the recent popularity of temporal logics on finite traces. In this paper, we introduce SC-HyperLTL, a logic for asynchronous hyperproperties on finite traces and with past operators, by adapting and combining two existing logics for asynchronous hyperproperties: stuttering HyperLTL ( HyperLTL_S ) and context HyperLTL ( HyperLTL_C ). We show that SC-HyperLTL is decidable and can encode many hyperproperties of interest. We present two practical algorithms that reduce the model checking problem of SC-HyperLTL to inputs of two existing tools: AutoHyper (which can model check hyperproperties on infinite traces) and nuXmv (a model checker for trace properties). We illustrate our algorithms on a prototype implementation.
Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on basic reachability properties. Instead of implementing algorithms for each possible specification, some verifiers implement known transformations from the given specification to reachability on their internal representations. Unfortunately, those internal transformations are not reusable by others. To improve this situation, we propose TransVer, a tool which offers transformations as modular stand-alone component, modifying the input program instead of the internal representation, enabling their usage as a preprocessing step by other verifiers. This way, we separate two concerns: improving the performance of reachability analyses and implementing efficient transformations of arbitrary specifications to reachability. We implement the transformations in a framework that is based on instrumentation automata, inspired by the BLAST query language. In our initial study, we support three important concrete specifications for C programs: termination, no-overflow, and memory cleanup. We conduct experiments with ten different verifiers. The experiments evaluate the efficiency and effectiveness of our transformations. The results are promising: Our transformations can extend existing verifiers to be effective on specifications for which they have no integrated support, and the efficiency is often similar or better to state-of-the-art verifiers that have integrated support for the considered specifications.
Model checking is a framework for automated formal verification of transition systems, like hardware designs. Two leading model-checking techniques, PDR and CAR, are based on multiple calls to a SAT solver, for the purpose of finding a path to a bug or proving its absence. They build sequences of formulas, called frames, that represent approximated sets of states, e.g., a frame can contain an over-approximation of the states that can reach the negated property within a given number of steps. Part of the process is to make these sets more precise, i.e., less approximating, and this is done by strengthening the frames with negation of states that were proven to be spurious. A key component for performance is the ability of these engines to generalize those states and thus accelerate the process of making the frames more precise. This is done by strengthening them with the unsatisfiable cores that the SAT solver returns. In this work, we suggest several performance improvements to this process, most notably a technique for generating multiple such cores in linear time and adding them simultaneously to the frames. Our results show that our implementation of these techniques, on top of SimpleCAR, not only improves its performance, but also solves more (unsafe) cases than any other model-checker in the public domain, and solves instances from the HWMCC that no other model checker can solve, hence it contributes to the state-of-the-art.
This paper addresses the shortest path problem for weighted interprocedural automata (WIPA), a simple model adapted to the analysis of low-level programs. We propose an efficient and versatile approach relying on Knuth’s generalization of Dijkstra’s algorithm to context-free grammars. Several variants of the problem are considered in the paper, depending on the starting and ending stacks. Moreover, we solve both the single-source and single-target versions. Each problem is translated into a succint context-free grammar, permitting the efficient computation of a solution in O(n log n + m) time, where n and m are the number of states and transitions in the underlying WIPA. We provide experimental results on real-size programs showing the scalability of the approach.
