The correctness of computer hardware and software is an area of growing theoretical interest as well as practical importance. It is now widely acknowledged that the best way to reason about program correctness hinges on two criteria: (i) the use of appropriate formalisms, such as temporal logic or automata, for rigorously specifying correct behavior; (ii) the use of mechanical reasoning algorithms, such as model checkers, to permit proofs of correctness to be constructed automatically that could not reasonably be constructed by hand owing to the intractable amount of tedious detail.
A principal limiting factor to automated verification is the computational complexity of various associated mechanical reasoning problems, which might be prohibitively high due to the combinatorial state explosion problem in various guises. The workshop will focus on such topics as the theoretical complexity as well as the practical efficiency of model checking algorithms and of testing satisfiability of logics, both in general and in applications-oriented special cases. Other methods for overcoming state explosion such as abstraction through the use of simulations and bisimulation relations are also important. Still other topics include the use of compositionality and modularity to simplify the construction of a correct program from correct constituent subprograms, program checking, testing and correcting, and program synthesis.
A portion of the workshop will be devoted to tools for verification and testing, evaluation of their strengths versus weaknesses, and reports on real experiences with industrial applications.
Next: Call for Participation
Workshop Index
DIMACS Homepage