# Franjo Ivancic, Princeton US

## Franjo Ivancic, Princeton, NJ US

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

20090094004 | METHODS AND SYSTEMS FOR EFFICIENT ANALYSIS OF HYBRID SYSTEMS USING TEMPLATE POLYHEDRA - In accordance with aspects of the present principles, an over-approximation of reachable states of a hybrid system may be determined by utilizing template polyhedra. Policy iteration may be utilized to obtain an over-approximation of reachable states in the form of a relaxed invariant based upon template polyhedra expressions. The relaxed invariant may be used to construct a flowpipe to refine the over-approximation and thereby determine the reachable states of the hybrid system. | 04-09-2009 |

20090192963 | SYSTEM AND METHOD FOR DYNAMICALLY INFERRING DATA PRECONDITIONS OVER PREDICATES BY TREE LEARNING - A system and method for inferring preconditions for procedures in a program includes formulating predicates based on inputs to a procedure, including formal arguments, global variables and external environment. Truth assignments are sampled to the predicates to provide truth assignments that lead to a feasible set of input values. Test cases are generated for testing the program in accordance with the truth assignments having feasible sets of input values. The truth assignments are classified to the predicates as providing an error or not providing an error. | 07-30-2009 |

20090193401 | PATH-SENSITIVE ANALYSIS THROUGH INFEASIBLE-PATH DETECTION AND SYNTACTIC LANGUAGE REFINEMENT - 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. | 07-30-2009 |

20100005454 | PROGRAM VERIFICATION THROUGH SYMBOLIC ENUMERATION OF CONTROL PATH PROGRAMS - 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. | 01-07-2010 |

20100058475 | FEEDBACK-GUIDED FUZZ TESTING FOR LEARNING INPUTS OF COMA - Embodiments of the present invention combine static analysis, source code instrumentation and feedback-guided fuzz testing to automatically detect resource exhaustion denial of service attacks in software and generate inputs of coma for vulnerable code segments. The static analysis of the code highlights portions that are potentially vulnerable, such as loops and recursions whose exit conditions are dependent on user input. The code segments are dynamically instrumented to provide a feedback value at the end of each execution. Evolutionary techniques are then employed to search among the possible inputs to find inputs that maximize the feedback score. | 03-04-2010 |

20100094611 | SYSTEM AND METHOD FOR FEEDBACK-GUIDED TEST GENERATION FOR CYBER-PHYSICAL SYSTEMS USING MONTE-CARLO - 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. | 04-15-2010 |

20100281086 | EFFICIENT DECISION METHOD FOR REAL NON-LINEAR ARITHMETIC CONSTRAINTS - A system and method for solving a decision problem having Boolean combinations of linear and non-linear operations includes translating the non-linear real operations using a COordinate Rotation DIgital Computer (CORDIC) method programmed on a computer device into linear operations maintaining a given accuracy. Linear and translated linear operations are combined into a formula. Satisfiablity of the formula is solved using a decision procedure for Boolean combinations of linear operations over integers and reals. | 11-04-2010 |

20100293530 | SYSTEMS AND METHODS FOR MODEL CHECKING THE PRECISION OF PROGRAMS EMPLOYING FLOATING-POINT OPERATIONS - 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. | 11-18-2010 |

20100299651 | ROBUST TESTING FOR DISCRETE-TIME AND CONTINUOUS-TIME SYSTEM MODELS - A system and method for testing robustness of a simulation model of a cyber-physical system includes computing a set of symbolic simulation traces for a simulation model for a continuous time system stored in memory, based on a discrete time simulation of given test inputs stored in memory. Simulation errors are accounted for due to at least one of numerical instabilities and numeric computations. The set of symbolic simulation traces are validated with respect to validation properties in the simulation model. Portions of the simulation model description are identified that are sources of the simulation errors. | 11-25-2010 |

20110173148 | INTEGRATING INTERVAL CONSTRAINT PROPAGATION WITH NONLINEAR REAL ARITHMETIC - 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. | 07-14-2011 |

20120084761 | Interprocedural Exception Method - 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. | 04-05-2012 |

20120117547 | EMBEDDING CLASS HIERARCHY INTO OBJECT MODELS FOR MULTIPLE CLASS INHERITANCE - 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. | 05-10-2012 |

20120151449 | Scope Bounding with Automated Specification Inference for Scalable Software Model Checking - 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. | 06-14-2012 |

20120233584 | Analysis of Interactions of C and C++ Strings - A computer implemented method for analyzing a computer software program comprising both C++ and C string components, wherein the method includes building a memory model abstraction of any memory used by the program strings. Various memory models are presented that find invalid memory accesses in terms of validity of memory regions and buffer overflows. The model supports analyzing the interaction of C and C++ componentsâ€”in particular, it focuses on the interaction of C and C++ strings. The conversion of C++ strings to C strings is accomplished through a non-transferable ownership attribute that is to be respected by the C strings. The models can then be analyzed using static analysis techniques such as abstract interpretation and model checking, or through dynamic analysis. In so doing we allow discovery of potential memory safety violations in programs involving conversions between C and C++ strings. | 09-13-2012 |

20120246626 | DONUT DOMAINS - EFFICIENT NON-CONVEX DOMAINS FOR ABSTRACT INTERPRETATION - A computer implemented program analysis method employing a set of new abstract domains applicable to non-convex invarients. The method analyzes programs statically using abstract interpretation while advantageously considering non-convex structures and in particular those situations in which an internal region of an unreachable state exists within a larger region of reachable states. The method employs a new set of non-convex domains (donut domains) based upon the notion of an outer convex region of reachable states (Domain D1) and an inner region of unreachable states (Domain D2) which advantageously permits capture of non-convex properties by using convex regions and operations. | 09-27-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 |

20130091495 | FEEDBACK-DIRECTED RANDOM CLASS UNIT TEST GENERATION USING SYMBOLIC EXECUTION - Methods and systems for generating software analysis test inputs include generating a path query to cover a target branch of a program by executing a symbolic test driver concretely and partially symbolically, where at least one symbolic expression is partially concretized with concrete values; determining whether it is feasible to execute the target branch based on whether the generated path query is satisfiable or unsatisfiable using a constraint solver; if the target branch is feasible, generating a new test driver by replacing symbolic values in the symbolic test driver with generated solution values; and if the target branch is not feasible, analyzing an unsatisfiable core to determine whether unsatisfiability is due to a concretization performed during generation of the path query. | 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 |