research
∙
07/19/2023
Learning Formal Specifications from Membership and Preference Queries
Active learning is a well-studied approach to learning formal specificat...
share
research
∙
07/06/2023
3D Environment Modeling for Falsification and Beyond with Scenic 3.0
We present a major new version of Scenic, a probabilistic programming la...
research
∙
06/01/2023
Genetic Algorithms for Searching a Matrix of Metagrammars for Synthesis
Syntax-guided synthesis is a paradigm in program synthesis in which the ...
research
∙
05/27/2023
Context-Aided Variable Elimination for Requirement Engineering
Deriving system-level specifications from component specifications usual...
research
∙
03/31/2023
Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design
Contract-based design is a method to facilitate modular system design. W...
research
∙
03/29/2023
Specification-Guided Data Aggregation for Semantically Aware Imitation Learning
Advancements in simulation and formal methods-guided environment samplin...
research
∙
02/27/2023
A Grammar for the Representation of Unmanned Aerial Vehicles with 3D Topologies
We propose a context-sensitive grammar for the systematic exploration of...
research
∙
12/06/2022
Emerging Technology and Policy Co-Design Considerations for the Safe and Transparent Use of Small Unmanned Aerial Systems
The rapid technological growth observed in the sUAS sector over the past...
research
∙
11/03/2022
Verifying RISC-V Physical Memory Protection
We formally verify an open-source hardware implementation of physical me...
research
∙
09/30/2022
Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing
Hardware enclaves rely on a disjoint memory model, which maps each physi...
research
∙
08/13/2022
Automated Conversion of Axiomatic to Operational Models: Theory and Practice
A system may be modelled as an operational model (which has explicit not...
research
∙
08/07/2022
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
UCLID5 is a tool for the multi-modal formal modeling, verification, and ...
research
∙
03/04/2022
DEC-LOS-RRT: Decentralized Path Planning for Multi-robot Systems with Line-of-sight Constrained Communication
Decentralized planning for multi-agent systems, such as fleets of robots...
research
∙
12/20/2021
Demonstration Informed Specification Search
This paper considers the problem of learning history dependent task spec...
research
∙
10/28/2021
A Scenario-Based Platform for Testing Autonomous Vehicle Behavior Prediction Models in Simulation
Behavior prediction remains one of the most challenging tasks in the aut...
research
∙
08/20/2021
Addressing the IEEE AV Test Challenge with Scenic and VerifAI
This paper summarizes our formal approach to testing autonomous vehicles...
research
∙
08/16/2021
Synthesizing Pareto-Optimal Interpretations for Black-Box Models
We present a new multi-objective optimization approach for synthesizing ...
research
∙
07/28/2021
Satisfiability and Synthesis Modulo Oracles
In classic program synthesis algorithms, such as counterexample-guided i...
research
∙
07/09/2021
Parallel and Multi-Objective Falsification with Scenic and VerifAI
Falsification has emerged as an important tool for simulation-based veri...
research
∙
06/18/2021
Scenic4RL: Programmatic Modeling and Generation of Reinforcement Learning Environments
The capability of reinforcement learning (RL) agent directly depends on ...
research
∙
05/26/2021
Hypercontracts
Contracts (or interface) theories have been proposed to formally support...
research
∙
05/26/2021
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference
We revisit the symbolic verification of Markov chains with respect to fi...
research
∙
05/26/2021
Runtime Monitoring for Markov Decision Processes
We investigate the problem of monitoring partially observable systems wi...
research
∙
10/13/2020
Scenic: A Language for Scenario Specification and Data Generation
We propose a new probabilistic programming language for the design and a...
research
∙
09/30/2020
Co-design of Control and Planning for Multi-rotor UAVs with Signal Temporal Logic Specifications
Urban Air Mobility (UAM), or the scenario where multiple manned and Unma...
research
∙
09/01/2020
A Review of Single-Source Deep Unsupervised Visual Domain Adaptation
Large-scale labeled training datasets have enabled deep neural networks ...
research
∙
08/21/2020
SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating System
We present an implementation of SOTER, a run-time assurance framework fo...
research
∙
07/20/2020
SynRG: Syntax Guided Synthesis of Expressions with Alternating Quantifiers
Program synthesis is the task of automatically generating expressions th...
research
∙
07/14/2020
Synthesis in Uclid5
We describe an integration of program synthesis into Uclid5, a formal mo...
research
∙
07/13/2020
Gradient Descent over Metagrammars for Syntax-Guided Synthesis
The performance of a syntax-guided synthesis algorithm is highly depende...
research
∙
07/07/2020
Learning Branching Heuristics for Propositional Model Counting
Propositional model counting or #SAT is the problem of computing the num...
research
∙
06/30/2020
Enforcing Almost-Sure Reachability in POMDPs
Partially-Observable Markov Decision Processes (POMDPs) are a well-known...
research
∙
05/14/2020
Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
We demonstrate a unified approach to rigorous design of safety-critical ...
research
∙
03/17/2020
Formal Scenario-Based Testing of Autonomous Vehicles: From Simulation to the Real World
We present a new approach to automated scenario-based testing of the saf...
research
∙
11/07/2019
Modularity in Query-Based Concept Learning
We define and study the problem of modular concept learning, that is, le...
research
∙
11/04/2019
Real-time Funnel Generation for Restricted Motion Planning
In autonomous systems, a motion planner generates reference trajectories...
research
∙
11/04/2019
Counterexample-Guided Synthesis of Perception Models and Control
We consider the problem of synthesizing safe and robust controllers for ...
research
∙
10/13/2019
On the Utility of Learning about Humans for Human-AI Coordination
While we would like agents that can coordinate with humans, current algo...
research
∙
07/26/2019
Learning Task Specifications from Demonstrations via the Principle of Maximum Causal Entropy
In many settings (e.g., robotics) demonstrations provide a natural way t...
research
∙
05/31/2019
Understanding and Extending Incremental Determinization for 2QBF
Incremental determinization is a recently proposed algorithm for solving...
research
∙
03/24/2019
A Formalization of Robustness for Deep Neural Networks
Deep neural networks have been shown to lack robustness to small input p...
research
∙
03/22/2019
A Model Counter's Guide to Probabilistic Systems
In this paper, we systematize the modeling of probabilistic systems for ...
research
∙
02/27/2019
A New Simulation Metric to Determine Safe Environments and Controllers for Systems with Unknown Dynamics
We consider the problem of extracting safe environments and controllers ...
research
∙
02/12/2019
VERIFAI: A Toolkit for the Design and Analysis of Artificial Intelligence-Based Systems
We present VERIFAI, a software toolkit for the formal design and analysi...
research
∙
09/25/2018
Scenic: Language-Based Scene Generation
Synthetic data has proved increasingly useful in both training and testi...
research
∙
09/07/2018
Cloud-based Quadratic Optimization with Partially Homomorphic Encryption
The development of large-scale distributed control systems has led to th...
research
∙
08/23/2018
SOTER: Programming Safe Robotics System using Runtime Assurance
Autonomous robots increasingly depend on third-party off-the-shelf compo...
research
∙
07/20/2018
Learning Heuristics for Automated Reasoning through Deep Reinforcement Learning
We demonstrate how to learn efficient heuristics for automated reasoning...
research
∙
05/17/2018
Counterexample-Guided Data Augmentation
We present a novel framework for augmenting data sets for machine learni...
research
∙
04/19/2018