首页>
外国专利>
Model Checking of Non-Terminating Software Programs
Model Checking of Non-Terminating Software Programs
展开▼
机译:非终止软件程序的模型检查
展开▼
页面导航
摘要
著录项
相似文献
摘要
A method for verifying software program code includes specifying a property that the software program code is expected to satisfy. The software program code and the property are transformed into an initial logical formula in a static single assignment (SSA) form, the formula including variables. A loop in the software program code is identified. Successive over-approximations are applied to a portion of the initial logical formula corresponding to the loop in order to produce a modified logical formula in the SSA form that represents a finite over-approximation of a set of states that are reachable by the loop. It is verified that the software program code satisfies the specified property by determining whether there is an assignment of the variables that satisfies the modified logical formula.
展开▼