PATH EXECUTION REDUCTION IN SOFTWARE PROGRAM VERIFICATION

摘要

A method of software program verification including receiving at least a portion of a software program that may further include a function under analysis (FUA). The method includes creating an FUA path based at least partially on a path through one or more functions of the received portion of the software program. The method includes determining whether the FUA path generates new coverage for the FUA. In response to the FUA path generating new coverage, the method includes selecting an FUA path statement from the FUA path. The method includes determining whether an uncovered code fragment of the FUA is reachable from the selected FUA path statement based at least partially on a set of covered FUA code fragments. In response to the uncovered code fragment being reachable from the selected FUA path statement, the method includes adding the selected FUA path statement to a set of covered statements.

主权项

1. A method of software program verification, the method comprising:
receiving at least a portion of a software program, the received portion of the software program including a function under analysis (FUA); creating an FUA path based at least partially on a path through one or more functions included in the received portion of the software program; determining whether the FUA path generates new coverage for the FUA; in response to the FUA path generating new coverage, selecting an FUA path statement from the FUA path; determining whether an uncovered code fragment of the FUA is reachable from the selected FUA path statement based at least partially on a set of covered FUA code fragments; and in response to the uncovered code fragment being reachable from the selected FUA path statement, adding the selected FUA path statement to a set of covered statements.