|
|
- The SLAM Process
- Thorough
Static Analysis of Device Drivers
(pdf),
Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob
Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani and
Abdullah Ustuner (Microsoft), EuroSys
2006
- The SLAM Project: Debugging
System Software via Static Analysis,
Thomas Ball, Sriram K. Rajamani, POPL 2002, January
2002, pages 1-3 [PS,PDF].
A three-page
high-level overview of SLAM. See the following paper for more details.
- Automatically Validating
Temporal Safety Properties of Interfaces [ PS,
PDF],
Thomas Ball, Sriram K. Rajamani, SPIN 2001, Workshop
on Model Checking of Software, LNCS
2057, May 2001, pp. 103-122.
- Boolean
Programs: A Model and Process for Software Analysis, Thomas
Ball, Sriram K. Rajamani, MSR Technical Report 2000-14. The original SLAM document, for a
simplified programming language. Refer to most recent papers in each
section for the most up-to-date snapshot of the SLAM process and tools.
- SLAM Specifications
- SLIC: A Specification
Language for Interface Checking (of C), Thomas Ball, Sriram K. Rajamani, MSR-TR-2001-21.
Describes the
language used in SLAM for specifying properties of interfaces to be
checked.
- Boolean Programs
- Bebop: A Path-sensitive
Interprocedural Dataflow Engine
[PS,
PDF],
Thomas Ball, Sriram K. Rajamani, PASTE
2001. Describes the
bebop tool for the programming languages community, going into detail on
the relationship to algorithms for interprocedural dataflow analysis.
See the following paper for a more complete description of bebop.
- Bebop: A Symbolic Model
Checker for Boolean Programs
[ PS,
PDF
], Thomas Ball, Sriram K. Rajamani, SPIN
2000 Workshop on Model Checking of Software, LNCS 1885,
August/September 2000, pp. 113-130. Describes the bebop
tool for the model checking community, presents the underlying
algorithm in detail and some preliminary experimental results.
- Predicate Abstraction of C Programs
- Polymorphic
Predicate Abstraction,
Thomas Ball, Todd Millstein, Sriram K. Rajamani, ACM TOPLAS Vol. 27,
No. 2, March 2005, pages 314-343 Generalizes the c2bp algorithm (see below) to work for
Boolean expressions that contain so-called "symbolic
constants".
- Automatic Predicate
Abstraction of C Programs,
[PS,
PDF]
Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani, PLDI
2001, SIGPLAN
Notices 36(5), pp. 203-213. Presents the design and implementation of a predicate
abstraction tool for C programs (c2bp) that translates a C program into
a Boolean program that precisely abstracts the C program with respect
to an input set of Boolean expressions.
- Boolean
and Cartesian Abstractions for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani, TACAS
2001, LNCS
2031, April 2001, pp. 268-283, (previous version as MSR
Technical Report 2000-115). This paper uses Abstract Interpretation to explain the
precision of the c2bp algorithm.
- Predicate Abstraction via
Symbolic Decision Procedures,
Shuvendu Lahiri, Thomas Ball, Byron Cook, CAV 2005. Describes a new algorithm
for performing predicate abstraction.
- Abstraction Refinement
- Refining Approximations in
Software Predicate Abstraction [PDF],
Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani. TACAS 2004. Describes how SLAM
compensates for imprecise Boolean abstractions.
- Generating Abstract
Explanations of Spurious Counterexamples in C Programs, Thomas Ball, Sriram K. Rajamani, MSR-TR-2002-09.
Describes the
Newton tool that generates new predicates based on infeasible paths.
- Relative Completeness of
Abstraction Refinement for Software Model Checking, Thomas Ball, Andreas Podelski, Sriram K. Rajamani, TACAS 2002, LNCS 2280,
April 2002, pp. 158-172 (previous version as MSR
Technical Report 2001-106). A theoretical investigation of the termination
properties of SLAM-like processes
- Zapato: Automatic theorem
proving for predicate abstraction refinement, Thomas Ball, Byron Cook, Shuvendu K. Lahiri and
Lintao Zhang, Tools paper in CAV
2004
- Formalizing Counterexample-driven
Refinement with Weakest Preconditions,
Thomas Ball, MSR-TR-2004-134
(appears in the proceedings of 2004
Marktoberdorf Summer School)
- Concurrency
- Miscellaneous
- From Symptom to Cause:
Localizing Errors in Counterexample Traces, Thomas Ball, Mayur Naik, Sriram Rajamani (POPL 2003): [PS,PDF,PPT]
- Speeding Up Dataflow
Analysis Using Flow-Insensitive Pointer Analysis [PS,
PDF],
Stephen Adams, Thomas Ball, Manuvir Das, Sorin Lerner, Sriram K.
Rajamani, Mark Seigle, Westley Weimer. SAS 2002, LNCS 2477
- Automatic Creation of
Environment Models via Training [PDF],
Thomas Ball, Vladimir Levin, and Fei Xie. TACAS 2004
- SLAM and Static Driver
Verifier: Technology Transfer of Formal Methods inside Microsoft, Thomas Ball, Byron Cook, Vladimir Levin and Sriram
K. Rajamani. MSR-TR-2004-8.
Invited talk/paper for Integrated Formal
Methods 2004.
- A short paper on specifying and
checking properties of software [PS,PDF], presented at the CSTB's July 2001 Symposium on
Fundamentals of Computer Science, July 2001. Powerpoint available.
- The SLAM Toolkit [PS,
PDF],
Thomas Ball, Sriram K. Rajamani, CAV 2001
- Checking Temporal Properties
of Software with Boolean Programs
[ PS,
PDF
], Thomas Ball, Sriram K. Rajamani, Workshop on Advances in
Verification (with CAV 2000)
|
