Naoki Kobayashi: Program Certification by Higher-Order Model Checking. CPP 2012: 9-10