Neural networks are an increasingly common tool for solving problems that require complex analysis and pattern matching, such as identifying stop signs or processing medical imagery. Accordingly, verification of neural networks for safety and correctness is of great importance, as mispredictions can have catastrophic results in safety critical domains. One metric for verification is robustness, which answers whether or not a misclassified input exists in a given input neighborhood. I am focusing my research at quantitative robustness---finding not only if there exist misclassified inputs within a given neighborhood but also how many exist as a proportion of the neighborhood size. My overall goal is to expand the research on quantitative neural network robustness verification and create a variety of quantitative verification tools geared towards expanding our understanding of neural network robustness.

We present a heuristic for approximating the likelihood of reaching a given program statement using 1) branch selectivity (representing the percentage of values that satisfy a branch condition), which we compute using model counting, 2) dependency analysis, which we use to identify input-dependent branch conditions that influence statement reachability, 3) abstract interpretation, which we use to identify the set of values that reach a branch condition, and 4) a discrete-time Markov chain model, which we construct to capture the control flow structure of the program together with the selectivity of each branch. Our experiments indicate that our heuristic-based probabilistic reachability analysis tool PReach can identify hard to reach statements with high precision and accuracy in benchmarks from software verification and testing competitions, Apache Commons Lang, and the DARPA STAC program. We provide a detailed comparison with probabilistic symbolic execution and statistical symbolic execution for the purpose of identifying hard to reach statements. PReach achieves comparable precision and accuracy to both probabilistic and statistical symbolic execution for bounded execution depth and better precision and accuracy when execution depth is unbounded and the number of program paths grows exponentially. Moreover, PReach is more scalable than both probabilistic and statistical symbolic execution.

Model counting procedures for data structures are crucial for advancing the field of automated quantitative program analysis. We present a tool for Model Counting for Bounded Array Theory (MCBAT). MCBAT works on quantified integer array constraints in which all arrays have a finite length. We employ reductions from the theory of arrays to uninterpreted functions and linear integer arithmetic (LIA). Once reduced to LIA, we leverage Barvinok's polynomial time integer lattice point enumeration algorithm. Finally, we present a case study demonstrating applicability to automated quantitative program analysis. MCBAT is available for immediate use as a Docker image and the source code is freely available in our Github repository.

Conditional logic and control structures are typically considered an important part of introductory computer science education, yet novices often struggle to correctly write and navigate such program logic. Previous research has largely attended to student difficulties with parsing Boolean expressions, but has not had much focus on the control structures themselves. To investigate how students work through complicated logic, we conducted a qualitative analysis of four one-on-one interviews with undergraduate students in which we gave students a piece of code with a complicated conditional control structure and asked them to write test cases for all paths. We found that several students struggled to determine the output the function would provide for a given input, and we hypothesize this occurred because they incorrectly treated an if statement as an else-if statement. One student simply wrote an incorrect output, which we believe occurred because they made this particular mistake, while another student got partway through the problem before verbally seeming to correct themself and re-identify a statement as an else-if. Based on our results, we hypothesize that novices may sometimes misidentify a sequential if statement as an else-if, which may lead them to incorrectly interpret a conditional control structure.