International Business Machines Corporation

Technion Research & Development Foundation Limited

Codota Dot Com Ltd.

Eran Yahav

Martin Vechev

Greta Yorsh

Matthew R Arnold

Nimrod Sebban Partush

Michael Kuperstein

Moshe Yaniv David

Omer Tripp

Marco Pistoia

Mark N Wegman

Ohad Shacham

Arun Raman

Vivek Sarkar

Raghavan Raman

A computer implemented method of estimating a similarity of binary records comprising executable code, comprising converting a first binary record and a second binary record to a first intermediate representation (IR) and a second IR respectively, decomposing each of the first IR and the second IR to a plurality of strands which are partial dependent chains of program instructions, calculating a probability score for each of the plurality of strands of the first IR to have an equivalent counterpart in the second IR by comparing each strand of the first IR to one or more strands of the second IR, adjusting the probability score for each strand according to a significance value calculated for each strand and calculating a similarity score defining a functional similarity between the first IR and the second IR by aggregating the adjusted probability score of the plurality of strands.

Similarity of binaries

A method, computerized apparatus and computer program product for providing a code segment in response to a query, the method comprising using at least one hardware processor for: receiving a multiplicity of code segments and meta data related to the code segments; analyzing each code segment of the multiplicity of code segments, said analyzing comprising: semantically analyzing the code segment to obtain a first rank, structurally analyzing the code segment to obtain a second rank, and analyzing the meta data associated with the code segment to obtain a third rank; combining the first rank, second rank and third rank into a total rank associated with the code segment; receiving a query; matching the query to each of the multiplicity of code segments to identify matching code segments; and providing the matching code segments in accordance with total ranks associated with each of the matching code segments.

Code searching and ranking

A method comprising: receiving a multiplicity of videos from a source; for each video: receiving meta data related to the video; extracting from the video a video frame containing computer code; identifying a region of interest (ROI) within the video frame; performing OCR of the ROI to extract a code segment; analyzing the code segment by: semantically analyzing the code segment to obtain a first rank, structurally analyzing the code segment to obtain a second rank, and analyzing the meta data to obtain a third rank; and combining the first rank, second rank and third rank into a total rank associated with the code segment; receiving a query; matching the query to each code segment to identify matching code segments and associated videos; and providing the associated videos in accordance with total ranks associated with the matching code segments.

Searching and ranking of code in videos

A profiler may identify potentially-independent remote data accesses in a program. A remote data access is independent if value returned from said remote data access is not computed from another value returned from another remote data access appearing logically earlier in the program. A program rewriter may generate a program-specific prefetcher that preserves the behavior of the program, based on profiling information including the potentially-independent remote data accesses identified by the profiler. An execution engine may execute the prefetcher and the program concurrently. The execution engine may automatically decide which of said potentially-independent remote data accesses should be executed in parallel speculatively. A shared memory shared by the program and the prefetcher stores returned data from a data source as a result of issuing the remote data accesses.

Speculative prefetching of remote data

Techniques are provided for automatic verification and inference of memory fences in concurrent programs that can bound the store buffers that are used to model relaxed memory models. A method is provided for determining whether a program employing a relaxed memory model satisfies a safety specification. An abstract memory model is obtained of the relaxed memory model. The abstract memory model represents concrete program states of the program as a finite number of abstract states. The safety specification is evaluated for the program on the abstract memory model having the finite number of abstract states. Fence positions at one or more locations can be determined to ensure that the safety specification is satisfied.

Automatic verification and synthesis for weak memory models

Given a program P, a specification S, and an abstraction function &#x3b1;, verification determines whether P satisfies the specification S under the abstraction &#x3b1;. If not, a trace T that violate the specification is selected, and either the abstraction &#x3b1; 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.

Abstraction-guided synthesis

Automatic verification of determinism in structured parallel programs includes sequentially establishing whether code for each of a plurality of tasks of the structured parallel program is independent, outputting sequential proofs corresponding to the independence of the code for each of the plurality of tasks and determining whether all memory locations accessed by parallel tasks of the plurality of tasks are independent based on the sequential proofs.

Automatic verification of determinism for parallel programs

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.

Synthesis of memory barriers

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.

Providing support for debugging heap related errors with heap assertions

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.

Runtime enforcement of security checks

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.

Asynchronous assertions

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.

Detecting defects in deployed systems

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.

Growing community of inventors

Haifa, Israel

Eran Yahav