专利快速检索-快速检索全球专利，免费商用专利数据库-IPRDB

1. 发明授权

US08131661B2 Efficient decision procedure for bounded integer non-linear operations using SMT(LIA) 有权
标题翻译：使用SMT（LIA）的有界整数非线性运算的有效决策程序
公开(公告)号：US08131661B2
公开(公告)日：2012-03-06
申请号：US12331325
申请日：2008-12-09
申请人： Malay K. Ganai
发明人： Malay K. Ganai
IPC分类号： G06N5/00
CPC分类号： G06F17/11
摘要： Systems and methods are disclosed for deciding a satisfiability problem with linear and non-linear operations by: encoding non-linear integer operations into encoded linear operations with Boolean constraints by Booleaning and linearizing, combining the linear and encoded linear operations into a formula, solving the satisifiability of the formula using a solver, wherein the encoding and solving includes at least one of following: a. Booleanizing one of the non-linear operands by bit-wise structural decomposition b. Linearizing a non-linear operator by selectively choosing one of the operands for Booleanization c. Solving using an incremental lazy bounding refinement (LBR) procedure without re-encoding formula, and verifying the linear and non-linear operations in a computer software.
摘要翻译：公开了用于通过以下方式来确定线性和非线性操作的可满足性问题的系统和方法：通过布莱恩分解和线性化将非线性整数运算编码为具有布尔约束的编码线性运算，将线性和编码线性运算组合成公式，使用求解器的公式的令人满意的，其中编码和求解包括以下中的至少一个：a。通过逐位结构分解布尔化非线性操作数之一b。通过选择一个布尔化操作数来对非线性运算符进行线性化c。使用增量懒惰边界细化（LBR）过程解决，而无需重新编码公式，并验证计算机软件中的线性和非线性操作。

2. 发明申请

US20090292941A1 PROOF-GUIDED ERROR DIAGNOSIS (PED) BY TRIANGULATION OF PROGRAM ERROR CAUSES 审中-公开
标题翻译：通过三角计划错误原因进行验证错误诊断（PED）
公开(公告)号：US20090292941A1
公开(公告)日：2009-11-26
申请号：US12331243
申请日：2008-12-09
申请人： Malay K. Ganai , Gogul Balakrishnan
发明人： Malay K. Ganai , Gogul Balakrishnan
IPC分类号： G06F11/07
CPC分类号： G06F11/366 , G06F11/3636
摘要： Systems and methods are disclosed for performing error diagnosis of software errors in a program by from one or more error traces, building a repair program containing one or more modified program semantics corresponding to fixes to observed errors; encoding the repair program with constraints, biases and priortization into a constraint weighted problem; and solving the constraint weighted problem to generate one or more repair solutions, wherein the encoding includes at least one of: a) constraining one or more repairs choices guided by automatically inferring one or more partial specifications of intended program behaviors and program structure; b) biasing one or more repair choices guided by typical programming mistakes; and c) prioritizing the repair solutions based on error locations and possible changes in program semantics.
摘要翻译：公开了系统和方法，用于通过一个或多个错误跟踪来执行程序中软件错误的错误诊断，构建包含对应于观察到的错误的修复的一个或多个修改的程序语义的修复程序; 编码修复程序的约束，偏见和优化成约束加权问题; 以及解决所述约束加权问题以产生一个或多个修复解决方案，其中所述编码包括以下至少一个：a）通过自动推断一个或多个预期程序行为和程序结构的部分规范来约束一个或多个维修选择; b）偏向一个或多个由典型编程错误引导的维修选择; 以及c）基于错误位置和程序语义的可能变化对修复方案进行优先排序。

3. 发明授权

US08538900B2 Integrating interval constraint propagation with nonlinear real arithmetic 有权
标题翻译：将间隔约束传播与非线性实数算法相结合
公开(公告)号：US08538900B2
公开(公告)日：2013-09-17
申请号：US12966710
申请日：2010-12-13
申请人： Malay K. Ganai , Sicun Gao , Franjo Ivancic , Aarti Gupta
发明人： Malay K. Ganai , Sicun Gao , Franjo Ivancic , Aarti Gupta
IPC分类号： G06F15/18 , G06F7/60
CPC分类号： G06N5/003
摘要： A system and method for deciding the satisfiability of a non-linear real decision problem is disclosed. Linear and non-linear constraints associated with the problem are separated. The feasibility of the linear constraints is determined using a linear solver. The feasibility of the non-linear constraints is determined using a non-linear solver which employs interval constraint propagation. The interval solutions obtained from the non-linear solver are validated using the linear solver. If the solutions cannot be validated, linear constraints are learned to refine a search space associated with the problem. The learned constraints and the non-linear constraints are iteratively solved using the non-linear solver until either a feasible solution is obtained or no solution is possible.
摘要翻译：公开了一种用于确定非线性真实决策问题的可满足性的系统和方法。与问题相关联的线性和非线性约束是分开的。使用线性求解器确定线性约束的可行性。使用采用间隔约束传播的非线性求解器来确定非线性约束的可行性。使用线性求解器验证从非线性求解器获得的间隔解。如果解决方案无法验证，则学习线性约束来优化与问题相关联的搜索空间。使用非线性求解器迭代地求解所学习的约束和非线性约束，直到获得可行解或者没有解是可行的。

4. 发明授权

US08532971B2 DPLL-based SAT solver using with application-aware branching 有权
标题翻译：基于DPLL的SAT解算器使用应用感知分支
公开(公告)号：US08532971B2
公开(公告)日：2013-09-10
申请号：US12872797
申请日：2010-08-31
申请人： Malay K. Ganai
发明人： Malay K. Ganai
IPC分类号： G06F17/50
CPC分类号： G06F17/11 , G06F11/3608 , G06F17/504
摘要： A system and method for determining satisfiability of a bounded model checking instance by restricting the decision variable ordering of the SAT solver to a sequence wherein a set of control state variables is given higher priority over the rest variables appearing in the formula. The order for control state variables is chosen based on an increasing order of the control path distance of corresponding control states from the target control state. The order of the control variables is fixed, while that of the rest is determined by the SAT search. Such a decision variable ordering strategy leads to improved performance of SAT solver by early detection and pruning of the infeasible path segments that are closer to target control state.
摘要翻译：一种用于通过将SAT求解器的判决变量排序限制到其中一组控制状态变量被赋予比公式中出现的其余变量更高优先级的序列来确定有界模型检查实例的可满足性的系统和方法。基于对应控制状态与目标控制状态的控制路径距离的增加顺序来选择控制状态变量的顺序。控制变量的顺序是固定的，而其余的顺序由SAT搜索决定。这种决策变量排序策略通过早期检测和修剪更接近目标控制状态的不可行路径段来修复SAT求解器的性能。

5. 发明申请

US20090132991A1 PARTIAL ORDER REDUCTION FOR SCALABLE TESTING IN SYSTEM LEVEL DESIGN 审中-公开
标题翻译：系统级设计中可扩展测试的部分订单减少
公开(公告)号：US20090132991A1
公开(公告)日：2009-05-21
申请号：US12265347
申请日：2008-11-05
申请人： Malay K. Ganai , Sudipta Kundu
发明人： Malay K. Ganai , Sudipta Kundu
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A system and method for program testing includes, using a static analysis, determining dependency relations of enabled running processes in a program. The dependency relations are organized in a matrix to provide an interface for exploring the program. A reduced set of possible executions obtained by removal of redundant interleavings as determined with respect to the dependency relation, is explored on the program in a stateless exploration process that analyzes executed states and transitions to verify operation of the program.
摘要翻译：用于程序测试的系统和方法包括使用静态分析来确定程序中启用的运行进程的依赖关系。依赖关系被组织成一个矩阵，以提供一个探索程序的界面。在分析执行状态和转换以验证程序的操作的无状态探查过程中的程序上，探索通过去除相对于依赖关系确定的冗余交错获得的可能执行的减少的集合。

6. 发明授权

US08589126B2 System and method for model checking by interleaving stateless and state-based methods 有权
标题翻译：通过交织无状态和基于状态的方法进行模型检查的系统和方法
公开(公告)号：US08589126B2
公开(公告)日：2013-11-19
申请号：US12753239
申请日：2010-04-02
申请人： Malay K. Ganai , Chao Wang , Weihong Li
发明人： Malay K. Ganai , Chao Wang , Weihong Li
IPC分类号： G06F7/60 , G06G7/48
CPC分类号： G06F11/3608
摘要： A method for symbolic model checking for sequential systems using a combination of state-based and state-less approaches. A state-based method is used to compute frontier states by building transition relations on-the-fly using control flow information of the system, and performing successive image computations until a memory bound is reached, and efficiently storing only the new frontier states as disjunctive partitions of Boolean and Arithmetic expressions. A stateless method is used to check reachability of given goal states from a heuristically chosen set of frontier states until depth/time bound is reached. These two methods are alternated until one of the following occurs: all frontier states are explored, all goal states are reached, all computing resources are exhausted. Even though we do not store the entire reachable state set, we guarantee a complete coverage for terminating programs without the need to compute a fixed-point.
摘要翻译：使用基于状态和无状态方法的组合的顺序系统的符号模型检查的方法。基于状态的方法用于通过使用系统的控制流信息在运行中构建过渡关系来计算前沿状态，并且执行连续的图像计算，直到达到存储器界限，并且仅有效地将新的前沿状态存储为分离分布布尔和算术表达式。使用无状态方法来检查来自启发式选择的边界状态集合的给定目标状态的可达性，直到达到深度/时间界限。这两种方法是交替的，直到发生以下情况之一：探索所有前沿状态，达到所有目标状态，所有计算资源都已用尽。即使我们不存储整个可达到的状态集，我们保证对终止程序的完整覆盖，而不需要计算定点。

7. 发明授权

US08539013B2 Efficient decision method for real non-linear arithmetic constraints 有权
标题翻译：实际非线性算术约束的有效决策方法
公开(公告)号：US08539013B2
公开(公告)日：2013-09-17
申请号：US12709947
申请日：2010-02-22
申请人： Malay K. Ganai , Franjo Ivancic
发明人： Malay K. Ganai , Franjo Ivancic
IPC分类号： G06F7/38 , G06F17/00
CPC分类号： G06F17/10
摘要： A system and method for solving a decision problem having Boolean combinations of linear and non-linear operations includes translating the non-linear real operations using a COordinate Rotation DIgital Computer (CORDIC) method programmed on a computer device into linear operations maintaining a given accuracy. Linear and translated linear operations are combined into a formula. Satisfiability of the formula is solved using a decision procedure for Boolean combinations of linear operations over integers and reals.
摘要翻译：用于解决具有线性和非线性操作的布尔组合的决策问题的系统和方法包括使用在计算机设备上编程的坐标旋转二进制计算机（CORDIC）方法将非线性实际操作转换成维持给定精度的线性运算。线性和平移线性运算组合成一个公式。公式的满意度通过使用整数和阶数的线性运算的布尔组合的决策程序来解决。

8. 发明授权

US07949511B2 System and method for tunneling and slicing based BMC decomposition 有权
标题翻译：基于BMC分解的隧道和切片的系统和方法
公开(公告)号：US07949511B2
公开(公告)日：2011-05-24
申请号：US12183387
申请日：2008-07-31
申请人： Malay K. Ganai
发明人： Malay K. Ganai
IPC分类号： G06F9/445
CPC分类号： G06F11/3608
摘要： A system and method for bounded model checking of computer programs includes providing a program having at least one reachable property node. The program is decomposed for bounded model checking (BMC) into subproblems by creating a tunnel based on disjunctive control paths through the program. A reduced BMC sub-problem obtained using BMC unrolling, while using path constraints imposed by the at least one tunnel. For the reachable property node, determining a quantifier-free formula (QFP) in a decidable subset of first order logic. Satisfiability of the QFP is checked, independently and individually, to determine whether the QFP is satisfiable for the subproblem. The decomposing is continued until the a BMC bound is reached.
摘要翻译：用于计算机程序的有界模型检查的系统和方法包括提供具有至少一个可达属性节点的程序。该程序通过基于通过程序的分离控制路径创建隧道，将有界模型检查（BMC）分解为子问题。使用BMC展开获得的减少的BMC子问题，同时使用由至少一个隧道施加的路径约束。对于可达性属性节点，在一阶逻辑的可判定子集中确定无量子公式（QFP）。单独和单独检查QFP的满意度，以确定QFP是否满足子问题。分解继续，直到达到BMC界限。

9. 发明授权

US08539451B2 Systems and methods for model checking the precision of programs employing floating-point operations 有权
标题翻译：用于模型检查使用浮点运算的程序精度的系统和方法
公开(公告)号：US08539451B2
公开(公告)日：2013-09-17
申请号：US12761575
申请日：2010-04-16
申请人： Franjo Ivancic , Malay K. Ganai , Sriram Sankaranarayanan , Aarti Gupta
发明人： Franjo Ivancic , Malay K. Ganai , Sriram Sankaranarayanan , Aarti Gupta
IPC分类号： G06F9/44 , G06F11/00
CPC分类号： G06F11/3608
摘要： Methods and systems for verifying the precision of a program that utilizes floating point operations are disclosed. Interval and affine arithmetic can be employed to build a model of the program including floating point operations and variables that are expressed as reals and integers, thereby permitting accurate determination of precision loss using a model checker. Abstract interpretation can be also employed to simplify the model. In addition, counterexample-guided abstraction refinement can be used to refine the values of parametric error constants introduced in the model.
摘要翻译：公开了用于验证利用浮点运算的程序的精度的方法和系统。可以采用间隔和仿射算法来构建程序的模型，包括浮点运算和表示为真值和整数的变量，从而可以使用模型检验器精确确定精度损失。抽象解释也可以用来简化模型。此外，反例引导的抽象改进可以用于细化模型中引入的参数误差常数的值。

10. 发明授权

US08448145B2 Methods and systems for reducing verification conditions for concurrent programs using mutually atomic transactions 有权
标题翻译：用于减少使用相互原子交易的并发程序的验证条件的方法和系统
公开(公告)号：US08448145B2
公开(公告)日：2013-05-21
申请号：US12569557
申请日：2009-09-29
申请人： Malay K. Ganai , Sudipta Kundu
发明人： Malay K. Ganai , Sudipta Kundu
IPC分类号： G06F9/44
CPC分类号： G06F9/52 , G06F11/3608
摘要： Methods and systems for generating verification conditions and verifying the correctness of a concurrent system of program threads are described. The methods and systems determine and employ mutually atomic transactions to reduce verification problem sizes and state space for concurrent systems. The embodiments provide both an adequate and an optimal set of token-passing constraints for a bounded unrolling of threads.
摘要翻译：描述了用于生成验证条件和验证程序线程的并发系统的正确性的方法和系统。方法和系统确定并采用相互原子的事务来减少并发系统的验证问题大小和状态空间。这些实施例为有限线性展开的线程提供了足够的和最佳的令牌传递约束集合。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式