CpSc 513: Formal Verification -- 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

• Type Systems for SMT. My Ph.D. student Yan Peng has been integrating the Z3 SMT solver into the ACL2 theorem prover. Our results so far have shown this combination, Smtlink, to be very powerful and flexible. Yan should be done writing her thesis by January, and I'm sure that the “future work” section will include many great ideas, including some that can be started as a course project. In particular, the logic of ACL2 is untyped -- all functions are defined for all values of their parameters, regardless of type. On the other hand, the logic of Z3 is many sorted. Bridging the gap between the two involves showing, in ACL2, that a typed-version of a claim is logically equivalent to the original, untyped version. Topics that I expect to be available as course projects include:
  • Subtypes and refinement types. Z3 understands that integers are a subtype of the reals -- every integer is a real number. But, Z3 does not support the notion that every list of integers is a list of real numbers. Nor does it support more general subtyping. On the other hand, a theory of subtyping seems like a natural fit for SMT solvers because it involves deducing and propagating equality constraints.
  • Supporting polymorphic functions. Because ACL2 is untyped, functions are inherently polymorphic. We can often deduce a precise type signature for a function, but some functions (e.g. the basic list constructor and destructor functions cons, car, and cdr) are unavoidably polymorphic. Yan has worked out solutions for these particular functions. Can this be generalized to support general, user-defined, polymorphic functions? I believe the answer is “yes”, and that showing so would be a fun and interesting project.
  • Other ideas for supporting “type disciplines” in ACL2 (e.g.
• Concurrent Algorithms. I'm working with Margo Seltzer on her Velosity project. Can we make a synthesized/verified operating system that designs in the key issues of the 21^st century from the start: security, distributed, mobility, heterogeneity. Velosity is a large, ambitious project. If you're interested in it, I'm happy to find any piece that we can define as a course project and (if you want) springboard to a thesis topic.
• 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. A few years ago, Mark Schmidt give me a challenge problem of “Can you prove convergence for a real-world optimization algorithm using a theorem prover?” At the time, the answer was “Yes, but it's too painful to do in practice.”. The goal is to be able to start with a simple proof, and then evolve it into a proof for a highly optimized version of the algorithm. Mark points out that the literature has lots of proofs for the simple versions, but few for the algorithms that are actually used. He believes we can change this if mechanized proofs can enable proof re-use. We've made a lot of progress. We now have Smtlink, and Carl Kwan has done an amazing job of formalizing real-vector spaces and convex functions. It's time to try a proof for a real example.

  My expectation is that proofs are possible now, but that doing one will quickly point to ways we could make such proofs way easier. ACL2 has extensive support for metaprogramming. This means that once we spot common patterns in proofs from a particular domain, then we should be able to automate much of the effort. Doing the first proof on a fairly simple example is a great course project. Implementing domain specific meta-functions for reasoning about machine learning algorithms and demonstrating them on real examples would be a great thesis topic.

• Learning Proofs. Can we use learning methods to synthesize proofs? Techniques such as Version Space Algebras have been used for simple program synthesis. For proof synthesis, we have the advantage that the theorem prover is an oracle for whether or not the proposed proof is valid. Humans tend to give high-level descriptions of proofs such as “complete the square”, or “take the limit as h goes to 0” etc. Can we pick a domain, and use these human provided hints as priors to guide a proof-exploration algorithm?
• Interval Verification Algorithms. Interval Verification Algorithms provide mathematically robust results using floating-point arithmetic and directed rounding (supported in the IEEE floating point standard). The key idea is to compute results using efficient numerical algorithms and compute tight error bounds a posteriori on the results. We recently published verification of an oscillator circuit where we showed that these methods can dramatically outperform the algorithms used in state-of-the-art SMT solvers.
  • Can we generalize these methods to include inequality constraints and/or under or over constrained problems? I believe that we can by using least-squares methods to “fill in” constraints. A test of this conjecture would make a great project.
  • Can we support methods other than Krawczyk's operator? The answer is “Of course!”. The interesting part is can we do this in a systematic way. For a course project, you could explore showing applications of one or two other verification algorithms to a formal verification problem. As a M.Sc. thesis topic, you could build an interval-verification API similar to what Matlab or Numpy support, but with rigorous, proven bounds for formal verification purposes.
• 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? Or how about Frank Wood's probabilistic programming?
• Will Bowman is doing awesome work on verified compilers, dependent types, and all kinds of other things related to formal methods and software development. He told me that if I teach you how to reason about software with induction proofs, he wants you as a student. He'll have more project ideas.

  Or, you can talk with Ivan Beschastnikh, or Ron Garcia, or Alan Hu, or Karthik Pattabiraman, or Julia Rubin, or Alex Summers (arriving at UBC in March), or any of the faculty I've mentioned above. I'm sure there are other faculty here with projects ideas that would fit well in CpSc 513. I'm always happy to discuss project ideas with you.