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

1. 发明授权

US08271404B2 Template based approach to discovering disjunctive and quantified invariants over predicate abstraction 有权
标题翻译：基于模板的方法来发现关于谓词抽象的分离和量化不变量
公开(公告)号：US08271404B2
公开(公告)日：2012-09-18
申请号：US12244674
申请日：2008-10-02
申请人： Sumit Gulwani , Ramarathnam Venkatesan , Saurabh Srivastava
发明人： Sumit Gulwani , Ramarathnam Venkatesan , Saurabh Srivastava
IPC分类号： G06F15/18
CPC分类号： G06F11/3608
摘要： 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.
摘要翻译：公开了在使用可满足性模理论（SMT）求解器的程序中生成复杂不变量的技术。在一个实施例中，生成的不变量可用于验证程序中的断言声明。另外或替代地，可以生成最弱的前置条件不变量，使得传递到满足最弱前置条件的程序的参数被保证满足程序的断言语句。另外或替代地，可以产生最强的后置条件，确定在程序完成时对程序的状态有保证是真实的。在一个实施例中，SMT求解器通过将谓词映射到模板中的未知变量来生成不变量。模板可以包括通过用分离定义的逻辑结构相关的未知变量，通用量词和存在量词。谓词可能包含程序变量之间的均等和不等式。

2. 发明授权

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.
摘要翻译：描述了一种技术，程序分析使用丰富的不变模板，可以为程序验证指定线性不等式的任意布尔组合。还描述了选择一个标识程序位置的剪辑，每个程序位置与不变模板相关联。验证产生二阶约束，将基于这些约束的二阶逻辑公式转换为一阶逻辑公式，然后将一阶逻辑公式转换为无量词的公式，然后将其转换为布尔可满足公式。现在可以将现成的约束求解器应用于布尔可满足公式以生成程序分析结果。可以使用各种模板来将二阶逻辑公式转换成一阶逻辑公式。进一步描述的是过程间分析以及最弱前提条件和最强后置条件的确定，适用于终止分析，时序界限分析，以及针对终端和安全属性生成大多数一般的反例。

3. 发明申请

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.
摘要翻译：描述了一种技术，程序分析使用丰富的不变模板，可以为程序验证指定线性不等式的任意布尔组合。还描述了选择一个标识程序位置的剪辑，每个程序位置与不变模板相关联。验证产生二阶约束，将基于这些约束的二阶逻辑公式转换为一阶逻辑公式，然后将一阶逻辑公式转换为无量词的公式，然后将其转换为布尔可满足公式。现在可以将现成的约束求解器应用于布尔可满足公式以生成程序分析结果。可以使用各种模板来将二阶逻辑公式转换成一阶逻辑公式。进一步描述的是过程间分析以及最弱前提条件和最强后置条件的确定，适用于终止分析，时序界限分析，以及针对终端和安全属性生成大多数一般的反例。

4. 发明申请

US20100088548A1 Using Constraint Solving to Discovering Disjunctive and Quantified Invariants Over Predicate Abstraction 有权
标题翻译：使用约束求解在谓词抽象上发现分离和量化不变量
公开(公告)号：US20100088548A1
公开(公告)日：2010-04-08
申请号：US12244674
申请日：2008-10-02
申请人： Sumit Gulwani , Ramarathnam Venkatesan , Saurabh Srivastava
发明人： Sumit Gulwani , Ramarathnam Venkatesan , Saurabh Srivastava
IPC分类号： G06F11/00
CPC分类号： G06F11/3608
摘要： 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.
摘要翻译：公开了在使用可满足性模理论（SMT）求解器的程序中生成复杂不变量的技术。在一个实施例中，生成的不变量可用于验证程序中的断言声明。另外或替代地，可以生成最弱的前置条件不变量，使得传递到满足最弱前置条件的程序的参数被保证满足程序的断言语句。另外或替代地，可以产生最强的后置条件，确定在程序完成时对程序的状态有保证是真实的。在一个实施例中，SMT求解器通过将谓词映射到模板中的未知变量来生成不变量。模板可以包括通过用分离定义的逻辑结构相关的未知变量，通用量词和存在量词。谓词可能包含程序变量之间的均等和不等式。

5. 发明授权

US08962016B2 Extended release dosage forms of metoprolol 有权
标题翻译：美托洛尔的延长释放剂型
公开(公告)号：US08962016B2
公开(公告)日：2015-02-24
申请号：US12954644
申请日：2010-11-25
申请人： Prashant Manohar Mandaogade , Venkatesh Madhavacharya Joshi , Saurabh Srivastava , Vinayak Dinkar Kadam , Girish Kumar Jain
发明人： Prashant Manohar Mandaogade , Venkatesh Madhavacharya Joshi , Saurabh Srivastava , Vinayak Dinkar Kadam , Girish Kumar Jain
IPC分类号： A61K9/48 , A61K9/00 , A61K9/20 , A61K9/50 , A61K31/435 , A61K31/138 , A61K31/554 , A61K31/18
CPC分类号： A61K31/138 , A61K9/2031 , A61K9/2054 , A61K9/2077 , A61K9/5047 , A61K9/5078
摘要： The present invention relates to extended release dosage forms of metoprolol or salts thereof comprising a water insoluble and non-swellable inert core and one or more pharmaceutically acceptable excipients. The invention also relates to processes for the preparation of an inert core and extended release dosage forms.
摘要翻译：本发明涉及美托洛尔或其盐的延长释放剂型，其包含水不溶性和不可溶胀的惰性核心和一种或多种药学上可接受的赋形剂。本发明还涉及制备惰性核心和延长释放剂型的方法。

6. 发明申请

US20090013070A1 SYSTEM AND METHOD FOR PROVIDING NETWORK APPLICATION PERFORMANCE MANAGEMENT IN A NETWORK 有权
标题翻译：网络中网络应用性能管理的系统和方法
公开(公告)号：US20090013070A1
公开(公告)日：2009-01-08
申请号：US11867288
申请日：2007-10-04
申请人： Saurabh Srivastava , Ravishankar Ravindran , Francois Blouin
发明人： Saurabh Srivastava , Ravishankar Ravindran , Francois Blouin
IPC分类号： G06F15/173
CPC分类号： H04L41/5038 , H04L43/12
摘要： The present invention relates to a system and method for network performance management for monitoring performance of network applications. The system comprises a transmitter for sending one or more types of probe packets to the network, a receiver for receiving the one or more network probe packets from the network and for receiving one or more network application performance queries from one or more network applications, a processor connected to the transmitter and the receiver and operable to process network probe packets received by the receiver to generate network performance statistics for each type of probe packet and to look up the network application performance requirements of the one or more network applications and compare the network application performance requirements with the corresponding network performance statistics to determine whether the network application should access the network. Network performance statistics may be obtained using lean packet probes, using real traffic test streams or obtaining network performance statistics from a service provider. Thus by providing a probe, lookup, feedback methodology, network parameters, or network application requirements, may be adjusted to meet performance requirements of one or more network applications.
摘要翻译：本发明涉及网络性能管理系统和方法，用于监控网络应用的性能。该系统包括用于向网络发送一种或多种类型的探测分组的发射机，用于从网络接收一个或多个网络探测分组并用于从一个或多个网络应用接收一个或多个网络应用性能查询的接收机，处理器连接到发射机和接收机，可操作以处理由接收机接收的网络探测分组，以生成每种类型的探测分组的网络性能统计信息，并查找一个或多个网络应用的网络应用性能要求，并比较网络应用性能要求与相应的网络性能统计确定网络应用是否应该访问网络。可以使用精简分组探测，使用实际流量测试流或从服务提供商获得网络性能统计信息来获得网络性能统计信息。因此，通过提供探测器，可以调整查找，反馈方法，网络参数或网络应用需求，以满足一个或多个网络应用的性能要求。

7. 发明申请

US20110169553A1 TEMPERATURE COMPENSATED CURRENT REFERENCE CIRCUIT 有权
标题翻译：温度补偿电流基准电路
公开(公告)号：US20110169553A1
公开(公告)日：2011-07-14
申请号：US12687849
申请日：2010-01-14
申请人： Sanjay K. Wadhwa , Saurabh Srivastava
发明人： Sanjay K. Wadhwa , Saurabh Srivastava
IPC分类号： H01L37/00
CPC分类号： G05F1/463
摘要： A temperature compensated current reference circuit has a differential amplifier and a first feedback transistor with a gate coupled to the differential amplifier output. The first feedback transistor couples a supply voltage line to an inverting input of the differential amplifier. There is also a second feedback transistor with a gate coupled to the differential amplifier output, which couples the supply voltage line to a non-inverting input of the differential amplifier. A first temperature dependent conductor couples the inverting input to ground. A primary reference resistor and a second temperature dependent conductor are connected in series and couple the non-inverting input to ground. An output current control transistor has a gate and one other electrode coupled together and a third electrode coupled to the supply voltage line. A secondary reference resistor and a conductivity change sensing transistor are connected in series and couple the gate of the output current control transistor to ground. The conductivity change sensing transistor has a gate coupled to the second one of the two differential inputs. There is a temperature compensation current reference output circuit that has a current reference transistor, an input coupled to the differential amplifier output and another input is coupled to the gate of the output current control transistor.
摘要翻译：温度补偿电流参考电路具有差分放大器和具有耦合到差分放大器输出的栅极的第一反馈晶体管。第一反馈晶体管将电源电压线耦合到差分放大器的反相输入端。还有一个第二反馈晶体管，其栅极耦合到差分放大器输出，其将电源电压线耦合到差分放大器的非反相输入端。第一温度依赖导体将反相输入端接地。主参考电阻和第二温度相关导体串联连接，并将非反相输入耦合到地。输出电流控制晶体管具有耦合在一起的栅极和另一个电极以及耦合到电源电压线的第三电极。二次参考电阻和电导率变化感测晶体管串联连接，并将输出电流控制晶体管的栅极耦合到地。电导率变化感测晶体管具有耦合到两个差分输入中的第二个的栅极。具有温度补偿电流基准输出电路，其具有电流参考晶体管，耦合到差分放大器输出的输入端和另一输入端耦合到输出电流控制晶体管的栅极。

8. 发明授权

US5959536A Task-driven distributed multimedia consumer system 失效
标题翻译：任务驱动的分布式多媒体消费系统
公开(公告)号：US5959536A
公开(公告)日：1999-09-28
申请号：US731624
申请日：1996-10-15
申请人： Paul Chambers , Saurabh Srivastava
发明人： Paul Chambers , Saurabh Srivastava
IPC分类号： G06F13/10 , G06F9/06 , G06F9/445 , H04L12/28 , G08B21/00 , G06F9/45
CPC分类号： H04L12/2814 , G06F9/4411 , H04L12/2805 , H04L12/2809 , H04L2012/285
摘要： A control system comprises multiple consumer electronics devices and task-driven control means coupled to the devices for controlling an interaction among the devices. The control means acts on respective software representations of each respective one of the consumer devices. By encapsulating the variable complexity of the task within a software representation, it can be made as simple or as sophisticated as needed to bring the capabilities up to a common level. Since the level of interface is common to the devices, applications can uniformly manipulate devices which embody very different levels of sophistication.
摘要翻译：控制系统包括多个消费电子设备和耦合到设备的任务驱动控制装置，用于控制设备之间的交互。控制装置作用于各个消费者装置的相应软件表示。通过将任务的可变复杂度封装在软件表示内，可以使其可以根据需要简单或复杂，以将功能提升到一个共同的水平。由于接口级别对于设备是通用的，应用程序可以均匀地操纵体现非常不同级别的复杂性的设备。

9. 发明授权

US08815285B2 Extended release dosage forms of metoprolol 有权
标题翻译：美托洛尔的延长释放剂型
公开(公告)号：US08815285B2
公开(公告)日：2014-08-26
申请号：US12225746
申请日：2007-03-28
申请人： Prashant Manohar Mandaogade , Venkatesh Madhavacharya Joshi , Saurabh Srivastava , Vinayak Dinkar Kadam , Girish Kumar Jain
发明人： Prashant Manohar Mandaogade , Venkatesh Madhavacharya Joshi , Saurabh Srivastava , Vinayak Dinkar Kadam , Girish Kumar Jain
IPC分类号： A61K9/62 , A61K9/58 , A61K9/22 , A61K9/16 , A61K31/138 , A61P9/00 , A61P9/04 , A61P9/12 , A61K9/20 , A61K9/50
CPC分类号： A61K31/138 , A61K9/2031 , A61K9/2054 , A61K9/2077 , A61K9/5047 , A61K9/5078
摘要： The present invention relates to extended release dosage forms of metoprolol or salts thereof comprising a water insoluble and non-swellable inert core and one or more pharmaceutically acceptable excipients. The invention also relates to processes for the preparation of an inert core and extended release dosage forms.
摘要翻译：本发明涉及美托洛尔或其盐的延长释放剂型，其包含水不溶性和不可溶胀的惰性核心和一种或多种药学上可接受的赋形剂。本发明还涉及制备惰性核心和延长释放剂型的方法。

10. 发明申请

US20130055144A1 CONVERSATION EXPLORER WITH SPLIT NAVIGATION USER INTERFACE 有权
标题翻译：具有分离导航用户界面的对话探测器
公开(公告)号：US20130055144A1
公开(公告)日：2013-02-28
申请号：US13219388
申请日：2011-08-26
申请人： Srivatsan Santhanam , Raghavendra Deshpande , Saurabh Srivastava , Muthuraman M. , Nakul P. Shenoy
发明人： Srivatsan Santhanam , Raghavendra Deshpande , Saurabh Srivastava , Muthuraman M. , Nakul P. Shenoy
IPC分类号： G06F3/048
CPC分类号： H04L51/16
摘要： According to some embodiments, a method and system provides receiving a list of a plurality of conversations, each of the conversations associated with a common set of characteristics and each of the conversations having associated conversation details; presenting at least a portion of the list of the plurality of conversations in a user interface, each of the conversations included in the presented portion of the list being separately represented; receiving a selection of a plurality of the conversations included in the presented portion of the list; and presenting, simultaneously and grouped together in the user interface, conversation details associated with each of the selected plurality of the conversations, separate and apart from the presented portion of the list.
摘要翻译：根据一些实施例，一种方法和系统提供接收多个对话的列表，每个对话与一组共同特征相关联，每个对话具有相关联的对话细节; 在用户界面中呈现多个对话的列表的至少一部分，包括在列表的呈现部分中的每个会话被分别表示; 接收列表中呈现的部分中包括的多个会话的选择; 并且在所述用户界面中呈现，同时并分组在一起，与所述所选择的多个对话中的每一个相关联的对话细节与所述列表的所呈现的部分分开并分开。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式