Software Model Synthesis by Identifying DFAs using Satisfiability Solvers

  • 2012-03-05
  • Research

We introduce a novel approach for synthesis of software models based on identifying deterministic finite state automata.


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) instead of randomly generated failures (negative data). 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.


Marijn J.H. Heule is a postdoc at Delft University of Technology, The Netherlands. His research focuses on construction of SAT solvers for general purposes. In contrast to most researchers in the field, he aims to achieve this merely by adding extensive reasoning to his solver March. This successful solver won a dozen awards in several SAT competitions. Apart from developing solvers, he applied the power of SAT solving to outperform alternative techniques for problems such as identifying deterministic finite state automata and improving lower bounds for numbers in Ramsey Theory. He is one of the editors of the Handbook of Satisfiability and editor of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT).

Contact person at the TU Vienna

Katja Hildebrandt: Tel. +43 1 588 01 – 188 04


This talk is organized by the Business Informatics Group at the Institute of Software Technology and Interactive Systems. Supported by the project „fFORTE-WIT-Women in Technology“, the WWTF project “FAME” and the Austrian Computer Society (OCG).


Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!