Qt operational model
Indeed, QtOM is integrated into a bounded model checking (BMC) tool based on satisfiability modulo theories (SMT),
known as the Efficient SMT-based Context-Bounded Model Checker (ESBMC++), in order to verify specific properties in Qt/C++ programs.
POINTER SAFETY
Ensures that the pointer is neither NULL or an invalid object, as well its offset does not exceed the object bounds.
ARRAY BOUNDS
Ensures that the value of the array index is within the known (and fixed) bounds.
OVERFLOW
Checks whether a sum or product exceeds the number representation.
Correctness
Ensures the correct usage of the Qt framework.
DIVISION BY ZERO
Checks for a division by zero in arithmetic expressions.
USER-SPECIFIED ASSERTIONS
Checks for user-specified assertions.
About us
QtOM
Software
Verification
QtOM
Qt Operational Model (QtOM) is an abstract representation of the Qt Cross-Platform Framework. Indeed, QtOM is integrated into a bounded model checking (BMC) tool based on satisfiability modulo theories (SMT), known as the Efficient SMT-based Context-Bounded Model Checker (ESBMC++), in order to verify specific properties in Qt/C++ programs.
ESBMC++
ESBMC++ is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solvers. It allows the verification engineer to verify single- and multi-threaded software (with shared variables and locks); to reason about arithmetic under- and overflow, pointer safety, memory leaks, array bounds, atomicity and order violations, deadlock and data race; to verify programs that make use of bit-level, pointers, structs, unions and fixed-point arithmetic.
Contributors
Eddie B. Lima Filho, Felipe R. Monteiro, Lucas C. Cordeiro and Mário A. P. Garcia.