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

1. 发明授权

US08473895B2 Providing diverse solutions using design space exploration 有权
标题翻译：使用设计空间探索提供多种解决方案
公开(公告)号：US08473895B2
公开(公告)日：2013-06-25
申请号：US12795669
申请日：2010-06-08
申请人： Ethan K. Jackson , Wolfram Schulte , Nikolaj S. Bjorner , Eunsuk Kang
发明人： Ethan K. Jackson , Wolfram Schulte , Nikolaj S. Bjorner , Eunsuk Kang
IPC分类号： G06F9/44
CPC分类号： G06F17/5045 , G06F2217/08
摘要： A design space exploration (DSE) system automatically discovers viable solutions within a design space. The DSE system operates by creating or receiving a design specification that is described using a design language. The design specification contains a collection of constraints that an acceptable architecture is expected to satisfy. The DSE system then symbolically executes the design specification to provide a logical formula. The DSE system then interacts with a theorem prover module to identify one or more solutions to the formula. Finally, the DSE system converts the solutions into a user-interpretable form (e.g., expressed in the format of the modeling language) for viewing by a user. Each solution pertains to an architecture that satisfies the collection of constraints. The DSE system ensures that the solutions are diverse by disfavoring any solution that is deemed similar to any solution that has been previously encountered.
摘要翻译：设计空间探索（DSE）系统在设计空间内自动发现可行的解决方案。 DSE系统通过创建或接收使用设计语言描述的设计规范进行操作。设计规范包含可接受架构预期满足的约束集合。 DSE系统然后象征性地执行设计规范以提供逻辑公式。然后，DSE系统与定理证明器模块进行交互，以识别公式的一个或多个解决方案。最后，DSE系统将解决方案转换成用户可解释的形式（例如，以建模语言的格式表示），以供用户观看。每个解决方案都涉及满足约束集合的体系结构。 DSE系统确保解决方案是多样的，因为不满意任何与以前遇到过的解决方案相似的解决方案。

2. 发明授权

US09489221B2 Matching based pattern inference for SMT solvers 有权
标题翻译：针对SMT求解器的匹配模式推理
公开(公告)号：US09489221B2
公开(公告)日：2016-11-08
申请号：US12146373
申请日：2008-06-25
申请人： Nikolaj S. Bjorner , Leonardo Mendonca de Moura
发明人： Nikolaj S. Bjorner , Leonardo Mendonca de Moura
IPC分类号： G06F9/44 , G06F9/445
CPC分类号： G06F9/44589
摘要： A method for automatically analyzing formulas and adding pattern annotations to quantifiers based on a database of common pattern idioms. The method involves matching base pattern inference for Satisfiability Modulo Theories (SMT) solvers. The method uses a database for fault detection in externally supplied pattern annotated formulas. The method also uses matching code trees to mixed second-order pattern matching.
摘要翻译：一种基于公共模式习语的数据库自动分析公式并向量词添加模式注释的方法。该方法涉及匹配基本模式推理的可满足性模理论（SMT）求解器。该方法使用外部提供的模式注释公式中的故障检测数据库。该方法还使用匹配代码树来混合二阶模式匹配。

3. 发明申请

US20090271528A1 EFFICIENT CHUNKING ALGORITHM 有权
标题翻译：有效的重组算法
公开(公告)号：US20090271528A1
公开(公告)日：2009-10-29
申请号：US12431483
申请日：2009-04-28
申请人： Yuri Gurevich , Nikolaj S. Bjorner , Dan Teodosiu
发明人： Yuri Gurevich , Nikolaj S. Bjorner , Dan Teodosiu
IPC分类号： G06F15/16
CPC分类号： H04L63/123 , G06F17/30194
摘要： The present invention provides a method for chunking an object. The method is arranged to provide efficient chunking of objects such that objects can be efficiently updated between a remote machine and a local machine over a network. The chunking algorithm is applicable in networked application such as file synchronization using remote differential compression (RDC) techniques. The chunking algorithm provides enhanced efficiencies by locating chunk boundaries around local maxima.
摘要翻译：本发明提供一种用于分块对象的方法。该方法被设置为提供对象的有效分块，使得可以通过网络在远程机器和本地机器之间有效地更新对象。分块算法适用于使用远程差分压缩（RDC）技术的文件同步等网络应用。分块算法通过在局部最大值周围定位块边界来提供更高的效率。

4. 发明授权

US07610378B2 Locator and tracking service for peer-to-peer resources 失效
公开(公告)号：US07610378B2
公开(公告)日：2009-10-27
申请号：US11057267
申请日：2005-02-11
申请人： Dan Teodosiu , Nikolaj S. Bjorner , Markus M. Breunig
发明人： Dan Teodosiu , Nikolaj S. Bjorner , Markus M. Breunig
IPC分类号： G06F15/173
CPC分类号： H04L61/1511 , H04L29/06 , H04L29/12066 , H04L29/12132 , H04L61/1552 , H04L67/104 , H04L67/1072 , H04L67/1093 , H04L69/329
摘要： A resource naming service (RNS) server receives peer resource requests from peer platforms through a networking environment. The RNS server, possibly in cooperation with other RNS servers and peer registrars generates a response to the request to enable the peer platforms to access the requested peer resources. In one embodiment, a response includes a list of locations of peer devices in the networking environment where a resource is expected to be available. A requesting device can then choose to access the resource from one or more of the listed peer locations.

5. 发明申请

US20090192767A1 MODEL-BASED THEORY COMBINATION 失效
标题翻译：基于模型的理论组合
公开(公告)号：US20090192767A1
公开(公告)日：2009-07-30
申请号：US12019500
申请日：2008-01-24
申请人： Leonardo M. de Moura , Nikolaj S. Bjorner
发明人： Leonardo M. de Moura , Nikolaj S. Bjorner
IPC分类号： G06F17/10
CPC分类号： G06F17/10
摘要： A method is described for combining models of a plurality of theory solvers in order to produce a model which may be satisfiable by each of the plurality of theory solvers. A model is accessed for a first theory solver which is satisfiable in the first theory solver. It is determined that one or more equalities are implied by the model and it is determined if the equalities are compatible with a second solver. The model is updated in accordance any equalities determined not to be compatible with the second solver. A method is also described for mutation of models using freedom intervals. A freedom interval is determined for a variable within a model and the model is updates by choosing a value for the variable which lies within the freedom interval.
摘要翻译：描述了用于组合多个理论解算器的模型的方法，以便产生可由多个理论解算器中的每一个满足的模型。第一个理论解算器访问一个模型，在第一个理论解算器中可以满足。确定模型隐含一个或多个等式，并且确定该等式是否与第二求解器兼容。该模型根据确定不与第二个求解器兼容的任何均等进行更新。还描述了使用自由间隔的模型突变的方法。为模型中的变量确定自由间隔，并且通过选择位于自由间隔内的变量的值来更新模型。

6. 发明授权

US07552148B2 Shutdown recovery 有权
标题翻译：关机恢复
公开(公告)号：US07552148B2
公开(公告)日：2009-06-23
申请号：US11363828
申请日：2006-02-28
申请人： Huisheng Liu , Guhan Suriyanarayanan , Nikolaj S. Bjorner , Dan Teodosiu
发明人： Huisheng Liu , Guhan Suriyanarayanan , Nikolaj S. Bjorner , Dan Teodosiu
IPC分类号： G06F12/00 , G06F17/30 , G01R31/28
CPC分类号： G06F11/1435 , Y10S707/99953
摘要： Aspects of the subject matter described herein relate to shutdown recovery for resource replication systems. In aspects, a mechanism is described in which a machine having replicated data thereon can recover from a dirty shutdown. First, the machine determines whether a dirty shutdown has occurred. If so, the machine automatically performs shutdown recovery by causing resource metadata stored by the machine to be consistent with resource data stored by the machine. This may involve fixing the resource metadata for updates to the resource data that were not flushed to disk or may involve deleting the resource metadata and restoring it from another machine replicating the data.
摘要翻译：本文描述的主题的方面涉及用于资源复制系统的关闭恢复。在一些方面，描述了一种机构，其中具有复制数据的机器可以从脏关闭恢复。首先，机器确定是否发生脏关闭。如果是这样，机器将通过使机器存储的资源元数据与机器存储的资源数据一致，自动执行关机恢复。这可能涉及将用于更新的资源元数据修复到未刷新到磁盘的资源数据，或者可能涉及删除资源元数据并将其从复制数据的另一个机器恢复。

7. 发明授权

US07200667B2 Universal naming scheme for peer-to-peer resources 失效
标题翻译：通用命名方案，用于对等资源
公开(公告)号：US07200667B2
公开(公告)日：2007-04-03
申请号：US11067572
申请日：2005-02-25
申请人： Dan Teodosiu , Nikolaj S. Bjorner , Markus M. Breunig
发明人： Dan Teodosiu , Nikolaj S. Bjorner , Markus M. Breunig
IPC分类号： G06F15/16
CPC分类号： H04L61/1552 , H04L29/12066 , H04L29/12132 , H04L61/1511 , H04L67/104 , H04L67/1046 , H04L67/1063
摘要： Peer devices register with a resource locator service so that the peer devices can be uniquely identified in a networking environment. An addressing scheme addresses a peer resource in the networking environment based on the unique identifier of a peer device that is a master publisher of the resource. Based on the addressing scheme, the resource locator service can track the location of the master publisher of the resource as well as additional locations of peer devices that have cached the resource and made it available. In various embodiments, the resource locator service can service requests for peer resources by providing a list of locations where the resource is expected to be available or, in the case of non-compatible requester, provide access to the resource itself.
摘要翻译：对等设备向资源定位器服务注册，以便可以在网络环境中唯一地标识对等设备。寻址方案基于作为资源的主发行者的对等设备的唯一标识符来寻址网络环境中的对等资源。基于寻址方案，资源定位器服务可以跟踪资源的主发行者的位置以及缓存资源并使其可用的对等设备的附加位置。在各种实施例中，资源定位器服务可以通过提供预期资源可用的位置列表来提供对对等资源的请求，或者在不兼容请求者的情况下提供对资源本身的访问。

8. 发明授权

US08819288B2 Optimized data stream compression using data-dependent chunking 有权
标题翻译：使用数据相关分块优化数据流压缩
公开(公告)号：US08819288B2
公开(公告)日：2014-08-26
申请号：US11855986
申请日：2007-09-14
申请人： Nadim Y. Abdo , Nikolaj S. Bjorner
发明人： Nadim Y. Abdo , Nikolaj S. Bjorner
IPC分类号： G06F15/173 , G06F15/16
CPC分类号： H03M7/3084
摘要： Systems and methods for compression of data to be transmitted are described. A data stream, such as a byte code sequence, is partitioned into one or more data chunks. The data chunks can be associated with an identifier, such as a signature that differentiates one data chunk from the other. Thus, different data chunks would be identifiable through different signatures. The data chunks associated with the signatures can be compared with a repository or a history buffer. The history buffer includes a collection of previously transmitted data chunks each associated with their respective signature.
摘要翻译：描述用于压缩要发送的数据的系统和方法。诸如字节码序列的数据流被划分成一个或多个数据块。数据块可以与诸如将一个数据块与另一个数据块区分开的签名的标识符相关联。因此，不同的数据块可以通过不同的签名来识别。与签名相关联的数据块可以与存储库或历史缓冲区进行比较。历史缓冲器包括先前传输的数据块的集合，每个与它们各自的签名相关联。

9. 发明授权

US08117173B2 Efficient chunking algorithm 有权
标题翻译：高效分块算法
公开(公告)号：US08117173B2
公开(公告)日：2012-02-14
申请号：US12431483
申请日：2009-04-28
申请人： Yuri Gurevich , Nikolaj S. Bjorner , Dan Teodosiu
发明人： Yuri Gurevich , Nikolaj S. Bjorner , Dan Teodosiu
IPC分类号： G06F17/30
CPC分类号： H04L63/123 , G06F17/30194
摘要： The present invention provides a method for chunking an object. The method is arranged to provide efficient chunking of objects such that objects can be efficiently updated between a remote machine and a local machine over a network. The chunking algorithm is applicable in networked application such as file synchronization using remote differential compression (RDC) techniques. The chunking algorithm provides enhanced efficiencies by locating chunk boundaries around local maxima.
摘要翻译：本发明提供一种用于分块对象的方法。该方法被设置为提供对象的有效分块，使得可以通过网络在远程机器和本地机器之间有效地更新对象。分块算法适用于使用远程差分压缩（RDC）技术的文件同步等网络应用。分块算法通过在局部最大值周围定位块边界来提供更高的效率。

10. 发明申请

US20100083233A1 Symbolic Runtime Checking of Quantified Contracts 有权
标题翻译：量化合同的符号运行时检查
公开(公告)号：US20100083233A1
公开(公告)日：2010-04-01
申请号：US12239526
申请日：2008-09-26
申请人： Dries Vanoverberghe , Nikolai Tillmann , Jonathan Paul de Halleux , Nikolaj S. Bjorner , Wolfram Schulte
发明人： Dries Vanoverberghe , Nikolai Tillmann , Jonathan Paul de Halleux , Nikolaj S. Bjorner , Wolfram Schulte
IPC分类号： G06F9/44
CPC分类号： G06F11/3612 , G06F11/3684 , G06F11/3692
摘要： An extension of symbolic execution for programs involving contracts with quantifiers over large and potentially unbounded domains is described. Symbolic execution is used to generate, from a program, concrete test cases that exhibit mismatches between the program code and its contracts with quantifiers. Quantifiers are instantiated using symbolic values encountered during a set of exhibited runs. In this setting, quantifier instantiation is limited to values supplied to or produced by a symbolic execution. Quantifier instantiation is controlled by performing a matching algorithm that uses run-time values of input and program variables in order to guide and limit the set of quantifier instantiations. With a sufficient set of instances, test cases are derived that directly witness limitations of the auxiliary assertions.
摘要翻译：描述了涉及与大型和潜在无界域上的量词相关联的程序的符号执行的扩展。符号执行用于从程序生成具有程序代码与其与量词的合同之间不匹配的具体测试用例。使用在一组展示的运行中遇到的符号值来实例化量词。在此设置中，量化器实例化被限制为提供给或由符号执行产生的值。量化器实例化是通过执行使用输入和程序变量的运行时值的匹配算法来控制的，以引导和限制一组量词实例。使用足够的一组实例，导出直接看到辅助断言的限制的测试用例。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式