SMT solvers are an interesting, and powerful, technology and can be leveraged as a reasoning engine in a variety of solutions. The most popular uses being symbolic execution systems, like KLEE and angr, and concolic execution/whitebox fuzzing systems, such as SAGE. Due to the nature of the technology, and the overwhelming number of academic publications on the topic, it can take a while for people to get to grips with the underlying theory, and even longer to figure out the strengths and limitations of such tools in practice.
For the above reasons, since 2013 I have taught the “Advanced Tool Development with SMT Solvers” course to students from a variety of backgrounds (you can see a high level syllabus here). It’s a fun course to teach as it’s a bit different from your usual info-sec training, and the material is constantly evolving as program analysis research progresses. While the material regularly changes, my goals for the class have remained the same: after the class students should be able to perform informed cost-benefit analysis when considering integrating SMT-backed technologies into their workflow, to use and to extend publicly available SMT-based tools, to begin to develop their own SMT-based systems, and to keep up with the published state of the art.
On to the point of this post: Bar one public version in Iceland in 2013, I have exclusively hosted private versions of this class. To do so requires organisations to have at least 6 individuals interested in the course and obviously that isn’t always possible. As a result I’ve had a number of requests for a public edition, which until now I haven’t got around to following up on! Over the summer/early fall I intend to host one or more public editions and I’m currently soliciting feedback as to where they will be. If you are interested, there is a poll here where you can let me know your location of choice (at the moment London and New York seem to be the most popular).
I’ll make a decision on the location in the next few weeks and if you’d like to be sent the details email contact@vertex.re or follow me on Twitter (@seanhn).
(If you do happen to have 6 or more people from your organisation interested in taking the course it is likely to be significantly more cost effective to organise a private, on-site training at your location. To do so email contact@vertex.re.)