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 Cohen | 1 | 86 | 5.63 |
Kedar S. Namjoshi | 2 | 948 | 50.41 |
Yaniv Sa'ar | 3 | 230 | 14.70 |