Code coverage is used by millions of developers in thousands of organizations on a daily basis. Despite this popularity, code coverage has well-understood limitations demonstrated by the software engineering research community, such as not providing enough insight into test oracles’ quality. In this research, we compute coverage gaps, a metric to detect the undertested program structures by analyzing the existing test oracles. We then propose a lightweight intra-procedural flow-insensitive static analysis technique that uses the system under test (SUT) and the coverage gaps as inputs to recommend actionable feedback to the developers to complement the test suite with additional test oracles, which demonstrated to improve the fault-detection effectiveness of the test suite.
Foundational Verification and Validation
Our group is currently leading work in the following areas:
Measuring and Mitigating Gaps in Structural Testing
Sponsors: This material is based in part upon work supported by the National Science Foundation under award 2129824, by the DARPA ARCOS program under contract FA8750-20-C-0507, by The Air Force Office of Scientific Research under award number FA9550-21-0164, and by Lockheed Martin Advanced Technology Laboratories.
Artifact Link: https://github.com/soneyahossain/hcc-gap-recommender
Improving Software Engineering Tools Via SMT Selection
SMT solvers are often used in the back end of different software engineering tools—e.g., program verifiers, test generators, or program synthesizers. There are a plethora of algorithmic techniques for solving SMT queries. Among the available SMT solvers, each employs its own combination of algorithmic techniques that are optimized for different fragments of logics and problem types. The most efficient solver can change with small changes in the SMT query, which makes it nontrivial to decide which solver to use. Consequently, designers of software engineering tools often select a single solver, based on familiarity or convenience, and tailor their tool towards it. Choosing an SMT solver at design time misses the opportunity to optimize query solve times and, for tools where SMT solving is a bottleneck, the performance loss can be significant.
In this work, we present Sibyl, an automated SMT selector based on graph neural networks (GNNs). Sibyl creates a graph representation of a given SMT query and uses GNNs to predict how each solver in a suite of SMT solvers would perform on said query. Sibyl learns to predict based on features of SMT queries that are specific to the population on which it is trained – avoiding the need for manual feature engineering. Once trained, Sibyl makes fast and accurate predictions which can substantially reduce the time needed to solve a set of SMT queries.
Sponsors: This material is based in part upon work supported by the National Science Foundation under award 2129824, by the DARPA ARCOS program under contract FA8750-20-C-0507, by The Air Force Office of Scientific Research under award number FA9550-21-0164, and by Lockheed Martin Advanced Technology Laboratories.
Artifact Link: https://github.com/will-leeson/sibyl
Cooperative Program Verification
Program verification is a powerful tool used to prove that safety critical software will not fail due to an unforeseen bug. However, its power comes with the trade off that it can be prohibitively expensive to run. In our group, we are developing ways to both lessen the expense of verification and enhance its precision. We are developing tools that leverage the power of existing verifiers to work in tandem and produce a more precise answer at a lesser expense. We are also creating tools that will divide a program in such a way that verification can be done in parallel and is simplified by reducing the state space tools have to reason about.
Sponsors: This effort is supported by NSF Awards #1617916 and #1901769, the U.S. Army Research Office #W911NF-19-1-0054, as well as by the DARPA ARCOS program under contract #FA8750-20-C-0507
Artifact Link: https://bitbucket.org/mgerrard/alpaca