CAV 2016 Banner

Last week, I attended the Verification Mentorship Workshop (VMW) held at CAV 2016. CAV is a conference where researchers meet to discuss their work in computer-aided verification. It is one of the top conferences in the field of formal methods and in computer science. This year it was held in Toronto, Ontario, Canada. VMW is a full-day workshop where graduate students meet junior and senior researchers and learn about the problems being adddressed by the CAV community.

The morning session of VMW focused on the major research themes in Formal Methods. Kenneth Mcmillan, from Microsoft Research, talked about model checking and the types of strategies researchers use. Nikolaj Bjorner, also from Microsoft Research and one of the creators of the Z3 theorem prover, followed with a history of SAT solvers, SMT solvers, and First-order Theorem provers. Anna Zaks, from Apple, gave a talk about how Apple uses static analysis to develop checkers and in the development of Swift. Sriram Sankaranarayanan closed the morning session with a talk on verifying cyber-physical systems.

The afternoon session focused on career management. Three researchers working in academia, a research Lab, and in industry talked about their individual career paths. Ruzica Piskac, an assistant professor at Yale, spoke about why she left industry to join academia. Arie Gurfinkel describe what it is like to conduct research at a research lab, SEI. Finally, Franjo Ivancic, told us about his experience at Google and about the importance of reviewing undergraduate computer science material for technical interviews. There was a panel session with additional researchers working at Amazon, Apple, Google, and Microsoft.

The chairs, Azadeh Farzan and Swarat Chaudhuri, finished the workshop with lessons about reviewing papers and applying for funding. In his talk, Swarat introduced me to The Heilmeier Questions:

  1. What are you trying to do? Articulate your objectives using absolutely no jargon.
  2. How is it done today? What are the limits in the current way?
  3. What is new in your approach and why do you think it will be successful??
  4. Who cares? If you are successful, what difference will it make?
  5. How much will it cost? How long will it take?

On Tuesday, Pavol Bielik gave an interesting overview of machine learning programs.

The main CAV conference took place from Wednesday through Saturday. I attended most technical research presentations. I especially enjoyed the talk gave by my lab colleague, Zhoulai Fu, titled “XSat: A Fast Floating-Point Satisfiability Solver”. In this paper, Fu and Su present a reduction from floating-point satisfiability to mathematical optimization.

Overall, my experience at VMW and CAV was enlightening. I gained a better understanding of the challenges in Formal Methods. I learned about approaches being used by researchers around the world in addressing these challenges. And I made new friends! I thank the organizers, Aarti Gupta, Ruzica Piskac, and Andrey Rybalchenko for making it possible.