课题基金 / 基金详情

CPA-SEL: Collaborative Research - Continuing Progress Toward Verified Software

CPA-SEL: Collaborative Research - Continuing Progress Toward Verified Software
CPA-SEL:协作研究 - 不断取得验证软件的进展
批准号:
0811748
负责人:
Murali Sitaraman
金额:
$13.74万
依托单位:
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
2008
资助国家:
美国
项目状态:
已结题
起止时间:
2008-09-01 至 2013-08-31

项目摘要

项目成果

Murali Sitaraman的其他基金

相似基金

相关文献

中文摘要
翻译
大多数工程文物,例如桥梁和核电站,都是通过使其经受操作条件并观察结果来进行测试的。软件则不同。 它在计算机上运行时表现出动态行为,软件质量(关于实现指定行为)通常以这种方式进行测试。 但是软件也可以被认为是纯符号的--一系列指令--因此可以接受数学上的正确性证明。实现这样的“验证软件”已被确定为计算研究的“重大挑战”。 该项目的跨学科团队的软件工程师和逻辑学家的工作重点是论文,实用,可扩展,自动化的软件验证是可行的,一次一个组件,通过结合精心的语言设计与自动化定理证明的最新进展。 该计划是评估这篇论文的经验,产生的逻辑验证条件的基准套件的软件组件,如那些在计算课程和商业软件,并自动证明它们。 该项目的意义将来自于其概念证明,即经过验证的软件大挑战是可以克服的,以及更好地理解下一代软件工程师需要学习什么来生产经过验证的软件。
英文摘要
Most engineered artifacts, such as bridges and nuclear power plants, are tested by subjecting them to operating conditions and observing results.Software is different. It manifests dynamic behavior when running on computers, and software quality (with respect to achieving specifiedbehavior) is normally tested that way. But software also can be considered purely symbolic -- a sequence of instructions -- and hence can be subjected to mathematical proof of correctness. Achieving such "verified software" has been identified as a "grand challenge" for computing research. The work of this project's interdisciplinary team of software engineers and logicians focuses on the thesis that practical, scalable, automated software verification is feasible, one component at a time, by combining careful language design with recent advances in automated theorem proving. The plan is to evaluate this thesis empirically by generating the logical verification conditions for a benchmark suite of software components like those used in computing courses and commercial software, and proving them automatically. The project's significance will derive from its proof of concept that the verified software grand challenge can be conquered, and from a better understanding of what the next generation of software engineers need to be taught to produce verified software.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
Overcoming Impediments to Computer Science Students' Understanding of Code: Scaling Up Automated Methods and Broadening Participation
  • 批准号:
    1914667
  • 项目类别:
    Standard Grant
  • 资助金额:
    $29.51万
  • 财政年份:
    2019
  • 负责人:
    Murali Sitaraman
  • 依托单位:
IUSE: Understanding and Propagating the Essence of Successful Computing Education Projects
  • 批准号:
    1646691
  • 项目类别:
    Standard Grant
  • 资助金额:
    $4.13万
  • 财政年份:
    2016
  • 负责人:
    Murali Sitaraman
  • 依托单位:
Collaborative Research: IUSE: EHR: Engaged Student Learning Exploration and Design Tier: Engaging and Enabling Learners to Reason Logically about Code
  • 批准号:
    1611714
  • 项目类别:
    Standard Grant
  • 资助金额:
    $21.36万
  • 财政年份:
    2016
  • 负责人:
    Murali Sitaraman
  • 依托单位:
SHF: Medium: Collaborative Research: Specification and Mathematics Engineering for the Verified Software End-Game
  • 批准号:
    1161916
  • 项目类别:
    Standard Grant
  • 资助金额:
    $24.21万
  • 财政年份:
    2012
  • 负责人:
    Murali Sitaraman
  • 依托单位:
国内基金
海外基金
C19ORF18通过抑制SEL1L-HRD1 ERAD功能 激活IRE1α在肝脏脂代谢紊乱中的作用 及机制
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    10.0万元
  • 批准年份:
    2025
  • 负责人:
    高荣
  • 依托单位:
刺参METTL3靶向内质网相关降解蛋白SEL1L激活体腔细胞凋亡的分子机制
  • 批准号:
    LY23C190003
  • 项目类别:
    省市级项目
  • 资助金额:
    --
  • 批准年份:
    2023
  • 负责人:
    梁伟康
  • 依托单位:
基于Sel1L探讨ERAD在泌乳调节中的作用与机制
  • 批准号:
    82301824
  • 项目类别:
    青年科学基金项目
  • 资助金额:
    30万元
  • 批准年份:
    2023
  • 负责人:
    刘力
  • 依托单位:
内质网相关降解关键因子Sel1L调控CD8+T细胞稳态及免疫应答机制研究
  • 批准号:
    --
  • 项目类别:
    面上项目
  • 资助金额:
    53万元
  • 批准年份:
    2022
  • 负责人:
    张连军
  • 依托单位: