ITEM METADATA RECORD
Title: Software model synthesis using satisfiability solvers
Authors: Heule, Marijn ×
Verwer, Sicco #
Issue Date: 2013
Publisher: Kluwer Academic Publishers
Series Title: Empirical Software Engineering vol:18 issue:4 pages:825-856
Abstract: We introduce a novel approach for synthesis of software models based on identifying deterministic finite state automata. Our approach consists of three important contributions. First, we argue that in order to model software, one should focus mainly on observed executions (positive data), and use the randomly generated failures (negative data) only for testing consistency. We present a new greedy heuristic for this purpose, and show how to integrate it in the state-of-the-art evidence-driven state-merging (EDSM) algorithm. Second, we apply the enhanced EDSM algorithm to iteratively reduce the size of the problem. Yet during each iteration, the evidence is divided over states and hence the effectiveness of this algorithm is decreased. We propose—when EDSM becomes too weak—to tackle the reduced identification problem using satisfiability solvers. Third, in case the amount of positive data is small, we solve the identification problem several times by randomizing the greedy heuristic and combine the solutions using a voting scheme. The interaction between these contributions appeared crucial to solve hard software models synthesis benchmarks. Our implementation, called DFASAT, won the StaMinA competition.
URI: 
ISSN: 1382-3256
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
heule_verwer2012.pdfOA article Published 555KbAdobe PDFView/Open

 


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science