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

1. 发明授权

US09659082B2 Semantic query language 有权
公开(公告)号：US09659082B2
公开(公告)日：2017-05-23
申请号：US13594883
申请日：2012-08-27
申请人： Sumit Gulwani , Geoffrey Gerson Zweig
发明人： Sumit Gulwani , Geoffrey Gerson Zweig
IPC分类号： G06F17/30
CPC分类号： G06F17/30672 , G06F17/30657 , G06F17/30684 , G06F17/30696
摘要： Various technologies described herein pertain to executing a mixed query to search a database retained in a data repository. The mixed query includes a regular expression, which is a pattern of elements, and a semantic constraint. The elements in the regular expression include a first wildcard, where the semantic constraint restricts a meaning of the first wildcard. Moreover, the elements in the regular expression include explicit lexical constraint(s) and/or disparate wildcard(s). For instance, semantic constraint(s) can restrict meaning(s) of the disparate wildcard(s). The mixed query is executed to retrieve results that match the pattern of the elements in the regular expression and satisfy the semantic constraint(s).

2. 发明授权

US08752029B2 Computing a symbolic bound for a procedure 有权
标题翻译：计算程序的符号约束
公开(公告)号：US08752029B2
公开(公告)日：2014-06-10
申请号：US12568710
申请日：2009-09-29
申请人： Sumit Gulwani , Florian Franz Zuleger , Sudeep Dilip Juvekar
发明人： Sumit Gulwani , Florian Franz Zuleger , Sudeep Dilip Juvekar
IPC分类号： G06F9/44
CPC分类号： G06F11/302 , G06F11/3089 , G06F11/3604
摘要： 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.
摘要翻译：这里描述了有助于计算相对于计算设备上的处理器可执行的过程的符号约束的系统。系统包括一个过渡系统发生器组件，该组件接收该过程并计算该过程中控制位置的分离过渡系统。计算边界分量计算过渡系统的边界，其中边界以过渡系统的输入表示。该系统还包括翻译器组件，其翻译由计算绑定组件计算的绑定，使得该界限以该过程的输入来表示。

3. 发明申请

US20140013299A1 GENERALIZATION AND/OR SPECIALIZATION OF CODE FRAGMENTS 审中-公开
标题翻译：代码片段的通用化和/或专业化
公开(公告)号：US20140013299A1
公开(公告)日：2014-01-09
申请号：US13542975
申请日：2012-07-06
申请人： Lucas Julien Bordeaux , Sumit Gulwani , Youssef Hamadi , Yi Wei
发明人： Lucas Julien Bordeaux , Sumit Gulwani , Youssef Hamadi , Yi Wei
IPC分类号： G06F9/44
CPC分类号： G06F8/30 , G06F8/36
摘要： Generalization and/or specialization of code fragments is described, for example, as part of a tool for software developers. In an embodiment, a developer inserts natural language expressing a programming task into code he or she is developing in an integrated development environment; a program synthesizer obtains relevant (possibly non-compiling) code fragments for the task, merges those together to form a snippet, specializes the snippet for the context of the code and inserts the specialized snippet into the code. For example, a pair of code fragments are obtained from a search engine and are merged by discarding statements which are not common to each of the pair. In examples, pairs of code fragments are selected using search engine ranks, user input, or frequency. In embodiments, placeholders replace variable names in the merged fragments. An example takes a syntax tree of the code being developed and uses that to specialize snippets.
摘要翻译：例如，作为软件开发人员工具的一部分，描述了代码片段的泛化和/或专业化。在一个实施例中，开发人员将表达编程任务的自然语言插入他或她正在集成开发环境中开发的代码; 一个程序合成器获得相关的（可能是非编译的）代码片段的任务，将这些代码段合并在一起形成一个代码段，专门为代码的上下文提供了一个代码段，并将专门的代码段插入到代码中。例如，从搜索引擎获得一对代码片段，并且通过丢弃对于每个对不常见的语句来合并。在示例中，使用搜索引擎排名，用户输入或频率来选择代码片段对。在实施例中，占位符替换合并的片段中的变量名。一个例子是正在开发的代码的语法树，并使用它来专门化代码段。

4. 发明授权

US08402439B2 Program analysis as constraint solving 有权
标题翻译：程序分析作为约束求解
公开(公告)号：US08402439B2
公开(公告)日：2013-03-19
申请号：US12147908
申请日：2008-06-27
申请人： Sumit Gulwani , Saurabh Srivastava , Ramarathnam Venkatesan
发明人： Sumit Gulwani , Saurabh Srivastava , Ramarathnam Venkatesan
IPC分类号： G06F9/44
CPC分类号： G06F8/49
摘要： 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.
摘要翻译：描述了一种技术，程序分析使用丰富的不变模板，可以为程序验证指定线性不等式的任意布尔组合。还描述了选择一个标识程序位置的剪辑，每个程序位置与不变模板相关联。验证产生二阶约束，将基于这些约束的二阶逻辑公式转换为一阶逻辑公式，然后将一阶逻辑公式转换为无量词的公式，然后将其转换为布尔可满足公式。现在可以将现成的约束求解器应用于布尔可满足公式以生成程序分析结果。可以使用各种模板来将二阶逻辑公式转换成一阶逻辑公式。进一步描述的是过程间分析以及最弱前提条件和最强后置条件的确定，适用于终止分析，时序界限分析，以及针对终端和安全属性生成大多数一般的反例。

5. 发明申请

US20120011152A1 Generating Programs Based on Input-Output Examples Using Converter Modules 有权
标题翻译：基于使用转换器模块的输入输出示例生成程序
公开(公告)号：US20120011152A1
公开(公告)日：2012-01-12
申请号：US12834031
申请日：2010-07-12
申请人： Sumit Gulwani , David P. Walker
发明人： Sumit Gulwani , David P. Walker
IPC分类号： G06F17/30
CPC分类号： G06F17/30569 , G06F8/51
摘要： 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.
摘要翻译：描述了基于多个输入输出示例生成程序的程序生成系统。输入输出示例包括输入项和相应的输出项。程序生成系统可以包括三个组件模块。解析模块分别处理输入项目和输出项目以分别提供多个输入部分和输出部分。变换模块针对每个输出部分确定是否可以使用从候选转换器模块的集合中选择的一个或多个转换器模块从相应的输入部分产生输出部分。格式化模块生成格式化指令，将选择的输出部分转换为由输出项指定的形式。这三个模块提供了一个生成的程序，体现了从输入输出示例中学到的逻辑; 生成的程序可以随后用于将新的输入项变换成新的相应的输出项。

6. 发明申请

US20090326907A1 PROGRAM ANALYSIS AS CONSTRAINT SOLVING 有权
标题翻译：程序分析作为约束解
公开(公告)号：US20090326907A1
公开(公告)日：2009-12-31
申请号：US12147908
申请日：2008-06-27
申请人： Sumit Gulwani , Saurabh Srivastava , Ramarathnam Venkatesan
发明人： Sumit Gulwani , Saurabh Srivastava , Ramarathnam Venkatesan
IPC分类号： G06F9/45 , G06F7/60
CPC分类号： G06F8/49
摘要： 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.
摘要翻译：描述了一种技术，程序分析使用丰富的不变模板，可以为程序验证指定线性不等式的任意布尔组合。还描述了选择一个标识程序位置的剪辑，每个程序位置与不变模板相关联。验证产生二阶约束，将基于这些约束的二阶逻辑公式转换为一阶逻辑公式，然后将一阶逻辑公式转换为无量词的公式，然后将其转换为布尔可满足公式。现在可以将现成的约束求解器应用于布尔可满足公式以生成程序分析结果。可以使用各种模板来将二阶逻辑公式转换成一阶逻辑公式。进一步描述的是过程间分析以及最弱前提条件和最强后置条件的确定，适用于终止分析，时序界限分析，以及针对终端和安全属性生成大多数一般的反例。

7. 发明申请

US20080172650A1 PROGRAM VERIFICATION AND DISCOVERY USING PROBABILISTIC INFERENCE 有权
标题翻译：使用概率论的程序验证和发现
公开(公告)号：US20080172650A1
公开(公告)日：2008-07-17
申请号：US11622904
申请日：2007-01-12
申请人： Sumit Gulwani , Vladimir Jojic , Nebojsa Jojic
发明人： Sumit Gulwani , Vladimir Jojic , Nebojsa Jojic
IPC分类号： G06F9/44
CPC分类号： G06F11/3608
摘要： In one embodiment, a computer system performs a method for verifying the validity or invalidity of a software routine by learning appropriate invariants at each program point. A computer system chooses an abstract domain that is sufficiently precise to express the appropriate invariants. The computer system associates an inconsistency measure with any two abstract elements of the abstract domain. The computer system searches for a set of local invariants configured to optimize a total inconsistency measure which includes a sum of local inconsistency measures. The computer system optimizes the total inconsistency measure for all input/output pairs of the software routine. In one embodiment, the optimization of total inconsistency is achieved by the computer system which repeatedly replaces a locally inconsistent invariant with a new invariant, randomly selected among the possible invariants which are locally less inconsistent with the current invariants at the neighboring program points.
摘要翻译：在一个实施例中，计算机系统通过在每个程序点学习适当的不变量来执行用于验证软件例程的有效性或无效性的方法。计算机系统选择足够精确的表示适当不变量的抽象域。计算机系统将不一致性度量与抽象域的任意两个抽象元素相关联。计算机系统搜索一组局部不变量，其被配置为优化包括本地不一致性度量的总和的总不一致性度量。计算机系统优化软件程序的所有输入/输出对的总不一致性测量。在一个实施例中，总体不一致性的优化是通过计算机系统实现的，该计算机系统在局部地与邻近程序点的当前不变量局部较不一致的可能不变量中随机选择新的不变量来重复地替换局部不一致的不变量。

8. 发明授权

US09613115B2 Generating programs based on input-output examples using converter modules 有权
公开(公告)号：US09613115B2
公开(公告)日：2017-04-04
申请号：US12834031
申请日：2010-07-12
申请人： Sumit Gulwani , David P. Walker
发明人： Sumit Gulwani , David P. Walker
IPC分类号： G06F17/30 , G06F9/45
CPC分类号： G06F17/30569 , G06F8/51
摘要： 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.

9. 发明授权

US09400639B2 Generating programs using context-free compositions and probability of determined transformation rules 有权
标题翻译：使用无上下文的构图和确定的转换规则的概率生成程序
公开(公告)号：US09400639B2
公开(公告)日：2016-07-26
申请号：US13530138
申请日：2012-06-22
申请人： Adam Kalai , Butler Lampson , Sumit Gulwani , Aditya Krishna Menon , Omer Tamuz
发明人： Adam Kalai , Butler Lampson , Sumit Gulwani , Aditya Krishna Menon , Omer Tamuz
IPC分类号： G06F9/44 , G06N5/02 , G06F17/22
CPC分类号： G06F8/30 , G05B19/0423 , G05B2219/23246 , G06F8/34 , G06F17/2282 , G06N5/025 , G06N99/005
摘要： There is provided a method and system for generating a program. The method includes detecting a number of steps for performing a task on a computing device and detecting an example relating to each of the steps, wherein the example includes input data and corresponding output data relating to the step. The method also includes, for each example, determining a rule that transforms the input data to the corresponding output data based on cues including textual features within the input data and the corresponding output data. The method further includes generating a program for performing the task based on the rules.
摘要翻译：提供了一种用于生成程序的方法和系统。该方法包括检测用于在计算设备上执行任务的步骤的数量，并且检测与每个步骤相关的示例，其中该示例包括与步骤相关的输入数据和对应的输出数据。该方法还包括，对于每个示例，确定基于包括输入数据和对应的输出数据内的文本特征的提示将输入数据变换为相应的输出数据的规则。该方法还包括基于规则生成用于执行任务的程序。

10. 发明授权

US08799234B2 Semantic entity manipulation using input-output examples 有权
标题翻译：使用输入输出示例的语义实体操作
公开(公告)号：US08799234B2
公开(公告)日：2014-08-05
申请号：US13020153
申请日：2011-02-03
申请人： Sumit Gulwani , Rishabh Singh
发明人： Sumit Gulwani , Rishabh Singh
IPC分类号： G06F17/30
CPC分类号： G06F17/246 , G06F17/2282 , G06F17/2715 , G06N7/005
摘要： 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.
摘要翻译：提出了语义实体操纵技术实施例，其生成能够基于输入输出示例来操纵表示语义实体的字符串的概率程序。然后可以使用该程序产生与输入输出示例一致的期望输出，该输入输出示例包括在示例中的类型的输入。概率程序是基于解析，转换和格式化模块的输出生成的。解析模块采用概率方法来解析输入输出示例。变换模块识别能够从输入输出示例的输入项产生到其分配权重所指定的似然性的输出项的加权变换集合。格式化模块生成格式化指令，将指定的输出部分转换为输入输出示例中输出项所指定的格式。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式