Invention Grant
US07653520B2 Method for combining decision procedures with satisfiability solvers
有权
将决策程序与可满足性求解者相结合的方法
- Patent Title: Method for combining decision procedures with satisfiability solvers
- Patent Title (中): 将决策程序与可满足性求解者相结合的方法
-
Application No.: US10431780Application Date: 2003-05-08
-
Publication No.: US07653520B2Publication Date: 2010-01-26
- Inventor: Leonardo De Moura , Harald Ruess
- Applicant: Leonardo De Moura , Harald Ruess
- Applicant Address: US CA Menlo Park
- Assignee: SRI International
- Current Assignee: SRI International
- Current Assignee Address: US CA Menlo Park
- Main IPC: G06F17/10
- IPC: G06F17/10
Abstract:
The invention provides bounded model checking of a program with respect to a property of interest comprising unfolding the program for a number of steps to create a program formula; translating the property of interest into an automaton; encoding the transition system of the automaton into a Boolean formula creating a transition formula; conjoining the program formula with the transition formula to create a conjoined formula; and deciding the satisfiability of the conjoined formula.
Public/Granted literature
- US20040019468A1 Method for combining decision procedures with satisfiability solvers Public/Granted day:2004-01-29
Information query
