CAREER: Marlin: A Unified Framework for Automatic and Interactive Quantitative Program Analysis
职业:Marlin:自动和交互式定量程序分析的统一框架
基本信息
- 批准号:1845514
- 负责人:
- 金额:$ 51.88万
- 依托单位:
- 依托单位国家:美国
- 项目类别:Continuing Grant
- 财政年份:2019
- 资助国家:美国
- 起止时间:2019-07-01 至 2024-06-30
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
Achieving reliability and security of software systems that we use on a daily basis is one of the most pressing challenges of modern technology. It has been demonstrated that software verification with mathematical methods is an important component in meeting this challenge. However, most extant verification projects and tools focus on demonstrating the functional correctness of software. They do not analyze important quantitative properties of software such as resource usage, side channels, and probabilistic guarantees, which are crucial for reliability and security. The project's novelty is the design and implementation of a general framework for quantitative verification that can be applied to analyze resource usage, probabilistic programs (that incorporate randomness), and side channels. The project's impact is that this framework enables software developers to reduce the energy consumption of data centers, to mitigate serious security vulnerabilities, and to connect statistical safety guarantees to software systems that have machine-learning components. The project also provides a pedagogical opportunity for curriculum development and outreach activities. Quantitative verification and analysis tools implemented in the project are being integrated in Carnegie-Mellon's undergraduate courses on functional programming and data structures and algorithms, to both help students reason about the complexity of their code, and help instructors and teaching assistants automatically grade programming assignments by verifying complexity requirements. As part of the project's outreach activities, the investigator is designing two course modules for high-school students that are rolled out through existing programs at Carnegie-Mellon.Current research on quantitative analysis and verification is often problem-specific, separated into manual or automatic techniques, and there is little cross-fertilization between different areas. The aim of this project is to develop Marlin, a unified framework for quantitative verification. A distinctive feature of Marlin is the tight integration of interactive and automatic reasoning. This includes converting manually derived quantitative properties into constraints that can be consumed by automatic techniques and supporting more lightweight forms of automation beyond full inference. Marlin is based on a full-featured probabilistic programming language and an expressive quantitative program logic that supports compositional and relational reasoning. Specific innovations of Marlin include easily-understood descriptions of sub-languages for which the automation is guaranteed to succeed, the automatic generation of worst-case inputs, tail-bound analysis with higher moments, and automatic relational reasoning. Marlin's foundation is shared by three specialized quantitative analysis tools: Resource Aware ML (RaML), a language for static resource analysis; ParML, a new language for side-channel free programming; and Borel, a tool for probabilistic inference.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.
实现我们日常使用的软件系统的可靠性和安全性是现代技术最紧迫的挑战之一。它已被证明,软件验证的数学方法是在满足这一挑战的一个重要组成部分。然而,大多数现存的验证项目和工具集中在证明软件的功能正确性。它们不分析软件的重要定量属性,如资源使用、边信道和概率保证,这些对于可靠性和安全性至关重要。该项目的新奇在于设计和实现了一个通用的定量验证框架,该框架可用于分析资源使用情况、概率程序(包含随机性)和侧通道。该项目的影响是,该框架使软件开发人员能够减少数据中心的能源消耗,减轻严重的安全漏洞,并将统计安全保证与具有机器学习组件的软件系统连接起来。该项目还为课程编制和外联活动提供了一个教学机会。在该项目中实现的定量验证和分析工具正在整合到Functional-Mellon的函数式编程和数据结构和算法本科课程中,以帮助学生推理代码的复杂性,并帮助教师和助教通过验证复杂性要求自动评分编程作业。作为该项目推广活动的一部分,研究人员正在为高中生设计两个课程模块,并通过现有的项目在梅勒基-梅隆大学推出。目前关于定量分析和验证的研究通常是针对具体问题的,分为手动或自动技术,不同领域之间几乎没有交叉。该项目的目的是开发马林,一个统一的定量验证框架。马林的一个显著特点是交互式推理和自动推理的紧密集成。这包括将手动导出的定量属性转换为可由自动技术使用的约束,并支持超越完全推理的更轻量级的自动化形式。马林是基于一个全功能的概率编程语言和表达的定量程序逻辑,支持组合和关系推理。马林的具体创新包括易于理解的子语言描述,保证自动化成功,自动生成最坏情况的输入,尾边界分析与更高的时刻,自动关系推理。 马林的基金会由三个专门的定量分析工具共享:资源感知ML(RaML),一种用于静态资源分析的语言; ParML,一种用于侧通道自由编程的新语言;和Borel,一种用于概率推理的工具。该奖项反映了NSF的法定使命,并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。
项目成果
期刊论文数量(12)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Resource-Aware Session Types for Digital Contracts
数字合约的资源感知会话类型
- DOI:10.1109/csf51468.2021.00004
- 发表时间:2021
- 期刊:
- 影响因子:0
- 作者:Das, Ankush;Balzer, Stephanie;Hoffmann, Jan;Pfenning, Frank;Santurkar, Ishani
- 通讯作者:Santurkar, Ishani
Probabilistic Resource-Aware Session Types
- DOI:10.1145/3571259
- 发表时间:2020-11
- 期刊:
- 影响因子:0
- 作者:Ankush Das;Di Wang;Jan Hoffmann
- 通讯作者:Ankush Das;Di Wang;Jan Hoffmann
Raising expectations: automating expected cost analysis with types
- DOI:10.1145/3408992
- 发表时间:2020-06
- 期刊:
- 影响因子:0
- 作者:Di Wang;David M. Kahn;Jan Hoffmann
- 通讯作者:Di Wang;David M. Kahn;Jan Hoffmann
A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism
- DOI:10.1016/j.entcs.2019.09.016
- 发表时间:2019-11
- 期刊:
- 影响因子:0
- 作者:Di Wang;Jan Hoffmann;T. Reps
- 通讯作者:Di Wang;Jan Hoffmann;T. Reps
Central moment analysis for cost accumulators in probabilistic programs
- DOI:10.1145/3453483.3454062
- 发表时间:2021-06
- 期刊:
- 影响因子:0
- 作者:Di Wang;Jan Hoffmann;T. Reps
- 通讯作者:Di Wang;Jan Hoffmann;T. Reps
{{
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 }}
Jan Hoffmann其他文献
Reactive probabilistic belief modeling for mobile robots
移动机器人的反应概率信念建模
- DOI:
10.18452/15731 - 发表时间:
2008 - 期刊:
- 影响因子:0
- 作者:
Jan Hoffmann - 通讯作者:
Jan Hoffmann
m6A RNA modification by METTL3 regulates chemo- and radioresistance in pancreatic cancer cells
METTL3 修饰的 m6A RNA 调节胰腺癌细胞的化疗和放射抗性
- DOI:
- 发表时间:
2019 - 期刊:
- 影响因子:0
- 作者:
菅野貴之;Jan Hoffmann;Jan Janssen;澁谷孝行;小野口昌久;樋口隆弘;Nobutaka Mukumoto;立川章太郎 - 通讯作者:
立川章太郎
Gene Expression Changes in Leukocytes During Cardiopulmonary Bypass Are Dependent on Circuit Coating
体外循环期间白细胞基因表达的变化取决于电路涂层
- DOI:
10.1161/circulationaha.104.525378 - 发表时间:
2005 - 期刊:
- 影响因子:37.8
- 作者:
J. Seeburger;Jan Hoffmann;H. Wendel;G. Ziemer;H. Aebert - 通讯作者:
H. Aebert
Arrays and References in Resource Aware ML
资源感知机器学习中的数组和引用
- DOI:
- 发表时间:
2017 - 期刊:
- 影响因子:0
- 作者:
Benjamin Lichtman;Jan Hoffmann - 通讯作者:
Jan Hoffmann
A Real-Time Auto-Adjusting Vision System for Robotic Soccer
一种实时自动调节足球机器人视觉系统
- DOI:
10.1007/978-3-540-25940-4_19 - 发表时间:
2003 - 期刊:
- 影响因子:0
- 作者:
Matthias Jüngel;Jan Hoffmann;Martin Lötzsch - 通讯作者:
Martin Lötzsch
Jan Hoffmann的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Jan Hoffmann', 18)}}的其他基金
SHF: Medium: Language Support for Sound and Efficient Programmable Inference
SHF:中:对健全且高效的可编程推理的语言支持
- 批准号:
2311983 - 财政年份:2023
- 资助金额:
$ 51.88万 - 项目类别:
Continuing Grant
SHF: Small: Automatic Qualitative and Quantitative Verification of CUDA Code
SHF:Small:CUDA代码的自动定性和定量验证
- 批准号:
2007784 - 财政年份:2020
- 资助金额:
$ 51.88万 - 项目类别:
Standard Grant
SHF: Small: Collaborative Research: Resource-Guided Program Synthesis
SHF:小型:协作研究:资源引导程序综合
- 批准号:
1812876 - 财政年份:2018
- 资助金额:
$ 51.88万 - 项目类别:
Standard Grant
相似海外基金
Project MARLIN (Maritime, Acoustic, Realtime, Learning, Information and Notification)
MARLIN 项目(海事、声学、实时、学习、信息和通知)
- 批准号:
10065619 - 财政年份:2023
- 资助金额:
$ 51.88万 - 项目类别:
Collaborative R&D
MARLIN AQUA - Sustainable Energy Access for Offshore Aquaculture
MARLIN AQUA - 近海水产养殖的可持续能源获取
- 批准号:
10050623 - 财政年份:2022
- 资助金额:
$ 51.88万 - 项目类别:
Collaborative R&D
MARLIN STAR Community Access to Stored and Transferrable Energy from Floating Renewables
MARLIN STAR 社区从浮动可再生能源中获取储存和可转移的能源
- 批准号:
105915 - 财政年份:2020
- 资助金额:
$ 51.88万 - 项目类别:
Collaborative R&D
MARLIN Modular Floating Platform for OffShore Wind: Concept Assessment
用于海上风电的 MARLIN 模块化浮动平台:概念评估
- 批准号:
132491 - 财政年份:2017
- 资助金额:
$ 51.88万 - 项目类别:
Feasibility Studies
MARLIN Modular Floating Platform for Offshore Wind: Concept Assessment
MARLIN 海上风电模块化浮动平台:概念评估
- 批准号:
EP/P032958/1 - 财政年份:2017
- 资助金额:
$ 51.88万 - 项目类别:
Research Grant
MARLIN Modular Floating Platform for Offshore Wind : Concept Assessment
MARLIN 海上风电模块化浮动平台:概念评估
- 批准号:
EP/P030645/1 - 财政年份:2017
- 资助金额:
$ 51.88万 - 项目类别:
Research Grant
Group hunting behaviour in striped marlin, Kajikia audax
条纹马林鱼、Kajikia audax 的群体狩猎行为
- 批准号:
455800376 - 财政年份:
- 资助金额:
$ 51.88万 - 项目类别:
Research Grants