CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A liveness checking algorithm that counts

Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Niklas Sörensson
2012 Formal Methods in Computer-Aided Design, FMCAD 2012 p. 52-59. (2012)
[Konferensbidrag, refereegranskat]

We present a simple but novel algorithm for checking liveness properties of finite-state systems, called k-Liveness, which is based on counting and bounding the number of times a fairness constraint can become true. Our implementation of the algorithm is completely SAT-based, works fairly well in practice, and is competitive in performance with alternative methods. In addition, we present a pre-processing technique which can automatically derive extra fairness constraints for any given liveness problem. These constraints can be used to potentially boost the performace of any liveness algorithm. The experimental results show that the extra constraints are particularly beneficial in combination with our k-Liveness algorithm.



Denna post skapades 2013-03-20.
CPL Pubid: 174862