首页>
外国专利>
Method and apparatus for reducing a program size while maintaining branching time properties and automated checking of such reduced programs
Method and apparatus for reducing a program size while maintaining branching time properties and automated checking of such reduced programs
展开▼
机译:用于在保持分支时间属性的同时减小程序大小并自动检查这种减小的程序的方法和装置
展开▼
页面导航
摘要
著录项
相似文献
摘要
A method and apparatus are provided a method and apparatus for reducing a program that preserves branching time properties, including existential and universal aspects. An alternating transition system (ATS) is abstracted, formed by a product of a program, M, with an alternating tree automaton, A, for a property, f. The disclosed program abstraction method generates the abstract program and an altered version of the branching time property, f. An automated program check, such as a model check, is performed on the abstract program for the altered branching time property. The invention provides semantic completeness: i.e., whenever a program satisfies a property, this can be shown using a finite-state abstract ATS produced by the method. Choice predicates can be employed to help resolve nondeterminism at OR states, and rank functions can be employed to help preserve progress properties.
展开▼