--%>
Assignment Help - homework help

Describe MCP or Model Checker for C plus

MCP: Model Checker for C++ (MCP) is an explicit-state software model checker being introduced by the Robust Software Engineering group at NASA Ames Research Center (Thompson and Brat, 2008). MCP was constructed specifically to allow programs written in C or C++ to be model-checked directly, devoid of requiring prior translation or model extraction. It builds upon the LLVM (low level virtual machine) compiler infrastructure (LLVM website), thereby avoiding the requirement to directly recognize the extremely complex C++ language at source-level. This approach allows MCP to support the entire C++ language, comprising templates. The C language is handled fully, not merely as an improper subset of C++. Experience from the JPF project has demonstrated the utility of program model checking. However, current flight software is mostly implemented in C, not Java, and in the future it seems increasingly likely that C++ will become the platform of choice. The MCP model checker was developed to fill the requirement for an explicit-state software model checker, in the style of JPF, that fully supports the C++ language. As a test example, it was applied to the unmodified C code of the prototype CEV Onboard Abort Executive Flight Rules Checker.

   Related Questions in Programming Languages

  • Q : What is an Immutable object Immutable

    Immutable object: It is an object whose state might not be modified. The objects of String class are immutable, for example - their length and contents are fixed once formed.

    		•
  • Q : Explain way to open one resistance of

    Explain the way to open just one resistance of vb application (.exe).

    		•
  • Q : What is an Integer What is an Integer :

    What is an Integer: It is a negative or positive whole number. The primitive types are: short, byte, int and long are utilized to hold integer values in narrower or broader ranges.

    		•
  • Q : What is Disk drive Disk drive : It is a

    Disk drive: It is a hardware device employed to store the data. They come in numerous forms, like floppy disks, compact disks, and hard disks.

    		•
  • Q : Features of WordPress Normal 0 false

    Normal 0 false false

  • Q : What is an Unchecked exception

    Unchecked exception: An exception for which it is not needed to give a local try statement or to propagate through a throws clause stated in the method header. An exception which is not handled will cause program annihilation when it is thrown.

    		•
  • 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 Class method What is Class

    What is Class method: It is a synonym for the static method.

    		•
  • Q : Illustrates the parts of an XML

    Illustrates the parts of an XML document are case-sensitive.

    		•
  • Q : Explain VeriSoft VeriSoft (Godefroid,

    VeriSoft (Godefroid, 2005) is a model checker for C and C++; other languages can be used, but components in other languages are treated as black boxes. VeriSoft has been used to find defects in very large telecommunications programs (Chandra, Godefroi

    		•