Constructor Education and Research Genossenschaft

Huang Li

Bertrand Meyer

A method for verifying a set of computer-executable instructions using at least one failing test generated by a test-case generator is disclosed herein. The method comprises verifying the set of computer-executable instructions by a verification module using a plurality of predefined verification conditions; determining if the verification is successful; in response to successful verification, label the set of computer-executable instructions as successful; and in response to unsuccessful verification, generate at least one counterexample, with respect to a proof failure and corresponding to at least one failed verification condition of the plurality of the predefined verification conditions, and generate a failing test, by a test-case generator, based on at least one counterexample. A program verification tool for testing the set of computer-executable instructions is also disclosed.

Growing community of inventors

Shenzen, China

Huang Li