High Performance Model Construction

高性能模型构建

• 批准号: 0098093
• 负责人: Hantao Zhang
• 金额: $ 29.27万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-06-01 至 2006-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0098093&HistoricalAwards=false
• 关键词: Performance; Model; Construction

Two software systems, SATO (SAtisfiability Test Optimized) and SEM (a System for Enumerating Models), developed with the NSF support, have been widely and successfully used for solving many problems often considered a challenge for automated reasoning systems. SATO and SEM were used to solve over a hundred cases of of previously open problems in algebras and logics. The proposed research will further increase the reasoning power of SATO and SEM. A new experimental software system called HOTTER (a Humble OTTER) will be fine-tuned for the high-performance first-order satisfiability testing. The main objective of this research is to develop high performance model generation techniques. These software systems will be serve as an environment for experimenting and developing these techniques, and will be available to the public. Many computational problems from a variety of fields, i.e., software and hardware verification, circuit design verification, scheduling and planning, can be reformulated as a model generation problems. Instead of creating special-purpose software for these problems, an alternative and competitive approach is to write the problems in a model-generation language and then submit the problems to a model generator optimized to this language. Another objective of this research is to support this approach by designing a general-purpose language for model generation, and implementing it with SATO, SEM, and HOTTER as its components. The language will provide an easy-to-use model generator for people in various fields.

两个软件系统，SATO （SAtisfiability Test Optimized）和SEM (a System for enumating Models)，是在NSF的支持下开发的，已经被广泛并成功地用于解决许多通常被认为是自动推理系统的挑战的问题。SATO和SEM被用于解决代数和逻辑学中一百多个以前开放的问题。所提出的研究将进一步提高SATO和SEM的推理能力。一个名为HOTTER （A Humble OTTER）的新实验软件系统将被微调用于高性能一阶满意度测试。本研究的主要目的是开发高性能的模型生成技术。这些软件系统将作为试验和开发这些技术的环境，并将向公众开放。来自各个领域的许多计算问题，如软件和硬件验证、电路设计验证、调度和规划，都可以重新表述为模型生成问题。与为这些问题创建专用软件不同，另一种有竞争力的方法是用模型生成语言编写问题，然后将问题提交给针对该语言进行优化的模型生成器。本研究的另一个目标是通过设计用于模型生成的通用语言来支持该方法，并使用SATO、SEM和HOTTER作为其组件来实现它。该语言将为各个领域的人们提供一个易于使用的模型生成器。