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

点击翻译按钮获取中文摘要

EIA-0216592James L .CaldwellJeffrey Van BaalenGamboa RubenMRI: Acquisition of a Network of Workstations Serving as a Platform for Distributed Automated ReasoningThis 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.