沈胜宇

作品数：12被引量：28H指数：3
导出分析报告
供职机构：国防科学技术大学更多>>
发文主题：报文缓冲区网络接口卡形式化验证可测性设计更多>>
发文领域：自动化与计算机技术更多>>
发文期刊：《计算机工程与应用》《电子学报》《微电子学与计算机》《计算机辅助设计与图形学学报》更多>>
所获基金：国家自然科学基金国家高技术研究发展计划高等学校全国优秀博士学位论文作者专项资金更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一种新型混合互连网络拓扑结构的分析与优化被引量：2
《计算机工程与科学》2014年第12期2400-2409,共10页杨明英 雷斐 董德尊 沈胜宇 庞征斌 
国家863计划资助项目(2013AA014301;2013AA01A208);全国优秀博士学位论文作者专项资金资助项目(201450);国家自然科学基金资助项目(61272482;61303066)
随着高性能互连网络规模的增大,如何通过互连网络拓扑结构的设计来提升系统的性能和降低物理开销成为了系统设计的关键之一。传统的拓扑结构(可分为直接网络和间接网络)在网络规模增加时,不能很好地折衷网络性能和物理开销的关系。2012...
关键词：直接网络 间接网络 混合拓扑结构 物理开销 网络性能 优化 
基于悖论证明与局部搜索的不可满足子式求解算法被引量：4
《计算机学报》2014年第11期2262-2267,共6页张建民 沈胜宇 李思昆 
国家自然科学基金(61103083;61133007);国家"八六三"高技术研究发展计划项目基金(2012AA01A301)资助~~
随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法...
关键词：形式化验证 可满足问题 不可满足子式 悖论证明 局部搜索 
基于否证蕴含的极小一阶不可满足子式求解算法被引量：1
《计算机学报》2010年第3期415-426,共12页张建民 沈胜宇 李思昆 
国家自然科学基金(60603088)资助~~
解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小...
关键词：一阶逻辑公式 可满足模理论问题 极小不可满足子式 消解否证 否证蕴含图 
可满足性求解技术研究被引量：4
《计算机工程与科学》2010年第1期50-54,共5页张建民 沈胜宇 李思昆 
国家自然科学基金资助项目(60603088;90707003)
求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值,成为近年来的研究热点。本文针对命题公式与一阶公式的可满足性问题,重点介绍了布尔可满足性与可满足性模理论求解技术的基...
关键词：布尔可满足问题 可满足性模理论问题 完全方法 不完全方法 
求解极小SMT不可满足子式的宽度优先搜索算法被引量：2
《计算机辅助设计与图形学学报》2009年第7期984-990,共7页张建民 沈胜宇 李思昆 
国家自然科学基金(60603088;90707003)
极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3...
关键词：可满足性模理论 极小不可满足子式 DPLL(T) 搜索树 宽度优先搜索 
最小布尔不可满足子式的求解算法被引量：6
《电子学报》2009年第5期993-999,共7页张建民 沈胜宇 李思昆 
国家自然科学基金(No.60603088)
解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而最小不可满足子公式能够为公式不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误,诊断问题失败的缘由.针对最小不可满足子式的求解问题,提出并证明了...
关键词：形式化验证 最小不可满足子式 极大可满足子式 贪心遗传算法 蚁群算法 
一种求解布尔不可满足子式的局部搜索算法
《计算机工程与科学》2009年第4期56-59,105,共5页张建民 沈胜宇 李思昆 
国家自然科学基金资助项目(60603088;90707003)
解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由。近年来涌现了许多基于SAT求解器DPLL回...
关键词：布尔可满足问题 不可满足子式 消解序列 局部搜索 
布尔不可满足子式的求解方法研究进展被引量：1
《计算机辅助设计与图形学学报》2008年第10期1253-1260,共8页李思昆 张建民 沈胜宇 
国家自然科学基金(60603088;90707003)
解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由....
关键词：形式化验证 布尔公式 可满足问题 不可满足子式 DPLL算法 
基于悖论分析和增量求解的快速反例压缩算法被引量：5
《软件学报》2006年第5期1034-1041,共8页沈胜宇 李思昆 
国家自然科学基金~~
使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的BFL（brute force lifting）算法,其时间开销过大.为此,提出一种基于悖论分析和增量式SAT（boolean satisfiablilty problem）的快...
关键词：模型检验 反例压缩 悖论分析 增量式求解 安全断言 
基于指令分解的微处理器验证与RTL级错误定位
《计算机工程与科学》2005年第5期97-100,共4页沈胜宇 李思昆 
国家自然科学基金资助项目(90207019)国家863计划资助项目(2002AA1Z1480)
本文提出并实现了一种新的基于指令分解的微处理器验证与RTL级错误定位方法。该方法从指令集模拟器的模拟结果中将指令分解为功能单元上的操作序列,并且输入和输出数据。将该结果与RTL模型的模拟结果比较,使RTL级错误定位精确到功能单...
关键词：微处理器 指令分解 动态模拟 控制电路 指令集模拟器 RTL级错误定位方法 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部