{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:13:15Z","timestamp":1769731995496,"version":"3.49.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,8,9]],"date-time":"2012-08-09T00:00:00Z","timestamp":1344470400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10664-012-9222-z","type":"journal-article","created":{"date-parts":[[2012,8,8]],"date-time":"2012-08-08T08:35:51Z","timestamp":1344414951000},"page":"825-856","source":"Crossref","is-referenced-by-count":40,"title":["Software model synthesis using satisfiability solvers"],"prefix":"10.1007","volume":"18","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sicco","family":"Verwer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,8,9]]},"reference":[{"key":"9222_CR1","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/978-3-642-15375-4_6","volume-title":"CONCUR","author":"F Aarts","year":"2010","unstructured":"Aarts F, Vaandrager F (2010) Learning I\/O automata. In: CONCUR. Lecture notes in computer science, vol 6269. Springer, New York, pp 71\u201385"},{"key":"9222_CR2","series-title":"LNCS","first-page":"28","volume-title":"ICGI","author":"J Abela","year":"2004","unstructured":"Abela J, Coste F, Spina S (2004) Mutually compatible and incompatible merges for the search of the smallest consistent DFA. In: ICGI. LNCS, vol 3264. Springer, New York, pp 28\u201339"},{"key":"9222_CR3","doi-asserted-by":"crossref","unstructured":"Ammons G, Bodik R, Larus JR (2002) Mining specifications. In: Proceedings of the symposium on principles of programming languages. ACM, pp 4\u201316","DOI":"10.1145\/503272.503275"},{"key":"9222_CR4","doi-asserted-by":"crossref","unstructured":"Antunes J, Neves N, Verissimo P (2011) Reverse engineering of protocols from network traces. In: Working conference on reverse engineering, pp 169\u2013178","DOI":"10.1109\/WCRE.2011.28"},{"key":"9222_CR5","doi-asserted-by":"crossref","unstructured":"Bertolino A, Inverardi P, Pelliccione P, Tivoli M (2009) Automatic synthesis of behavior protocols for composable web-services. In: Proceedings of the joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering. ACM, pp 141\u2013150","DOI":"10.1145\/1595696.1595719"},{"key":"9222_CR6","doi-asserted-by":"crossref","unstructured":"Biere A (2008) PicoSAT essentials. JSAT 4(2\u20134):75\u201397. http:\/\/jsat.ewi.tudelft.nl\/content\/volume4\/JSAT4_5_Biere.pdf","DOI":"10.3233\/SAT190039"},{"key":"9222_CR7","first-page":"193","volume-title":"TACAS \u201999","author":"A Biere","year":"1999","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: TACAS \u201999. Springer, London, UK, pp 193\u2013207"},{"key":"9222_CR8","volume-title":"Handbook of satisfiability, frontiers in artificial intelligence and applications, handbook of satisfiability, vol 185","year":"2009","unstructured":"Biere A, Heule MJH, van Maaren H, Walsh T (eds) (2009) Handbook of satisfiability, frontiers in artificial intelligence and applications, handbook of satisfiability, vol 185. IOS Press, Amsterdam, The Netherlands"},{"issue":"6","key":"9222_CR9","doi-asserted-by":"crossref","first-page":"592","DOI":"10.1109\/TC.1972.5009015","volume":"21","author":"AW Biermann","year":"1972","unstructured":"Biermann AW, Feldman JA (1972) On the synthesis of finite-state machines from samples of their behavior. IEEE Trans Comput 21(6):592\u2013597. doi: 10.1109\/TC.1972.5009015","journal-title":"IEEE Trans Comput"},{"key":"9222_CR10","volume-title":"Model-based testing of reactive systems. Lecture notes in computer science, vol 3472","year":"2005","unstructured":"Broy M, Jonsson B, Katoen JP, Leucker M, Pretschner A (eds) (2005) Model-based testing of reactive systems. Lecture notes in computer science, vol 3472. Springer, New York"},{"key":"9222_CR11","doi-asserted-by":"crossref","first-page":"1457","DOI":"10.1016\/j.patcog.2004.03.027","volume":"38","author":"M Bugalho","year":"2005","unstructured":"Bugalho M, Oliveira AL (2005) Inference of regular languages using state merging algorithms with search. Pattern Recognit 38:1457\u20131467","journal-title":"Pattern Recognit"},{"key":"9222_CR12","doi-asserted-by":"crossref","unstructured":"Castro J, Gavald\u00e0 R (2008) Towards feasible PAC-learning of probabilistic deterministic finite automata. In: ICGI, pp 163\u2013174","DOI":"10.1007\/978-3-540-88009-7_13"},{"key":"9222_CR13","unstructured":"Clark A, Thollard F (2004) PAC-learnability of probabilistic deterministic finite state automata. J Mach Learn Res 5:473\u2013497"},{"key":"9222_CR14","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/BFb0058022","volume-title":"Foundations of software technology and theoretical computer science","author":"E Clarke","year":"1997","unstructured":"Clarke E (1997) Model checking. In: Foundations of software technology and theoretical computer science. LNCS, vol 1346. Springer, New York, pp 54\u201356"},{"key":"9222_CR15","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/287000.287001","volume":"7","author":"JE Cook","year":"1998","unstructured":"Cook JE, Wolf AL (1998) Discovering models of software processes from event-based data. ACM Trans Softw Eng Methodol 7:215\u2013249","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"9222_CR16","unstructured":"Coste F, Nicolas J (1997) Regular inference as a graph coloring problem. In: Workshop on grammatical inference, automata induction, and language acquisition (ICML\u201997)"},{"key":"9222_CR17","unstructured":"Cui W, Kannan J, Wang HJ (2007) Discoverer: automatic protocol reverse engineering from network traces. In: Proceedings of 16th USENIX security symposium, p 14"},{"key":"9222_CR18","doi-asserted-by":"crossref","unstructured":"Dallmeier V, Lindig C, Wasylkowski A, Zeller A (2006) Mining object behavior with ADABU. In: Proceedings of the 2006 international workshop on dynamic systems analysis, ACM, WODA \u201906, pp 17\u201324","DOI":"10.1145\/1138912.1138918"},{"key":"9222_CR19","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139194655","volume-title":"Grammatical inference: learning automata and grammars","author":"C Higuera de la","year":"2010","unstructured":"de\u00a0la Higuera C (2010) Grammatical inference: learning automata and grammars. Cambridge University Press, New York, NY, USA"},{"key":"9222_CR20","doi-asserted-by":"crossref","unstructured":"Denis F, Lemay A, Terlutte A (2000) Learning regular languages using non deterministic finite automata. In: ICGI, pp 39\u201350","DOI":"10.1007\/978-3-540-45257-7_4"},{"key":"9222_CR21","doi-asserted-by":"crossref","unstructured":"Dietterich T (2000) Ensemble methods in machine learning. In: Multiple classifier systems. LNCS, vol 1857. Springer, pp 1\u201315","DOI":"10.1007\/3-540-45014-9_1"},{"issue":"1\u20132","key":"9222_CR22","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1080\/08839510701853200","volume":"22","author":"P Dupont","year":"2008","unstructured":"Dupont P, Lambeau B, Damas C, van Lamsweerde A (2008) The QSM algorithm and its application to software behavior model induction. Appl Artif Intell 22(1\u20132):77\u2013115","journal-title":"Appl Artif Intell"},{"issue":"2\u20133","key":"9222_CR23","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis J, Waldmann J, Zantema H (2008) Matrix interpretations for proving termination of term rewriting. J Autom Reason 40(2\u20133):195\u2013220. 10.1007\/s10817-007-9087-9","journal-title":"J Autom Reason"},{"key":"9222_CR24","volume-title":"Computers and intractability: a guide to the theory of NP-completeness","author":"MR Garey","year":"1979","unstructured":"Garey MR, Johnson DS (1979) Computers and intractability: a guide to the theory of NP-completeness. W. H. Freeman & Co., New York, NY, USA"},{"issue":"3","key":"9222_CR25","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1016\/S0019-9958(78)90562-4","volume":"37","author":"EM Gold","year":"1978","unstructured":"Gold EM (1978) Complexity of automaton identification from given data. Inf Control 37(3):302\u2013320","journal-title":"Inf Control"},{"key":"9222_CR26","doi-asserted-by":"crossref","unstructured":"Grinchtein O, Jonsson B, Petterson P (2006a) Inference of event-recording automata using timed decision trees. In: CONCUR. LNCS, vol 4137. Springer, pp 435\u2013449","DOI":"10.1007\/11817949_29"},{"key":"9222_CR27","doi-asserted-by":"crossref","unstructured":"Grinchtein O, Leucker M, Piterman N (2006b) Inferring network invariants automatically. In: Automated reasoning. LNCS, vol 4130. Springer, pp 483\u2013497","DOI":"10.1007\/11814771_40"},{"key":"9222_CR28","unstructured":"Heule MJH, Verwer S (2010) Exact DFA identification using SAT solvers. In: ICGI. LNCS, vol 6339. Springer, pp 66\u201379"},{"issue":"2","key":"9222_CR29","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/j.tcs.2003.11.009","volume":"313","author":"Cdl Higuera","year":"2004","unstructured":"Higuera Cdl, Janodet JC (2004) Inference of omega-languages from prefixes. Theor Comp Sci 313(2):295\u2013312","journal-title":"Theor Comp Sci"},{"key":"9222_CR30","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6610.001.0001","volume-title":"Systems that learn","author":"S Jain","year":"1999","unstructured":"Jain S, Osherson D, Royer JS, Sharma A (1999) Systems that learn. MIT Press, Cambridge, MA"},{"key":"9222_CR31","doi-asserted-by":"crossref","unstructured":"Jarvisalo M, Biere A, Heule MJH (2010) Blocked clause elimination. In: TACAS 2010. LNCS, vol 6015. Springer, pp 129\u2013144","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"9222_CR32","unstructured":"Juill\u00e9 H, Pollack JB (1998) A sampling-based heuristic for tree search applied to grammar induction. In: Innovative applications of artificial intelligence. American Association for Artificial Intelligence, Menlo Park, CA, USA, AAAI \u201998, pp 776\u2013783. http:\/\/dl.acm.org\/citation.cfm?id=295240.295804"},{"key":"9222_CR33","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An introduction to computational learning theory","author":"MJ Kearns","year":"1994","unstructured":"Kearns MJ, Vazirani UV (1994) An introduction to computational learning theory. MIT Press, Cambridge, MA"},{"issue":"1","key":"9222_CR34","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"97","author":"O Kullmann","year":"1999","unstructured":"Kullmann O (1999) On a generalization of extended resolution. Discrete Appl Math 96\u201397(1):149\u2013176. doi: 10.1016\/S0166-218X(99)00037-2","journal-title":"Discrete Appl Math"},{"key":"9222_CR35","unstructured":"Lang KJ (1999) Faster algorithms for finding minimal consistent DFAs. Tech. rep., NEC Research Institute"},{"key":"9222_CR36","doi-asserted-by":"crossref","unstructured":"Lang KJ, Pearlmutter BA, Price RA (1998) Results of the Abbadingo one DFA learning competition and a new evidence-driven state merging algorithm. In: ICGI. LNCS. Springer, vol 1433","DOI":"10.1007\/BFb0054059"},{"key":"9222_CR37","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1109\/TSE.2010.93","volume":"37","author":"L Mariani","year":"2011","unstructured":"Mariani L, Pastore F, Pezze M (2011) Dynamic analysis for diagnosing integration faults. IEEE Trans Softw Eng 37:486\u2013508","journal-title":"IEEE Trans Softw Eng"},{"key":"9222_CR38","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1145\/307418.307477","volume-title":"Proceedings of DATE \u201999","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva JP, Glass T (1999) Combinational equivalence checking using satisfiability and recursive learning. In: Proceedings of DATE \u201999. ACM, New York, NY, USA, p\u00a033. doi: 10.1145\/307418.307477"},{"key":"9222_CR39","doi-asserted-by":"crossref","unstructured":"Oliveira AL, Marques-Silva JP (1998) Efficient search techniques for the inference of minimum sized finite state machines. String processing and information retrieval, pp 81\u201389","DOI":"10.1109\/SPIRE.1998.712986"},{"key":"9222_CR40","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1142\/9789812797902_0004","volume-title":"Pattern recognition and image analysis, series in machine perception and artificial intelligence, vol\u00a01","author":"J Oncina","year":"1992","unstructured":"Oncina J, Garcia P (1992) Inferring regular languages in polynomial update time. In: Pattern recognition and image analysis, series in machine perception and artificial intelligence, vol\u00a01. World Scientific, Singapore, pp 49\u201361"},{"key":"9222_CR41","unstructured":"Pitt L, Warmuth M (1989) The minimum consistent DFA problem cannot be approximated within and polynomial. In: Annual ACM symposium on theory of computing. ACM, pp 421\u2013432"},{"key":"9222_CR42","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/s10009-009-0111-8","volume":"11","author":"H Raffelt","year":"2009","unstructured":"Raffelt H, Steffen B, Berg T, Margaria T (2009) Learnlib: a framework for extrapolating behavioral models. Int J Softw Tools Technol Transf 11:393\u2013407","journal-title":"Int J Softw Tools Technol Transf"},{"key":"9222_CR43","unstructured":"Sakallah KA (2009) Symmetry and satisfiability, chap\u00a010, pp 289\u2013338. Vol 185 of Biere et\u00a0al. (2009)"},{"key":"9222_CR44","volume-title":"Languages and machines: an introduction to the theory of computer science","author":"TA Sudkamp","year":"2006","unstructured":"Sudkamp TA (2006) Languages and machines: an introduction to the theory of computer science, 3rd edn. Addison-Wesley, Reading, MA","edition":"3"},{"key":"9222_CR45","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19345-3","volume-title":"Process mining\u2014discovery, conformance and enhancement of business processes","author":"WMP Aalst van der","year":"2011","unstructured":"van\u00a0der Aalst WMP (2011) Process mining\u2014discovery, conformance and enhancement of business processes. Springer, New York"},{"key":"9222_CR46","unstructured":"Verwer S (2010) Efficient identification of timed automata: theory and practice. PhD thesis, Delft University of Technology"},{"key":"9222_CR47","doi-asserted-by":"crossref","unstructured":"Walkinshaw N, Bogdanov K, Holcombe M, Salahuddin S (2007) Reverse engineering state machines by interactive grammar inference. In: Proceedings of the 14th working conference on reverse engineering. IEEE, pp 209\u2013218","DOI":"10.1109\/WCRE.2007.45"},{"key":"9222_CR48","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1868044.1868045","volume-title":"Proceedings of the first international workshop on model inference in testing, MIIT \u201910","author":"N Walkinshaw","year":"2010","unstructured":"Walkinshaw N, Bogdanov K, Damas C, Lambeau B, Dupont P (2010) A framework for the competitive evaluation of model inference techniques. In: Proceedings of the first international workshop on model inference in testing, MIIT \u201910. ACM, New York, NY, USA, pp 1\u20139"},{"key":"9222_CR49","first-page":"441","volume-title":"CP \u201902: proceedings of the 6th international conference on principles and practice of constraint programming","author":"T Walsh","year":"2000","unstructured":"Walsh T (2000) SAT v CSP. In: CP \u201902: proceedings of the 6th international conference on principles and practice of constraint programming. Springer, London, UK, pp 441\u2013456"},{"key":"9222_CR50","unstructured":"Yokomori T (1993) Learning non-deterministic finite automata from queries and counterexamples. In: Machine intelligence. University Press, pp 196\u2013189"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-012-9222-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10664-012-9222-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-012-9222-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,25]],"date-time":"2022-01-25T22:29:49Z","timestamp":1643149789000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10664-012-9222-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,9]]},"references-count":50,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["9222"],"URL":"https:\/\/doi.org\/10.1007\/s10664-012-9222-z","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"value":"1382-3256","type":"print"},{"value":"1573-7616","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,9]]}}}