# Vineet Kahlon, Princeton US

## Vineet Kahlon, Princeton, NJ US

Patent application number | Description | Published |
---|---|---|

20080229286 | SYSTEM AND METHOD FOR SCALABLE FLOW AND CONTEXT-SENSITIVE POINTER ALIAS ANALYSIS - A system and method for pointer analysis for computer program verification includes forming a subset or cluster of pointers from pointers in a program by applying increasingly accurate alias analyses in a cascaded fashion such that each analysis works on a subset of pointers generated by a previous analysis's results. Aliases are computed for any pointer by computing aliases in the subsets in parallel instead of an entire program. For carrying out context and flow-sensitive alias analysis, function summaries are computed on small subsets in a top-down manner based on the points-to hierarchy which reduces the sizes of the summaries. | 09-18-2008 |

20080282221 | ACCELERATING MODEL CHECKING VIA SYNCHRONY - A system and method for program verification by model checking in concurrent programs includes modeling each of a plurality of program threads as a circuit model, and generating a full circuit for an entire program by combining the circuit models including constraints which enforce synchronous execution of the program threads. The program is verified using the synchronous execution to reduce an amount of memory needed to verify the program and a number of steps taken to uncover an error. | 11-13-2008 |

20090089783 | PARTIAL ORDER REDUCTION USING GUARDED INDEPENDENCE RELATIONS - A system and method for conducting symbolic partial order reduction for concurrent systems includes determining a guarded independence relation which includes transitions from different threads that are independent for a set of states, when a condition or predicate holds. Partial order reduction is performed using the guarded independence relation to permit automatic pruning of redundant thread interleavings when the guarded independence condition holds. | 04-02-2009 |

20090125887 | SYSTEM AND METHOD FOR GENERATING ERROR TRACES FOR CONCURRENCY BUGS - A system and method for program verification includes generating a product transaction graph for a concurrent program, which captures warnings for potential errors. The warnings are filtered to remove bogus warnings, by using constraints from synchronization primitives and invariants that are derived by performing one or more dataflow analysis methods for concurrent programs. The dataflow analysis methods are applied in order of overhead expense. Concrete execution traces are generated for remaining warnings using model checking. | 05-14-2009 |

20090193416 | DECIDABILITY OF REACHABILITY FOR THREADS COMMUNICATING VIA LOCKS - A system and method for deciding reachability includes inputting a concurrent program having threads interacting via locks for analysis. Bounds on lengths of paths that need to be explored are computed to decide reachability for lock patterns by assuming bounded lock chains. Reachability is determined for a pair of locations using a bounded model checker. The program is updated in accordance with the reachability determination. | 07-30-2009 |

20090193417 | TRACTABLE DATAFLOW ANALYSIS FOR CONCURRENT PROGRAMS VIA BOUNDED LANGUAGES - A system and method for dataflow analysis includes inputting a concurrent program comprised of threads communicating via synchronization primitives and shared variables. Synchronization constraints imposed by the primitives are captured as an intersection problem for bounded languages. A transaction graph is constructed to perform dataflow analysis. The concurrent program is updated in accordance with the dataflow analysis. | 07-30-2009 |

20090204968 | SYSTEM AND METHOD FOR MONOTONIC PARTIAL ORDER REDUCTION - A system and method for analyzing concurrent programs that guarantees optimality in the number of thread inter-leavings to be explored. Optimality is ensured by globally constraining the inter-leavings of the local operations of its threads so that only quasi-monotonic sequences of threads operations are explored. For efficiency, a SAT/SMT solver is used to explore the quasi-monotonic computations of the given concurrent program. Constraints are added dynamically during exploration of the concurrent program via a SAT/SMT solver to ensure quasi-montonicity for model checking. | 08-13-2009 |

20100235817 | FAST AND ACCURATE DATA RACE DETECTION FOR CONCURRENT PROGRAMS WITH ASYNCHRONOUS CALLS - A system and method for analyzing a concurrent program employ asynchronous function calls for communication and recursion. A control flow graph is constructed based on a context-sensitive pointer analysis, whereupon encountering a function pointer, a points-to set of the function pointer is computed in a context-sensitive fashion to determine a set of potential function calls. The context-sensitive pointer analysis is terminated when no new potential function calls are encountered and where the potential function calls may contribute new data races other than those that exist in the contexts traversed thus far. To decide this, a characterization of pointer aliasing based upon complete update sequences is employed. A set of contexts that may contribute to different data races are enumerated by tracking update sequences for function and lock pointers and pointers that are shared or point to shared memory locations. Data race detection is carried out on the control flow graph. | 09-16-2010 |

20110010693 | SYSTEM AND METHOD FOR VERIFICATION OF PROGRAMS USING THREADS HAVING BOUNDED LOCK CHAINS - A system and method for model checking of concurrent multi-threaded programs with bounded lock chains includes analyzing individual program threads in a concurrent multi-threaded program to determine sets of reachable states and lock access patterns for bounded lock chains by tracking sets of states reachable from a given set of states and tracking lock acquisitions and releases by maintaining a bi-directional lock causality graph. Analysis results from multiple threads are combined using an acceptance condition of the lock causality graph to determine whether there is a violation of a correctness property in the concurrent multi-threaded program. | 01-13-2011 |

20110167412 | UNIVERSAL CAUSALITY GRAPHS FOR BUG DETECTION IN CONCURRENT PROGRAMS - A system and method for predictive analysis includes generating an execution trace on an instrumented version of source code for a multithreaded computer program. Interleavings which potentially lead to a violation in the program are statically generated by performing a static predictive analysis using a Universal Causality Graph (UCG) to generate alternative interleavings that might lead to an error. The UCG includes a unified happens-before model for the concurrent program and a property being analyzed. The interleavings are symbolically checked to determine errors in the program. | 07-07-2011 |

20110276969 | LOCK REMOVAL FOR CONCURRENT PROGRAMS - A system and method are disclosed for removing locks from a concurrent program. A set of behaviors associated with a concurrent program are modeled as causality constraints. The causality constraints which preserve the behaviors of the concurrent program are identified. Having identified the behavior preserving causality constraints, the corresponding lock and unlock statements in the concurrent program are identified which enforce the identified causality constraints. All identified lock and unlock statements are retained, while all other lock and unlock statements are discarded. | 11-10-2011 |

20120079483 | Computer Implemented Automatic Lock Insertion in Concurrent Programs - Method provides a fully automatic lock insertion procedure to enforce critical sections that guarantees deadlock freedom and tries to minimize the lengths of the resulting critical sections. Method encapsulates regions of code meant to be executed atomically in a critical section induced by a pair of lock unlock statements and enlarges the critical section of the first thread by propagating the newly introduced lock statement backwards till it no longer participates in a deadlock. If the newly introduced lock statement participates in a deadlock, the process terminates. If lock statement of the second thread participates in a deadlock the method enlarges the critical section of the second thread by propagating the newly introduced lock statement backwards until it no longer participates in a deadlock. | 03-29-2012 |

20120179935 | DYNAMIC TEST GENERATION FOR CONCURRENT PROGRAMS - A computer implemented method for dynamic test generation for concurrent programs, which uses a combination of concrete and symbolic execution of the program to systematically cover all the intra-thread program branches and inter-thread interleavings of shared accesses. In addition, a coverage summary based pruning technique, which is a general framework for soundly removing both redundant paths and redundant interleavings and is capable of speeding up dynamic testing exponentially. This pruning framework also allows flexible trade-offs between pruning power and computational overhead to be exploited using various approximations. | 07-12-2012 |

20120290883 | Computer Implemented Method for Precise May-Happen-in-Parallel Analysis with Applications to Dataflow Analysis of Concurrent Programs - A computer implemented method for automatically for determining errors in concurrent program using lock localization graphs for capturing few relevant lock/unlock statements and function calls required for reasoning about interference at a thread location at hand, responsive to first and second threads of a concurrent program, constructing generalized lock causality graphs and computing cycle signatures, and determining errors in the concurrent program responsive to computing an interference graph and data flow analysis. | 11-15-2012 |

20130091080 | PROBABILISTIC MODEL CHECKING OF SYSTEMS WITH RANGED PROBABILITIES - Systems and methods for model checking of live systems are shown that include learning an interval discrete-time Markov chain (IDTMC) model of a deployed system from system logs; and checking the IDTMC model with a processor to determine a probability of violating one or more probabilistic safety properties. Checking the IDTMC model includes calculating a linear part exactly using affine arithmetic; and over-approximating a non-linear part using interval arithmetic. | 04-11-2013 |

20130332906 | CONCURRENT TEST GENERATION USING CONCOLIC MULTI-TRACE ANALYSIS - A method to test a concurrent program by performing a concolic multi-trace analysis (CMTA) to analyze the concurrent program by taking two or more test runs over many threads and generating a satisfiability modulo theory (SMT) formula to select alternate inputs, alternate schedules and parts of threads from one or more test runs; using an SMT solver on the SMT formula for generating a new concurrent test comprising input values, thread schedules and parts of thread selections; and executing the new concurrent test. | 12-12-2013 |

20140019946 | LAYERED DECOMPOSITION FOR SCALABLE STATIC DATA RACE DETECTION OF CONCURRENT PROGRAMS - Disclosed is a method of performing static data race detection in concurrent programs wherein a control flow graph (CFG) is decomposed into layers of bounded call-depth which are then used to perform a resulting analysis. Next, a set of pointers of interest are segmented into classes such that each pointer may only be aliased to pointers within its own class, these classes related to computation of shared variables, locksets, waitsets, and notifysets. A flow sensitive context sensitive points-to-analysis for program statements that impact aliases of members within the given class is performedâ€”advantageously reducing the overall size of the problem at hand. Notably, the analysis for individual threads is performed independently of one another, on multiple layers of the CFG, and subsequently merging the results from the individual layers. | 01-16-2014 |