SymFusion devises a novel hybrid instrumentation approach for concolic execution, where the core components of an application can be instrumented at compilation time ù (e.g., using an LLVM pass), while the remaining components can be dynamically instrumented at execution time (e.g., using QEMU DBT). The goal is to achieve the benefits of both approaches in terms of efficiency and flexibility.

Framework for testing the reachability of native functions in Android applications. Solving this task can be essential for several security tasks, e.g., to show that a vulnerable function within a library is indeed reachable by an application and thus it requires immediate attention.

Fuzzolic is a new concolic executor based on QEMU. It can be paired with a coverage-guided fuzzer, such as AFL++, to find bugs in real-world programs.

Fuzzy-SAT is an approximate solver that can efficiently solve queries generated by concolic execution using techniques borrowed from the fuzzing domain.

A prototype tool that visualizes the state of a symbolic execution analysis by plotting relevant data on a sunburst (that represent the symbolic execution tree), and on the control flow graph of the program. Furthermore, the tool allows the user to interact and refine the analysis, allowing him to interactively prune the symbolic execution tree.

A new approach to symbolic memory that reduces the need for concretization, hence offering the opportunity for broader state explorations and more precise pointer reasoning.

A Valgrind tool for performance profiling designed to help developers discover hidden asymptotic inefficiencies in the code. From one or more runs of a program, aprof measures how the performance of individual routines scales as a function of the input size, yielding clues to its growth rate.

Some notes describing Apache Hadoop internals (2.3.0 or later).

A prototype of an adaptive memory allocator.