John Regehr described the “correctness argument” in this paper in his blog post Who verifies the verifiers?.
Eliminating stack overflow by abstract interpretation
John Regehr, Alastair D. Reid, Kirk Webb[doi] [Google Scholar] [DBLP] [Citeseer]
Embedded Software, Third International Conference (EMSOFT 2003)
Lecture Notes in Computer Science, volume 2855
Philadelphia, PA, USA
Springer
Pages 306-322
13-15 October 2003
Note(s): abstract interpretation, ISA specification
Lecture Notes in Computer Science, volume 2855
Philadelphia, PA, USA
Springer
Pages 306-322
13-15 October 2003
Note(s): abstract interpretation, ISA specification