Computation Infrastructure for Knowledge-Based Development of Reliable Software Systems

摘要

The Verification and Automated Reasoning research group at Cornell is involved in several DoD-related research projects that use formal methods, theorem proving, and knowledge management techniques to support the development of reliable software systems. These activities aim at making formal logical tools capable of solving difficult DoD tasks, using them for the development of safety-critical DoD software, making formalized algorithmic knowledge and logical software development tools accessible to researchers and programmers, and providing highly automated support for the training of researchers and programmers in the systematic design of reliable software. Due to the huge search spaces and high processing demands of formal reasoning tools, our prototype Logical Programming Environment and its associated Formal Digital Library require a large number of processors and large amounts of memory to run efficiently in state-of-the-art applications. With additional computing resources, funded under this grant the Cornell group contributed significantly to the DoD mission. The research instrumentation, described below provided the necessary computation infrastructure for making our research on system verification feasible, and it opened our proof system to remote users.