DETAILED ACTION The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA. Claims 1-20 have been presented for examination based on the application filed on December 16, 2022. Claims 1-20 are new and original. Claims 1-20 are rejected under 35 U.S.C. 102(a)(1) as being anticipated by Wang (U.S. Patent Application Publication 2010/0088681A1; hereinafter “Wang”) This action is made Non-Final. Notice of Pre-AIA or AIA Status The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA. Acknowledgement of References Cited By Applicant The information disclosure statements (IDS) submitted on 03/11/2024, 01/28/2025, and 01/06/2026 are in compliance with the provisions of 37 CFR 1.97. Accordingly, the information disclosure statement has been considered by the examiner. Specification The lengthy specification has not been checked to the extent necessary to determine the presence of all possible minor errors. Applicant's cooperation is requested in correcting any errors of which applicant may become aware in the specification. Examiner Notes Examiner cites particular columns, paragraphs, figures and line numbers in the references as applied to the claims below for the convenience of the applicant. Although the specified citations are representative of the teachings in the art and are applied to the specific limitations within the individual claim, other passages and figures may apply as well. It is respectfully requested that, in preparing responses, the applicant fully consider the references in their entirety as potentially teaching all or part of the claimed invention, as well as the context of the passage as taught by the prior art or disclosed by the examiner. The entire reference is considered to provide disclosure relating to the claimed invention. The claims & only the claims form the metes & bounds of the invention. Office personnel are to give the claims their broadest reasonable interpretation in light of the supporting disclosure. Unclaimed limitations appearing in the specification are not read into the claim. Prior art was referenced using terminology familiar to one of ordinary skill in the art. Such an approach is broad in concept and can be either explicit or implicit in meaning. Examiner's Notes are provided with the cited references to assist the applicant to better understand how the examiner interprets the applied prior art. Such comments are entirely consistent with the intent & spirit of compact prosecution. Claim Rejections - 35 USC § 102 In the event the determination of the status of the application as subject to AIA 35 U.S.C. 102 and 103 (or as subject to pre-AIA 35 U.S.C. 102 and 103) is incorrect, any correction of the statutory basis for the rejection will not be considered a new ground of rejection if the prior art relied upon, and the rationale supporting the rejection, would be the same under either status. The following is a quotation of the appropriate paragraphs of 35 U.S.C. 102 that form the basis for the rejections under this section made in this Office action: A person shall be entitled to a patent unless – (a)(1) the claimed invention was patented, described in a printed publication, or in public use, on sale, or otherwise available to the public before the effective filing date of the claimed invention. Claim s 1 -20 are rejected under 35 U.S.C. 102(a)( 1 ) as being anticipated by Wang (U.S. Patent Application Publication 2010/0088681A1 ; hereinafter “ Wang ”). Regarding claim 1, Wang discloses: “ A method for model checking a program, the method including:” ( Wang: abstract; para [0007] software program verification) “ 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” ( Wang: paras [0114, 0158] - performs static analysis of the program to identify, for each unobserved branch, the set of write-variables ) “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,” ( Wang: figs. 4(A), 7 (items 702, 705), 14; paras [0026, 0115, 0116, 0160, 0161] - code instrumentation; instrumented code with a hybrid lockset; Loe containing Ientry and lexit symbolizing lock and unlock condition ) “wherein the instrumented equivalent version of the program is configured for enumerative model checking that avoids execution of the subset of the interleavings . ” ( Wang : figs. 4(A), 5; paras [0113-0121] - checking local assertions with instrumented version ) Regarding claim 2 , Wang discloses all of the features with respect to claim 1 as outlined above and further Wang discloses: “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.” ( Wang: paras [0026, 0034, 0035, 0039-0042, 0115] - Lo c containing I entry and Iexit symbolizing lock and unlock condition) Regarding claim 3 , Wang discloses all of the features with respect to claim s 1 and 2 as outlined above and further Wang discloses: “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 .” ( Wang: figs. 4(a), 5; paras [0113-0121]) Regarding claim 4 , Wang discloses all of the features with respect to claim 1 as outlined above and further Wang discloses: “wherein the interleavings and the at least one invariant result from thread interactions in the program.” ( Wang: fig. 1; paras [0026-0031] - variants disclosed during thread execution) Regarding claim 5 , Wang discloses all of the features with respect to claim 1 as outlined above and further Wang discloses: “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 .” ( Wang: fig. 1 ; paras [0039-0042] - lock insertion for multiple thread execution) Regarding claim 6 , Wang discloses all of the features with respect to claim 1 as outlined above and further Wang discloses: “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.” ( Wang: paras [0005, 0009, 0058] - pruning redundant interleavings based on lock conditions) Regarding claim 7 , Wang discloses all of the features with respect to claim 1 as outlined above and further Wang discloses: “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.” ( Wang: paras [0112, 0115, 0116, 0150] - static instrumentation of shared variables SV; a multithreaded program (block 701) is instrumented at a source code level) Regarding claim 8 , Wang discloses all of the features with respect to claim 1 as outlined above and further Wang discloses: “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.” ( Wang: paras [0063, 0150] - The algorithm is implemented in a so-called scheduler process, running concurrently with the program under verification (a separate process) Regarding claim 9 , Wang discloses all of the features with respect to claims 1 and 8 as outlined above and further Wang discloses: “performing, by the processor, the enumerative model checking by executing dynamic partial order reduction (DPOR) on the instrumented equivalent version of the program.” ( Wang: table l ; paras [0147, 0154-0156] - use of DPOR) ) Regarding claim 10 , Wang discloses all of the features with respect to claim 1 as outlined above and further Wang discloses: “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.” ( Wang: paras [0039-0042, 0054] - locking based on constraints) Regarding claim 1 1 , Wang discloses: “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;” ( Wang: abstract; para [0007] software program verification) “ perform static analysis of the source code of the program to inductively determine at least one invariant present in interleavings of the program; and ” ( Wang: paras [0114, 0158] - performs static analysis of the program to identify, for each unobserved branch, the set of write-variables) “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,” ( Wang: figs. 4(A), 7 (items 702, 705), 14; paras [0026, 0115, 0116, 0160, 0161] - code instrumentation; instrumented code with a hybrid lockset; Loe containing Ientry and lexit symbolizing lock and unlock condition) “wherein the instrumented equivalent version of the program is configured for enumerative model checking that avoids execution of the subset of the interleavings .” ( Wang: figs. 4(A), 5; paras [0113-0121] - checking local assertions with instrumented version) Regarding claim 12 , incorporating the rejections of claim 2 , and claims 1 and 1 1 respectively, claim 12 is rejected as discussed above for substantially similar rationale. Regarding claim 1 3 , incorporating the rejections of claim 3 , and claims 1 -2 and 11 -12 respectively, claim 1 3 is rejected as discussed above for substantially similar rationale. Regarding claim 1 4 , incorporating the rejections of claim 4 , and claims 1 and 11 respectively, claim 1 4 is rejected as discussed above for substantially similar rationale. Regarding claim 1 5 , incorporating the rejections of claim 5 , and claims 1 and 11 respectively, claim 1 5 is rejected as discussed above for substantially similar rationale. Regarding claim 1 6 , incorporating the rejections of claim 6 , and claims 1 and 11 respectively, claim 1 6 is rejected as discussed above for substantially similar rationale. Regarding claim 1 7 , incorporating the rejections of claim 7 , and claims 1 and 11 respectively, claim 1 7 is rejected as discussed above for substantially similar rationale. Regarding claim 1 8 , incorporating the rejections of claim 8 , and claims 1 and 11 respectively, claim 1 8 is rejected as discussed above for substantially similar rationale. Regarding claim 1 9 , incorporating the rejections of claim 9 , and claims 1 , 8, 11 , and 18 respectively, claim 1 9 is rejected as discussed above for substantially similar rationale. Regarding claim 20 , incorporating the rejections of claim 10 , and claims 1 and 11 respectively, claim 20 is rejected as discussed above for substantially similar rationale. Conclusion Any inquiry concerning this communication or earlier communications from the examiner should be directed to FILLIN "Examiner name" \* MERGEFORMAT JUSTIN C MIKOWSKI whose telephone number is FILLIN "Phone number" \* MERGEFORMAT (571)272-8525 . The examiner can normally be reached FILLIN "Work Schedule?" \* MERGEFORMAT generally Monday through Thursday 8 am to 4:30 pm, EST . Examiner interviews are available via telephone, in-person, and video conferencing using a USPTO supplied web-based collaboration tool. To schedule an interview, applicant is encouraged to use the USPTO Automated Interview Request (AIR) at http://www.uspto.gov/interviewpractice. If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, FILLIN "SPE Name?" \* MERGEFORMAT Namrata Boveja can be reached at FILLIN "SPE Phone?" \* MERGEFORMAT (571) 272-8105 . The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300. Information regarding the status of published or unpublished applications may be obtained from Patent Center. Unpublished application information in Patent Center is available to registered users. To file and manage patent submissions in Patent Center, visit: https://patentcenter.uspto.gov. Visit https://www.uspto.gov/patents/apply/patent-center for more information about Patent Center and https://www.uspto.gov/patents/docx for information about filing in DOCX format. For additional questions, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000. /JUSTIN C MIKOWSKI/ Supervisory Patent Examiner, Art Unit 3673