| Patent application number | Description | Published |
|---|
| 20090077252 | Optimized Data Stream Compression Using Data-Dependent Chunking - 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. | 03-19-2009 |
| 20090164501 | E-MATCHING FOR SMT SOLVERS - Embodiments are introduced which provide for creation of an E-matching code tree index which works on E-graphs to make E-matching more efficient. Use of the E-matching code tree allows performing matching of several patterns simultaneously. Embodiments are also described which provide for the generation of inverted path indexes. An inverted path index may be used to filter an E-graph to determine terms which may potentially match patterns when an E-graph is updated. | 06-25-2009 |
| 20090192767 | MODEL-BASED THEORY COMBINATION - 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. | 07-30-2009 |
| 20090271528 | EFFICIENT CHUNKING ALGORITHM - 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. | 10-29-2009 |
| 20090328015 | Matching Based Pattern Inference for SMT Solvers - 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. | 12-31-2009 |
| 20100083233 | Symbolic Runtime Checking of Quantified Contracts - 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. | 04-01-2010 |
