Martin T Vechev

8374978, Feb 12, 2013

May 28, 2010

12/789668

Ohad Shacham - Kfar Monash, IL
Martin Vechev - Yorktown Heights NY, US
Eran Yahav - Yorktown Heights NY, US

International Business Machines Corporation - Armonk NY

G06F 15/18

706 12

Methods and apparatus are provided for a context-sensitive dynamic bloat detection system. A profiling tool is disclosed that selects an appropriate collection implementation for a given application. The disclosed profiling tool uses semantic profiling together with a set of collection selection rules to make an informed choice. A collection implementation, such as an abstract data entity, is selected for a given program by obtaining collection usage statistics from the program. The collection implementation is selected based on the collection usage statistics using a set of collection selection rules. The collection implementation is one of a plurality of interchangeable collection implementations having a substantially similar logical behavior for substantially all collection types. The collection usage statistics indicate how the collection implementation is used in the given program. One or more suggestions can be generated for improving the collection allocated at a particular allocation context.

8495427, Jul 23, 2013

Oct 14, 2009

12/578975

Matthew R. Arnold - Hawthorne NY, US
Martin Vechev - Hawthorne NY, US
Eran Yahav - Hawthorne NY, US

International Business Machines Corporation - Armonk NY

G06F 11/00

714 35, 714 471, 714 381, 717130

Detecting defects in deployed systems, in one aspect, identify one or more monitoring agents used in a computer program. Total execution metric of the computer program and execution metric associated with the one or more monitoring agents are measured and the measure execution metric is compared with a specified overhead criteria. The execution of the one or more monitoring agents is adjusted based on the comparing step while the computer program is executing to meet the specified overhead criteria.

8495588, Jul 23, 2013

Apr 16, 2010

12/762002

Martin Vechev - Yorktown Heights NY, US
Eran Yahav - Yorktown Heights NY, US
Greta Yorsh - Tarrytown NY, US

International Business Machines Corporation - Armonk NY

G06F 9/44

717128

Given a program P, a specification S, and an abstraction function α, verification determines whether P satisfies the specification S under the abstraction α. If not, a trace T that violate the specification is selected, and either the abstraction α is refined or a constraint that avoids the trace T is computed and added to a set of constraints. The set of constraints are used to modify the program P.

8548966, Oct 1, 2013

Jan 11, 2011

13/004506

Martin Vechev - Yorktown Heights NY, US
Eran Yahav - Yorktown Heights NY, US

International Business Machines Corporation - Armonk NY

G06F 7/00
G06F 17/00

707701

A snapshot of an application executing on a processor is taken in response to detecting an assertion in a running application. The assertion is evaluated based on the snapshot asynchronously while allowing the application to continue executing. The results of the assertion evaluation are returned to the application.

8645917, Feb 4, 2014

Oct 14, 2009

12/578943

Matthew R. Arnold - Hawthorne NY, US
Martin Vechev - Hawthorne NY, US
Eran Yahav - Hawthorne NY, US

International Business Machines Corporation - Armonk NY

G06F 9/44

717118, 717116, 717117, 717119

A programming language support for debugging heap related errors includes one or more queries for determining one or more global properties associated with use of the area by the program. The one or more queries may be executed in parallel or concurrently and dynamically utilize available number of cores.

8646088, Feb 4, 2014

Jan 3, 2011

12/983407

Marco Pistoia - Amawalk NY, US
Omer Tripp - Har-Adar, IL
Martin Vechev - Yorktown Heights NY, US
Eran Yahav - Yorktown Heights NY, US

International Business Machines Corporation - Armonk NY

G06F 21/00

726 25, 726 22

A method is disclosed that includes tracking untrusted inputs through an executing program into a sink, the tracking including maintaining context of the sink as strings based on the untrusted inputs flow into the sink. The method also includes, while tracking, in response to a string based on an untrusted input being about to flow into the sink and a determination the string could lead to an attack if the string flows into a current context of the sink, endorsing the string using an endorser selected based at least on the current context of the sink, and providing the endorsed string to the sink. Computer program products and apparatus are also disclosed.

20100011362, Jan 14, 2010

Jul 14, 2008

12/172577

Maged M. Michael - Danbury CT, US
Vijay Anand Saraswat - Mahopac NY, US
Martin Vechev - White Plains NY, US

G06F 9/46

718100

There are provided methods for single-owner multi-consumer work queues for repeatable tasks. A method includes permitting a single owner thread of a single owner, multi-consumer, work queue to access the work queue using atomic instructions limited to only a single access and using non-atomic operations. The method further includes restricting the single owner thread from accessing the work queue using atomic instructions involving more than one access. The method also includes synchronizing amongst other threads with respect to their respective accesses to the work queue.

20110296424, Dec 1, 2011

May 28, 2010

12/789726

Michael Kuperstein - New York NY, US
Martin Vechev - Yorktown Heights NY, US
Eran Yahav - Yorktown Heights NY, US

INTERNATIONAL BUSINESS MACHINES CORPORATION - Armonk NY

G06F 9/46

718102

A framework is provided for automatic inference of memory fences in concurrent programs. A method is provided for generating a set of ordering constraints that prevent executions of a program violating a specification. One or more incoming avoidable transitions are identified for a state and one or more ordering constraints are refined for the state. The set of ordering constraints are generated by taking a conjunction of ordering constraints for all states that violate the specification. One or more fence locations can optionally be selected based on the generated set of ordering constraints.