字符串和字符串操作在真实世界的编程任务中随处可见。主流编程语言的类型系统往往只用一种统一的String类型来表示任意字符串。为了更好的区分具有不同结构和语义的字符串（如 IPv4 v.s. IPv6 address），我们可以引入正则语言作为refinement type进行更加精确的分析和验证。其难点在于如何对正则语言和常见的字符串操作（如substring, contains, split）进行高效的推理。提起正则语言，人们往往会自然联想到自动机。但这种通用的、能登大雅之堂的理论方法复杂度较高。本次讲座将从Brzozowski derivatives的视角重新审视正则语言的推理问题，介绍一种不使用自动机，而完全通过操作正则表达式的抽象语法树的新方法。它可以用来验证Python的IPv6 address parser。
欢迎大家一起来玩！
活动信息：
清华大学 TUNA 协会原名清华大学学生网管会，注册名清华大学学生网络与开源软件协会，是由清华大学网络技术和开源软件爱好者、技术宅组成的团体。现阶段向校内外提供开源软件镜像等服务。
The best team on the planet.
