--%>

Define BOOP Toolkit

BOOP Toolkit: The BOOP Toolkit has been developed at the Institute for Software Technology at Graz
University of Technology. It is based on the SLAM project and uses the same main concept of verification by abstraction and refinement to determine the reachability of program points in a C program. The BOOP Toolkit follows three phases:

1. Abstraction using theorem proving and predicate abstraction

2. Model Checking of the abstract program to search for erroneous execution traces (with respect to a specification that should be provided by the user)

3. Refinement. If the model checker found an error path that is feasible in the original C program, it is reported to the user. If the path is not feasible, the abstraction is refined by adding up more detail and the procedure is reiterated.

   Related Questions in Programming Languages

  • Q : What is Static initializer Static

    Static initializer: An initializer prefixed with ‘static’ reserved word. The static initializer is stated outside the methods of its enclosing class, and might access only the static fields and methods of its enclosing class.

  • Q : Explain Look-and-feel Look-and-feel :

    Look-and-feel: The visual impression and interaction style given by a user interface. This is mainly the responsibility of the window manager (that is, in collaboration with the fundamental operating system) running on a specific computer. This refers

  • Q : What is a Method body What is a Method

    What is a Method body: It is a body of a method: everything within the outermost block of the method.

  • Q : Define the term Pixel Define the term

    Define the term Pixel: It is a `picture element' - usually a colored dot on a screen.

  • Q : Explain shell variables Explain the

    Explain the shell variables?

  • Q : Define the term Dynamic type Define the

    Define the term Dynamic type: This type of an object is the name of the class employed to construct it.

  • Q : Explain Out-of-bounds value

    Out-of-bounds value: It is a redundant value employed to point out that a different action from the norm is needed at some point. The read technique of InputStream returns -1 to point out that the end of a stream has been reached, for illustration, ra

  • Q : Explain AJAX Control Extender Toolkit

    Explain the AJAX Control Extender Toolkit.

  • Q : Environment Modeling in Java Pathfinder

    Environment Modeling: In JPF, Java class files can be processed in two different ways: A) As ordinary Java classes managed and executed by the host JVM (e.g., standard Java library classes, JPF implementation class

  • Q : State Sub type Sub type: It is a type

    Sub type: It is a type with a parent super type. The sub-type or super-type relationship is more common than the sub-class or super-class relationship. A class which implements an interface is a sub type of interface. An interface which expands the ot