Computer verification of algorithms using a formal proof system. - Markus Kaiser 004 (2010)