Symbolic types for lenient symbolic execution
Symbolic types for lenient symbolic execution
复制标题
用于宽松符号执行的符号类型
DOI：
10.1145/3158128
复制
发表时间：
2017
影响因子：
--
通讯作者：
Torlak, Emina
中科院分区：
文献类型：
--
作者：
Chang, Stephen;Knauth, Alex;Torlak, Emina
我们提出了lambda_sym，一个类型λ演算宽松的符号执行，其中一些语言结构不识别符号值。然而，它的类型系统确保了程序中所有符号值的安全行为。我们的演算扩展了一个基本的发生类型系统的符号类型和可变状态，使其成为一个合适的模型，功能和强制性的符号执行语言。在这种混合环境中允许变异会引入可靠性问题，因此我们进一步添加了具体性多态性，它可以在不拒绝太多有效程序的情况下恢复可靠性。为了表明我们的演算是一个有用的模型，一个真实的语言，我们实现了类型化的玫瑰，类型化的扩展求解器辅助玫瑰语言。我们评估类型玫瑰移植一个大的代码库，表明我们的类型系统可以容纳各种各样的象征性执行的程序。
We present lambda_sym, a typed λ-calculus forlenient symbolic execution, where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our calculus extends a base occurrence typing system with symbolic types and mutable state, making it a suitable model for both functional and imperative symbolically executed languages. Naively allowing mutation in this mixed setting introduces soundness issues, however, so we further addconcreteness polymorphism, which restores soundness without rejecting too many valid programs. To show that our calculus is a useful model for a real language, we implemented Typed Rosette, a typed extension of the solver-aided Rosette language. We evaluate Typed Rosette by porting a large code base, demonstrating that our type system accommodates a wide variety of symbolically executed programs.
登录
查看更多内容
将系统类型作为宏
DOI：
10.1145/3009837.3009886
发表时间：
2017
期刊：
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
影响因子：
--
作者：
Stephen Chang;Alex Knauth;B. Greenman
通讯作者：
B. Greenman
使用 PLT Redex 进行语义工程
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
M. Felleisen;R. Findler;M. Flatt
通讯作者：
M. Flatt
DOI：
--
发表时间：
2017
期刊：
影响因子：
--
作者：
Rohin Shah
通讯作者：
Rohin Shah
实用可变数量多态性
DOI：
--
发表时间：
2009
期刊：
European Symposium on Programming
影响因子：
--
作者：
T. Strickland;Sam Tobin;M. Felleisen
通讯作者：
M. Felleisen
语言作为库
DOI：
10.1145/1993498.1993514
发表时间：
2011
期刊：
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Sam Tobin;Vincent St;Ryan Culpepper;M. Flatt;M. Felleisen
通讯作者：
M. Felleisen