EECS 219C Suggested Projects

• Diagnosing the Root Cause in an Error Trace: Model checkers and debuggers often generate a very long counterexample trace which starts in an initial state and ends in a error state (or error infinite loop). However, to fix the circuit/program, we really need to locate the few points in the trace where something went wrong.

  Problem: Come up with a semi-automatic strategy for error localization in error traces. This could involve building a visualization tool as a front-end that allows the user to query various parts of the error trace. The back-end would be an optimization engine that solves a constraint problem to locate the fewest points in the trace at which a different system action could have avoided the error.

  Note: Bryan Brady will be the mentor for this project, which will be conducted with the UCLID verification system.

• All-SAT Solver: An all-SAT solver is a Boolean satisfiability solver that generates not just one satisfying solution, but all of the solutions. The set of these solutions are typically representated as a Boolean function (e.g., as a BDD). Such a solver finds many applications, including SAT-based model checking and abstraction (predicate abstraction).

  Problem: Write an all-SAT solver that improves over the state-of-the-art over some problems. Circuit minimization techniques might be useful to optimize the size of the Boolean function representing the set of solutions.

• Interface Generation for Real-Time Systems: Techniques for automatically generating a interface specifications for finite-state systems from execution traces and program descriptions have been recently explored. These are based on machine learning of finite automata from traces. However, similar techniques are yet to be fully explored for real-time systems.

  Problem: The simplest form of timing constraint is a partial order between events. Last year, a group of 219C students came up with an algorithm for learning partial orders between events from event traces (from simulations or executions). Their paper will appear at DATE this year. You can start with their work and apply it to an entirely new application area. One possibility is generating real-time interface specifications -- the assumptions that a system has about the real-time behavior of its environment.
   

• Analyzing Correctness and Timeliness of Finite-State Systems with Queues : Motivation: Many concurrent systems can be formally modeled as finite-state systems communicating through queues. Examples include network packet processing systems, automotive systems, and the "transactor" model for multi-processor designs. Many of these systems must attain high performance and/or reliability standards.

  Research Plan: The project must address the following questions. What is the right modeling formalism for this class of systems? How are timing properties best specified and verified? We can foresee at least three challenging problems. The first is that of state-space explosion, which will necessitate the use of techniques such as abstraction and compositional reasoning. Secondly, finite-state sub-systems might not share the same clock, thereby requiring novel ways to model them and specify real-time properties, possibly using relative timing assumptions. Thirdly, many system properties are likely to be highly data-dependent, which, for efficiency reasons, could need models that are higher-level than just Boolean models.

• Verifying FLEET Programs: FLEET is a one-instruction computer, where that one instruction is "MOVE." Click here for more documentation on FLEET. This project has been proposed by Ivan Sutherland.

  Problem: FLEET programs are extremely concurrent, where instructions are organized in bags without imposing conventional sequencing. The problem with that added concurrency is that some orderings of instructions generate wrong programs. The goal of this project is to adapt current automated verification tools and techniques to verify FLEET programs.

• Model Checking Security Properties: Problem: Identify and analyze an interesting subset of security properties that existing software model checkers (e.g., MOPS, Blast) have not been used for, or a significant new code base that those model checkers have not been used on. This project can be combined with a "MOPS++" project that Daniel Wilkerson has proposed. Click here for Daniel's description of the project and background.
   
• Owner/Surfer Analysis with SAT: Problem (suggested by Daniel Wilkerson ): Click here for Daniel's description of the project and background.