Verified Human Interfaces, Control, and Learning for Semi-Autonomous Systems


VeHICaL is an NSF Cyber-Physical Systems (CPS) Frontier project that is developing the foundations of verified co-design of interfaces and control for human cyber-physical systems (h-CPS) --- cyber-physical systems that operate in concert with human operators. VeHICaL aims to bring a formal approach to designing both interfaces and control for h-CPS, with provable guarantees. The VeHICaL approach is bringing a conceptual shift of focus away from separately addressing the design of control systems and human-machine interaction and towards the joint co-design of human interfaces and control using common modeling formalisms and requirements on the entire system. This co-design approach is making novel intellectual contributions to the areas of formal methods, control theory, sensing and perception, cognitive science, security and privacy, and human-machine interfaces.

The foundational work being pursued in the VeHICaL project is being validated in two application domains: semi-autonomous ground vehicles that interact with human drivers, and semi-autonomous aerial vehicles (drones) that interact with human operators.

Overview of the VeHICaL Approach


Principal Investigators

University of California, Berkeley


Richard Murray

UNC-Chapel Hill

Cynthia Sturton




  • Using a Driver's Eye Data to Predict Accident-Causing Drowsiness Levels. Alyssa Byrnes and Cynthia Sturton. The 21st IEEE International Conference on Intelligent Transportation Systems, November 2018. Drowsy Driver Dataset.
  • HindSight: Enhancing Spatial Awareness by Sonifying Detected Objects in Real-Time 360-Degree Video. Eldon Schoop, James Smith, and Bjoern Hartmann. 2018. In Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems (CHI '18)
  • Vazquez-Chanlatte, Marcell, et al. "Logical Clustering and Learning for Time-Series Data." International Conference on Computer Aided Verification. Springer, Cham, 2017.
  • Active Preference-Based Learning of Reward Functions Dorsa Sadigh, Anca Dragan, S. Shankar Sastry, Sanjit A. Seshia Robotics: Science and Systems (RSS), July 2017.
  • Stochastic Predictive Freeway Ramp Metering from Signal Temporal Logic Specifications Negar Mehr, Dorsa Sadigh, Roberto Horowitz, S. Shankar Sastry, Sanjit A. Seshia 2017 American Control Conference (ACC), May 2017.
  • Information Gathering Actions over Human Internal State Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia, Anca Dragan IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), October 2016.
  • Towards Trustworthy Automation: User Interfaces that Convey Internal and External Awareness Tara Rezvani, Katherine Driggs-Campbell, Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia, Ruzena Bajcsy IEEE Intelligent Transportation Systems Conference (ITSC), November 2016.
  • Safe and Interactive Autonomy: Control, Learning, and Verification. Ph.D. Dissertation, EECS Department, University of California, Berkeley, 2017.
  • Systematic Testing of Convolutional Neural Networks for Autonomous Driving T. Dreossi, S. Ghosh, A. Sangiovanni-Vincentelli, S. A. Seshia Reliable Machine Learning in the Wild (RMLW 2017)
  • Compositional Falsification of Cyber-Physical Systems with Machine Learning Components T. Dreossi, A. Donzé, S. A. Seshia NASA Formal Methods (NFM 2017)
  • Datasets

  • The Visual-Acoustic Vehicle Dataset is a set of multimodal data collected from a Lincoln MKS car including vehicle sensors information, 360º image data collected from eight cameras on top of the car, and LiDAR information. Visual-Acoustic Vehicle Dataset.
  • Collaboration between:

    Supported by the National Science Foundation under the Cyber-Physical Systems program