System and method for generating error traces for concurrency bugs
AssigneeNEC Laboratories America, Inc.
InventorsVineet Kahlon, Sriram Sankarnarayanan, Aarti Gupta
Life of this patent
Estimating the term…
Abstract
A system and method for program verification includes generating a product transaction graph for a concurrent program, which captures warnings for potential errors. The warnings are filtered to remove bogus warnings, by using constraints from synchronization primitives and invariants that are derived by performing one or more dataflow analysis methods for concurrent programs. The dataflow analysis methods are applied in order of overhead expense. Concrete execution traces are generated for remaining warnings using model checking.
Claims13
A method implemented in a computer system for verification of a concurrent program, the method comprising:
- removing statically unreachable nodes using constraints due to synchronization primitives on a product control graph;
- performing static program analyses on the product control graph to derive sound invariants;
- further removing statically unreachable nodes using the derived invariants;
- and
- detecting violations of correctness properties using a resulting product control graph for subsequent analysis or verification.
Dependencies are inferred from the claim text.