一句话:提出教学用集成程序分析框架 Chiron,以游戏化方式帮助研究生学习分析、验证与测试,并通过课程调查验证其有效性。
程序分析、验证与测试是程序语言和软件工程研究生课程的重要主题,但教学需要兼顾理论理解与工具实践。Chiron 是为此设计的专用教学框架:代码规模小、统一中间表示、模块化架构便于插入新算法,并采用“乌龟冒险”式游戏化语言。它集成数据流分析引擎(驱动编译优化)、抽象解释验证引擎、符号执行引擎、模糊测试与演化测试生成器,以及基于频谱的统计缺陷定位模块。动画展示乌龟移动以帮助理解概念,详细日志辅助助教评分。Chiron 已在两轮研究生课程中使用;问卷调查显示所有学生一致认为它极有帮助并推荐用于类似课程。
Program analysis, verification and testing are important topics in programming languages and software engineering. They aim to produce engineers who are not only capable of empirically evaluating but, also formally reasoning on the correctness of software systems. We propose a specialized framework, Chiron, designed to teach graduate-level courses on these topics. Chiron has a small code base for easy understanding, uses a unified intermediate representation across all its analysis modules, maintains a modular architecture for plugging in new algorithms and uses a “fun” programming language to provide a gamified experience. Currently, it packages a dataflow analysis engine for driving compiler optimizations, an abstract interpretation engine for verification, a symbolic execution engine, a fuzzer and an evolutionary test generator for program testing, and a spectrum based statistical bug localization module. Within Chiron, program analysis tasks are posed in an unconventional setting (as adventures of a turtle) to provide a gamified experience; the accompanying animations (showing the movements of the turtle) allow the student to understand the underlying concepts better, and the detailed logs allow the teaching assistants in their grading activities. Chiron has been used in two offerings of a graduate level course on program analysis, verification and testing. In response to our survey questionnaire, all the students unanimously held the opinion that Chiron was extremely helpful in aiding their learning, and recommended its use in similar courses.
@inproceedings{ChatterjeeKLMSTR23,
title = {An Integrated Program Analysis Framework for Graduate Courses in Programming Languages and Software Engineering},
author = {Prantik Chatterjee and Pankaj Kumar Kalita and Sumit Lahiri and Sujit Kumar Muduli and Vishal Singh and Gourav Takhar and Subhajit Roy},
booktitle = {ASE},
year = {2023},
doi = {10.1109/ase56229.2023.00101}
}