Patent application number | Description | Published |
20090043560 | FEATURE ORIENTED PROTOCOL MODELING - Modeling protocols. A method includes accessing a number of model programs. Each model program includes computer-executable instructions. The computer-executable instructions describe the behavior of at least one of another program, system, or component. Model programs may be disjointed in that they have independent meaning or dependent in that they include at least one of a state variable, action, or precondition that is dependent on another model program to impart meaning to the model program. An output model program is composed by unification including substituting state variables into another of the model programs without executing the model programs. Traces are generated from the output model program. Each of the traces includes a path of labels. The labels describe actions of the output model program from an initial state to an accepting state where a run is allowed to stop. The traces are output to a user. | 02-12-2009 |
20110055237 | Symbolic Query Exploration - A symbolic query exploration (QEX) module automatically produces output information that can be used to evaluate a database. The QEX module operates by converting an input query into a formula for processing by a satisfiability module theories (SMT) solver module. The SMT solver module generates a model that satisfies the formula. The model yields table information that is used to populate the database and, optionally, parameter information that is used to instantiate the query. A query evaluation module then submits the instantiated query to the populated database and evaluates whether an evaluation result produced thereby agrees with pre-specified condition information. The QEX module can preprocess the formula using either (or both) an eager expansion approach (in which the formula is expanded in an upfront manner) or a lazy expansion approach (in which axioms are identified for later possible expansion by the SMT solver module). | 03-03-2011 |
20120130932 | SYMBOLIC FINITE AUTOMATA - Described are symbolic finite automata for symbolically expressing and analyzing regular expression constraints, such as for use in program analysis and testing. A regular expression or pattern is transformed into a symbolic finite automaton having transitions that are labeled by formulas that denote sets of characters (rather than individual characters). Also described is composing two or more symbolic finite automata into a resulting symbolic finite automaton that is fully satisfiable. A constraint solver may be used to ensure satisfiability. | 05-24-2012 |
20120151592 | STRING OPERATIONS WITH TRANSDUCERS - There is provided a computer-implemented method for analyzing string-manipulating programs. An exemplary method comprises describing a string-manipulating program as a finite state transducer. The finite state transducer may be evaluated with a constraint solving methodology to determine whether a particular string may be provided as output by the string-manipulating program. The constraint solving methodology may involve the use of one or more satisfiability modulo theories (SMT) solvers. A determination may be made regarding whether the string-manipulating program may contain a potential security risk depending on whether the particular string may be provided as output by the string-manipulating program. | 06-14-2012 |
20150071555 | Managing Access by Applications to Perceptual Information - Functionality is described herein by which plural environment-sensing applications capture information from an environment in a fine-grained and least-privileged manner. By doing so, the functionality reduces the risk that private information that appears within the environment will be released to unauthorized parties. Among other aspects, the functionality provides an error correction mechanism for reducing the incidence of false positives in the detection of objects, an offloading technique for delegating computationally intensive recognition tasks to a remote computing framework, and a visualization module by which a user may inspect the access rights to be granted (or already granted) to each application. | 03-12-2015 |