Project Jumpstart

Goal. Go on a quest exploring and discovering around the topics of this course.

Process. You will develop an algorithm or a method or a tool for verifying or synthesizing systems. Then you will evaluate this algorithm / tool. To get off the starting blocks, think, Google, and answer the following questions. Stuck? Talk to your instructor. A writeup answering these questions with supporting reasoning will become your project proposal. 

Project proposal due 3/3. You can find the LaTeX template here.

A. What is the target system ? 

Examples of target systems: a robot or a vehicle, a neural network, a program, a probabilistic program, a distributed system, a multi-robot system, a circuit, and many others. 

Related questions:

A.1. Do you have a model of the system? If not, first find or create a model or simulation code. 

A.2. What is the model like? Is it a mathematical model that can be described and simulated by solving a set of equations? OR, is the model available as a piece of code like this autonomous racing framework but without an explicit mathematical model? 

B. What is the target requirement?

Examples: Vehicle does not collide and stays within the lanes, neural network produces safe outputs, program always terminates, etc.

B.1. Can the requirement be expressed as an invariant or a temporal property in terms of the variables of the model? If not, revisit A and B.

B.2. What are the primary sources of uncertainty? Example: initial conditions, inputs, model parameter variations, environmental factors like other agents and noise. 

B.3. Will your verification be about statistical or worst-case reasoning about uncertainty? In the former case, you will need to have the necessary background in Applied Probability (Markov chains, etc.) that we will not cover in this class.

C. Who else has solved similar problems?

C.1. Find the top 5 closest papers addressing similar target systems and properties. Did the papers appear in a verification, controls, or robotics conference/journal? If not, do you have the domain knowledge to create models and properties quickly? If not, this is probably not a good project for you, reconsider A, B.

C.2. How will your algorithm/tool/method improve on the previous papers? Possible answers include: usability, scalability, sample efficiency, and possibly others. 

C.3. See the Resources page for list of tools. Would you use/modify one of these tools for your project, or build your own from scratch? 

Writing your proposal/final report

You don’t have to follow the exact format, but below is an outline for your project proposal and report that might help you think about how to structure the problem.

1. Introduction

Introduction of the problem or system under study and why it is important?
Motivate the reader.

2. Problem statement

Give a clear mathematical description of your problem.

The statement needs to be very specific and accurate. Do not talk about things generally and broadly. Be precise on the exact problem you are going to solve, using rigorous mathematical language.

If you want to address a fairly complex problem, you can decompose the problem into smaller and simplified parts. Make sure the problem is feasible.

3. Related work

Related work (What has been done before? Do a thorough literature review.)

4. Methodology

Proposed methodology (what is your planned technique to solve this problem? ).

Name the tools or algorithms that may be helpful for solving your problem in your project proposal.

Discuss the algorithms and tools you used to solve your problem in the final report.

Evaluate the technical risks of your project – if the proposed methodology does not work, what are the potential causes?

5. Results

For project proposal: give your timeline and targets (what goals do you aim to achieve? what are the deliverables?)

For final report: report your findings and summarize your results.

In general, your final report should look similar to an academic paper published at a first-tier conference or journal.
In our class, you have been assigned several papers to read. Your final report should look similar to these papers you have read.

Some project directions

Below are some high-level directions for potential course projects:

1. Verifying neural network controlled hybrid systems

As you will learn in a few lectures, a hybrid system is a very general and explicit mathematical modeling framework that combines computation and physics (A.1). There are several existing tools verifying hybrid systems like C2E2, HyLAA, DryVR, Flow*, and SpaceEx. Typically these tools handle invariant and temporal logic requirements (B.1). However, these tools are not specialized in handling hybrid systems with neural network controllers. On the other hand, specialized neural network verifiers such as α,β-CROWN, or Marabou perform well for problems with pure network, and their combination with cyber physical systems still has a large room for improvement. Your project will include extending existing tools, potentially with new algorithms, to enable verification of neural network controlled hybrid CPS.

2. Improve the scalability, expressivity, and precision of verification systems for machine learning

The emerging application of machine learning poses a great challenge for verification. Unlike well-established fields such as SAT/SMT solving, there are many open problems in the formal verification problems involving machine learning systems (such as deep neural networks and gradient boosted decision trees). In this course, we will cover the basic algorithms used in the state-of-the-art α,β-CROWN neural network verifier. Your project will include developing and implementing a new algorithm that improves the scalability (faster on larger models), expressivity (better support for realistic verification settings), and precision (such as floating point soundness).

3. Verifying controller for autonomous vehicle. 

Your system could be a controlled autonomous  vehicle in a simulated environment (A.1). A number of which are now available for free F1/10, GRAIC, Gazebo, CARLA, FlightGoggles, AirSim, CommonRoad, Waymax. To work with these simulators you may need access to a high-end workstation with GPUs. Check the simulator minimum system requirements.  In most cases, you will not have an explicit model of the vehicle (A.2), and you might have the model/code for the controller. B.1. The system’s requirements can be the obvious ones like collision avoidance, but you can also add more nuanced requirements like passenger comfort. There are many many papers related to controller design for vehicles in simulated environments. Verification of these systems (with incomplete models) is a hot topic. You may want to look at simulation-driven verification approaches like DryVR.

4. Verification case studies

Choose a benchmark model from existing literature or benchmark suite and an appropriate tool, and verify the benchmark. This project will provide you a deep understanding of both the application domain and the tool, and it could lead to formulation of new theoretical questions.

The two choices—tool and model—of course, do not completely determine the verification process, and therefore, the outcome of the case study. Your creativity will be needed in formulating the verification problem in the tool (e.g., do you check invariants? Do you create abstractions? and refinements, etc.). Consequently, the ideal outcome of a case study is not a binary answer—but an analysis and evaluation of your design decisions, the algorithms, and the tool. 

Some notable course projects from previous years

(Note: UIUC network access is needed for accessing some of the reports because they were hosted at UIUC internal servers)

Checking Assumptions in Probabilistic Programs, Zixin Huang, 2019. report, presentation, 

Controller synthesis for cyber-physical systems, Kristina Miller, 2019, presentation, report, related publication 1, 2.

Optimistic optimization for statistical model checking, Dawei Sun, 2019, report, related publication

Learning models from simulation data, Yangge Li, 2019, presentation, report.

Exploiting symmetries for efficient verification, Navid Mokhlesi, 2019, paper. report, presentation, related publication.

Using K framework for hybrid systems, Nishant Rodrigues, 2019.

Black-box optimization for verification, Sung-Woo Jeon, 2019.

Efficient verification of neural networks and some performance boosting heuristics, Chen, 2017, proposal, report.

Probabilistic reasoning for networks using PRISM and Bayonet, Dutta, 2017, proposal, report.

DryVR for model-free hybrid system verification, Qi, 2017, report.

Consensus and flocking algorithms in C2E2, Peña, 2017, proposal, report.

Modeling game of life cellular automata in PVS, Walker, 2017, report.

Modeling and verification of probabilistic systems in Maude, Hildenbrandt, 2017, report.

Reachability analysis of mobile robots in polygons with SpaceEx, Nilles, 2017, report.

An iterative method for proving safety of nonlinear systems, Ahmadyan and Mancuso, 2016.

Programming stabilizing distributed robot swarms, Zimmerman, 2016.

Bounded verification with on-the-fly discrepancy computation, Fan, 2014.