Please use this identifier to cite or link to this item:
|Title:||Compositional encoding for bounded model checking||Authors:||Sun, J.
|Keywords:||Bounded model checking
Communication Sequential Processes (CSP)
Linear Temporal Logic (LTL)
|Issue Date:||2008||Citation:||Sun, J.,Liu, Y.,Dong, J.S.,Sun, J. (2008). Compositional encoding for bounded model checking. Frontiers of Computer Science in China 2 (4) : 368-379. ScholarBank@NUS Repository. https://doi.org/10.1007/s11704-008-0035-6||Abstract:||Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit onthe-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems. © 2008 Higher Education Press and Springer-Verlag GmbH.||Source Title:||Frontiers of Computer Science in China||URI:||http://scholarbank.nus.edu.sg/handle/10635/38949||ISSN:||16737350||DOI:||10.1007/s11704-008-0035-6|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Mar 25, 2020
checked on Mar 31, 2020
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.