This paper presents a tool for formally verifying ANSI-C programs using Bounded Model Checking (BMC). The tool supports all ANSI-C language features, including pointers, dynamic memory allocation, recursion, and floating-point data types. It is designed to be user-friendly, with a graphical user interface (GUI) that simplifies the verification process. The user only needs to specify the BMC bound, and the tool automatically performs the verification. If a counterexample is found, the GUI allows stepping through the trace, similar to a debugger. The tool is used for two main purposes: checking safety properties of ANSI-C programs and comparing an ANSI-C program with a hardware design (e.g., a Verilog circuit). The verification process involves unwinding the program and the circuit to generate a Boolean formula. This formula is then checked using a SAT solver. If the formula is satisfiable, a counterexample is extracted. The tool handles complex constructs such as loops, function calls, and pointers by transforming the program into a form suitable for BMC. It also supports dynamic memory allocation by using uninterpreted functions instead of allocating literals for each potential array element. This allows the tool to handle large arrays efficiently. The GUI is designed to be familiar to software engineers and hardware designers. It allows users to step through the trace forward or backward, and it displays waveform diagrams for Verilog designs. This makes it easier for hardware designers to analyze the behavior of their designs. The tool is available online and provides binaries for Linux, Windows, and Solaris. It also includes a detailed manual and an introductory tutorial. The paper concludes that the tool is a valuable resource for verifying ANSI-C programs and comparing them with hardware designs. Future work includes improving error localization and expanding the tool's capabilities.This paper presents a tool for formally verifying ANSI-C programs using Bounded Model Checking (BMC). The tool supports all ANSI-C language features, including pointers, dynamic memory allocation, recursion, and floating-point data types. It is designed to be user-friendly, with a graphical user interface (GUI) that simplifies the verification process. The user only needs to specify the BMC bound, and the tool automatically performs the verification. If a counterexample is found, the GUI allows stepping through the trace, similar to a debugger. The tool is used for two main purposes: checking safety properties of ANSI-C programs and comparing an ANSI-C program with a hardware design (e.g., a Verilog circuit). The verification process involves unwinding the program and the circuit to generate a Boolean formula. This formula is then checked using a SAT solver. If the formula is satisfiable, a counterexample is extracted. The tool handles complex constructs such as loops, function calls, and pointers by transforming the program into a form suitable for BMC. It also supports dynamic memory allocation by using uninterpreted functions instead of allocating literals for each potential array element. This allows the tool to handle large arrays efficiently. The GUI is designed to be familiar to software engineers and hardware designers. It allows users to step through the trace forward or backward, and it displays waveform diagrams for Verilog designs. This makes it easier for hardware designers to analyze the behavior of their designs. The tool is available online and provides binaries for Linux, Windows, and Solaris. It also includes a detailed manual and an introductory tutorial. The paper concludes that the tool is a valuable resource for verifying ANSI-C programs and comparing them with hardware designs. Future work includes improving error localization and expanding the tool's capabilities.