Dataflow analysis is a fundamental code analysis technique that identifies dependencies between program values.

Tabular reinforcement learning methods cannot operate directly on continuous state spaces. One solution for this problem is to partition the state space. A good partitioning enables generalization during learning and more efficient exploitation of prior experiences. Consequently, the learning process becomes faster and produces more reliable policies. However, partitioning introduces approximation, which is particularly harmful in the presence of nonlinear relations between state components. An ideal partition should be as coarse as possible, while capturing the key structure of the state space for the given problem. This work extracts partitions from the environment dynamics by symbolic execution. We show that symbolic partitioning improves state space coverage with respect to environmental behavior and allows reinforcement learning to perform better for sparse rewards. We evaluate symbolic state space partitioning with respect to precision, scalability, learning agent performance and state space coverage for the learnt policies.

Dataflow analysis is a powerful code analysis technique that reasons dependencies between program values, offering support for code optimization, program comprehension, and bug detection. Existing approaches require the successful compilation of the subject program and customizations for downstream applications. This paper introduces LLMDFA, an LLM-powered dataflow analysis framework that analyzes arbitrary code snippets without requiring a compilation infrastructure and automatically synthesizes downstream applications. Inspired by summary-based dataflow analysis, LLMDFA decomposes the problem into three sub-problems, which are effectively resolved by several essential strategies, including few-shot chain-of-thought prompting and tool synthesis. Our evaluation has shown that the design can mitigate the hallucination and improve the reasoning ability, obtaining high precision and recall in detecting dataflow-related bugs upon benchmark programs, outperforming state-of-the-art (classic) tools, including a very recent industrial analyzer.

Probabilistic software analysis extends classic static analyses techniques to consider the effects of probabilistic uncertainty, whether explicitly embedded within the code - as in probabilistic program - or externalized in a probabilistic input distribution [Dwyer et al. 2016]. Similarly to their classic counterparts, these analyses aim at inferring the probability of a target event to occur during execution, e.g., reaching a program state or triggering an exception. For the probabilistic analysis of programs written in general-purpose programming languages, probabilistic symbolic execution (PSE) [Geldenhuys et al. 2012] exploits established symbolic execution engines for the language to extract constraints on probabilistic input or program variables that lead to the occurrence of the target event. The probability of satisfying any such constraints is then computed via model counting or inferred via solution space quantification methods, depending on the variable types and the characteristic of the constraints. Variations of PSE include incomplete analyses inferring probability bounds from a finite sample of program paths executed symbolically [Filieri et al. 2014], methods for non-deterministic programs [Luckow et al. 2014] and data structures [Filieri et al. 2015].