CpSc 583G: Formal Verification and Analysis -- Project Ideas

Here, I describe my expectations for a project, and suggest some possible ideas for projects. If you have an idea of what you'd like to pursue for a project, that's great. Look at this list for ideas, and feel free to talk with me and we can brainstorm to find a fun and interesting project.

Basic Expectations for a Project

The goal of the project is for you to go a bit deeper into some aspect of formal verification than what we covered in class. A realistic project should take about 40-60 hours of your time -- a term is 14 weeks; a 3 credit course should be about 9 hours/week of total work; the project is 40% of your grade, that works out to (14 weeks) *(9 hours/week) *.4 = 50.4 hours.

The final product of your project is a report. If you're a M.Sc. student, this report should be a M.Sc. thesis proposal. You're not obligated to do your M.Sc. with me, it's practice for formulating a thesis proposal no matter who you end up choosing to work with. Of course, if you're project leads to our working together, I'll be happy with that as well, but it's not required, and it's certainly not part of your grade. As such, the proposal should:

State the problem you are addressing.
Include a literature review (4-6 papers, more is fine) showing what has been done previously and why your proposed approach is new.
A description of how you plan to address the problem -- this is a draft thesis statement. Ideally, in 30 words or less, what are you contributing that hasn't been done before.
A schedule with milestones.
A description of any special resources that you'll need: software packages, special hardware, access to data or design information from industry, human volunteers to assess a new tool, etc.
Identify the main risks in the research. Research is new. What part of the proposal depends on something that might not work? What is your “plan B”

Typically, a project will include a proof-of-concept implementation of the main idea that you will try on a few examples and report the results. This shows that the basic idea is feasible. It also means that you'll have the experience of doing something with formal methods that goes beyond what we cover in the homework assignments.

I will also consider projects that are primarily a literature survey or address a theoretical aspect of formal methods using paper-and-pencil proofs. A literature survey project will be much more extensive in the papers that it covers (e.g.\ 15-20 papers) and should present them in an organized, coherent way, for example, putting forward a taxonomy of the research approaches and results. If you want to do a literature survey or theory project, please talk to me first.

I am sometimes asked if a team or partner project is acceptable. Yes, but only if there is a really good reason for it. I prefer to avoid projects where student X depends on student Y to pass. If the team or partner project can be divided into separate projects (at least from an evaluation perspective), then I strongly prefer that. Otherwise, the project needs to clearly state who is responsible for what, and the milestones and dependencies make sure that each member of the team has a clear path to success.

Some Project Ideas

This is just a list of some ideas I've been thinking about. Formal methods connect to pretty much any area in computer science, robotics, control, hardware design, and many other areas. If you already have an idea, that's great. If you don't see what you're looking for, let's discuss it. I'm always happy to discuss project ideas.

Buffer overflow checks. Buffer overflows are responsible for a large number of security exploits. While C and C++ don't provide built-in array bounds checking, in most cases, the reason that the bounds are safe is fairly “local” or else the code is wrong. What is the state-of-the-art in this area? Can we do better? What can be done by fully automatic methods? For security critical code, could we expect the programmer to add a few annotations to their code to make checking possible? What should these annotations be?

Exception handling. Many bugs, especially in distributed systems, arise from errors in exceptions handlers. Exception handlers are often seen has hard to test, and therefore end-up with inadequate tests. When a minor error occurs, a bug in an untested exception handler can make it much worse. Can we use formal methods to better exercise exception handlers and find errors? Can we find the errors by some kind of static analysis? What is the state-of-the-art in this area? Can we do better?

Machine Learning Algorithms. Convex optimization algorithms are used extensively in machine learning. Details of the algorithms can have a large impact on performance, but the reasoning often involves complicated, tedious proofs. Can we simplify this using symbolic algebra packages (such as Maple or Sympy), or using SMT solvers (such as Z3), or theorem provers (such as ACL2)? I'm working on this with Mark Schmidt, and I'm sure we can find aspects of this work that would make a great course project.

SMT for monotonic functions. SMT solvers such as Z3 can do amazing things, but they also are up against exponential complexity for some of the decision procedures, and the procedure for polynomial arithmetic has worst-case doubly-exponential time! Often, we know that a function is monotonic which provides us with opportunities to simplify the reasoning. Monotonic functions are invertible, and that suggests that we can eliminate. How does this interact with the quantifier-elimination methods used in Z3 and other SMT solvers? How can we exploit monotonicity efficiently?

SMT for probabilistic AI. Can we use SMT techniques to implement a more efficient solvers for logics such as David Poole's Independent Choice Logic?
Adding a richer type system to Smtlink. Yan Peng has implemented an interface that allows proofs in the ACL2 theorem prover to use the Z3 SMT solver. We have used this primarily for reasoning about polynomial inequalities. Z3 offers many other decision procedures including support for algebraic data types such as lists, trees, and unions. ACL2 has a library for such types. Can we connect them? Can we use such a connection to simplify proofs about type-correctness of specifications and models written in ACL2?
Learning when to use a solver. SAT and SMT solvers are great, until the problem gets too big to solve with a practical amount of time and memory. A common “noob” mistake is to tell the solver “everything you know” and see if it can solve the problem. This works fine for small problems, but can choke the solver for realistic problems. Can we use ML techniques to identify the relevant facts to give to the solver? Can we automatically identify when a clause is a good candidate for automatic solution? Can ML techniques automatically suggest simplifications?
Model Checking clock-domain crossings. This one is for the hardware people. Logical equivalence checking, property checking, and model checking have done an amazing job of finding bugs in single-clock-domain modules before chip fabrication. Bugs can still creep-in at the system level. Clock-domain crossing protocols are often designed making assumptions about the relative frequencies of the clocks (e.g. the sender is slower than the receiver, or …). Can we document these assumptions with Verilog assertions and use model-checking to show that the assumptions are guaranteed to hold? with

This list is just a sample. Many more ideas are available on request. ☺
Just ask. Feel free to let me know what area of theory or application appeals to you.

Last modified (GMT)