Journal article icon

Journal article

Verification of Boolean programs with unbounded thread creation.

Abstract:

Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S.K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN 00, in: Lecture Notes in Computer Science, vol. 1885, Springer, 2000, pp. 113-130] are the most popular representation for these abstractions. Unfortunately, today's symbolic software model checkers are limited to the analysis of sequential pr...

Expand abstract
Publication status:
Published

Actions


Access Document


Publisher copy:
10.1016/j.tcs.2007.07.050

Authors


Kroening, D More by this author
Sharygina, N More by this author
Journal:
Theor. Comput. Sci.
Volume:
388
Issue:
1-3
Pages:
227-242
Publication date:
2007
DOI:
ISSN:
0304-3975
URN:
uuid:8f25e1b6-2e9f-4522-b746-21438f5d652f
Source identifiers:
327167
Local pid:
pubs:327167

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP