下载中心
会议室预定
电子邮箱
【08-27】知行融创论坛：含整数类型的字符串约束求解
| 知行融创论坛-实验室月度学术交流 | |
| Speaker: | 胡登杭 |
| Time: | 2025年8月27日 |
| Venue: | 中国科学院软件园区5号楼三层 334报告厅 |
| Abstract: | 含有复杂字符串处理函数，比如 replaceAll 和含整数类型的字符串约束求解是很有挑战性的问题，一般来讲是不可判定的。Chen 等人以符号执行为背景提出了字符串约束直线子集，并为该子集设计了基于有限自动机的判定算法，而且开发了字符串约束求解器 OSTRICH。OSTRICH 的一个局限是不能处理涉及整数数据类型的字符串约束，比如含有字符串长度、Substring、indexOf 的字符串约束。我们基于整数代价存储自动机对 OSTRICH 的判定算法进行了扩展，可同时处理字符串和整数数据类型，从而获得了含有以下字符串操作的直线子集的判定算法：连接操作、模式串为正则表达式替换串为常数串的 replaceAll 函数、reverse、函数转换器、字符串长度、Substring、和 indexOf。并实现了该判定算法，形成了原形工具。 |
| Download | 含整数类型的字符串约束求解 |