公开(公告)号：US20130325778A1

公开(公告)日：2013-12-05

申请号：US13487279

申请日：2012-06-04

申请人： Yael Ben-Haim ,  Alexander Ivrii ,  Arie Matsliah ,  Oded Margalit

发明人： Yael Ben-Haim ,  Alexander Ivrii ,  Arie Matsliah ,  Oded Margalit

IPC分类号： G06N5/00

CPC分类号： G06N5/02 ,  G06N5/00

摘要： A method, apparatus and product for encoding a cardinality constraint in Conjunctive Normal Form (CNF). The method comprising: having a Boolean formula comprising a cardinality constraint, wherein the cardinality constraint relating to a set of Boolean variables, the set of variables consisting of N variables, the cardinality constraint given in a non-Conjunctive Normal Form; and encoding the cardinality constraint in Conjunctive Normal Form based on a mapping by a Perfect Hash Family, whereby said memory is modified to retain the CNF encoded cardinality constraint.

摘要翻译： 用于编码结合正常形式（CNF）中的基数约束的方法，装置和产品。 该方法包括：具有包括基数约束的布尔公式，其中与一组布尔变量相关的基数约束，由N个变量组成的变量集合，以非结合正则形式给出的基数约束; 并且基于完美哈希族的映射来编码结合正态形式中的基数约束，由此修改所述存储器以保留CNF编码的基数约束。

公开(公告)号：US20130035908A1

公开(公告)日：2013-02-07

申请号：US13195873

申请日：2011-08-02

申请人： Alexander Ivrii ,  Arie Matsliah

发明人： Alexander Ivrii ,  Arie Matsliah

IPC分类号： G06F17/10

CPC分类号： G06F17/5081 ,  G06F17/504

摘要： Candidate invariants are selected from a proof of a property. In some exemplary embodiments, a proof of a property with respect to a bounded model having a bounded number of cycles may be obtained. The bounded model may comprise an initial axiom and a transition relation axiom. The proof of the property is a Directed Acyclic Graph (DAG). Each non-leaf node of the DAG is deducible from its child nodes. A root of the DAG is the property. Leaves of the DAG are associated with an axiom of the bounded model. A set of candidate invariants may be selected from the DAG. A subset of the set of candidates may be determined such that the subset comprises invariants which are held during each cycle of an unbounded model, wherein the unbounded model is an unbounded version of the bounded model. The invariants may be utilized for model checking of the unbounded model.

摘要翻译： 候选不变量是从财产证明中选出的。 在一些示例性实施例中，可以获得关于具有有界数量的循环的有界模型的属性的证明。 有限模型可以包括初始公理和过渡关系公理。 属性的证明是定向非循环图（DAG）。 DAG的每个非叶节点都可以从其子节点中推导出来。 DAG的根是属性。 DAG的叶与有界模型的公理相关联。 可以从DAG中选择一组候选不变量。 可以确定候选集合的子集，使得子集包括在无界模型的每个周期期间保持的不变量，其中无界模型是有界模型的无界版本。 不变量可用于无界模型的模型检查。

公开(公告)号：US08996339B2

公开(公告)日：2015-03-31

申请号：US13226513

申请日：2011-09-07

申请人： Hana Chockler ,  Alexander Ivrii ,  Arie Matsliah ,  Shiri Moran ,  Ziv Nevo

发明人： Hana Chockler ,  Alexander Ivrii ,  Arie Matsliah ,  Shiri Moran ,  Ziv Nevo

IPC分类号： G06F7/60 ,  G06F17/50

CPC分类号： G06F17/504

摘要： Method, apparatus, and product for performing incremental formal verification. A computer-implemented method performed by a computerized device. The method comprises: obtaining invariants with respect to a first model; determining a portion of the invariants that are invariants with respect to a second model, and utilizing the portion of the invariants to check that the second model holds a property.

摘要翻译： 执行递增形式验证的方法，设备和产品。 由计算机化设备执行的计算机实现的方法。 该方法包括：获得关于第一模型的不变量; 确定相对于第二模型是不变量的不变量的一部分，以及利用所述不变量的所述部分来检查所述第二模型是否具有属性。

公开(公告)号：US08996435B2

公开(公告)日：2015-03-31

申请号：US13195876

申请日：2011-08-02

申请人： Alexander Ivrii ,  Sharon Keidar-Barner ,  Arie Matsliah

发明人： Alexander Ivrii ,  Sharon Keidar-Barner ,  Arie Matsliah

IPC分类号： G06N5/02 ,  G06F17/50 ,  G06F17/11

CPC分类号： G06N5/02 ,  G06F17/11 ,  G06F17/5022

摘要： A method, apparatus and product for determining invariants in a model. One exemplary embodiments is a computer-implemented method performed by a computerized device, comprising: obtaining a set of candidates of invariants with respect to a model, the model comprising a transition relation axiom and an initial axiom; for substantially each candidate, adding to the model a first auxiliary variable, the first auxiliary variable is defined to be implied from the candidate being held in a predetermined cycle; iteratively trying to prove an inductive step with respect to a subset of the candidates, wherein in response to determining that a candidate is not held inductively removing the candidate from the subset of the candidates, wherein determining which candidate is not held inductively is performed based on values of the first auxiliary variables.

摘要翻译： 一种用于确定模型中不变量的方法，装置和产品。 一个示例性实施例是由计算机化设备执行的计算机实现的方法，包括：获得关于模型的一组不变量候选，所述模型包括过渡关系公理和初始公理; 对于基本上每个候选者，向模型添加第一辅助变量，第一辅助变量被定义为从保持在预定周期中的候选者隐含; 迭代地尝试证明相对于候选的子集的归纳步骤，其中响应于确定候选没有被保持感应性地从候选的子集中移除候选，其中基于 第一个辅助变量的值。

公开(公告)号：US08909579B2

公开(公告)日：2014-12-09

申请号：US13195873

申请日：2011-08-02

申请人： Alexander Ivrii ,  Arie Matsliah

发明人： Alexander Ivrii ,  Arie Matsliah

IPC分类号： G06N5/02 ,  G06F17/50

CPC分类号： G06F17/5081 ,  G06F17/504

摘要： Candidate invariants are selected from a proof of a property. In some exemplary embodiments, a proof of a property with respect to a bounded model having a bounded number of cycles may be obtained. The bounded model may comprise an initial axiom and a transition relation axiom. The proof of the property is a Directed Acyclic Graph (DAG). Each non-leaf node of the DAG is deducible from its child nodes. A root of the DAG is the property. Leaves of the DAG are associated with an axiom of the bounded model. A set of candidate invariants may be selected from the DAG. A subset of the set of candidates may be determined such that the subset comprises invariants which are held during each cycle of an unbounded model, wherein the unbounded model is an unbounded version of the bounded model. The invariants may be utilized for model checking of the unbounded model.

摘要翻译： 候选不变量是从财产证明中选出的。 在一些示例性实施例中，可以获得关于具有有界数量的循环的有界模型的属性的证明。 有限模型可以包括初始公理和过渡关系公理。 属性的证明是定向非循环图（DAG）。 DAG的每个非叶节点都可以从其子节点中推导出来。 DAG的根是属性。 DAG的叶与有界模型的公理相关联。 可以从DAG中选择一组候选不变量。 可以确定候选集合的子集，使得子集包括在无界模型的每个周期期间保持的不变量，其中无界模型是有界模型的无界版本。 不变量可用于无界模型的模型检查。

公开(公告)号：US20130036079A1

公开(公告)日：2013-02-07

申请号：US13195876

申请日：2011-08-02

申请人： Alexander Ivrii ,  Sharon Keidar-Barner ,  Arie Matsliah

发明人： Alexander Ivrii ,  Sharon Keidar-Barner ,  Arie Matsliah

IPC分类号： G06N5/02

CPC分类号： G06N5/02 ,  G06F17/11 ,  G06F17/5022

摘要： A method, apparatus and product for determining invariants in a model. One exemplary embodiments is a computer-implemented method performed by a computerized device, comprising: obtaining a set of candidates of invariants with respect to a model, the model comprising a transition relation axiom and an initial axiom; for substantially each candidate, adding to the model a first auxiliary variable, the first auxiliary variable is defined to be implied from the candidate being held in a predetermined cycle; iteratively trying to prove an inductive step with respect to a subset of the candidates, wherein in response to determining that a candidate is not held inductively removing the candidate from the subset of the candidates, wherein determining which candidate is not held inductively is performed based on values of the first auxiliary variables.

摘要翻译： 一种用于确定模型中不变量的方法，装置和产品。 一个示例性实施例是由计算机化设备执行的计算机实现的方法，包括：获得关于模型的一组不变量候选，所述模型包括过渡关系公理和初始公理; 对于基本上每个候选者，向模型添加第一辅助变量，第一辅助变量被定义为从保持在预定周期中的候选者隐含; 迭代地尝试证明相对于候选的子集的归纳步骤，其中响应于确定候选没有被保持感应性地从候选的子集中移除候选，其中基于 第一个辅助变量的值。

公开(公告)号：US08825575B2

公开(公告)日：2014-09-02

申请号：US13487279

申请日：2012-06-04

申请人： Yael Ben-Haim ,  Alexander Ivrii ,  Arie Matsliah ,  Oded Margalit

发明人： Yael Ben-Haim ,  Alexander Ivrii ,  Arie Matsliah ,  Oded Margalit

IPC分类号： G06N5/00 ,  G06N5/02

CPC分类号： G06N5/02 ,  G06N5/00

摘要： A method, apparatus and product for encoding a cardinality constraint in Conjunctive Normal Form (CNF). The method comprising: having a Boolean formula comprising a cardinality constraint, wherein the cardinality constraint relating to a set of Boolean variables, the set of variables consisting of N variables, the cardinality constraint given in a non-Conjunctive Normal Form; and encoding the cardinality constraint in Conjunctive Normal Form based on a mapping by a Perfect Hash Family, whereby said memory is modified to retain the CNF encoded cardinality constraint.

摘要翻译： 用于编码结合正常形式（CNF）中的基数约束的方法，装置和产品。 该方法包括：具有包括基数约束的布尔公式，其中与一组布尔变量相关的基数约束，由N个变量组成的变量集合，以非结合正则形式给出的基数约束; 并且基于完美哈希族的映射来编码结合正态形式中的基数约束，由此修改所述存储器以保留CNF编码的基数约束。

公开(公告)号：US20130060545A1

公开(公告)日：2013-03-07

申请号：US13226513

申请日：2011-09-07

申请人： Hana Chockler ,  Alexander Ivrii ,  Arie Matsliah ,  Shiri Moran ,  Ziv Nevo

发明人： Hana Chockler ,  Alexander Ivrii ,  Arie Matsliah ,  Shiri Moran ,  Ziv Nevo

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： Method, apparatus, and product for performing incremental formal verification. A computer-implemented method performed by a computerized device. The method comprises: obtaining invariants with respect to a first model; determining a portion of the invariants that are invariants with respect to a second model, and utilizing the portion of the invariants to check that the second model holds a property.

摘要翻译： 执行递增形式验证的方法，设备和产品。 由计算机化设备执行的计算机实现的方法。 该方法包括：获得关于第一模型的不变量; 确定相对于第二模型是不变量的不变量的一部分，以及利用所述不变量的所述部分来检查所述第二模型是否具有属性。

公开(公告)号：US20120046918A1

公开(公告)日：2012-02-23

申请号：US12857588

申请日：2010-08-17

申请人： Oded Fuhrmann ,  Alexander Ivrii ,  Tatyana Veksler

发明人： Oded Fuhrmann ,  Alexander Ivrii ,  Tatyana Veksler

IPC分类号： G06F17/10

CPC分类号： G06F17/504

摘要： An UNSAT core may be reused during iterations of a bounded model checking process. When increasing the bound, signals corresponding to signals within the UNSAT core may be used to represent the functionality of the model during cycles between the original bound and the increased bound. In case, consecutive unsatisfiability is determined in respect to different bounds, the same UNSAT core may be reused instead of computing a new UNSAT core.

公开(公告)号：US08201116B2

公开(公告)日：2012-06-12

申请号：US12857588

申请日：2010-08-17

申请人： Oded Fuhrmann ,  Alexander Ivrii ,  Tatyana Veksler

发明人： Oded Fuhrmann ,  Alexander Ivrii ,  Tatyana Veksler

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： An UNSAT core may be reused during iterations of a bounded model checking process. When increasing the bound, signals corresponding to signals within the UNSAT core may be used to represent the functionality of the model during cycles between the original bound and the increased bound. In case, consecutive unsatisfiability is determined in respect to different bounds, the same UNSAT core may be reused instead of computing a new UNSAT core.

摘要翻译： 在有限模型检查过程的迭代期间，可以重新使用UNSAT核心。 当增加绑定时，对应于UNSAT核心内的信号的信号可以用于在原始绑定和增加绑定之间的周期期间表示模型的功能。 在不同界限下确定连续的不满足性的情况下，可以重复使用相同的UNSAT核心，而不是计算新的UNSAT核心。