0
$\begingroup$

The SLAM project at Microsoft (as detailed in this slide) was highly regarded for detecting bugs in Windows device drivers. Some of its key strengths include discovering real bugs, scalability (handling 100k+ lines of code), and fully automated analysis. I’m curious about how this area of research (and its application in industry) has progressed since then. (There's some information from 2009 in this paper, but not much on how this was used in industry other than Microsoft)

  1. Are there any successor tools or modern equivalents of SLAM in use today, particularly in the context of static analysis or model checking?
  2. What verification tasks, beyond Windows device driver verification, is SLAM or similar tools commonly used for in research or industry?
  3. While SLAM was fully automated, users needed to manually define invariants (referred to as "API rules" in SLAM). How does this compare to tools like CBMC or Dafny? Could these newer tools be considered replacements for SLAM?
  4. What are the advantages or disadvantages of modern tools in comparison to SLAM?

Disclaimer: I’m not an expert in static analysis, so these questions may come across as naive. I’d appreciate any clarifications or insights.

I’m interested in the evolution of this line of work, including the tools and methodologies being used today for large-scale static analysis and verification.

Improve this question
$\endgroup$
1
  • $\begingroup$ Please ask only one question per post. When you have multiple questions, they can be asked separately. $\endgroup$ Commented Feb 13 at 23:35

0

Reset to default

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.