# US 2024/0202098 A1 · Static analysis for sound interleaving pruning in enumerative model checking > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 2024/0202098 A1 - Document ID: US20240202098A1 - Status: Published application - Kind: A1 - Application number: 18/082,676 - Filed: 2022-12-16 - Published: 2024-06-20 - Earliest claimed: 2022-12-16 - Assignees: Technology Innovation Institute - Sole Proprietorship LLC - Applicants: Technology Innovation Institute - Sole Proprietorship LLC - Inventors: Ridhi Jain - Web page: https://patentgrep.com/patent/US20240202098A1 ## CPC - G06F 11/3608: {using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013)} - G06F 11/3676: {for coverage analysis} - G06F 11/3688: {for test execution, e.g. scheduling of test suites} - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract An example embodiment includes a method for model checking a program. The method includes performing, by a processor, static analysis of source code of the program to inductively determine at least one invariant present in interleavings of by the program, and performing, by the processor, static instrumentation of the source code of program to generate an instrumented equivalent version of the program. The instrumented equivalent version of the program comprises locks to avoid execution of a subset of the interleavings corresponding to the at least one invariant. The instrumented equivalent version of the program is configured for enumerative model checking that avoids execution of the subset of the interleavings. ## Claims ### Claim 1 A method for model checking a program, the method including: performing, by a processor, static analysis of source code of the program to inductively determine at least one invariant present in interleavings of the program; and performing, by the processor, static instrumentation of the source code of program to generate an instrumented equivalent version of the program, the instrumented equivalent version of the program comprising locks to avoid execution of a subset of the interleavings corresponding to the at least one invariant, wherein the instrumented equivalent version of the program is configured for enumerative model checking that avoids execution of the subset of the interleavings. ### Claim 2 (depends on 1) The method of claim 1, further comprising: positioning, by the processor, the locks in the source code to avoid execution of a redundant subset of the interleavings during the enumerative model checking. ### Claim 3 (depends on 2) The method of claim 2, further comprising: executing, by the processor, the enumerative model checking of at least one interleaving of the redundant subset of the interleavings, while avoiding remaining interleavings of the redundant subset of the interleavings. ### Claim 4 (depends on 1) The method of claim 1, wherein the interleavings and the at least one invariant result from thread interactions in the program. ### Claim 5 (depends on 1) The method of claim 1, further comprising: generating, by the processor, the instrumented equivalent version of the program by inserting the locks into the source code for multiple threads executing in the program to avoid execution of the subset of the interleavings. ### Claim 6 (depends on 1) The method of claim 1, further comprising: positioning, by the processor, the locks in the source code to filter redundant sub-trees of a search space introduced by the subset of the interleavings during the enumerative model checking. ### Claim 7 (depends on 1) The method of claim 1, further comprising: performing, by the processor, the static instrumentation of shared variables between threads in the source code of the program to position the locks in positions to avoid execution of a subset of the interleavings caused by the shared variables in the source code. ### Claim 8 (depends on 1) The method of claim 1, further comprising: performing, by the processor, enumerative model checking of the instrumented equivalent version of the program by driving execution of the instrumented equivalent version of the program with a run-time scheduler. ### Claim 9 (depends on 8) The method of claim 8, further comprising: performing, by the processor, the enumerative model checking by executing dynamic partial order reduction (DPOR) on the instrumented equivalent version of the program. ### Claim 10 (depends on 1) The method of claim 1, further comprising: positioning, by the processor, the locks in the source code based on constraints due to the at least one invariant in the interleavings. ### Claim 11 A system for model checking a program, the system including: a memory device storing source code of a program; and a processor configured to: in response to instructions to execute the model checking program, retrieve the source code of the program from the memory device; perform static analysis of the source code of the program to inductively determine at least one invariant present in interleavings of the program; and perform static instrumentation of the source code of program to generate an instrumented equivalent version of the program, the instrumented equivalent version of the program comprising locks to avoid execution of a subset of the interleavings corresponding to the at least one invariant, wherein the instrumented equivalent version of the program is configured for enumerative model checking that avoids execution of the subset of the interleavings. ### Claim 12 (depends on 11) The system of claim 11, wherein the processor is further configured to position the locks in the source code to avoid execution of a redundant subset of the interleavings. ### Claim 13 (depends on 12) The system of claim 12, wherein the processor is further configured to execute the enumerative model checking of at least one interleaving of the redundant subset of the interleavings, while avoiding remaining interleavings of the redundant subset of the interleavings. ### Claim 14 (depends on 11) The system of claim 11, wherein the processor is further configured to perform the static analysis of source code of the program to inductively determine the at least one invariant resulting from thread interactions in the program. ### Claim 15 (depends on 11) The system of claim 11, wherein the processor is further configured to generate the instrumented equivalent version of the program by inserting the locks into the source code for multiple threads executing in the program to avoid execution of the subset of the interleavings. ### Claim 16 (depends on 11) The system of claim 11, wherein the processor is further configured to position the locks in the source code to filter redundant sub-trees of a search space introduced by the subset of the interleavings during the enumerative model checking. ### Claim 17 (depends on 11) The system of claim 11, wherein the processor is further configured to perform the static instrumentation of shared variables between threads in the source code of the program to position the locks in positions to avoid execution of a subset of the interleavings caused by the shared variables in the source code. ### Claim 18 (depends on 11) The system of claim 11, wherein the processor is further configured to perform the enumerative model checking of the instrumented equivalent version of the program by driving execution of the instrumented equivalent version of the program with a run-time scheduler. ### Claim 19 (depends on 18) The system of claim 18, wherein the processor is further configured to perform the during the enumerative model checking by executing dynamic partial order reduction (DPOR) on the instrumented equivalent version of the program. ### Claim 20 (depends on 11) The system of claim 11, wherein the processor is further configured to position the locks in the source code based on constraints due to the at least one invariant in the interleavings.