ITR: Little Engines of Proof

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

Computers are primarily used for automating numericalcalculation but they can also be programmed to make inferences throughsymbolic calculation. Powerful automated inference is key to a flexibleand reliable computing infrastructure. Such technology can be used tobuild and analyze abstract models of complex systems, find bugs andoptimizations in software and hardware designs, and in the design of moreexpressive programming languages. These engineering applications ofinference technology require lightweight inference tools that areembeddable and composable.The Infer! project is a collaborative effort between SRI International,Clarkson University, and Pace University to construct an open foundationalinfrastructure for inferential software components. The Infer! projectprovides an abstract interface to a range of basic inference capabilitiesthrough a logic middleware layer. The Infer! middleware also includesmechanisms for combining and mapping between different theories and levelsof abstraction. The theoretical and pedagogical foundations for theInfer! project are developed in a discipline called "inferential analysis"that studies efficient inference components and the architecturalframework within which they can be combined. The Infer! technology isused to explore novel and exciting applications including the qualitativemodeling of complex phenomena and high-assurance open-source software.Broader impacts in research and education are sought for this projectby decomposing traditionally monolithic inference frameworks into usefulcomponents that can be exchanged in open source form and embedded withinopen verification technology. A key part of the project is an outreacheffort to establish standards and interfaces for an open exchange ofcomponents within the verification and analysis research community. Thiseffort includes active cooperation with the open source software communitythrough the development of verification components that can be integratedfor use in constructing dependable, verified, and self-checking software.