Qt operational model

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.

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 is developed at the Federal University of Amazonas.

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.