US 12,287,726 B2
System and method for generating failing tests from failed proofs
Huang Li, Shenzen (CN); and Bertrand Meyer, Zurich (CH)
Assigned to Constructor Education and Research Genossenschaft, Schaffhausen (CH)
Filed by Constructor Technology AG, Schaffhausen (CH); and Constructor Education and Research Genossenschaft, Schaffhausen (CH)
Filed on Aug. 8, 2022, as Appl. No. 17/818,348.
Prior Publication US 2024/0045791 A1, Feb. 8, 2024
Int. Cl. G06F 11/36 (2006.01); G06F 11/3604 (2025.01); G06F 11/3668 (2025.01)
CPC G06F 11/3684 (2013.01) [G06F 11/3608 (2013.01); G06F 11/3688 (2013.01)] 20 Claims
OG exemplary drawing
 
1. A method for verifying a set of computer-executable instructions using at least one failing test generated by a test-case generator, the method comprising:
verifying the set of computer-executable instructions by a verification module using a plurality of predefined verification conditions, wherein at least one of the plurality of predefined verification conditions are associated with the execution of the set of computer-executable instructions;
determining if the verification is successful;
in response to successful verification, labeling the set of computer-executable instructions as successful; and
in response to unsuccessful verification, generating at least one counterexample, with respect to at least one proof failure and corresponding to at least one failed verification condition of the plurality of the predefined verification conditions,
wherein the at least one counterexample is a specific one or more inputs to a dataset or function of software code associated with the set of computer-executable instructions wherein at least one of the plurality of the predefined verification conditions fail and are indicative of the at least one proof failure, and generating a failing test, by a test-case generator, based on at least one counterexample including the specific one or more inputs to a dataset or function associated with the set of computer-executable instructions.