At Google, fuzzing C/C++ libraries has discovered tens of thousands of security and robustness bugs. However, these bugs are often reported much after they were introduced. Developers are provided only with fault-inducing test inputs and replication instructions that highlight a crash, but additional debugging information may be needed to localize the cause of the bug. Hence, developers need to spend substantial time debugging the code and identifying commits that introduced the bug. In this paper, we discuss our experience with automating a fuzzing-enabled bisection that pinpoints the commit in which the crash first manifests itself. This ultimately reduces the time critical bugs stay open in our code base. We report on our experience over the past year, which shows that developers fix bugs on average 2.23 times faster when aided by this automated analysis.

We present VerifAI , a software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components. VerifAI particularly addresses challenges with applying formal methods to ML components such as perception systems based on deep neural networks, as well as systems containing them, and to model and analyze system behavior in the presence of environment uncertainty. We describe the initial version of VerifAI , which centers on simulation-based verification and synthesis, guided by formal models and specifications. We give examples of several use cases, including temporal-logic falsification, model-based systematic fuzz testing, parameter synthesis, counterexample analysis, and data set augmentation.

We consider the problem of learning structured, closed-loop policies (feedback laws) from demonstrations in order to control under-actuated robotic systems, so that formal behavioral specifications such as reaching a target set of states are satisfied. Our approach uses a “counterexample-guided” iterative loop that involves the interaction between a policy learner, a demonstrator and a verifier. The learner is responsible for querying the demonstrator in order to obtain the training data to guide the construction of a policy candidate. This candidate is analyzed by the verifier and either accepted as correct, or rejected with a counterexample. In the latter case, the counterexample is used to update the training data and further refine the policy.The approach is instantiated using receding horizon model-predictive controllers (MPCs) as demonstrators. Rather than using regression to fit a policy to the demonstrator actions, we extend the MPC formulation with the gradient of the cost-to-go function evaluated at sample states in order to constrain the set of policies compatible with the behavior of the demonstrator. We demonstrate the successful application of the resulting policy learning schemes on two case studies and we show how simple, formally-verified policies can be inferred starting from a complex and unverified nonlinear MPC implementations. As a further benefit, the policies are many orders of magnitude faster to implement when compared to the original MPCs.

We present an approach to path following using so-called control funnel functions. Synthesizing controllers to “robustly” follow a reference trajectory is a fundamental problem for autonomous vehicles. Robustness, in this context, requires our controllers to handle a specified amount of deviation from the desired trajectory. Our approach considers a timing law that describes how fast to move along a given reference trajectory and a control feedback law for reducing deviations from the reference. We synthesize both feedback laws using “control funnel functions” that jointly encode the control law as well as its correctness argument over a mathematical model of the vehicle dynamics. We adapt a previously described demonstration-based learning algorithm to synthesize a control funnel function as well as the associated feedback law. We implement this law on top of a 1/8th scale autonomous vehicle called the Parkour car. We compare the performance of our path following approach against a trajectory tracking approach by specifying trajectories of varying lengths and curvatures. Our experiments demonstrate the improved robustness obtained from the use of control funnel functions.

We investigate the problem of synthesizing robust controllers that ensure that the closed loop satisfies an input reach-while-stay specification, wherein all trajectories starting from some initial set I, eventually reach a specified goal set G, while staying inside a safe set S. Our plant model consists of a continuous-time switched system controlled by an external switching signal and plant disturbance inputs. The controller uses a state feedback law to control the switching signal in order to ensure that the desired correctness properties hold, regardless of the disturbance actions.

In this project, we address the problem of synthesizing region-stabilizing controllers for switched systems. The plant model consists of a continuous-time switched system with finitely many switching modes. Our approach searches for a state-feedback that chooses between finitely many switching modes at each time instant: (a) guaranteeing a minimum dwell time between mode changes and (b) region stabilizing to a suitably small set around a given state.

This paper presents a controller synthesis approach using disjunctive polyhedral abstract interpretation. Our approach synthesizes infinite time-horizon controllers for safety properties with discrete-time, linear plant model and a switching feedback controller that is suitable for time-triggered implementations. The core idea behind our approach is to perform an abstract interpretation over disjunctions of convex polyhedra to identify states that are potentially uncontrollable. Complementing this set yields the set of controllable states, starting from which, the safety property can be guaranteed by an appropriate controller feedback function. Since, a straightforward disjunctive domain is computationally inefficient, we present an abstract domain based on a state partitioning scheme that allows us to efficiently control the complexity of the intermediate representations. Next, we focus on the automatic generation of controller implementation from the abstract interpretation results. We show that a balanced tree approach can yield efficient controller code with guarantees on the worst-case execution time. Finally, we evaluate our approach on a suite of benchmarks, comparing different instantiations with related synthesis tools. The evaluation shows that our approach can successfully synthesize controller implementations for small to medium sized benchmarks.