Please use this identifier to cite or link to this item:
|Title:||Exploiting Partial Knowledge for Efficient Model Analysis|
|Authors:||Nuno Moreira Macedo|
|Abstract:||The advancement of constraint solvers and model checkers has enabled the effective analysis of high-level formal specification languages. However, these typically handle a specification in an opaque manner, amalgamating all its constraints in a single monolithic verification task, which often proves to be a performance bottleneck. This paper addresses this issue by proposing a solving strategy that exploits user-provided partial knowledge, namely by assigning symbolic bounds to the problem’s variables, to automatically decompose a verification task into smaller ones, which are prone to being independently analyzed in parallel and with tighter search spaces. An effective implementation of the technique is provided as an extension to the Kodkod relational constraint solver. Evaluation shows that, in average, the proposed technique outperforms the regular amalgamated verification procedure. © Springer International Publishing AG 2017.|
|Appears in Collections:||HASLab - Articles in International Conferences|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.