Suresh Jagannathan博士2013年9月加入DARPA。他的研究亚博体育官网兴趣包括编程语言，编译器，程序验证，并发和分布式系统。亚博体育苹果app官方下载
加入DARPA之前，Jagannathan博士是普渡大学(Purdue University)的计算机科学教授。他还曾担任剑桥大学(Cambridge University)的访问教员，在那里度过了2010年的休假年;他还是新泽西州普林斯顿日本电气研亚博体育官网究所(NEC research Institute)的高级研究员
Jagannathan博士发表了超过125份同行评议会议和期刊出版物，并合著了一本教科书。他拥有三项专利。他任职于多个项目和指导委员会，并担任多家期刊的编辑委员会成员。
Jagannathan博士举办了Massachusetts理工学院电气工程与计算机科学哲学哲学和科学学位硕士学位。他赢得了纽约州立大学的计算机科学理学学士学位，Stony Brook。
路加福音Muehlhauser:从您的角度来看，在过去的十年中，在高阶验证方面有哪些最有趣或最重要的发展?
苏雷什Jagannathan我将过去十年的发展分为四大类:
- 开发高阶递归方案（或高阶模型检查）。这种方法基于在（递归）树语语法方面定义语言语义。我们现在可以询问语法生成的树是否满足特定的安全性。因为递归方案是非常一般的和富有表现力的结构，所以它们可以基于下推自动机或有限状态系统被视为模型检查器的自然扩展。亚博体育苹果app官方下载在过去的十年中，有很大的进步，已经提出了高阶模型，检查了实际的努力，伴随着现实的实现。
- Liquid Types将函数式语言中的经典类型推理技术的方面与模型检查器中使用的谓词抽象技术结合起来，以足够的精度自动推断依赖的类型细化，从而证明关于高阶函数式程序的有用的安全属性。OCaml、SML和Haskell中的这种方法的实现已经证明了这一点可以在没有重大类型注释负担的情况下验证重要的程序属性。
- 围绕丰富的依赖类型系统构建的新语言的开发已经取得了实质性的进展，这些系统支持对高阶程序的丰富安全性、安全性规范和属性的表达和静态验证。亚博体育苹果app官方下载这些包括支持像Coq、Agda或Epigram这样的机械化证明助手的语言，像F*这样面向安全分布式编程的语言，像Ynot这样封装命定(有状态)特性和高阶依赖类型框架中的hoare逻辑前/后条件的库，以及在GHC等语言中发现的gadt和类型类等特性。
- CFA2或高阶合同等多Variant控制流程分析是两种技术，便于验证和分析动态高阶语言。CFA2采用程序分析用于一阶语言的预推动模型，以获得更高阶设置，从而实现呼叫/返回序列的精确匹配。高阶合同允许运行时验证和责备高阶计划的分配，并完全纳入球拍，是LISP /方案的多范式方言。
卢基你提到的高阶模型检查的一些“实际实现”是什么?
苏雷什：迄今为止最可扩展的实现是工具前言（Ramsay et。al，popl'14)，能够处理几千个规则的递归方案(即函数定义)。早期的工作，如TRecS (Kobayshi，Popl'09）对高达数百条规则的递归方案具有良好的性能。
卢基:关于液体类型和多变量控制流量分析方面最近的有趣工作，您推荐阅读什么?
苏雷什:
液体的类型
- Vazou, Rondon, Jhala，”抽象细分类型，《欧洲编程研讨会》，2013年，第209-228页
- 朗登，川口，贾哈拉，”低级液体类型“，ACM编程语言原理（POPL），2010，PP。131-144。
- 朗登，川口，贾哈拉，”液体的类型"， ACM程序设计与实现会议，2008，第159-169页。
- 川口，朗登，巴克斯特，贾哈拉，”通过液体效应确定不同的并行性“编程语言设计与实现”，计算机学报，2012，第45-54页。
- 朱,Jagannathan。”面向ML的组合和轻量级依赖类型推断，《模型检验与抽象解释》，2013年第1期，第295-314页。
多变量控制流动分析
- Midtgaard。”功能计划的控制流程分析“，ACM计算调查，2012,44（3）。
- 厄尔，谢尔盖，梅，范霍恩，"高阶程序的内省下推分析“，国际功能规划国际会议，2012年，第177-188页。
- Might, Smaragdakis, Van Horn， "解决和利用K-CFA悖论：照明功能与面向对象的程序分析，《编程语言设计与实现》，2010年，第305-315页。
- Vardoulakis颤抖,“CFA2:控制流分析的上下文无关方法，《计算机科学与技术》，2011年第2期。
卢基：您希望在未来5到10年的研究中看到高阶验证技术的关键开发和解决方案是什么？亚博体育官网如果我们目前的理解，那么哪种突破可能是最重要的，如果我们可以实现他们的理解？
苏雷什：目前，大部分工作都在基础上进行高阶验证中心（表达模型的定义，用于描述在HO程序中出现的突出属性，以及当前在高阶递归方案中的情况下工作，依赖类型系统或亚博体育苹果app官方下载控制流程分析）或语用学（减少液体类型的型注释负担）。展望未来，我希望能够看到这些技术的融合，使得能够以规模应用新的表现和基础模型。
一个重要的突破将是将这些系统集成到现实的编译器中，这将超越简单的安全性和属性检查，提供新的可验证的优化和程序转换。亚博体育苹果app官方下载我们可以设想使用这些技术来使用HO验证技术支持的规范，作为在经过验证的编译器和运行时系统中实现切实的代码改进和性能提高的一种方式。亚博体育苹果app官方下载另一个重要的进步是更深层次地理解高阶验证技术和其他类型的规范系统(例如，会话类型)之间潜在的协同作用。亚博体育苹果app官方下载这里的问题是我们将如何表达丰富的协议，不仅捕获安全需求，而且活性和其他种类的复杂模式。
卢基:谢谢,苏雷什!
你喜欢这篇文章吗？你可以享受我们的另一个对话的帖子,包括:
