Berkeley Lazy Abstraction Software Verification Tool
Overview
Group information  
Group name blast
Title Berkeley Lazy Abstraction Software Verification Tool
Summary Berkeley Lazy Abstraction Software Verification Tool
Description BLAST is a software model checker for C programs. The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses. Blast uses counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties. The abstraction is constructed on-the-fly, and only to the required precision.
Group type Software project Special interest group Administrative group
People involved in this group  
Administrators Dirk Beyer beyer
Christopher Brooks cxh cxh@eecs.berkeley.edu
Tom Henzinger tah
Members Dirk Beyer beyer
Christopher Brooks cxh cxh@eecs.berkeley.edu
Tom Henzinger tah
Ranjit Jhala jhala
Rupak Majumdar rupak
Group configuration  
Configuration options Is enabled Has members Has administrator
Fancy HTML Fix HTML Is searchable
Is advertised
Workspace options Home page Discussion forum Private forum
FAQ Member mail list Member notification list
Developer mail list VC mail list Public interest list
Public announce list VC module Bugs
Calendar src directory Notify Developers
Wiki Application Form Show Publications
HTML authoring None VC checkin
You are not logged in 
Contact 
©2002-2017 U.C. Regents