课题基金 / 基金详情

SHF: Small: Model-Based Bit-Precise Reasoning

SHF: Small: Model-Based Bit-Precise Reasoning
SHF:小型:基于模型的位精确推理
批准号:
1528153
负责人:
Dejan Jovanovic
金额:
$49.91万
依托单位:
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
2015
资助国家:
美国
项目状态:
已结题
起止时间:
2015-07-01 至 2018-06-30
关键词:

项目摘要

项目成果

相似基金

相关文献

中文摘要
翻译
形式化方法正越来越广泛地用于确保我们日常生活中所依赖的硬件和软件系统的正确性、安全性和可靠性。许多现代验证工具依赖于推理引擎,这些推理引擎可以自动有效地在机器算法级别上推理系统属性。这些推理引擎,称为可满足性模理论(SMT)求解器,可以证明该属性始终为真,或者如果不是这种情况,则提供反例。大多数SMT求解器不直接在字级进行推理,而是将问题编译成位级布尔表示(位爆破),然后将其委托给可满足性(SAT)求解器。这种方法的可扩展性是有限的,而且,编译SAT消除了初始问题的高层次结构,这使得获得简洁和有用的推理工件非常困难。这些工件对于现代验证方法的可扩展性至关重要,并且缺乏对获取它们的支持阻碍了位精确验证的进展。基于最新的进展,基于模型的推理,该项目开发了新的决策程序的位向量理论,在实践中是有效的,利用字级推理,并提供本地字级支持插值和泛化。新的过程与现有技术正交,并探索了这些关键的新思想:(1)基于模型的推理,不依赖于位爆破;(2)支持插值,不依赖于证明生成;(3)支持泛化,不依赖于量词消除。
英文摘要
Formal methods are becoming more widely used to ensure correctness, safety, and security of the hardware and software systems we rely on in our daily lives. Many modern verification tools depend on reasoning engines that can automatically and effectively reason about system properties at the level of machine arithmetic. These reasoning engines, called satisfiability modulo theories (SMT) solvers, can prove that the property is always true, or provide a counter-example if this is not the case. Most SMT solvers do not reason directly at the word-level but, instead, compile the problem into its bit-level Boolean representation (bit-blasting) and then delegate it to a satisfiability (SAT) solver. The scalability of this approach is limited and, moreover, the compilation to SAT eliminates the high-level structure of the initial problem, which makes obtaining concise and useful reasoning artifacts very difficult. These artifacts are crucial for scalability of modern verification methods, and the lack of support for obtaining them hinders progress in bit-precise verification. Based on recent advances in model-based reasoning this project develops novel decision procedures for the theory of bit-vectors that are effective in practice, take advantage of word-level reasoning, and provide native word-level support for interpolation and generalization. The new procedures are orthogonal to existing techniques, and explores these key novel ideas: (1) model-based reasoning that does not rely on bit-blasting; (2) support for interpolation that does not rely on proof generation; and (3) support for generalization that does not rely on quantifier elimination.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
国内基金
海外基金
昼夜节律性small RNA在血斑形成时间推断中的法医学应用研究
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    --
  • 批准年份:
    2024
  • 负责人:
  • 依托单位:
tRNA-derived small RNA上调YBX1/CCL5通路参与硼替佐米诱导慢性疼痛的机制研究
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    10.0万元
  • 批准年份:
    2022
  • 负责人:
    张祥忠
  • 依托单位:
Small RNA调控I-F型CRISPR-Cas适应性免疫性的应答及分子机制
Small RNAs调控解淀粉芽胞杆菌FZB42生防功能的机制研究
  • 批准号:
    31972324
  • 项目类别:
    面上项目
  • 资助金额:
    58.0万元
  • 批准年份:
    2019
  • 负责人:
    高学文
  • 依托单位: