Software has proliferated throughout our lives, playing critical roles in everything ranging from cars to phones to medical devices. The correctness of this software has profound implications on safety and security. There are two ways of establishing correctness: testing and formal verification. For maximum impact, both methods require that the correct behavior of the software components is specified. However, in real systems, a complete specification is often missing. And, in nearly all cases, the specification is not written in machine-readable language needed for automatic test generation and verification. The lack of checkable specifications can be explained, in large part, by the high labor cost of writing specifications with existing tools.
The VeriWeb project seeks to reduce the cost of establishing program correctness by lowering the skill barrier to formal specification and verification and enabling the use of efficient labor allocation techniques, such as crowdsourcing. The tool verifies the absence of runtime exceptions (unexpected program crashes) by generating a JML specification that is checked with ESC/Java2. It decomposes the task of verification into managable subproblems that users solve using a web interface.
Adaptive Problem Ordering
VeriWeb decomposes the problem of specifying and verifying a program into managable subproblems of writing preconditions and postconditions for a single method at a time. The subproblem that is shown to the user depends on (1) deficiencies in the method’s specification identified by VeriWeb or a user, and (2) the dependence of the subproblem on other subproblems.
Drag and Drop Contract Construction
Users new to specification and verification often attempt to write malformed contracts — contracts that are either syntactically or semantically incorrect. VeriWeb includes a drag and drop interface for constructing contracts that prevents users from creating malformed contracts.
Contract Suggestions
A partial program specification is inferred automatically using the Daikon tool. VeriWeb users can accept or reject these conditions (the tool automatically checks the postconditions) or use the condition as the starting point for writing a new condition.
Concrete Counterexamples
VeriWeb automatically “executes” conditions that users write on a reference trace of the program. When the condition is violated in the trace, users can explore the relevant expressions in two ways: (1) hover their mouse over a subexpression in the contract to view its value, and (2) expand expressions in the tree to see the values of their subfields (the before-and-after values are displayed in a tree-based table).