Suresh Jagannathan为您介绍高阶程序验证

||对话

苏雷什Jagannathan肖像苏雷什Jagannathan博士2013年9月加入DARPA。他的研究金宝博娱乐兴趣包括编程语言，编译器，程序验证，并发和分布式系统。金宝博官方

加入DARPA之前，Jagannathan博士是普渡大学(Purdue University)的计算机科学教授。他还曾担任剑桥大学(Cambridge University)的访问教员，在那里度过了2010年的休假年;他还是新泽西州普林斯顿日本电气研金宝博娱乐究所(NEC research Institute)的高级研究员

Jagannathan博士发表了超过125份同行评议会议和期刊出版物，并合著了一本教科书。他拥有三项专利。他任职于多个项目和指导委员会，并担任多家期刊的编辑委员会成员。

Jagannathan博士拥有麻省理工学院(Massachusetts Institute of Technology)的电气工程和计算机科学的哲学博士和理学硕士学位。他获得了纽约州立大学石溪分校的计算机科学学士学位。

路加福音Muehlhauser:从您的角度来看，在过去的十年中，在高阶验证方面有哪些最有趣或最重要的发展?

苏雷什Jagannathan我将过去十年的发展分为四大类:

  1. 开发高阶递归方案(或高阶模型检查)。这种方法基于根据(递归)树语法定义语言语义。现在我们可以问语法生成的树是否满足特定的安全属性。因为递归方案是非常通用和表达性的结构，它们可以被看作是基于下推自动机或有限状态系统的模型检查器的自然扩展。金宝博官方在过去的十年中，已经有了实质性的进展，使高阶模型检查成为一种实际的努力，并伴随着现实的实现。
  2. Liquid Types将函数式语言中的经典类型推理技术的方面与模型检查器中使用的谓词抽象技术结合起来，以足够的精度自动推断依赖的类型细化，从而证明关于高阶函数式程序的有用的安全属性。OCaml、SML和Haskell中的这种方法的实现已经证明了这一点可以在没有重大类型注释负担的情况下验证重要的程序属性。
  3. 围绕丰富的依赖类型系统构建的新语言的开发已经取得了实质性的进展，这些系统支持对高阶程序的丰富安全性、安全性规范和属性的表达和静态验证。金宝博官方这些包括支持像Coq、Agda或Epigram这样的机械化证明助手的语言，像F*这样面向安全分布式编程的语言，像Ynot这样封装命定(有状态)特性和高阶依赖类型框架中的hoare逻辑前/后条件的库，以及在GHC等语言中发现的gadt和类型类等特性。
  4. 多变量控制流分析(如CFA2或高阶契约)是促进动态高阶语言验证和分析的两种技术。CFA2采用了一阶语言程序分析中使用的下推模型进行高阶设置，实现了调用/返回序列的精确匹配。高阶契约允许对高阶程序进行运行时验证和责任分配，并完全纳入到Lisp/Scheme的多范式方言Racket中。

路加福音你提到的高阶模型检查的一些“实际实现”是什么?

苏雷什:迄今为止最可伸缩的实现是工具Ramsay等人，POPL ' 14)，能够处理几千个规则的递归方案(即函数定义)。早期的工作，如TRecS (Kobayshi POPL ' 09)对于多达数百条规则的递归方案具有良好的性能。

路加福音:关于液体类型和多变量控制流量分析方面最近的有趣工作，您推荐阅读什么?

苏雷什:
液体的类型

  1. Vazou, Rondon, Jhala，”抽象细分类型，《欧洲编程研讨会》，2013年，第209-228页
  2. 朗登，川口，贾哈拉，”低级液体类型，《编程语言原理》，2010年，第131-144页。
  3. 朗登，川口，贾哈拉，”液体的类型"， ACM程序设计与实现会议，2008，第159-169页。
  4. 川口，朗登，巴克斯特，贾哈拉，”通过液体效应确定并行性“编程语言设计与实现”，计算机学报，2012，第45-54页。
  5. 朱,Jagannathan。”面向ML的组合和轻量级依赖类型推断，《模型检验与抽象解释》，2013年第1期，第295-314页。

Polyvariant控制流分析

    1. Midtgaard。”函数式程序的控制流分析”，《计算机学报》，2012,44(3)。
    2. 厄尔，谢尔盖，梅，范霍恩，"高阶程序的内省下推分析，《函数式编程国际会议》，2012，第177-188页。
    3. Might, Smaragdakis, Van Horn， "解决和开发k-CFA悖论:启发性函数和面向对象程序分析，《编程语言设计与实现》，2010年，第305-315页。
    4. Vardoulakis颤抖,“CFA2:控制流分析的上下文无关方法，《计算机科学与技术》，2011年第2期。

路加福音在未来5-10年的高阶验证技术研究中，您希望看到哪些关键的发展和解决方案?金宝博娱乐根据我们目前的理解，如果这些突破能够实现，哪些可能是最重要的?

苏雷什:目前，高阶验证的大部分工作都围绕着基础(描述HO程序中出现的显著特性的表达模型的定义，就像当前高阶递归方案、依赖类型系统或控制流分析的工作一样)，金宝博官方或语用学(减少液体类型中的类型注释负担)。展望未来，我希望看到这些技术的融合，从而能够大规模地应用新的表达性和基础模型。

一个重要的突破将是将这些系统集成到现实的编译器中，这将超越简单的安全性和属性检查，提供新的可验证的优化和程序转换。金宝博官方我们可以设想使用这些技术来使用HO验证技术支持的规范，作为在经过验证的编译器和运行时系统中实现切实的代码改进和性能提高的一种方式。金宝博官方另一个重要的进步是更深层次地理解高阶验证技术和其他类型的规范系统(例如，会话类型)之间潜在的协同作用。金宝博官方这里的问题是我们将如何表达丰富的协议，不仅捕获安全需求，而且活性和其他种类的复杂模式。

路加福音:谢谢,苏雷什!