Static analysis for sound interleaving pruning in enumerative model checking

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.