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 |
20110302550 | Providing Diverse Solutions Using Design Space Exploration - 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. | 12-08-2011 |
20150082370 | SYSTEM AND METHOD FOR COMPACT FORM EXHAUSTIVE ANALYSIS OF SECURITY POLICIES - A system is described that analyzes and validates network security policies associated with network devices. The system includes a compiler and a security policy analysis and validation tool. The compiler encodes a security policy associated with a network device into a predicate expressed in bit-vector logic and generates a bit-vector formula based on the predicate. The tool receives the bit-vector formula and applies a Satisfiability Modulo Theories (SMT) solver thereto to identify and enumerate solutions to the bit-vector formula. The enumerated solutions provide information about the validity of the first security policy. The solutions may be compactly enumerated in a as product of intervals or a product of unions of intervals. | 03-19-2015 |