| 摘要 |
PROBLEM TO BE SOLVED: To apply an SMT (Satisfiability Module Theories) solver to the property matching determination processing of software handling a variable length data structure.SOLUTION: An extractor 2 of shortest record length by predicate extracts a predicate pertinent to a predicate list storage part 12 from the property of software, and specifies the shortest record length of record length satisfying a predicate. A determination predicate extractor 3 extracts a record set to be processed by the extracted predicate and a determination predicate determining determination conditions from the extracted predicate, and generates a determination predicate set by summarizing the determination predicates extracted for each record set. A record length determination unit 4 determines the satisfiability of each determination predicate set, and on the basis of the result of the determination processing, calculates the record length of a record set corresponding to the determination predicate set. |
