ABSTRACT. Uppaal Stratego facilitates optimization of quantitative measures on complex stochastic timed systems. In this paper we propose alternatives to the optimization algorithms of Uppaal Stratego, demonstrating that a significant improvement can be achieved in terms of convergence tendencies. In particular, we propose two online learning algorithms, using online partition refinement techniques, and argue for its theoretical convergence. We have implemented the proposed algorithms in Uppaal Stratego and support our claims with experimentson a range of models. We also provide the core algorithms as an Open Source library under the permissive LGPL license.

ABSTRACT. In this paper, we investigate how symmetry transformations of equivariant dynamical systems can reduce the computation effort for safety verification. Symmetry transformations of equivariant systems map solutions to other solutions. We build upon this result, producing reach sets from other previously computed reach sets. We augment the standard simulation-based verification algorithm with a new procedure that attempts to verify the safety of the system starting from a new initial set of states by transforming previously computed reach sets. This new algorithm required the creation of a new cache-tree data structure for multi-resolution reachtubes. Our implementation has been tested on several benchmarks and has achieve significant improvements in verification time.

ABSTRACT. Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time. We address the following problem: given a timed system, synthesize the execution times for which one cannot deduce whether the system performed some secret behavior. We solve this problem in the setting of timed automata (TAs). We first provide a general solution, and then extend the problem to parametric TAs, by synthesizing internal timings making the TA secure. We study decidability, devise algorithms, and show that our method can also apply to program analysis.

ABSTRACT. Online first-order monitoring is the task of detecting temporal patterns in streams of events carrying data. Considerable research has been devoted to scaling up monitoring using parallelization by partitioning events based on their data values and processing the partitions concurrently. To be effective, partitioning must account for the event stream’s statistics, e.g., the relative event frequencies, and these statistics may change rapidly. We develop the first parallel online first-order monitor capable of adapting to such changes. A central problem we solve is how to manage and exchange states between the parallel executing monitors. To this end, we develop state exchange operations and prove their correctness. Moreover, we extend the implementation of the MonPoly monitoring tool with these operations, thereby supporting parallel adaptive monitoring, and show empirically that adaptation can yield up to a tenfold improvement in run-time.

ABSTRACT. We present a novel approach to the offline monitoring of specifications expressed in metric temporal logic (MTL). Our monitoring algorithm exploits multiple one-way reading heads that traverse a trace sequentially. We present both theoretical and practical results that show this substantially improves upon the state-of-the-art. In particular, our algorithm is the first offline monitoring algorithm for MTL with past and bounded-future temporal operators that is almost trace-length independent and outputs a trace of Boolean verdicts denoting the monitored formula's satisfaction at every position in the input trace. In addition, our algorithm's worst-case space complexity is linear in the formula size, while previous algorithms were exponential. Moreover, we compare our implementation of the algorithm with another almost trace-length independent tool that outputs non-standard verdicts to achieve this space complexity. Our tool used less memory and runs significantly faster, for example yielding a 10-fold improvement on average on random formulas, while producing a better output.

ABSTRACT. Causality Checking has been proposed as a finite state space exploration technique which computes ordered sequences of events that are considered to cause the violation of a reachability property. A crucial point in the implementation of Causality Checking is the computation and storage of all minimal counterexamples found during state space exploration. We refer to the set of all minimal counterexamples as a causal trace set. However, the Duplicate State Prefix Matching (DSPM) Algorithm that is currently used in Causality Checking only under-approximates the causal trace set. As we argue, without the approximation the DSPM algorithm is inefficient. We propose the, to the best of our knowledge, first efficient algorithm that precisely computes a causal trace set, avoiding approximation, called Causal Trace Backward Search (CTBS). We compare the DSPM and CTBS algorithms with respect to their worst case complexities, and by applying them to several case studies.

ABSTRACT. There are several powerful automatic test-case generators available, each with different strengths and weaknesses. To immediately benefit from different strengths of different tools, we need to investigate ways for quick and easy combination of techniques. Until now, research has mostly investigated integrated combinations, which require extra implementation effort. We propose the concept of conditional software testing and a set of combination techniques that do not require implementation effort: Different testers can be taken `off the shelf' and combined in a way that they cooperatively solve the problem of test generation for a given program and test specification. This way, the latest advances in test generation can be combined without delay. Conditional software testing passes the test goals that a first test generator leaves uncovered to the next test generator, so that the next test generator does not repeat work (as in combinations without information passing) but can focus on the remaining test goals. Our combinations do not require changes to the implementation of a test generator, because we leverage a testability transformation (i.e., we reduce the program to those parts that are relevant to the remaining test goals). To evaluate conditional software testing and our proposed combination techniques, we implemented the required transformations and ran experiments on a large amount of benchmark tasks; the obtained results are promising.

ABSTRACT. Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numeric domains, existing symbolic execution techniques for heap-based programs are limited due to the lack of a succinct and precise description for symbolic values over unbounded heaps. In this work, we present a new symbolic execution method for heap-based programs based on separation logic. The essence of our proposal is context-sensitive lazy initialization, a novel approach for efficient test input generation. Our approach differs from existing approaches in two ways. Firstly, our approach is based on separation logic, which allows us to precisely capture pre-conditions of heap-based programs so that we avoid generating invalid test inputs. Secondly, we generate only fully initialized test inputs, which are more useful in practice compared to those partially initialized test inputs generated by the state-of-the-art tools. We have implemented our approach as a tool, called Java StarFinder, and evaluated it on a set of programs with complex heap inputs. The results show that our approach significantly reduces the number of invalid test inputs and improves the test coverage.

ABSTRACT. An important goal of software engineering research is to create methods for efficient verification and detecting bugs. In this context, we focus on two challenges: (1) scalability to large and realistic software systems and (2) tools unable to directly analyze programs that perform I/O operations and interact with their environment. The common sources of problems with scalability include the huge number of thread interleavings and usage of large libraries. Programs written in managed languages, such as Java, cannot be directly analyzed by many verification tools due to insufficient support for native library methods. Both issues affect especially path-sensitive verification techniques. We present the BUBEN system that automatically generates abstractions of complex software systems written in Java. The whole process has three phases: (1) dynamic analysis that records under-approximate information about behavior of native methods and library methods that perform I/O, (2) static analysis that computes over-approximate summaries of side effects of library methods, and (3) program code transformation that replaces calls of native methods and creates abstractions of library methods. Software systems abstracted in this way can be analyzed, e.g. for the presence of bugs, without the risk of a tool failure caused by unsupported libraries and much more efficiently too. We evaluated BUBEN on several programs from popular benchmark suites, including DaCapo.

ABSTRACT. Whitebox fuzzing (a.k.a. concolic testing) has been shown to be an effective bug finding technique on its own as well as in combination with coverage-guided greybox fuzzing. However, there is currently a lack of whitebox fuzzers operating above the binary code level. We present KLUZZER, a whitebox fuzzer targeting LLVM bitcode, and thus can be easily combined with the widely deployed LLVM's coverage-guided greybox fuzzer LibFuzzer. Experimental evaluation on a set of benchmarks shows encouraging results.