CAREER: Live Programming for Finite Model Finders
职业:有限模型查找器的实时编程
基本信息
- 批准号:2337667
- 负责人:
- 金额:$ 52.5万
- 依托单位:
- 依托单位国家:美国
- 项目类别:Continuing Grant
- 财政年份:2024
- 资助国家:美国
- 起止时间:2024-06-01 至 2029-05-31
- 项目状态:未结题
- 来源:
- 关键词:
项目摘要
As software permeates every aspect of our everyday lives, the problem of software reliability has grown both in importance and complexity. Software modeling has shown promise in providing ways to improve software reliability, however the specialization required to build accurate software models has limited their adoption. Current model development environments are rather “bare bones,” providing no guidance or feedback other than the output itself, and limiting the revision process to the age-old “edit and check.” This project aims to address these challenges through the creation of a new model development environment. The project’s novelties are new tools that combine live programming innovations with the strengths inherent to modeling languages to provide a range of contextualized feedback during development. The project’s impacts are in lowering the barrier to entry for software modeling and aiding formal methods education. Concretely, this project focuses on bringing live programming to finite model finders to interweave the process of writing and evaluating a software model. To achieve this, the project investigates the efficacy of different live development interfaces that suggest edits to complete formulas and that help users explore and contrast how different edits impact the collection of scenarios produced. Since live programming elevates the role of the output, this project also explores a new model development workflow, output directed debugging, that enables users to edit the scenarios in order to correct the underlying model. In addition, these live interfaces will form the basis for an interactive learning environment for mathematical logic to improve formal methods education at both the undergraduate and graduate level.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
随着软件渗透到我们日常生活的各个方面,软件可靠性问题变得越来越重要和复杂。软件建模在提供提高软件可靠性的方法方面已显示出希望,但是构建准确的软件模型所需的专业化限制了它们的采用。当前的模型开发环境相当“简单”,除了输出本身之外不提供任何指导或反馈,并将修订过程限制为古老的“编辑和检查”。该项目旨在通过创建新的模型开发环境来应对这些挑战。该项目的新颖之处在于新工具将实时编程创新与建模语言固有的优势相结合,在开发过程中提供一系列上下文反馈。该项目的影响在于降低软件建模的进入门槛并帮助正式方法教育。具体来说,该项目的重点是将实时编程引入有限模型查找器中,以将编写和评估软件模型的过程交织在一起。为了实现这一目标,该项目研究了不同实时开发界面的功效,这些界面建议进行编辑以完成公式,并帮助用户探索和对比不同的编辑如何影响所生成的场景集合。由于实时编程提升了输出的作用,因此该项目还探索了一种新的模型开发工作流程,即输出定向调试,使用户能够编辑场景以纠正底层模型。此外,这些实时界面将构成数理逻辑交互式学习环境的基础,以改善本科和研究生水平的形式方法教育。该奖项反映了 NSF 的法定使命,并通过使用基金会的智力价值和更广泛的影响审查标准进行评估,被认为值得支持。
项目成果
期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
数据更新时间:{{ journalArticles.updateTime }}
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
Allison Sullivan其他文献
Evaluating State Modeling Techniques in Alloy
评估合金状态建模技术
- DOI:
- 发表时间:
2017 - 期刊:
- 影响因子:0
- 作者:
Allison Sullivan;Kaiyuan Wang;S. Khurshid;D. Marinov - 通讯作者:
D. Marinov
Live Programming for Finite Model Finders
有限模型查找器的实时编程
- DOI:
10.1109/ase56229.2023.00016 - 发表时间:
2023 - 期刊:
- 影响因子:0
- 作者:
Allison Sullivan - 通讯作者:
Allison Sullivan
LLM4TDD: Best Practices for Test Driven Development Using Large Language Models
LLM4TDD:使用大型语言模型进行测试驱动开发的最佳实践
- DOI:
10.48550/arxiv.2312.04687 - 发表时间:
2023 - 期刊:
- 影响因子:0
- 作者:
Sanyogita Piya;Allison Sullivan - 通讯作者:
Allison Sullivan
Mutation testing for temporal alloy models (extended version)
- DOI:
10.1007/s10270-024-01220-x - 发表时间:
2024-10-28 - 期刊:
- 影响因子:3.200
- 作者:
Ana Jovanovic;Allison Sullivan - 通讯作者:
Allison Sullivan
Crucible: Graphical Test Cases for Alloy Models
Crucible:合金模型的图形测试用例
- DOI:
10.1109/issre59848.2023.00065 - 发表时间:
2023 - 期刊:
- 影响因子:0
- 作者:
Adam G. Emerson;Allison Sullivan - 通讯作者:
Allison Sullivan
Allison Sullivan的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Allison Sullivan', 18)}}的其他基金
SHF: Small: INCA: Incremental Analysis of Software Specification for Evolving Systems
SHF:小型:INCA:不断发展的系统软件规范的增量分析
- 批准号:
2204536 - 财政年份:2022
- 资助金额:
$ 52.5万 - 项目类别:
Standard Grant
FmitF: Track II: KeenEye: Enhancing Scenario Exploration
FmitF:轨道 II:KeenEye:增强场景探索
- 批准号:
2123341 - 财政年份:2021
- 资助金额:
$ 52.5万 - 项目类别:
Standard Grant
FMiTF: Track II: Alloy Analyzer Plus: An Integrated Development Environment for Alloy
FMiTF:轨道 II:合金分析仪 Plus:合金集成开发环境
- 批准号:
2042871 - 财政年份:2020
- 资助金额:
$ 52.5万 - 项目类别:
Standard Grant
FMiTF: Track II: Alloy Analyzer Plus: An Integrated Development Environment for Alloy
FMiTF:轨道 II:合金分析仪 Plus:合金集成开发环境
- 批准号:
1918189 - 财政年份:2019
- 资助金额:
$ 52.5万 - 项目类别:
Standard Grant
相似国自然基金
虚拟集群Live迁移关键技术研究
- 批准号:61170004
- 批准年份:2011
- 资助金额:56.0 万元
- 项目类别:面上项目
相似海外基金
Sex-specific fitness landscapes in the evolution of egg-laying vs live-birth
产卵与活产进化中的性别特异性适应性景观
- 批准号:
NE/Y001672/1 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
Research Grant
RII Track-4: NSF: Developing 3D Models of Live-Endothelial Cell Dynamics with Application Appropriate Validation
RII Track-4:NSF:开发活内皮细胞动力学的 3D 模型并进行适当的应用验证
- 批准号:
2327466 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
Standard Grant
A platform for rapidly generating live attenuated enterovirus vaccines
快速生成减毒肠道病毒活疫苗的平台
- 批准号:
24K02286 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
Grant-in-Aid for Scientific Research (B)
I-Corps: Translation potential of an efficient method to generate live-attenuated and replication-defective DNA viruses for vaccine development
I-Corps:一种有效方法的转化潜力,可生成用于疫苗开发的减毒活病毒和复制缺陷型 DNA 病毒
- 批准号:
2420924 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
Standard Grant
Understanding the coordination of DNA mismatch repair using live-cell single-molecule imaging
使用活细胞单分子成像了解 DNA 错配修复的协调
- 批准号:
BB/Y001567/1 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
Research Grant
CAREER: Optoelectronic lab-on-a-chip technology for high content automated multiparametric physiological analyses of live cells
职业:用于活细胞高内涵自动化多参数生理分析的光电芯片实验室技术
- 批准号:
2339030 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
Continuing Grant
An innovative cyber compliance platform using AI, live monitoring data and machine learning to automate compliance and due diligence completion.
一个创新的网络合规平台,使用人工智能、实时监控数据和机器学习来自动完成合规和尽职调查。
- 批准号:
10100493 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
Collaborative R&D
IENgine: developing a subscription-based membership application to connect live/location-based immersive experience, (LIE) creatives with employers.
IENgine:开发基于订阅的会员应用程序,将基于实时/位置的沉浸式体验 (LIE) 创意人员与雇主联系起来。
- 批准号:
ES/Y011104/1 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
Research Grant
Bio-HhOST: Next Generation 3D Tissue Models: Bio-Hybrid Hierarchical Organoid-Synthetic Tissues (Bio-HhOST) Comprised of Live and Artificial Cells.
Bio-HhOST:下一代 3D 组织模型:由活细胞和人造细胞组成的生物混合分层类器官合成组织 (Bio-HhOST)。
- 批准号:
10106841 - 财政年份:2024
- 资助金额:
$ 52.5万 - 项目类别:
EU-Funded
Live cell spinning disk confocal microscope with single molecule localization module
具有单分子定位模块的活细胞转盘共聚焦显微镜
- 批准号:
514497685 - 财政年份:2023
- 资助金额:
$ 52.5万 - 项目类别:
Major Research Instrumentation