Sequentialization translates concurrent programs into equivalent non-deterministic sequential programs so that the different concurrent schedules no longer need to be handled explicitly. It can thus be used as a concurrency pre-processor for many sequential program verification techniques. CSeq implements sequentialization for C and uses ESBMC as sequential verification backend.
CSeq: A Sequentialization Tool for C
PARLATO G
2013-01-01
Abstract
Sequentialization translates concurrent programs into equivalent non-deterministic sequential programs so that the different concurrent schedules no longer need to be handled explicitly. It can thus be used as a concurrency pre-processor for many sequential program verification techniques. CSeq implements sequentialization for C and uses ESBMC as sequential verification backend.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
