A Decade of Software Model Checking with SLAM.

The article discusses what the authors call a SLAM engine, software code that lets computer programmers set usage rules regarding state and check to see if clients are conforming to those rules. One application for the SLAM engine devised by the authors is a static driver verifier (SDV) that verifie...

Descripción completa

Detalles Bibliográficos
Publicado en:Communications of the ACM Vol. 54; no. 7; pp. 68 - 77
Autores principales: BALL, THOMAS, LEVIN, VLADIMIR, RAJAMANI, SRIRAM K.
Formato: Artículo
Publicado: Association for Computing Machinery Jul2011
Materias:
Acceso en línea:Ver este registro en EBSCOhost
fields @attributes:
  recordID: 1
pdfLink:
plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=63023210&site=ehost-live
header:
  @attributes:
    shortDbName: hlh
    uiTerm: 63023210
    longDbName: Humanities International Complete
    uiTag: AN
  controlInfo:
    bkinfo:
    jinfo:
      jid:
        00010782
        ACM
      jtl: Communications of the ACM
      issn: 00010782
      maglogo: N
    pubinfo:
      dt: Jul2011
      vid: 54
      iid: 7
      pid: 68
      pub: Association for Computing Machinery
    artinfo:
      ui:
        63023210
        10.1145/1965724.1965743
      ppf: 68
      ppct: 9
      formats:
      tig:
        atl: A Decade of Software Model Checking with SLAM.
      aug:
        au:
          BALL, THOMAS
          LEVIN, VLADIMIR
          RAJAMANI, SRIRAM K.
        affil:
          Principal researcher, managing the Software Reliability Research group in Microsoft Research, Redmond, WA.
          Assistant managing director of Microsoft Research India, Bangalore.
      su:
        Application program interfaces
        Microsoft operating systems
        Computer programming
        Compilers (Computer programs)
        Computer software
        Computer software quality control
      sug:
        subj:
          Application program interfaces
          Microsoft operating systems
          Computer programming
          Compilers (Computer programs)
          Computer software
          Computer software quality control
      ab: The article discusses what the authors call a SLAM engine, software code that lets computer programmers set usage rules regarding state and check to see if clients are conforming to those rules. One application for the SLAM engine devised by the authors is a static driver verifier (SDV) that verifies whether device drivers used by the Windows operating system satisfy the usage rules of application program interfaces (APIs). The authors present an overview of their ten-year experience with SLAM and SDV, and describe how they extended SLAM to become an SDV product.
      pubtype: Periodical
      doctype: Article
      src: R
    language: English
    refInfo:
    copyright:
      @attributes:
        flag: Y
      dt:
        @attributes:
          year: 2011
    holdings:
      @attributes:
        islocal: N