PV4 tools in ProVerBPV4

PV4 tools operate within a particular paradigm and derive their actions, conclusions and even properties that they need to check, from a built-in formal specification. For example, such a tool can guarantee freedom of deadlocks in a multi-threaded application, or data consistency in a database management system. Generated property set cannot be explicitly adjusted for tools of this level.

101 items on this list.

ProVerB is a part of SLEBoK. Last updated: February 2023.