Title
SPLIT: a compositional LTL verifier
Abstract
This paper describes Split, a compositional verifier for safety and general Ltl properties of shared-variable, multi-threaded programs The foundation is a computation of compact local invariants, one for each process, which are used for constructing a proof for the property An automatic refinement procedure gradually exposes more local information, until a decisive result (proof/disproof) is obtained.
Year
DOI
Venue
2010
10.1007/978-3-642-14295-6_47
CAV
Keywords
Field
DocType
compositional ltl verifier,local information,compact local invariants,multi-threaded program,compositional verifier,general ltl property,decisive result,automatic refinement procedure
Computer science,Algorithm,Theoretical computer science,Invariant (mathematics),Cache coherence,Computation
Conference
Volume
ISSN
ISBN
6174
0302-9743
3-642-14294-X
Citations 
PageRank 
References 
5
0.51
14
Authors
3
Name
Order
Citations
PageRank
Ariel Cohen1865.63
Kedar S. Namjoshi294850.41
Yaniv Sa'ar323014.70