Method for Multithreaded Program Output Uniqueness Testing and Proof-Generation, Based on Program Constraint Construction
Number of patents in Portfolio can not be more than 2000
United States of America Patent
Stats
-
N/A
Issued Date -
N/A
app pub date -
Sep 20, 2016
filing date -
Jul 7, 2014
priority date (Note) -
Abandoned
status (Latency Note)
Importance
Abstract
Provided is a method for multithreaded program output uniqueness testing and proof-generation, based on program constraint construction; according to multithreaded program semantics, a constraint expression is constructed; an output uniqueness verification problem is converted to a constraint solving problem; a constraint solver is used to detect the presence of different outputs, and a counterexample execution path describing different outputs is generated; first, a tested program is stubbed, and the program is executed to obtain an execution path; then, according to multithreaded program execution semantics, the execution path is converted to a first-order logic expression having no quantifiers, the constraint expression encompassing all possible thread interleavings; then, uniqueness verification conditions are constructed for the output of a first run; lastly, the constraint solver is used for verifying whether a path is causing the output value and the run result to be inconsistent. The present method detects whether the output of a multithreaded program is unique from a given input; if outputs are not unique, a counterexample sequence is displayed to describe the triggering process of same.
First Claim
Other Claims data not available