Selected publications at LSV

Recent work studied the unfolding construction for contextual nets, i.e. nets with read arcs. Such unfoldings are more concise and can usually be constructed more efficiently than for Petri nets. However, concrete verification algorithms exploiting these advantages were lacking so far. We address this question and propose SAT-based verification algorithms for deadlock and reachability of contextual nets. Moreover, we study optimizations of the SAT encoding and report on experiments.

   address = {Newcastle, UK},
   author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
   booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)},
   DOI = {10.1007/978-3-642-32940-1_33},
   editor = {Koutny, Maciej and Ulidowski, Irek},
   month = sep,
   pages = {471-485},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Verification of {P}etri Nets with Read Arcs},
   url = {},
   volume = {7454},
   year = {2012},

About LSV