Mechanized Metatheory Model-Checking
James Cheney

Full, machine-checkable formal verification appears to be the highest
attainable standard of evidence for the correctness of a system.
However, formal verification tools that can prove properties of
programming languages have high learning curves, require considerable
effort even from knowledgeable users, and are unhelpful in the
(common) case that there is a shallow syntactic bug in the system or
its specification. 

In this note, I outline an alternative approach to analyzing a formal
system called \emph{stress-testing}, inspired by the model checking
approach to verification of finite-state systems.  This approach
searches exhaustively for counterexamples to proposed properties of a
system.  Thus, it cannot guarantee that the system is correct, but is
capable of identifying flaws in a system.  Moreover, it may be more
immediately usable by non-experts, takes the user's brain out of the
inner loop, and produces concrete counterexamples illustrating bugs.
This approach may complement other traditional lightweight techniques
for gaining confidence in the correctness of a system, such as unit
testing and informal proof sketches, prior to attempting a complete
formalization.

Stress-testing can already be programmed directly in a logic
programming setting using generate-and-test and negation-as-failure.
However, writing useful stress-tests as logic programs is neither
exciting nor easy.  Therefore, I have developed a lightweight
extension to the alphaProlog system that reads in a program and
specification and automatically searches for counterexamples up to a
given resource bound.  I will present the approach using an example,
then explain an implementation, discuss some additional experience
with it, and sketch how it might be improved.