We introduce a novel notion of perception contracts to reason about the safety of controllers that interact with an environment using neural perception. Perception contracts capture errors in ground-truth estimations that preserve invariants when systems act upon them. We develop a theory of perception contracts and design symbolic learning algorithms for synthesizing them from a finite set of images. We implement our algorithms and evaluate synthesized perception contracts for two realistic vision-based control systems, a lane tracking system for an electric vehicle and an agricultural robot that follows crop rows. Our evaluation shows that our approach is effective in synthesizing perception contracts and generalizes well when evaluated over test images obtained during runtime monitoring of the systems.

We present an approach to learn contracts for object-oriented programs where guarantees of correctness of the contracts are made with respect to a test generator. Our contract synthesis approach is based on a novel notion of tight contracts and an online learning algorithm that works in tandem with a test generator to synthesize tight contracts. We implement our approach in a tool called Precis and evaluate it on a suite of programs written in C#, studying the safety and strength of the synthesized contracts, and compare them to those synthesized by Daikon.

Flaky tests are tests that can non-deterministically pass and fail. They pose a major impediment to regression testing, because they provide an inconclusive assessment on whether recent code changes contain faults or not. Prior studies of flaky tests have proposed tools to detect flaky tests and identified various sources of flakiness in tests, e.g., order-dependent (OD) tests that deterministically fail for some order of tests in a test suite but deterministically pass for some other orders. Several of these studies have focused on OD tests. We focus on an important and under-explored source of flakiness in tests: non-order-dependent tests that can nondeterministically pass and fail even for the same order of tests. Instead of using specialized tools that aim to detect flaky tests, we run tests using the tool configured by the developers. Specifically, we perform our empirical evaluation on Java projects that rely on the Maven Surefire plugin to run tests. We re-execute each test suite 4000 times, potentially in different test-class orders, and we label tests as flaky if our runs have both pass and fail outcomes across these reruns. We obtain a dataset of 107 flaky tests and study various characteristics of these tests. We find that many tests previously called “non-order-dependent” actually do depend on the order and can fail with very different failure rates for different orders.

Cyber-physical software delivers context-aware services through continually interacting with its physical environment and adapting to the changing surroundings. However, when the software's assumptions on the environment no longer hold, the interactions can introduce errors for leading to unexpected behaviors and even system failures. One promising solution to this problem is to conduct runtime monitoring of invariants. Violated invariants reflect latent erroneous states (i.e., abnormal states that could lead to failures). In turn, monitoring when program executions violate the invariants can allow the software to take alternative measures to avoid danger. In this article, we present context-based Multiinvariant detection (CoMID), an approach that automatically infers invariants and detects abnormal states for cyber-physical programs. CoMID consists of two novel techniques, namely context-based trace grouping and multiinvariant detection. The former infers contexts to distinguish different effective scopes for CoMID's derived invariants, and the latter conducts ensemble evaluation of multiple invariants to detect abnormal states during runtime monitoring. We evaluate CoMID on real-world cyber-physical software. The results show that CoMID achieves a 5.7-28.2% higher true-positive rate and a 6.8-37.6% lower false-positive rate in detecting abnormal states, as compared with the existing approaches. When deployed in field tests, CoMID's runtime monitoring improves the success rate of cyber-physical software in its task executions by 15.3-31.7%.

Enrollment in introductory programming (CS1) courses continues to surge and hundreds of CS1 students can produce thousands of submissions for a single problem, all requiring timely and accurate grading. One way that instructors can efficiently grade is to construct a custom instructor test suite that compares a student submission to a reference solution over randomly generated or hand-crafted inputs. However, such test suite is often insufficient, causing incorrect submissions to be marked as correct. To address this issue, we propose the Grasa (GRAding-based test Suite Augmentation) approach consisting of two techniques. Grasa first detects and clusters incorrect submissions by approximating their behavioral equivalence to each other. To augment the existing instructor test suite, Grasa generates a minimal set of additional tests that help detect the incorrect submissions. We evaluate our Grasa approach on a dataset of CS1 student submissions for three programming problems. Our preliminary results show that Grasa can effectively identify incorrect student submissions and minimally augment the instructor test suite.

In this paper, we present a novel learning framework for inferring stateful preconditions (i.e., preconditions constraining not only primitive-type inputs but also non-primitive-type object states) modulo a test generator, where the quality of the preconditions is based on their safety and maximality with respect to the test generator. We instantiate the learning framework with a specific learner and test generator to realize a precondition synthesis tool for C#. We use an extensive evaluation to show that the tool is highly effective in synthesizing preconditions for avoiding exceptions as well as synthesizing conditions under which methods commute.

When tests fail (e.g., throwing uncaught exceptions), automatically inferred preconditions can bring various debugging benefits to developers. If illegal inputs cause tests to fail, developers can directly insert the preconditions in the method under test to improve its robustness. If legal inputs cause tests to fail, developers can use the preconditions to infer failure-inducing conditions. To automatically infer preconditions for better support of debugging, in this paper, we propose PREINFER, a novel approach that aims to infer accurate and concise preconditions based on symbolic analysis. Specifically, PREINFER includes two novel techniques that prune irrelevant predicates in path conditions collected from failing tests, and that generalize predicates involving collection elements (i.e., array elements) to infer desirable quantified preconditions. Our evaluation on two benchmark suites and two real-world open-source projects shows PREINFER's high effectiveness on precondition inference and its superiority over related approaches.

Dynamic Symbolic Execution (DSE) is among the most effective techniques for structural test generation, i.e., test generation to achieve high structural coverage. Despite its recent success, DSE still suffers from various problems such as the boundary problem when applied on various programs in practice. To assist problem diagnosis for structural test generation, in this paper, we propose a visualization approach named PexViz. Our approach helps the tool users better understand and diagnose the encountered problems by reducing the large search space for problem root causes by aggregating information gathered through DSE exploration.