METHOD, SYSTEM, AND COMPUTER PROGRAM PRODUCT FOR GENERATING AUTOMATED ASSUMPTION FOR COMPOSITIONAL VERIFICATION

摘要

PPROBLEM TO BE SOLVED: To provide a method, system, and computer program product for computing a minimal deterministic finite-state automaton separating two languages from each other. PSOLUTION: The methods, systems, and computer program products for computing an exact minimal automaton to act as an intermediate assertion in assume-guarantee reasoning are provided. In one embodiment, computing of the exact minimal automaton is performed by using a sampling approach and a Boolean satisfiability, The methods described herein may be used as a part of a tool for formal verification. PCOPYRIGHT: (C)2009,JPO&INPIT