Patrice I Godefroid

6697840, Feb 24, 2004

Feb 29, 2000

09/515737

Patrice Ismael Godefroid - Naperville IL
James David Herbsleb - Naperville IL
Lalita Jategaonkar Jagadeesan - Naperville IL
Du Li - Los Angeles CA

Lucent Technologies Inc. - Murray Hill NJ

G06F 1516

709205, 709204, 709227, 709224

Presence awareness initiatives are implemented in a collaborative system that enables a user to set presence awareness policies, and that provides a reasonably high assurance that the system will correctly implement those policies. Specifically, the collaborative presence awareness system is such as to enable users to specify complex presence awareness policies. The presence awareness system is also such as to have been verified by employing systematic state-space exploration tools to establish a high level of assurance that the presence awareness system has the capability to implement correctly, substantially all possible presence awareness policies. Further, in accordance with another aspect of the invention, the presence awareness policy specifications are modular relative to the rest of the presence awareness system, and can be modified without having to modify computational modules or user interface program code of the presence awareness system. In accordance with another aspect of the invention, a user has the capability to update his or her presence information. In accordance with still another aspect of the invention, the system automatically collects presence information about the user and automatically updates his or her presence information.

6708328, Mar 16, 2004

Dec 17, 1999

09/465578

Glenn R. Bruns - Naperville IL
Patrice Ismael Godefroid - Naperville IL

Lucent Technologies Inc. - Murray Hill NJ

G06F 944

717135, 703 17, 709318, 714 38

A first system for analysis of a portion of a partial state space includes a representation component and an analysis component. The portion of the partial state space is related to a part of a second system. The representation component of the first system employs a value in the portion of the partial state space to represent that information for the part of the second system is unknown. The analysis component of the first system employs the value in the portion of the partial state space to analyze, in response to an analysis question that is related to the part of the second system, the portion of the partial state space.

7002903, Feb 21, 2006

May 23, 2001

09/863857

Satish Chandra - Naperville IL, US
Patrice I. Godefroid - Naperville IL, US
Christopher D. Palm - Naperville IL, US
Steven M. Welsh - Aurora IL, US

Lucent Technologies Inc. - Murray Hill NJ

H04J 11/00

370209, 370342

A method of verifying that a CDMA code allocator maintains mutual orthogonality between all concurrently busy codes includes the steps of identifying a code being allocated by the allocator, and determining if the identified code is busy. It is also determined if any ancestral parent of the identified code is busy, and if any descendant of the identified code is busy. If the identified code, one of the identified code's ancestral parents, or one of the identified code's descendants is determined to be busy, then an error in allocator operation is indicated.

7716322, May 11, 2010

Sep 23, 2002

10/252210

Michael Abraham Benedikt - Chicago IL, US
Juliana Freire Silva - Portland OR, US
Patrice Ismael Godefroid - Naperville IL, US
Avinash Vyas - North Plainfield NJ, US

Alcatel-Lucent USA Inc. - Murray Hill NJ

G06F 15/173
G06F 15/16
G06F 17/00
G06F 17/27

709224, 709217, 715224, 715226

A unique tool, i. e. , “VeriWeb”, is employed to automatically discover and systematically explore Web-site execution paths that can be followed by a user in a Web application. Unlike traditional spiders (or crawlers) that are limited to the exploration of static links, VeriWeb can navigate automatically through dynamic components of Web sites, including form submissions and execution of client-side scripts. Whenever examining a new Web page, the system determines all possible actions a user might perform—be it a link, via a button with a JavaScript handler, or via form submission—and can execute them in a systematic way. In order to systematically test different paths in a Web site, VeriWeb addresses two critical problems: systematic Web site exploration and automatically filling out forms.

8549486, Oct 1, 2013

Apr 21, 2008

12/106811

Patrice Godefroid - Mercer Island WA, US
Michael Y. Levin - Sammamish WA, US
David Molnar - Berkeley CA, US

Microsoft Corporation - Redmond WA

G06F 9/44

717128

An exemplary method includes providing software for testing; during execution of the software, performing a symbolic execution of the software to produce path constraints; injecting issue constraints into the software where each issue constraint comprises a coded formula; solving the constraints using a constraint solver; based at least in part on the solving, generating input for testing the software; and testing the software using the generated input to check for violations of the injected issue constraints. Such a method can actively check properties of the software. Checking can be performed on a path for a given input using a constraint solver where, if the check fails for the given input, the constraint solver can also generate an alternative input for further testing of the software. Various exemplary methods, devices, systems, etc. , are disclosed.

8578344, Nov 5, 2013

Jun 17, 2010

12/817291

Patrice Godefroid - Mercer Island WA, US
Shuvendu Kumar Lahiri - Redmond WA, US
Cindy Rubio-Gonzalez - Madison WI, US

Microsoft Corporation - Redmond WA

G06F 9/44

717131, 717122, 717124

Concepts and technologies are described herein for incremental compositional dynamic test generation. The concepts and technologies described herein are used to increase the code coverage and security vulnerability identification abilities of testing applications and devices, without significantly increasing, and in some cases decreasing, computational and time costs associated with the testing. Test summaries that describe how code is tested by a test engine are generated and stored during testing of code. These test summaries can be evaluated when additional iterations or versions of the code are tested. If functions corresponding to the test summaries are unchanged from, or logically equivalent to, a version of the function previously tested, the test summary may be used when testing the new version of the code.

20060253739, Nov 9, 2006

May 3, 2005

11/120776

Patrice Godefroid - Naperville IL, US
Nils Klarlund - Chatham NJ, US
Koushik Sen - Champaign IL, US

G06F 11/00

714038000

A method and apparatus for performing unit testing of software modules uses a novel directed automated random testing approach that advantageously combines automated extraction of the interface of a program with its external environment using static source code parsing; automatic generation of a test driver for this interface that advantageously performs random testing to simulate the most general environment the program can operate in; and dynamic analysis of how the program behaves under random testing and automatic generation of new test inputs to direct systematically the execution along alternative program paths. Together, these techniques constitute a directed automated random testing approach (DART). With DART, testing can be performed completely automatically on any program that compiles without the need to write any test driver or harness code. During testing, DART detects standard errors such as program crashes, assertion violations, and non-termination conditions.

20100251221, Sep 30, 2010

Mar 24, 2009

12/410177

Aditya V. Nori - Bangalore, IN
Patrice Godefroid - Mercer Island WA, US
Sriram Rajamani - Bangalore, IN
Sai Deep Tetali - Bangalore, IN

MICROSOFT CORPORATION - Redmond WA

G06F 11/36

717131

A method of analyzing a computer application is disclosed. The method may break an application into components and the method may determine if the components have already been analyzed for errors, either through static analysis or by a code analysis. If the component has already been analyzed, the previous analysis may be used and the method may move on to the next code section. If the component has not been analyzed, it may be determined if the component may be reached from a given starting point. If the component cannot be reached from a given starting point, the component may not be analyzed. Both static and code testing tools may be used to determine if errors exist. The fined-grained coupling and alternation of may (universal) and must (existential) summaries allow the method to easily navigate through these code fragments while traditional may-only, must-only or non-compositional may-must al-gorithms are stuck in their specific analyses.