Efficient coverability analysis by proof minimization
We consider multi-threaded programs with an unbounded number of threads executing a finite-state, non-recursive procedure. Safety properties of such programs can be checked via reduction to the coverability problem for well-structured transition systems (WSTS). In this paper, we present a novel, sou...
Autori principali: | Kaiser, A, Kroening, D, Wahl, T |
---|---|
Altri autori: | Koutny, M |
Natura: | Conference item |
Pubblicazione: |
Springer
2012
|
Documenti analoghi
Model and proof generation for heap-manipulating programs
di: Brain, M, et al.
Pubblicazione: (2014)
di: Brain, M, et al.
Pubblicazione: (2014)
Documenti analoghi
-
Lost in abstraction: monotonicity in multi-threaded programs
di: Kaiser, A, et al.
Pubblicazione: (2016) -
Lost in abstraction: monotonicity in multi-threaded programs
di: Kaiser, A, et al.
Pubblicazione: (2014) -
A widening approach to multithreaded program verification
di: Kaiser, A, et al.
Pubblicazione: (2014) -
Proof-graphs for Minimal Implicational Logic
di: Marcela Quispe-Cruz, et al.
Pubblicazione: (2014-03-01) -
Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs
di: Kroening, D, et al.
Pubblicazione: (2007)