Title: User-friendly Support for Common Concepts in a Lightweight Verifier
Author: Andrei Lapets
Data: May 14, 2010
Abstract:
Machine verification of formal arguments can only increase our confidence in
the correctness of those arguments, but the costs of employing machine
verification still outweigh the benefits for some common kinds of formal
reasoning activities. As a result, usability is becoming increasingly
important in the design of formal verification tools. We describe the
``aartifact" lightweight verification system, designed for processing formal
arguments involving basic, ubiquitous mathematical concepts. The system is a
prototype for investigating potential techniques for improving the usability
of formal verification systems. It leverages techniques drawn both from
existing work and from our own efforts. In addition to a parser for a
familiar concrete syntax and a mechanism for automated syntax lookup, the
system integrates (1) a basic logical inference algorithm, (2) a database of
propositions governing common mathematical concepts, and (3) a data
structure that computes congruence closures of expressions involving
relations found in this database. Together, these components allow the
system to better accommodate the expectations of users interested in
verifying formal arguments involving algebraic and logical manipulations of
numbers, sets, vectors, and related operators and predicates. We demonstrate
the reasonable performance of this system on typical formal arguments and
briefly discuss how the system's design contributed to its usability in two
case studies.