Follower's

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

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

7 comments:

imHepPie said...

adess x paham

Mr Aan said...

aduh...cmne nk terangkn eh

Cikyuyu said...

Ahu ehh..

Mr Aan said...

thu...mls nk trg lebih detail lg...hehe

cikyuyu said...

Hahahahahaha.
10si0n.

cikyuyu said...

Hahahahahaha.
10si0n.

meo188 said...

welcome to rare sh** - my chemical romance