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:	Application program interfaces Microsoft operating systems Computer programming Compilers (Computer programs) Computer software Computer software quality control
Acceso en línea:	Ver este registro en EBSCOhost

Descripción
Sumario:	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.