Screenshot
Welcome to the NJIT Software Engineering Lab

The Software Engineering LABoratoy (SELAB) is a research lab within the College of Computing Sciences at the New Jersey Institute of Technology.

Research interests at SELAB center on Software Engineering in general, with a special emphasis on Software Correctness.


Current Research Projects
  • Analyzing while loops with Invariant Relations
    • Invariant Relations
    • Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them.
      The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, hence may help us enhance techniques for generating invariant assertions.


    • Termination and Abort Freedom
    • The study of the termination condition of a loop is an important part of the analysis of loops. Our definition of termination encompasses not only the condition that the number of iterations is finite, but also the condition that each iteration of the loop executes without raising an exception, such an array reference out of bounds, a division by zero, an overflow / underflow, an illegal pointer reference, etc.


    • Correctness and Incorrectness
    • Traditionally, invariant assertions are used to verify the partial correctness of while loops with respect to pre/post specifications. We show how invariant relations are a more potent tool in the analysis of while loops:

      • Whereas invariant assertions can only be used to prove partial correctness, invariant relations can be used to prove total correctness;
      • Also, whereas invariant assertions can only be used to prove correctness, invariant relations can be used to prove correctness and can also be used to prove incorrectness;
      • Finally, where traditional studies of loop termination equate termination with iterating a finite number of times, we broaden the definition of termination to also capture the condition that each individual iteration proceeds without raising an exception.

    • Other Attributes

  • Faults and Faulty Programs
    • Definition
    • A fault is an attribute of a program that precludes it from satisfying its specification; while this definition may sound clear-cut, it leaves many details unspecified. An incorrect program may be corrected in many different ways, involving different numbers of modifications. Hence neither the location nor the number of of faults may be defined in a unique manner; this, in turn, sheds a cloud of uncertainty on such concepts as fault density, and fault forecasting.

      We present a more precise definition of a program fault, that has the following properties: it recognizes that the same incorrect behavior may be remedied in more than one way; it recognizes that removing a fault does not necessarily make the program correct, but may make it less incorrect (in a sense to be defined); it characterizes fault removals that make the program less incorrect, as opposed to fault removals that may remedy one aspect of program behavior at the expense of others; it recognizes that isolating a fault in a program is based on implicit assumptions about the remaining program parts; it identifies instances when a fault may be localized in a program with absolute certainty.

    • Applications

  • Semantic Metrics
  • Whereas traditional software metrics are typically based on a syntactic analysis of software products, we introduce and discuss metrics that are based on a semantic analysis.These semantic metrics do not reflect the form or structure of software products, but rather the properties of their function.

    At a time when software systems grow increasingly large and complex, the focus on diagnosing, identifying and removing every fault in the software product ought to relinquish the stage to a more measured, more balanced, and more realistic approach, which emphasizes failure avoidance, in addition to fault avoidance and fault removal.

    Semantic metrics are a good fit for this purpose, reflecting as they do, a system's ability to avoid failure rather than its proneness to being free of faults.


  • Mean Failure Cost
  • This is an ongoing work pertaining to the automated systematic derivation of loop functions.
    The function of a loop captures, possibly in closed form, the effect of executing the loop on program variables.