Sorry, for being ‘missing in action’.
I was super busy organizing the first international SAT/SMT Solver summer school @ MIT from June 12th to June 17th, 2011 (I was the main organizer). It was an awesome event. We had 40 lecturers, and 225 participants. Of these 50 were professors at various American, European and Asian universities. The rest of the participants were PhD students, hackers, industrial researchers and people from Government labs.
All the slides and some videos of the lectures will be available at the summer school website soon. The talks ranged from
- Modern SAT solvers
- Modern SMT solvers (eager solvers like STP, and lazy solvers like Z3)
- Applications in interactive theorem proving, model checking of many kinds, program analysis, invariant generation and checking, synthesis, bug finding, concolic testing, automatic exploit generation, AI, etc.
- Theory talks. These were very enlightening since many participants were not theorists, and didn’t already know about these results.
What was cool about the SAT/SMT Solver summer school was that it compressed in 6 days a lot of knowledge about software engineering, allowing the audience to learn about both well-known techniques and bleeding-edge ideas. Another important feature of the summer school was its diversity: The speakers ranged from systems researchers all the way to those working in verification and programming languages. The summer school highlighted the power and utility of SAT/SMT solvers in a wide-range of settings.
The best part was that the talks were delivered by the very people who invented these high-power ideas. We had Turing award winner (2007) Ed Clarke, CAV award winners (2009) Sharad Malik, Karem Sakallah and Joao Marques-Silva, and HVC 2010 award winners Clark Barrett, Cesare Tinelli, and Leonardo DeMoura.
Sean Heelan’s blog gives a talk by talk account of the summer school. I strongly recommend it. He really has a knack for writing well.
I will get back to my blogging routine soon. Ta ta for now!!