SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft
作者： Thomas Ball , Byron Cook , Vladimir Levin , Sriram K. Rajamani
DOI: 10.1007/978-3-540-24756-2_1
关键词: Source code 、 Formal methods 、 Microsoft Windows 、 Programming language 、 Model checking 、 Symbolic data analysis 、 Program analysis 、 Computer science 、 Interface (Java) 、 Symbolic execution 、 Simulation
摘要: The SLAM project originated in Microsoft Research early 2000. Its goal was to automatically check that a C program correctly uses the interface an external library. used and extended ideas from symbolic model checking, analysis theorem proving novel ways address this problem. engine forms core of new tool called Static Driver Verifier (SDV) systematically analyzes source code Windows device drivers against set rules define what it means for driver properly interact with operating system kernel.
springer.com
core.ac.uk 
sci-hub.st 参考文章(40)
Sriram K. Rajamani, Thomas Ball, Generating Abstract Explanations of Spurious Counterexamples in C Programs pp. 15- ,(2002)
Sriram K. Rajamani, Thomas Ball, Boolean Programs: A Model and Process for Software Analysis pp. 29- ,(2000)
Sriram Rajamani, Thomas Ball, SLIC: A Specification Language for Interface Checking (of C) pp. 12- ,(2002)
Emmanuel Chailloux, Pascal Manoury, Bruno Pagano, Objective Caml : développment d'applications avec O'Reilly. ,(2000)
Thomas Ball, Vladimir Levin, Fei Xie, Automatic Creation of Environment Models via Training tools and algorithms for construction and analysis of systems. pp. 93- 107 ,(2004) , 10.1007/978-3-540-24730-2_7
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)
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
Thomas Ball, Andreas Podelski, Sriram K. Rajamani, Relative Completeness of Abstraction Refinement for Software Model Checking tools and algorithms for construction and analysis of systems. pp. 158- 172 ,(2002) , 10.1007/3-540-46002-0_12
Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang, Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement Computer Aided Verification. pp. 457- 461 ,(2004) , 10.1007/978-3-540-27813-9_36