...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Abstract interpretation of microcontroller code: Intervals meet congruences
【24h】

Abstract interpretation of microcontroller code: Intervals meet congruences

机译：微控制器代码的抽象解释：时间间隔满足全等

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Bitwise instructions, loops and indirect data access present challenges to the verification of microcontroller programs. In particular, since registers are often memory mapped, it is necessary to show that an indirect store operation does not accidentally mutate a register. To prove this and related properties, this article advocates using the domain of bitwise linear congruences in conjunction with intervals to derive accurate range information. The paper argues that these two domains complement one another when reasoning about microcontroller code. The paper also explains how SAT solving, which applied with dichotomic search, can be used to recover branching conditions from binary code which, in turn, further improves interval analysis.
机译：按位指令，循环和间接数据访问对微控制器程序的验证提出了挑战。特别是，由于寄存器通常是内存映射的，因此有必要表明间接存储操作不会意外地使寄存器发生突变。为了证明这一点和相关特性，本文主张结合使用位域线性同余域和区间来得出准确的范围信息。本文认为，在对微控制器代码进行推理时，这两个领域是相辅相成的。本文还解释了如何应用SAT解决方案（适用于二分搜索）从二进制代码中恢复分支条件，从而进一步改善间隔分析。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号