{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T21:52:28Z","timestamp":1767909148857,"version":"3.49.0"},"reference-count":66,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,8,6]],"date-time":"2023-08-06T00:00:00Z","timestamp":1691280000000},"content-version":"vor","delay-in-days":248,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["Task 2707.001"],"award-info":[{"award-number":["Task 2707.001"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006558","name":"Balliol College, University of Oxford","doi-asserted-by":"publisher","award":["Jason Hu Scholarship"],"award-info":[{"award-number":["Jason Hu Scholarship"]}],"id":[{"id":"10.13039\/501100006558","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a new active model-learning approach to generating abstractions of a system from its execution traces. Given a system and a set of observables to collect execution traces, the abstraction produced by the algorithm is guaranteed to admit all system traces over the set of observables. To achieve this, the approach uses a pluggable model-learning component that can generate a model from a given set of traces. Conditions that encode a certain completeness hypothesis, formulated based on simulation relations, are then extracted from the abstraction under construction and used to evaluate its degree of completeness. The extracted conditions are sufficient to prove model completeness but not necessary. If all conditions are true, the algorithm terminates, returning a system overapproximation. A condition falsification may not necessarily correspond to missing system behaviour in the abstraction. This is resolved by applying model checking to determine whether it corresponds to any concrete system trace. If so, the new concrete trace is used to iteratively learn new abstractions, until all extracted completeness conditions are true. To evaluate the approach, we reverse-engineer a set of publicly available Simulink Stateflow models from their C implementations. Our algorithm generates an equivalent model for 98% of the Stateflow models.<\/jats:p>","DOI":"10.1007\/s10703-023-00433-y","type":"journal-article","created":{"date-parts":[[2023,8,6]],"date-time":"2023-08-06T15:01:26Z","timestamp":1691334086000},"page":"164-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Enhancing active model learning with equivalence checking using simulation relations"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3676-1843","authenticated-orcid":false,"given":"Natasha","family":"Yogananda Jeppu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Melham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,8,6]]},"reference":[{"key":"433_CR1","doi-asserted-by":"publisher","unstructured":"Aarts F, Jonsson B, Uijen J (2010) Generating models of infinite-state communication protocols using regular inference with abstraction. In: Petrenko A, Sim\u00e3o A, Maldonado JC (eds) Testing software and systems. Springer, pp 188\u2013204. https:\/\/doi.org\/10.1007\/978-3-642-16573-3_14","DOI":"10.1007\/978-3-642-16573-3_14"},{"key":"433_CR2","doi-asserted-by":"publisher","unstructured":"Aarts F, Heidarian F, Kuppens H, et\u00a0al (2012) Automata learning through counterexample guided abstraction refinement. In: Giannakopoulou D, M\u00e9ry D (eds) Formal methods. Springer, pp 10\u201327. https:\/\/doi.org\/10.1007\/978-3-642-32759-9_4","DOI":"10.1007\/978-3-642-32759-9_4"},{"key":"433_CR3","doi-asserted-by":"publisher","unstructured":"Alur R, Benedikt M, Etessami K, et\u00a0al (2005) Analysis of recursive state machines. In: ACM Trans. Program. Lang. Syst., vol\u00a027. Association for Computing Machinery, pp 786-818. https:\/\/doi.org\/10.1145\/1075382.1075387","DOI":"10.1145\/1075382.1075387"},{"key":"433_CR4","doi-asserted-by":"publisher","unstructured":"Angluin D (1987) Learning regular sets from queries and counterexamples. In: Inf. Comput., vol\u00a075. Academic Press, Inc., pp 87\u2013106. https:\/\/doi.org\/10.1016\/0890-5401(87)90052-6","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"433_CR5","doi-asserted-by":"publisher","unstructured":"Argyros G, D\u2019Antoni L (2018) The learnability of symbolic automata. In: Chockler H, Weissenbacher G (eds) Computer aided verification. Springer, pp 427\u2013445. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_23","DOI":"10.1007\/978-3-319-96145-3_23"},{"key":"433_CR6","doi-asserted-by":"publisher","unstructured":"Ashar P, Ghosh A, Devadas S (1992) Boolean satisfiability and equivalence checking using general binary decision diagrams. In: Integration, pp 1\u201316. https:\/\/doi.org\/10.1016\/0167-9260(92)90015-Q","DOI":"10.1016\/0167-9260(92)90015-Q"},{"key":"433_CR7","doi-asserted-by":"publisher","unstructured":"Berg T, Jonsson B, Raffelt H (2008) Regular inference for state machines using domains with equality tests. In: Fiadeiro JL, Inverardi P (eds) Fundamental approaches to software engineering. Springer, pp 317\u2013331.https:\/\/doi.org\/10.1007\/978-3-540-78743-3_24","DOI":"10.1007\/978-3-540-78743-3_24"},{"key":"433_CR8","doi-asserted-by":"publisher","unstructured":"Biermann AW, Feldman JA (1972) On the synthesis of finite-state machines from samples of their behavior. In: IEEE Trans. Comput., vol\u00a021. IEEE Computer Society, pp 592\u2013597. https:\/\/doi.org\/10.1109\/TC.1972.5009015","DOI":"10.1109\/TC.1972.5009015"},{"key":"433_CR9","doi-asserted-by":"publisher","unstructured":"Botin\u010dan M, Babi\u0107 D (2013) Sigma*: Symbolic learning of input-output specifications. In: Principles of programming languages. ACM, POPL \u201913, pp 443\u2013456. https:\/\/doi.org\/10.1145\/2429069.2429123","DOI":"10.1145\/2429069.2429123"},{"key":"433_CR10","unstructured":"Cassel S, Howar F, Jonsson B (2015) RALib: a LearnLib extension for inferring EFSMs. In: DIFTS"},{"key":"433_CR11","doi-asserted-by":"publisher","unstructured":"Cassel S, Howar F, Jonsson B, et\u00a0al (2016) Active learning for extended finite state machines. In: Formal aspects of computing, pp 233\u2013263. https:\/\/doi.org\/10.1007\/s00165-016-0355-5","DOI":"10.1007\/s00165-016-0355-5"},{"key":"433_CR12","doi-asserted-by":"publisher","unstructured":"Chockler H, Kesseli P, Kroening D, et\u00a0al (2020) Learning the language of software errors. In: Journal artificial intelligence research, vol\u00a067. Morgan Kaufmann Publishers, Inc., pp 881\u2013903. https:\/\/doi.org\/10.1613\/jair.1.11798","DOI":"10.1613\/jair.1.11798"},{"key":"433_CR13","doi-asserted-by":"publisher","unstructured":"Clarke E, Grumberg O, Jha S, et\u00a0al (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP (eds) Computer aided verification. Springer, pp 154\u2013169. https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"433_CR14","doi-asserted-by":"publisher","unstructured":"Clarke E, Kroening D, Yorav K (2003) Behavioral consistency of C and Verilog programs using bounded model checking. In: Design automation conference. Association for Computing Machinery, DAC \u201903, pp 368\u2013371.https:\/\/doi.org\/10.1145\/775832.775928","DOI":"10.1145\/775832.775928"},{"key":"433_CR15","doi-asserted-by":"publisher","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Tools and algorithms for the construction and analysis of systems. Springer, pp 168\u2013176. https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"433_CR16","unstructured":"Clarke EM, Grumberg O, Kroening D et al (2018) Model checking, 2nd edn. MIT Press"},{"key":"433_CR17","doi-asserted-by":"publisher","unstructured":"Cobleigh JM, Giannakopoulou D, P\u0103s\u0103reanu CS (2003) Learning assumptions for compositional verification. In: Garavel H, Hatcliff J (eds) Tools and algorithms for the construction and analysis of systems. Springer, pp 331\u2013346. https:\/\/doi.org\/10.1007\/3-540-36577-X_24","DOI":"10.1007\/3-540-36577-X_24"},{"key":"433_CR18","doi-asserted-by":"publisher","unstructured":"Dorofeeva R, El-Fakih K, Maag S, et\u00a0al (2010) FSM-based conformance testing methods: a survey annotated with experimental evaluation. In: Information and software technology, pp 1286\u20131297. https:\/\/doi.org\/10.1016\/j.infsof.2010.07.001","DOI":"10.1016\/j.infsof.2010.07.001"},{"key":"433_CR19","doi-asserted-by":"publisher","unstructured":"Dupont P, Lambeau B, Damas C, et\u00a0al (2008) The QSM algorithm and its application to software behavior model induction. In: Applied artificial intelligence, vol\u00a022. Taylor & Francis, pp 77\u2013115. https:\/\/doi.org\/10.1080\/08839510701853200","DOI":"10.1080\/08839510701853200"},{"key":"433_CR20","doi-asserted-by":"publisher","unstructured":"Feng L, Kwiatkowska M, Parker D (2011) Automated learning of probabilistic assumptions for compositional reasoning. In: Giannakopoulou D, Orejas F (eds) Fundamental approaches to software engineering. Springer, pp 2\u201317. https:\/\/doi.org\/10.1007\/978-3-642-19811-3_2","DOI":"10.1007\/978-3-642-19811-3_2"},{"key":"433_CR21","doi-asserted-by":"publisher","unstructured":"Fiter\u0103u-Bro\u015ftean P, Howar F (2017) Learning-based testing the sliding window behavior of TCP implementations. In: Petrucci L, Seceleanu C, Cavalcanti A (eds) Critical systems: formal methods and automated verification. Springer, pp 185\u2013200. https:\/\/doi.org\/10.1007\/978-3-319-67113-0_12","DOI":"10.1007\/978-3-319-67113-0_12"},{"key":"433_CR22","doi-asserted-by":"publisher","unstructured":"Gallier J, La\u00a0Torre S, Mukhopadhyay S (2003) Deterministic finite automata with recursive calls and DPDAs. In: Inf. Process. Lett., pp 187\u2013193. https:\/\/doi.org\/10.1016\/S0020-0190(03)00281-3","DOI":"10.1016\/S0020-0190(03)00281-3"},{"key":"433_CR23","doi-asserted-by":"publisher","unstructured":"Garhewal B, Vaandrager F, Howar F, et\u00a0al (2020) Grey-box learning of register automata. In: Integrated formal methods. Springer, pp 22\u201340. https:\/\/doi.org\/10.1007\/978-3-030-63461-2_2","DOI":"10.1007\/978-3-030-63461-2_2"},{"key":"433_CR24","doi-asserted-by":"publisher","unstructured":"Giannakopoulou D, Rakamari\u0107 Z, Raman V (2012) Symbolic learning of component interfaces. In: Min\u00e9 A, Schmidt D (eds) Static analysis. Springer, pp 248\u2013264. https:\/\/doi.org\/10.1007\/978-3-642-33125-1_18","DOI":"10.1007\/978-3-642-33125-1_18"},{"key":"433_CR25","doi-asserted-by":"publisher","unstructured":"Goldberg E, Prasad M, Brayton R (2001) Using SAT for combinational equivalence checking. In: Design, automation and test in Europe, pp 114\u2013121. https:\/\/doi.org\/10.1109\/DATE.2001.915010","DOI":"10.1109\/DATE.2001.915010"},{"key":"433_CR26","doi-asserted-by":"publisher","unstructured":"Groce A, Peled D, Yannakakis M (2002) Adaptive model checking. In: Katoen JP, Stevens P (eds) Tools and algorithms for the construction and analysis of systems. Springer, pp 357\u2013370. https:\/\/doi.org\/10.1007\/3-540-46002-0_25","DOI":"10.1007\/3-540-46002-0_25"},{"key":"433_CR27","doi-asserted-by":"publisher","unstructured":"Heule MJH, Verwer S (2010) Exact DFA identification using SAT solvers. In: Sempere JM, Garc\u00eda P (eds) Grammatical inference: theoretical results and applications. Springer, pp 66\u201379. https:\/\/doi.org\/10.1007\/978-3-642-15488-1_7","DOI":"10.1007\/978-3-642-15488-1_7"},{"key":"433_CR28","doi-asserted-by":"publisher","unstructured":"Howar F, Steffen B (2018) Active automata learning in practice: an annotated bibliography of the years 2011 to 2016. In: Bennaceur A, H\u00e4hnle R, Meinke K (eds) Machine learning for dynamic software analysis, lecture notes in computer science, vol 11026. Springer, pp 123\u2013148. https:\/\/doi.org\/10.1007\/978-3-319-96562-8_5","DOI":"10.1007\/978-3-319-96562-8_5"},{"key":"433_CR29","doi-asserted-by":"publisher","unstructured":"Howar F, Steffen B, Merten M (2011) Automata learning with automated alphabet abstraction refinement. In: Jhala R, Schmidt D (eds) Verification, model checking, and abstract interpretation. Springer, pp 263\u2013277.https:\/\/doi.org\/10.1007\/978-3-642-18275-4_19","DOI":"10.1007\/978-3-642-18275-4_19"},{"key":"433_CR30","doi-asserted-by":"publisher","unstructured":"Howar F, Giannakopoulou D, Rakamari\u0107 Z (2013) Hybrid learning: Interface generation through static, dynamic, and symbolic analysis. In: Symposium on software testing and analysis. Association for Computing Machinery, ISSTA, pp 268\u2013279. https:\/\/doi.org\/10.1145\/2483760.2483783","DOI":"10.1145\/2483760.2483783"},{"key":"433_CR31","doi-asserted-by":"publisher","unstructured":"Howar F, Jonsson B, Vaandrager F (2019) Combining black-box and white-box techniques for learning register automata. In: Steffen B, Woeginger G (eds) Computing and software science: state of the art and perspectives. Springer, pp 563\u2013588. https:\/\/doi.org\/10.1007\/978-3-319-91908-9_26","DOI":"10.1007\/978-3-319-91908-9_26"},{"key":"433_CR32","doi-asserted-by":"publisher","unstructured":"Isberner M, Howar F, Steffen B (2014) The TTT algorithm: A redundancy-free approach to active automata learning. In: Bonakdarpour B, Smolka SA (eds) Runtime verification. Springer, pp 307\u2013322. https:\/\/doi.org\/10.1007\/978-3-319-11164-3_26","DOI":"10.1007\/978-3-319-11164-3_26"},{"key":"433_CR33","unstructured":"Jeppu NY (2020) Trace2Model Github repository. https:\/\/github.com\/natasha-jeppu\/Trace2Model"},{"key":"433_CR34","unstructured":"Jeppu NY (2021) ActiveLearning. https:\/\/github.com\/natasha-jeppu\/ActiveLearning"},{"key":"433_CR35","doi-asserted-by":"publisher","unstructured":"Jeppu NY (2023). Active learning implementation. https:\/\/doi.org\/10.5287\/ora-aownkwvym","DOI":"10.5287\/ora-aownkwvym"},{"key":"433_CR36","doi-asserted-by":"publisher","unstructured":"Jeppu NY, Melham T, Kroening D, et\u00a0al (2020) Learning concise models from long execution traces. In: 57th ACM\/IEEE design automation conference (DAC), pp 1\u20136. https:\/\/doi.org\/10.1109\/DAC18072.2020.9218613","DOI":"10.1109\/DAC18072.2020.9218613"},{"key":"433_CR37","doi-asserted-by":"crossref","unstructured":"Kearns MJ, Vazirani UV (1994) An introduction to computational learning theory. MIT Press","DOI":"10.7551\/mitpress\/3897.001.0001"},{"key":"433_CR38","doi-asserted-by":"publisher","unstructured":"King JC (1976) Symbolic execution and program testing. In: Commun. ACM, vol\u00a019. Association for Computing Machinery, pp 385\u2013394. https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"433_CR39","doi-asserted-by":"publisher","unstructured":"Kroening D, Clarke E (2004) Checking consistency of C and Verilog using predicate abstraction and induction. pp 66\u201372. https:\/\/doi.org\/10.1109\/ICCAD.2004.1382544","DOI":"10.1109\/ICCAD.2004.1382544"},{"key":"433_CR40","doi-asserted-by":"publisher","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: Honavar V, Slutzki G (eds) Grammatical inference. Springer, pp 1\u201312. https:\/\/doi.org\/10.1007\/BFb0054059","DOI":"10.1007\/BFb0054059"},{"key":"433_CR41","doi-asserted-by":"publisher","unstructured":"Lorenzoli D, Mariani L, Pezz\u00e8 M (2008) Automatic generation of software behavioral models. In: ACM\/IEEE 30th international conference on software engineering, pp 501\u2013510. https:\/\/doi.org\/10.1145\/1368088.1368157","DOI":"10.1145\/1368088.1368157"},{"key":"433_CR42","doi-asserted-by":"publisher","unstructured":"Maler O, Mens I (2014a) Learning regular languages over large ordered alphabets. In: Logical methods in computer science. https:\/\/doi.org\/10.2168\/LMCS-11(3:13)2015","DOI":"10.2168\/LMCS-11(3:13)2015"},{"key":"433_CR43","doi-asserted-by":"publisher","unstructured":"Maler O, Mens IE (2014b) Learning regular languages over large alphabets. In: \u00c1brah\u00e1m E, Havelund K (eds) Tools and algorithms for the construction and analysis of systems. Springer, pp 485\u2013499. https:\/\/doi.org\/10.1007\/978-3-642-54862-8_41","DOI":"10.1007\/978-3-642-54862-8_41"},{"key":"433_CR44","doi-asserted-by":"publisher","unstructured":"Marques-Silva J, Glass T (1999) Combinational equivalence checking using satisfiability and recursive learning. In: Design, automation and test in Europe, pp 145\u2013149. https:\/\/doi.org\/10.1109\/DATE.1999.761110","DOI":"10.1109\/DATE.1999.761110"},{"key":"433_CR45","doi-asserted-by":"publisher","unstructured":"Marquez CIC, Strum M, Chau WJ (2013) Formal equivalence checking between high-level and RTL hardware designs. In: Latin American test workshop (LATW), pp 1\u20136. https:\/\/doi.org\/10.1109\/LATW.2013.6562666","DOI":"10.1109\/LATW.2013.6562666"},{"key":"433_CR46","doi-asserted-by":"publisher","unstructured":"Mukherjee R, Kroening D, Melham T, et\u00a0al (2015) Equivalence checking using trace partitioning. In: VLSI, pp 13\u201318. https:\/\/doi.org\/10.1109\/ISVLSI.2015.110","DOI":"10.1109\/ISVLSI.2015.110"},{"key":"433_CR47","doi-asserted-by":"publisher","unstructured":"Park DMR (1981) Concurrency and automata on infinite sequences. In: Theoretical computer science, lecture notes in computer science, vol 104. Springer, pp 167\u2013183. https:\/\/doi.org\/10.1007\/BFb0017309","DOI":"10.1007\/BFb0017309"},{"key":"433_CR48","doi-asserted-by":"publisher","unstructured":"Peled D, Vardi M, Yannakakis M (2002) Black box checking. In: Journal of automata, languages and combinatorics, pp 225\u2013246. https:\/\/doi.org\/10.1007\/978-0-387-35578-8_13","DOI":"10.1007\/978-0-387-35578-8_13"},{"key":"433_CR49","doi-asserted-by":"publisher","unstructured":"Rivest RL, Schapire RE (1989) Inference of finite automata using homing sequences. In: Theory of computing. Association for Computing Machinery, STOC \u201989, pp 411\u2013420. https:\/\/doi.org\/10.1145\/73007.73047","DOI":"10.1145\/73007.73047"},{"key":"433_CR50","doi-asserted-by":"publisher","unstructured":"Ruf J, Hoffmann D, Kropf T, et\u00a0al (2001) Simulation-guided property checking based on multi-valued AR-automata. In: Design, automation and test in Europe. IEEE, pp 742\u2013748. https:\/\/doi.org\/10.1109\/DATE.2001.915111","DOI":"10.1109\/DATE.2001.915111"},{"key":"433_CR51","doi-asserted-by":"publisher","unstructured":"Shahbaz M, Groz R (2009) Inferring Mealy machines. In: Cavalcanti A, Dams DR (eds) Formal methods. Springer, pp 207\u2013222. https:\/\/doi.org\/10.1007\/978-3-642-05089-3_14","DOI":"10.1007\/978-3-642-05089-3_14"},{"key":"433_CR52","doi-asserted-by":"publisher","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Hunt WA, Johnson SD (eds) Formal methods in computer-aided design. Springer, pp 127\u2013144. https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"433_CR53","unstructured":"Simulink (2021) Embedded Coder. https:\/\/uk.mathworks.com\/products\/embedded-coder.html"},{"key":"433_CR54","unstructured":"Simulink (2021a) Simulation and Model-Based Design. https:\/\/www.mathworks.com\/products\/simulink.html"},{"key":"433_CR55","unstructured":"Simulink (2021b) Stateflow Examples. https:\/\/uk.mathworks.com\/help\/stateflow\/examples.html?s_tid=CRUX_topnav"},{"key":"433_CR56","unstructured":"Smetsers R, Moerman J, Janssen M, et\u00a0al (2016) Complementing model learning with mutation-based fuzzing. arXiv:1611.02429"},{"key":"433_CR57","doi-asserted-by":"publisher","unstructured":"Steffen B, Hungar H (2003) Behavior-based model construction. In: Zuck LD, Attie PC, Cortesi A, et\u00a0al (eds) Verification, model checking, and abstract interpretation. Springer, pp 5\u201319. https:\/\/doi.org\/10.1007\/s10009-004-0139-8","DOI":"10.1007\/s10009-004-0139-8"},{"key":"433_CR58","doi-asserted-by":"publisher","unstructured":"Ulyantsev V, Tsarev F (2011) Extended finite-state machine induction using SAT-solver. In: International conference on machine learning and applications and workshops, pp 346\u2013349. https:\/\/doi.org\/10.1109\/ICMLA.2011.166","DOI":"10.1109\/ICMLA.2011.166"},{"key":"433_CR59","doi-asserted-by":"publisher","unstructured":"Ulyantsev V, Buzhinsky I, Shalyto A (2018) Exact finite-state machine identification from scenarios and temporal properties. In: International journal on software tools for technology transfer. https:\/\/doi.org\/10.1007\/s10009-016-0442-1","DOI":"10.1007\/s10009-016-0442-1"},{"key":"433_CR60","doi-asserted-by":"publisher","unstructured":"Vaandrager F, Bloem R, Ebrahimi M (2021) Learning Mealy machines with one timer. In: Leporati A, Mart\u00edn-Vide C, Shapira D, et\u00a0al (eds) Language and automata theory and applications. Springer, pp 157\u2013170. https:\/\/doi.org\/10.1007\/978-3-030-68195-1_13","DOI":"10.1007\/978-3-030-68195-1_13"},{"key":"433_CR61","doi-asserted-by":"publisher","unstructured":"van Eijk CAJ (2000) Sequential equivalence checking based on structural similarities. In: IEEE Transactions on computer-aided design of integrated circuits and systems, pp 814\u2013819. https:\/\/doi.org\/10.1109\/43.851997","DOI":"10.1109\/43.851997"},{"key":"433_CR62","doi-asserted-by":"publisher","unstructured":"Walkinshaw N, Bogdanov K (2008) Inferring finite-state models with temporal constraints. In: Automated software engineering, pp 248\u2013257. https:\/\/doi.org\/10.1109\/ASE.2008.35","DOI":"10.1109\/ASE.2008.35"},{"key":"433_CR63","doi-asserted-by":"publisher","unstructured":"Walkinshaw N, Hall M (2016) Inferring computational state machine models from program executions. In: International conference on software maintenance and evolution (ICSME). IEEE, pp 122\u2013132. https:\/\/doi.org\/10.1109\/ICSME.2016.74","DOI":"10.1109\/ICSME.2016.74"},{"key":"433_CR64","doi-asserted-by":"publisher","unstructured":"Walkinshaw N, Derrick J, Guo Q (2009) Iterative refinement of reverse-engineered models by model-based testing. In: Cavalcanti A, Dams DR (eds) Formal methods. Springer, pp 305\u2013320. https:\/\/doi.org\/10.1007\/978-3-642-05089-3_20","DOI":"10.1007\/978-3-642-05089-3_20"},{"key":"433_CR65","doi-asserted-by":"publisher","unstructured":"Walkinshaw N, Taylor R, Derrick J (2016) Inferring extended finite state machine models from software executions. In: Empirical software engineering, pp 811\u2013853. https:\/\/doi.org\/10.1007\/s10664-015-9367-7","DOI":"10.1007\/s10664-015-9367-7"},{"key":"433_CR66","unstructured":"Zalewski M (2013) American Fuzzy Lop (AFL) fuzzer. https:\/\/lcamtuf.coredump.cx\/afl\/"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00433-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00433-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00433-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,4]],"date-time":"2024-03-04T13:21:26Z","timestamp":1709558486000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00433-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":66,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["433"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00433-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12]]},"assertion":[{"value":"1 April 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 June 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 August 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}