Hello everyone! I’ve finally gotten around to making myself a website. Since Jekyll makes blogging so easy, I thought I’d give it a try.
I started working in the formal methods area about a year and a half ago. Specifically, I’ve been applying SMT solvers for various applications – primarily hardware verification. I’ve found it to be an engaging and exciting field with a very cool body of literature. That being said, there seems to be a horrifying lack of well-curated, introductory resources for formal verification. Of course, there are a few good websites and classes, but compared to a field like machine learning, there’s a relatively high barrier to entry. In other words, it’s difficult to understand right away and it’s easy to get discouraged. This could be inherent to the field, but I doubt that. At least for me, a better set of introductory materials could have dramatically improved my learning curve. I’ve spoken with other students new to the field and the consensus seems to be similar – the first year in formal methods is rough. There are several fantastic summer school programs aimed at graduate students, but it would be great to have more online resources targeting a less experienced audience.
Because of this need in the field, I have the ambitious goal of creating an introductory set of materials for model checking through this blog. My dream would be to start with basic propositional logic and work up to word-level model checking techniques. This will clearly take time – of which I don’t have enough – so in the meantime I’ve collected a few resources that I found useful for learning about formal verification and model checking. This list is biased towards seminal papers in model checking approaches to hardware (as opposed to software or hybrid systems) verification. While this is a biased choice because of my research area, this also seems reasonable as most of the initial formal verification research was for hardware. The majority of the papers on this list were suggested to me by Dr. Cristian Matterei. I’m also throwing in a couple resources for SAT and SMT.
This is by no means an exhaustive list, there are plenty of great papers and resources. If you feel that there is an important missing resource, please let me know!