14% of SV-COMP’s “Correct Programs” are Undefined!

Capture

Last April (2016), I gave a tutorial on K at ETAPS'16 in Eindhoven, Netherlands, where I also demonstrated RV-Match.  During the week that I spent there, I heard several friends and colleagues who were involved with the Competition on Software Verification, SV-COMP, that some of the benchmark's correct programs appear to be undefined.  What?  So some of the assumed-correct C programs that are used to evaluate the best program verifiers in the world are actually wrong programs? Continue reading