# US 10,372,584 B2 · Software inspection apparatus > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 10,372,584 B2 - Document ID: US10372584B2 - Status: Granted - Kind: B2 - Application number: 15/543,101 - Filed: 2015-01-30 - Published: 2017-12-21 - Granted: 2019-08-06 - Earliest claimed: 2015-01-30 - Assignees: Hitachi, Ltd. - Applicants: Hitachi, Ltd. - Inventors: Masataka Nishi - Web page: https://patentgrep.com/patent/US10372584B2 ## CPC - G06F 11/3608: {using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013)} - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract While the effectiveness of a model inspection method as a means for detecting software defects is known, large-scale software cannot be handled due to great amounts of calculation required for inspection. According to the present invention, after a model inspection problem of software is attributed to be a satisfiability determination problem, the problem is converted to a type that can be solved by a solver used for solving a notification optimization problem having constrained conditions, and the satisfiability is determined in a numerically analytical manner. ## Claims ### Claim 1 A software inspection apparatus comprising a processor configured to: receive software to be inspected, an input value constraint having an inspection range for an input value to the software, and an inspection condition designating a requirement that the software is to satisfy as input values; inspect the software on the basis of the input values; and output an inspection condition determination result, wherein the processor executes the inspection of the software by satisfiability determination using a constrained optimization solver, wherein the processor is further configured to: convert the software into a constrained partially-ordered graphing SSA format; generate a list of constraint formats by merging the input value constraint and the inspection condition; generate a list of value range constrained constraint expressions and first and second derivative expressions of the constraint expression from the list of constraint formats; and convert an output value from the constrained numerical optimization solver into a report on whether or not an overflow in operation occurs and a report on a determination result of the inspection condition. ### Claim 2 (depends on 1) The software inspection apparatus according to claim 1, wherein the solver includes: a function of outputting an operation position causing overflow in a case where the overflow in operation occurs during a program execution process within a range of the input value constraint; and a function of outputting a program execution path leading violation of the inspection condition in a case where there is an improper input value that violates the inspection condition. ### Claim 3 A software inspection apparatus comprising a processor configured to: receive software to be inspected, an input value constraint having an inspection range for an input value to the software, and an inspection condition designating a requirement that the software is to satisfy as input values; inspect the software on the basis of the input values; and output an inspection condition determination result, wherein the processor executes the inspection of the software by satisfiability determination using a constrained optimization solver, wherein the constrained optimization solver includes: a function of outputting an operation position causing overflow in a case where the overflow in operation occurs during a program execution process within a range of the input value constraint; and a function of outputting a program execution path leading violation of the inspection condition in a case where there is an improper input value that violates the inspection condition, and wherein the processor is further configured to: convert the software into a constrained partially-ordered graphing SSA format and further generate a list of constraint formats by merging the input value constraint and the inspection condition; generate a list of value range constrained constraint expressions and first and second derivative expressions of the constraint expression from the list of constraint formats; and convert an output value from the constrained numerical optimization solver into a report on whether or not the overflow in operation occurs and a report on a determination result of the inspection condition. ### Claim 4 A software inspection apparatus comprising: a processor configured to: receive software to be inspected, an input value constraint having an inspection range for an input value to the software, and an inspection condition designating a requirement that the software is to satisfy as input values; inspect the software on the basis of the input values; and output an inspection condition determination result, wherein the processor executes the inspection of the software by satisfiability determination using a constrained optimization solver, wherein the constrained optimization solver includes: a function of outputting an operation position causing overflow in a case where the overflow in operation occurs during a program execution process within a range of the input value constraint; and a function of outputting a program execution path leading violation of the inspection condition in a case where there is an improper input value that violates the inspection condition, and wherein the processor is further configured to: convert the software into a constrained partially-ordered graphing SSA format; and generate a list of constraint formats by merging the input value constraint and the inspection condition. ### Claim 5 (depends on 4) The software inspection apparatus according to claim 4, wherein the processor is further configured to generate a list of value range constrained constraint expressions and first and second derivative expressions of the constraint expression from the list of constraint formats. ### Claim 6 (depends on 4) The software inspection apparatus according to claim 4, wherein the processor is further configured to convert an output value from the constrained numerical optimization solver into a report on whether or not the overflow in operation occurs and a report on a determination result of the inspection condition.