MRI: Acquisition of a Network of Workstations Serving as a Platform for Distributed Automated Reasoning

University Of Wyoming, Laramie WY

Investigators

Abstract

EIA-0216592 James L .Caldwell Jeffrey Van Baalen Gamboa Ruben MRI: Acquisition of a Network of Workstations Serving as a Platform for Distributed Automated Reasoning This proposal from an EPCoR state, adapting current parallel and distributed theorem proving technology to a setting in which different computation servers become available in an unpredictable fashion, aims at building a network of workstations that can be used as a computational server for research. A cluster of high-performance workstations running Linux and the required networking infrastructure will be acquired. The effort will make available a large proportion of the computational facilities of the department for theorem proving efforts. In this setting, the search for the proof of a single theorem will be spread between all the idle workstations participating in the distributed proof effort. In extending model checking to infinite state spaces, the research involves exploring two approaches for protocol verification: Development of, 1. On-the-fly model checker based on a 3-values logic and, 2. Theorem proving methods that can reduce a protocol's state space to a finite size.