学术报告

NetKAT: A Formal System for the Verification of Networks

作者:Dexter Kozen    发布时间:2015-12-13    浏览次数:
康奈尔的Dexter Kozen教授将于这周末来访一周,活动安排如下。 A 一次大会报告 报告题目: NetKAT: A Formal System for the Verification of Networks 报告日期:2015年12月13日9点, 报告地点:一号楼311会议室 ......

康奈尔的Dexter Kozen教授将于这周末来访一周,活动安排如下。

A 一次大会报告

报告题目: NetKAT: A Formal System for the Verification of Networks

报告日期:2015年12月13日9点,

报告地点:一号楼311会议室

报告人:Dexter Kozen, Cornell

(Joint work with Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Konstantinos Mamouras, Matthew Milano, Mark Reitblatt, Cole Schlesinger, Alexandra Silva, Laure Thompson, and David Walker)

摘要 : NetKAT (Anderson et al, POPL14; Foster et al, POPL15) is a relatively new language and logic for reasoning about packet switching networks that fits well with the popular software-defined networking (SDN) paradigm. The language is based on Kleene algebra with tests (KAT) and provides general-purpose programming constructs as well as special-purpose primitives for querying and modifying packet headers and encoding network topologies. It has a formal mathematical semantics, a sound and complete equational deductive system, and an efficient decision procedure. The system has been applied successfully in such applications as testing reachability and non-interference and correctness of a compiler that translates programs to hardware instructions for switches. In this talk I will present survey of this recent work.

B 给本科生讲四次算法方面的课

1. Operations Research: Network Flow, Transportation problems

运筹学: 网络流,运输问题 各讲一次

周一 34节 西十二 N112

周三 12节 西十二 N412

2. Algorithms: Balanced tree, Fast Fourier Transform.

算法: 平衡树,快速付立叶变换 各讲一次

周一7-8,周四3-4 西十二S404

Dexter C. Kozen教授是美国理论计算机科学家, 康奈尔大学工程学院Joseph Newton Pew, Jr. 冠名教授。Dexter Kozen 为美国ACM协会(Association for Computing Machinery)、美国科学促进会(American Association for the Advancement of Science,AAAS)及古根海姆基金会(Guggenheim) 会士。曾获IBM杰出创新奖和康奈尔大学计算机本科生教育年度奖, 顶级会议LICS十年最佳论文奖。也是最早获得荷兰内梅亨(Radboud University Nijmegen)大学Radboud Excellence Initiative奖的教授之一。

Dexter Kozen 教授的研究领域为算法和复杂性,特别是逻辑与代数决策问题的复杂性、编程语言的逻辑与语义、计算机安全。他以在逻辑与复杂性的交叉领域作出了开创性的工作而闻名。为动态逻辑的开创者(动态逻辑之父)之一,所提出的mu微积分一直沿用至今。主要论著有计算理论(theory of computation)、自动机理论(automata theory)、动态逻辑(dynamic logic)以及算法(algorithms)。在LICS(IEEE Symposium on Logic in Computer Science), STOC(ACM Symposium on Theory of Computing), FOCS(IEEE Symposium on Foundations of Computer Science)等顶级会议和期刊上发表了200多篇论文。他也是康奈尔大学算法课主讲,而康奈尔大学算法课为全美十佳课程之一。

欢迎各位老师前来参加讲座和旁听他的课程。