[1/2/20011][8:39 AM]
I'm offline

Friday, November 13, 2009

Symbolic Analysis Laboratory

To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, and utility can be derived from an emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems.

The heart of SAL is a language, developed in collaboration with Stanford and Berkeley, for specifying concurrent systems in a compositional way. It is supported by a tool suite that includes state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers, an experimental "Witness" model checker, and a unique "infinite" bounded model checker based on SMT solving. Auxiliary tools include a simulator, deadlock checker and an automated test generator.

Don't forget to comment when you are done reading


imHepPie said...

adess x paham

Mr Aan said...

aduh...cmne nk terangkn eh

Cikyuyu said...

Ahu ehh..

Mr Aan said... nk trg lebih detail lg...hehe

cikyuyu said...


cikyuyu said...


meo188 said...

welcome to rare sh** - my chemical romance