A decade of software model checking with SLAM

作者: Thomas Ball , Vladimir Levin , Sriram K. Rajamani

DOI: 10.1145/1965724.1965743

关键词:

摘要: SLAM is a program-analysis engine used to check if clients of an API follow the API's stateful usage rules.

参考文章(48)
Sriram K. Rajamani, Thomas Ball, Boolean Programs: A Model and Process for Software Analysis pp. 29- ,(2000)
David A. Molnar, Michael Y. Levin, Patrice Godefroid, Automated Whitebox Fuzz Testing. network and distributed system security symposium. ,(2008)
Sriram Rajamani, Thomas Ball, SLIC: A Specification Language for Interface Checking (of C) pp. 12- ,(2002)
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Susanne Graf, Hassen Saidi, Construction of Abstract State Graphs with PVS computer aided verification. pp. 72- 83 ,(1997) , 10.1007/3-540-63166-6_10
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
Byron Cook, Andreas Podelski, Andrey Rybalchenko, Abstraction Refinement for Termination Static Analysis. pp. 87- 101 ,(2005) , 10.1007/11547662_8
K. L. McMillan, Interpolation and SAT-Based Model Checking computer aided verification. pp. 1- 13 ,(2003) , 10.1007/978-3-540-45069-6_1
Javier Esparza, Stefan Schwoon, A BDD-Based Model Checker for Recursive Programs computer aided verification. pp. 324- 336 ,(2001) , 10.1007/3-540-44585-4_30