位置：立项数据库 > 立项详情页
计算机软件
  • 项目名称：计算机软件
  • 项目类别：国家杰出青年科学基金
  • 批准号：60125207
  • 申请代码：F0202
  • 项目来源：国家自然科学基金
  • 研究期限：2002-01-01-2005-12-31
  • 项目负责人：张健
  • 负责人职称：研究员
  • 依托单位：中国科学院软件研究所
  • 批准年度：2001
中文摘要：

申请者在一阶逻辑公式有限模型自动构造研究中取得了有国际影响的成果。创造性地提出了一种利用对称性减小搜索空间的方法，研制出高效的自动构模器FALCON 和SEM ，并用它们解决了国际著名专家提出的难题，受到这些专家的高度赞赏。这些工具已被二十多个国家和地区的研究人员用于代数学研究和软件形式规约检测等方面。还提出一种并发过程作为命题模态逻辑的判定算法。申请者的工作已被国际同行在公开发表的论著中广泛引用。

中文主题词： 程序分析；测试数据生成；约束求解；可满足性判定
结论摘要：

英文主题词Program Analysis; Test Data Generation; Constraint Solving; Satisfiability Checking

成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 16
  • 8
  • 0
  • 0
  • 0
期刊论文
Automated test case generation for the stress testing of multimedia systems
一种求解混合约束问题的快速完备算法
Automatic Generation of Symbolic Model for Parameterized Synchronous Systems
程序静态分析技术与工具
基于基本路径的程序自动化测试
Reducing symmetries to generate easier SAT instances
Generating SAT instances from first-order formulas
Solving Boolean combinations of nonlinear numerical constraints
Survey Propagation — 一种求解SAT的高效算法
多线程程序数据竞争的静态检测
基于约束的主动规则终止性分析
约束问题求解
会议论文
Symbolic execution of program paths involving pointer and structure variables
Path-oriented test data generation using symbolic execution and constraint solving techniques
Extending finite model searching with congruence closure computation
Quantitative analysis of symbolic execution
Parallel execution of stochastic search procedures on reduced SAT instances
Computer search for counterexamples to Wilkie's identity
Predicate-Oriented Isomorphism Elimination in Model Finding
Backtracking algorithms and search heuristics to generate test suites for combinatorial testing
相关项目
基于程序切片和遗传算法的软件测试数据生成技术
期刊论文 27 会议论文 11 专利 4
基于约束规划的语义Web服务动态组合技术研究
期刊论文 11 会议论文 29
面向并发的自动化代码重构技术研究
期刊论文 19 会议论文 3 获奖 2 专利 2
度量驱动的软件重构技术研究
期刊论文 19 会议论文 3
基于程序意识的软件安全性研究
期刊论文 6 会议论文 11
基于认识与理解途径的软件可信性度量与评估体系及支撑技术研究
期刊论文 56 会议论文 43 获奖 8
经典逻辑和描述逻辑中的可满足性问题
期刊论文 8 会议论文 10
面向方面软件的变化影响分析理论及其应用
期刊论文 4 会议论文 11
基于地址序列抽取的存储器加密认证研究
期刊论文 4 会议论文 7
张健的项目
　安全攸关软件系统的构造与质量保障方法研究
期刊论文 4
软件安全性分析的关键技术与工具
期刊论文 5
经典逻辑和描述逻辑中的可满足性问题
期刊论文 8 会议论文 10
中美欧系列研讨会之一基于组件的系统
反例生成技术与形式化方法
期刊论文 4 会议论文 4 著作 1
第七届人工智能与符号计算国际会议
一阶逻辑约束求解
基于EFSM模型的测试与错误诊断
期刊论文 13 会议论文 10