|Sequentialization and Bounded Model-checking|
du groupe Modélisation et Verification
|Date|| 2014-06-05 11:00-12:00|
|Titre||Sequentialization and Bounded Model-checking |
|Résumé||Bounded model checking (BMC) has successfully been used
for many practical program verification problems, but concurrency still
poses a challenge. Sequentializations have emerged as an efficient technique
to obtain analysis tools for concurrent programs by reusing tools designed for sequential programs.
In this talk, we describe some recent results concerning the design and the implementation of
efficient sequentializations targeted to using BMC tools as backends.
The presented sequentializations are implemented in the tool CSeq
|Orateur||Salvatore La Torre |
|Url||Univ. Salerno |
Aucun document lié à cet événement.RetourRetour à l'index