Patent application number | Description | Published |
20080276025 | LOCK INFERENCE FOR ATOMIC SECTIONS - Locks which protect data structures used within atomic sections of concurrent programs are inferred from atomic sections and acquired in a manner to avoid deadlock. Locks may be inferred by expression correspondence using a backward inter-procedural analysis of an atomic section. Locks may be sorted according to a total order and acquired early in an atomic section to prevent deadlock. Multiple granularity of locks are determined and employed. Fine grained locks may be inferred and acquired to reduce contention. Coarse grained locks may be determined and substituted for fine grained locks when necessary for unbounded locations or to reduce the number of finer grained locks. | 11-06-2008 |
20080282108 | PROGRAM SYNTHESIS AND DEBUGGING USING MACHINE LEARNING TECHNIQUES - One embodiment is directed to synthesizing code fragments in a software routine using known inputs and corresponding expected outputs. A computer system provides a software routine with known inputs and corresponding expected outputs, infers software routine instructions based on the known inputs and corresponding expected outputs, and synthesizes a correctly functioning code fragment based on the inferred instructions. Another embodiment is directed to automatically resolving semantic errors in a software routine. A computer system provides the software routine with known inputs and corresponding expected outputs for portions of a program fragment where an error has been localized. The computer system learns a correctly functioning program fragment from pairs of input-output descriptions of the program fragment, determines the program statements that can transform given input states into given output states after execution of those program statements, and alters portions of the software routine with the learned program fragments. | 11-13-2008 |
20080301655 | PROGRAM ABSTRACTION BASED ON PROGRAM CONTROL - Embodiments described herein relate to determining an abstraction of a computer program and to the refinement of an abstraction of a computer program. The computer program may be a sequential program or may be a concurrent (parallel) program. A directed graph represents a computer program and may be the cross product of threads within a concurrent program. Nodes within a representation of a program are reduced to a single node to produce an abstraction. An abstraction may be refined by determining constraints that produce a refined abstraction that does not comprise infeasible paths. | 12-04-2008 |
20090276763 | Bounding Resource Consumption Using Abstract Interpretation - Bounding resource consumption of code using abstract interpretation includes a static analysis to estimate a code's resource consumption in terms of units of resources utilized at any point during execution, expressed as a function of its scalar inputs. An instrumentation mechanism and an abstract interpretation mechanism are employed to compute bounds on the code resource consumption. The instrumentation mechanism includes incorporating one or more counter variables in the source code to count the number of loop iterations and recursive procedure call invocations. The abstract interpretation mechanism includes computing invariants on the instrumented counter variables and scalar program variables to obtain bounds on the number of loop iterations and recursive procedure call invocations, which are then composed together to obtain resource bounds for the entire program. | 11-05-2009 |
20090326907 | PROGRAM ANALYSIS AS CONSTRAINT SOLVING - Described is a technology by which program analysis uses rich invariant templates that may specify an arbitrary Boolean combination of linear inequalities for program verification. Also described is choosing a cut-set that identifies program locations, each of which is associated with an invariant template. The verification generates second-order constraints, converts second-order logic formula based on those constraints into first-order logic formula, then converts the first-order logic formula into a quantifier-free formula, which is then converted into a Boolean satisfiability formula. Off-the-shelf constraint solvers may then be applied to the Boolean satisfiability formula to generate program analysis results. Various templates may be used to convert the second-order logic formula into the first-order logic formula. Further described are interprocedural analysis and the determination of weakest precondition and strongest postcondition with applications to termination analysis, timing bounds analysis, and generation of most-general counterexamples for both termination and safety properties. | 12-31-2009 |
20090327997 | Timing Analysis of Concurrent Programs - Described are various techniques by which a concurrent program is analyzed with respect to timing. In one aspect, code fragments in a concurrent program are modified and/or instrumented by inserting iteration counters inside loops. Examples of modified fragments include those corresponding to concurrently executing code fragments, non-blocking concurrent code fragments, blocking concurrent code fragments, fragments having a loop that may not terminate, fragments having interlocked operation, or fragments having a timeout. Such fragments are modified and/or flagged so as to provide the summary data. When statically analyzed, the instrumented code provides complexity information regarding each fragment, or combinations of fragments, such as concurrent fragments. Summary data regarding the concurrent program is provided by processing the complexity information into at least one computation graph. | 12-31-2009 |
20100088548 | Using Constraint Solving to Discovering Disjunctive and Quantified Invariants Over Predicate Abstraction - Techniques are disclosed for generating complex invariants in a program using a Satisfiability Modulo Theories (SMT) solver. In one embodiment, the generated invariants may be used to validate assert statements in a program. Additionally or alternatively, a weakest pre-condition invariant may be generated such that parameters passed to the program that satisfy the weakest pre-condition are guaranteed to satisfy the program's assert statements. Additionally or alternatively, a strongest post-condition may be generated, determining what is guaranteed to be true about the state of the program upon completion of the program. In one embodiment, the SMT solver generates invariants by mapping predicates onto unknown variables in a template. The template may comprise unknown variables related by logical structures defined with disjunctions, universal quantifiers, and existential quantifiers. The predicates may comprise equalities and inequalities between program variables. | 04-08-2010 |
20100088684 | Calculating Resource Bounds Of Programs Manipulating Recursive Data Structures And Collections - Bounding resource consumption of code that processes recursive data structures and collections includes making use of quantitative functions (based on user input) that are associated with a tuple of data-structures and whose semantics is specified by describing the effect of various data-structure methods on the relevant quantitative functions. Counter variables are incorporated into source code to count loop iterations (and number of recursive procedure call invocations). Relevant quantitative functions are incorporated into the source code to allow computation of invariants (and hence bounds) on the incorporated counter variables in terms of the quantitative functions. | 04-08-2010 |
20100318980 | STATIC PROGRAM REDUCTION FOR COMPLEXITY ANALYSIS - Described is an analysis tool/techniques for determining the computational complexity of a computer program, including when the program includes procedures having nested loops and/or multi-path loops. First, multi-path loops are converted into code-fragments consisting of simpler loops via a transformation called control flow refinement. Progress invariants are determined for appropriate locations in the procedure to represent relationships between a state that can arise at that program location and the previous state at that location. A bound finding mechanism (such as one based on pattern matching) is then used to compute loop bounds from progress invariants. These bounds are then composed appropriately to determine a precise bound for the enclosing procedure. | 12-16-2010 |
20110078665 | COMPUTING A SYMBOLIC BOUND FOR A PROCEDURE - A system that facilitates computing a symbolic bound with respect to a procedure that is executable by a processor on a computing device is described herein. The system includes a transition system generator component that receives the procedure and computes a disjunctive transition system for a control location in the procedure. A compute bound component computes a bound for the transition system, wherein the bound is expressed in terms of inputs to the transition system. The system further includes a translator component that translates the bound computed by the compute bound component such that the bound is expressed in terms of inputs to the procedure. | 03-31-2011 |
20110302553 | GENERATING TEXT MANIPULATION PROGRAMS USING INPUT-OUTPUT EXAMPLES - A program creation system is described which generates a data manipulation program based on input-output examples. The created program may include a collection of subprograms together with a collection of corresponding selection conditions. When a new input item is received, a program execution module uses the selection conditions to select one of the subprograms. The program execution module then applies the selected subprogram to generate a new output item. The program creation system generates the program using a three-part approach, involving: generating sets of subprograms for the respective input-output examples; grouping the sets of programs into partitions and choosing representative subprograms for the partitions; and determining the selection conditions. A user interaction module provides various mechanisms which allow a user to interact with the program creation system and thereby improve the performance of the created program. | 12-08-2011 |
20120011084 | SEMANTIC ENTITY MANIPULATION USING INPUT-OUTPUT EXAMPLES - Semantic entity manipulation technique embodiments are presented that generate a probabilistic program capable of manipulating character strings representing semantic entities based on input-output examples. The program can then be used to produce a desired output consistent with the input-output examples from inputs of a type included in the examples. The probabilistic program is generated based on the output of parsing, transform and formatting modules. The parsing module employs a probabilistic approach to parsing the input-output examples. The transform module identifies a weighted set of transforms that are capable of producing the output item from the input items of an input-output example to a likelihood specified by their assigned weight. The formatting module generates formatting instructions that transform selected output parts into a form specified by the output items in the input-output examples. | 01-12-2012 |
20120011152 | Generating Programs Based on Input-Output Examples Using Converter Modules - A program generation system is described that generates a program based on a plurality of input-output examples. The input-output examples include input items and corresponding output items. The program generation system can include three component modules. A parsing module processes the input items and output items to provide a plurality of input parts and output parts, respectively. A transformation module determines, for each output part, whether the output part can be produced from a corresponding input part using one or more converter modules selected from a collection of candidate converter modules. A formatting module generates formatting instructions that transform selected output parts into a form specified by the output items. These three modules provide a generated program that embodies logic learned from the input-output examples; the generated program can be subsequently used to transform new input items into new respective output items. | 01-12-2012 |
20120197829 | QUANTIFIED BELIEF PROPAGATION - A quantified belief propagation (QBP) algorithm receives as input an existentially quantified boolean formula (QBF) of existentially quantified boolean variables, universally quantified variables, and boolean operators. A tripartite graph is constructed, and includes (i) there-exists nodes that correspond to and represent the existentially quantified variables, (ii) for-all nodes that correspond to and represent the universally quantified variables, and (iii) sub-formula nodes that correspond to and represent sub-formulas of the QBF. A set of boolean values of the existentially quantified variables is found by (i) passing a first message from an arbitrary sub-formula node to an arbitrary for-all node, and (ii) in response, passing a second message from the arbitrary for-all node to the arbitrary sub-formula node. | 08-02-2012 |
20120198322 | AUTOMATED TABLE TRANSFORMATIONS FROM EXAMPLES - Described herein are mechanisms for automatically generating a computer-executable program that transforms a first table in a first format to a second table in a second format by way of user-provided examples. A user provides an exemplary input table of a first format, where the input table may be a portion of the first table. The user also provides an exemplary output table of a second format, wherein contents of the output table correspond to contents of the input table. Based upon these user-provided examples, a table transform program is automatically generated, wherein the table transform program, when executed over the first table generates the second table. | 08-02-2012 |
20130144902 | INDUCTIVE SYNTHESIS OF TABLE-BASED STRING TRANSFORMATIONS - Inductive synthesis and combination framework technique embodiments are presented that generally perform string transformations involving lookup operations in one or more relational tables, either alone or in combination with other non-lookup operations. More particularly, a semantic string lookup transformation language is presented, which can be used to generate an inductive synthesis procedure that synthesizes a set of transformations involving lookup operations that are consistent with the given set of input-output examples. In addition, a combination framework for combining the lookup transformation language and its synthesis procedure, with other transformation languages and their associated synthesis procedures, is presented. The resulting combined synthesis procedures enable the combination framework to synthesize transformations on a rich variety of data-types. | 06-06-2013 |
20130188877 | SKETCH BEAUTIFICATION AND COMPLETION OF PARTIAL STRUCTURED-DRAWINGS - A sketch processing system is described herein for assisting a user in producing a drawing. In one implementation, the sketch processing system operates by: receiving ink strokes in response to creation of an original drawing; recognizing components and geometric constraints within the original drawing, to produce a recognized drawing; beautifying the original drawing by modifying at least one aspect of the recognized drawing in accordance with the recognized constraints, to produce a beautified drawing; and recognizing a recurring pattern in the beautified pattern (if any) and using that pattern to produce at least one added component to the beautified drawing. | 07-25-2013 |
20130275847 | AUTOMATED TABLE TRANSFORMATIONS FROM EXAMPLES - Described herein are mechanisms for automatically generating a computer-executable program that transforms a first table in a first format to a second table in a second format by way of user-provided examples. A user provides an exemplary input table of a first format, where the input table may be a portion of the first table. The user also provides an exemplary output table of a second format, wherein contents of the output table correspond to contents of the input table. Based upon these user-provided examples, a table transform program is automatically generated, wherein the table transform program, when executed over the first table generates the second table. | 10-17-2013 |
20140108305 | RANKING FOR INDUCTIVE SYNTHESIS OF STRING TRANSFORMATIONS - Ranking technique embodiments are presented that use statistical and machine learning techniques to learn the desired ranking function for use in inductive program synthesis for the domain of string transformations. This generally involves automatically creating a training dataset of positive and negative examples from a given set of training tasks, each including multiple input-output examples. From the training dataset, a ranking function is learned that assigns an expression in a program in the domain specific language to a likelihood measure. This ranking function is then used to compute likelihoods of learnt programs from a very small number of input-output examples for a new task. | 04-17-2014 |
20140282375 | Generating Program Fragments Using Keywords and Context Information - A program development framework (PDF) is described herein which allows a user to produce a program in piecemeal fashion by successively specifying program fragments. The PDF creates a new program fragment by receiving keyword information from the user that describes a new program fragment, and then identifies context information that pertains to a programmatic context in which the new program fragment appears within the overall program being created. The PDF then generates a set of candidate program fragments that satisfy the keyword information and the context information, and ranks those candidate program fragments based on ranking information. At least part of the ranking information may be based on statistical information that is produced by analyzing a corpus of previous programs produced by one or more users. The PDF then provides the ranked program fragments to the user using various user-friendly presentation strategies. | 09-18-2014 |