Nec Laboratories America, Inc.

Nec Corporation

Nec Usa, Inc.

Aarti Gupta

Pranav N Ashar

Franjo Ivancic

Malay K Ganai

Sriram Sankaranarayanan

Zijiang Yang

Vineet Kahlon

Chao Wang

Gogul Balakrishnan

Sharad Malik

Naoto Maeda

Yu Yang

Ilya Shlyakhter

Anand Raghunathan

Srihari Cadambi

Nishant Sinha

William Robert Harris

Subhrajit Bhattacharya

Albert E Casavant

Khalil Ghorbal

Sicun Gao

Parasara Sridhar Duggirala

Sriram Sankarnarayanan

Truong X Nghiem

Swarat Chaudhuri

Zijian Yang

Prakash Prabhu

Aleksandr Zaks

Himanshu Jain

Jing Yang

Lintao Zhang

Anubhav Gupta

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.

Probabilistic model checking of systems with ranged probabilities

An interprocedural exception analysis and transformation framework for computer programming languages such as C++ that (1) captures the control-flow induced by exceptions precisely, and (2) transforms the given computer program into an exception-free program that is amenable for precise static analysis, verification, and optimizations.

Interprocedural exception method

A scalable, computer implemented method for finding subtle flaws in software programs. The method advantageously employs 1) scope bounding which limits the size of a generated model by excluding deeply-nested function calls, where the scope bounding vector is chosen non-monotonically, and 2) automatic specification inference which generates constraints for functions through the effect of a light-weight and scalable global analysis. Advantageously, scalable software model checking is achieved while at the same time finding more bugs.

Scope bounding with automated specification inference for scalable software model checking

A model is provided for transforming a program with a priori given class hierarchy that is induced by inheritance. An inheritance remover is configured to remove inheritance from a given program to produce an analysis-friendly program which does not include virtual-function pointer tables and runtime libraries associated with inheritance-related operations. The analysis-friendly program preserves the semantics of the given program with respect to a given class hierarchy. A clarifier is configured to identify implicit expressions and function calls and transform the given program into at least one intermediate program having explicit expressions and function calls.

Embedding class hierarchy into object models for multiple class inheritance

A system and method for discovering a set of possible iteration sequences for a given loop in a software program is described, to transform the loop representation. In a program containing a loop, the loop is partitioned into a plurality of portions based on splitting criteria. Labels are associated with the portions, and an initial loop automaton is constructed that represents the loop iterations as a regular language over the labels corresponding to the portions in the program. Subsequences of the labels are analyzed to determine infeasibility of the subsequences permitted in the automaton. The automaton is refined by removing all infeasible subsequences to discover a set of possible iteration sequences in the loop. The resulting loop automaton is used in a subsequent program verification or analysis technique to find violations of correctness properties in programs.

Control structure refinement of loops using static analysis

A system and method for deciding the satisfiability of a non-linear real decision problem is disclosed. Linear and non-linear constraints associated with the problem are separated. The feasibility of the linear constraints is determined using a linear solver. The feasibility of the non-linear constraints is determined using a non-linear solver which employs interval constraint propagation. The interval solutions obtained from the non-linear solver are validated using the linear solver. If the solutions cannot be validated, linear constraints are learned to refine a search space associated with the problem. The learned constraints and the non-linear constraints are iteratively solved using the non-linear solver until either a feasible solution is obtained or no solution is possible.

Integrating interval constraint propagation with nonlinear real arithmetic

Methods and systems for verifying the precision of a program that utilizes floating point operations are disclosed. Interval and affine arithmetic can be employed to build a model of the program including floating point operations and variables that are expressed as reals and integers, thereby permitting accurate determination of precision loss using a model checker. Abstract interpretation can be also employed to simplify the model. In addition, counterexample-guided abstraction refinement can be used to refine the values of parametric error constants introduced in the model.

Systems and methods for model checking the precision of programs employing floating-point operations

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.

System and method for generating error traces for concurrency bugs

Systems and methods are disclosed to verify a program by symbolically enumerating path programs; verifying each path program to determine if the path program is correct or leads to a violation of a correctness property; determining a conflict set from the path program if the path program is proved correct; using the conflict set to avoid enumerating other related path programs that are also correct.

Program verification through symbolic enumeration of control path programs

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.

System and method for monotonic partial order reduction

A system and method for generating test vectors includes generating traces of a system model or program stored in memory using a simulation engine. Simulated inputs are globally optimized using a fitness objective computed using a computer processing device. The simulation inputs are adjusted in accordance with feedback from the traces and fitness objective values by computing a distance between the fitness objective value and a reachability objective. Test input vectors are output based upon optimized fitness objective values associated with the simulated inputs to test the system model or program stored in memory.

System and method for feedback-guided test generation for cyber-physical systems using monte-carlo

A system and method for infeasible path detection includes performing a static analysis on a program to prove a property of the program. If the property is not proved, infeasible paths in the program are determined by performing a path-insensitive abstract interpretation. Information about such infeasible paths is used to achieve the effects of path-sensitivity in path-insensitive program analysis.

Path-sensitive analysis through infeasible-path detection and syntactic language refinement

A computer implemented method for the verification of concurrent software programs wherein the concurrent software program is partitioned into subsets named concurrent trace programs (CTPs) and each of the CTPs is evaluated using a satisfiability-based (SAT) symbolic analysis. By applying the SAT analysis to individual CTPs in isolation the symbolic analysis is advantageously more scalable and efficient.

Symbolic reduction of dynamic executions of concurrent programs

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.

Growing community of inventors

Princeton, NJ, United States of America

Aarti Gupta