20240045791. System and method for generating failing tests from failed proofs simplified abstract (Rolos AG)
Contents
System and method for generating failing tests from failed proofs
Organization Name
Inventor(s)
Stanislav Protasov of Singapore (SG)
Nikolay Dobrovolskiy of Moscow (RU)
System and method for generating failing tests from failed proofs - A simplified explanation of the abstract
This abstract first appeared for US patent application 20240045791 titled 'System and method for generating failing tests from failed proofs
Simplified Explanation
The abstract describes a method for verifying a set of computer-executable instructions using failing tests generated by a test-case generator. The method involves verifying the instructions using predefined verification conditions, determining the success of the verification, labeling the instructions as successful if the verification is successful, and generating counterexamples and failing tests if the verification is unsuccessful. A program verification tool for testing the instructions is also disclosed.
- The method verifies computer-executable instructions using predefined verification conditions.
- If the verification is successful, the instructions are labeled as successful.
- If the verification is unsuccessful, counterexamples and failing tests are generated.
- The counterexamples correspond to proof failures and failed verification conditions.
- The failing tests are generated by a test-case generator based on the counterexamples.
- A program verification tool is provided for testing the instructions.
Potential applications of this technology:
- Software development and testing: This method can be used to verify the correctness of computer-executable instructions, ensuring that they behave as intended.
- Quality assurance: By generating failing tests and counterexamples, this method can help identify and fix bugs or errors in computer-executable instructions.
- Formal verification: The predefined verification conditions and the ability to generate counterexamples make this method suitable for formal verification of software systems.
Problems solved by this technology:
- Verification of computer-executable instructions: This method provides a systematic approach to verify the correctness of instructions, identifying any proof failures or failed verification conditions.
- Bug detection: By generating failing tests and counterexamples, this method helps in detecting bugs or errors in computer-executable instructions, allowing for their resolution.
- Efficiency in verification: The use of a test-case generator and predefined verification conditions improves the efficiency of the verification process, reducing the manual effort required.
Benefits of this technology:
- Improved software reliability: By verifying computer-executable instructions and generating failing tests, this method helps in improving the reliability and correctness of software systems.
- Time and cost savings: The automated verification process and the generation of failing tests reduce the time and cost involved in manual testing and bug fixing.
- Enhanced development process: The use of a program verification tool and predefined verification conditions streamlines the development process, ensuring that instructions are thoroughly tested and validated.
Original Abstract Submitted
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.
