METHOD FOR MULTITHREADED PROGRAM OUTPUT UNIQUENESS TESTING AND PROOF-GENERATION, BASED ON PROGRAM CONSTRAINT CONSTRUCTION

WIPO Patent Application WO/2016/004806

A1

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.

LIU TING (CN)
ZHANG XIAODONG (CN)
LIU PEI (CN)
YU LECHEN (CN)
ZHENG QINGHUA (CN)

PCT/CN2015/081055

January 14, 2016

June 09, 2015

Click for automatic bibliography generation  

UNIV XI AN JIAOTONG (CN)

G06F11/36

CN104077226A	2014-10-01
CN102799529A	2012-11-28
CN102063328A	2011-05-18

XI'AN CYDA INTELLECTUAL PROPERTY AGENCY (CN)
西安智大知识产权代理事务所 (CN)

View/Download PDF      PDF Help

Previous Patent: METHOD FOR PREPARING ERIBULIN INTERMEDIATE

Next Patent: PURINE INHIBITORS OF HUMAN PHOSPHATIDYLINOSITOL 3-KINASE DELTA