{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:07:11Z","timestamp":1784844431155,"version":"3.55.0"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,2,16]],"date-time":"2017-02-16T00:00:00Z","timestamp":1487203200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,2,16]],"date-time":"2017-02-16T00:00:00Z","timestamp":1487203200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["306484"],"award-info":[{"award-number":["306484"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["200020_159949"],"award-info":[{"award-number":["200020_159949"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["CNS 1228768"],"award-info":[{"award-number":["CNS 1228768"]}],"id":[{"id":"10.13039\/100000083","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":[[2019,12]]},"DOI":"10.1007\/s10703-017-0270-2","type":"journal-article","created":{"date-parts":[[2017,2,16]],"date-time":"2017-02-16T13:10:46Z","timestamp":1487250646000},"page":"73-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Refutation-based synthesis in SMT"],"prefix":"10.1007","volume":"55","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Morgan","family":"Deters","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,2,16]]},"reference":[{"key":"270_CR1","doi-asserted-by":"crossref","unstructured":"Aloul FA, Ramani A, Markov IL, Sakallah KA (2002) Solving difficult sat instances in the presence of symmetry. In: Proceedings of the 39th annual design automation conference. ACM, pp 731\u2013736","DOI":"10.1109\/DAC.2002.1012719"},{"key":"270_CR2","unstructured":"Alur R, Bodik R, Dallal E, Fisman D, Garg P, Juniwal G, Kress-Gazit H, Madhusudan P, Martin MMK, Raghothaman M, Saha S, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2014) Syntax-guided synthesis. In: Marktoberdrof NATO proceedings (to appear). http:\/\/sygus.seas.upenn.edu\/files\/sygus_extended.pdf , retrieved 2015-02-06"},{"key":"270_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Bod\u00edk R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: FMCAD. IEEE, pp 1\u201317","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"270_CR4","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-319-13338-6_7","volume-title":"Hardware and Software: Verification and Testing","author":"Rajeev Alur","year":"2014","unstructured":"Alur R, Martin MMK, Raghothaman M, Stergiou C, Tripakis S, Udupa A (2014) Synthesizing finite-state protocols from scenarios and requirements. In: Yahav E (ed) Haifa verification conference, LNCS, vol 8855, pp 75\u201391. Springer. doi: 10.1007\/978-3-319-13338-6_7"},{"key":"270_CR5","doi-asserted-by":"crossref","unstructured":"Barrett C, Conway C, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: Proceedings of CAV\u201911, LNCS, vol 6806. Springer, pp 171\u2013177","DOI":"10.1007\/978-3-642-22110-1_14"},{"issue":"3","key":"270_CR6","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10817-012-9246-5","volume":"50","author":"C Barrett","year":"2013","unstructured":"Barrett C, Deters M, de Moura LM, Oliveras A, Stump A (2013) 6 years of SMT-COMP. JAR 50(3):243\u2013277. doi: 10.1007\/s10817-012-9246-5","journal-title":"JAR"},{"key":"270_CR7","first-page":"21","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett C, Shikanian I, Tinelli C (2007) An abstract decision procedure for satisfiability in the theory of inductive data types. J Satisf Boolean Model Comput 3:21\u201346","journal-title":"J Satisf Boolean Model Comput"},{"key":"270_CR8","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-14203-1_27","volume-title":"Automated Reasoning","author":"Nikolaj Bj\u00f8rner","year":"2010","unstructured":"Bj\u00f8rner N (2010) Linear quantifier elimination as an abstract decision procedure. In: Giesl J, H\u00e4hnle R (eds) IJCAR, LNCS, vol 6173, pp 316\u2013330. Springer. doi: 10.1007\/978-3-642-14203-1_27"},{"issue":"3","key":"270_CR9","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem R, Jobstmann B, Piterman N, Pnueli A, Sa\u2019ar Y (2012) Synthesis of reactive(1) designs. J Comput Syst Sci 78(3):911\u2013938. doi: 10.1016\/j.jcss.2011.08.007","journal-title":"J Comput Syst Sci"},{"key":"270_CR10","volume-title":"Implementing mathematics with the Nuprl proof development system","author":"RL Constable","year":"1986","unstructured":"Constable RL, Allen SF, Bromley M, Cleaveland R, Cremer JF, Harper RW, Howe DJ, Knoblock TB, Mendler NP, Panangaden P, Sasaki JT, Smith SF (1986) Implementing mathematics with the Nuprl proof development system. Prentice Hall, Englewood Cliffs"},{"key":"270_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Lecture Notes in Computer Science","author":"Patrick Cousot","year":"2005","unstructured":"Cousot P (2005) Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot R (ed) VMCAI, LNCS, vol 3385. Springer, pp 1\u201324. doi: 10.1007\/978-3-540-30579-8_1"},{"key":"270_CR12","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe D, Fontaine P, Merz S, Paleo BW (2011) Exploiting symmetry in SMT problems. In: Automated deduction\u2014CADE-23. Springer, pp 222\u2013236","DOI":"10.1007\/978-3-642-22438-6_18"},{"key":"270_CR13","unstructured":"Detlefs D, Nelson G, Saxe, JB (2003) Simplify: a theorem prover for program checking. Technical report. J ACM"},{"key":"270_CR14","unstructured":"Dutertre B (2015) Solving exists\/forall problems with yices. In: Workshop on satisfiability modulo theories"},{"issue":"5\u20136","key":"270_CR15","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner B, Schewe S (2013) Bounded synthesis. STTT 15(5\u20136):519\u2013539. doi: 10.1007\/s10009-012-0228-z","journal-title":"STTT"},{"key":"270_CR16","doi-asserted-by":"publisher","unstructured":"Ge Y, Barrett C, Tinelli C (2007) Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning F (ed) CADE, LNCS, vol 4603. Springer, pp 167\u2013182. doi: 10.1007\/978-3-540-73595-3_12","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"270_CR17","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Yeting Ge","year":"2009","unstructured":"Ge Y, de\u00a0Moura L (2009) Complete instantiation for quantified formulas in satisfiability modulo theories. In: Proceedings of CAV\u201909, LNCS, vol 5643. Springer, pp 306\u2013320. doi: 10.1007\/978-3-642-02658-4_25"},{"key":"270_CR18","first-page":"219","volume-title":"IJCAI","author":"CC Green","year":"1969","unstructured":"Green CC (1969) Application of theorem proving to problem solving. In: Walker DE, Norton LM (eds) IJCAI. William Kaufmann, Los Altos, pp 219\u2013240"},{"key":"270_CR19","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-18275-4_20","volume-title":"Verification, model checking, and abstract interpretation","author":"S Jacobs","year":"2011","unstructured":"Jacobs S, Kuncak V (2011) Towards complete reasoning about axiomatic specifications. Verification, model checking, and abstract interpretation. Springer, Berlin, pp 278\u2013293"},{"key":"270_CR20","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"Mikol\u00e1\u0161 Janota","year":"2012","unstructured":"Janota M, Klieber W, Marques-Silva J, Clarke E (2012) Solving QBF with counterexample guided refinement. In: International conference on theory and applications of satisfiability testing. Springer Berlin, pp 114\u2013128 (2012)"},{"key":"270_CR21","doi-asserted-by":"crossref","unstructured":"Janota M, Silva JPM (2011) Abstraction-based algorithm for 2qbf. In: Theory and applications of satisfiability testing\u2014SAT 2011\u201414th international conference, SAT 2011, Proceedings, pp 230\u2013244, Ann Arbor, MI, USA, 19\u201322 June 2011","DOI":"10.1007\/978-3-642-21581-0_19"},{"key":"270_CR22","doi-asserted-by":"publisher","unstructured":"Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Kramer J, Bishop J, Devanbu PT, Uchitel S (eds) ICSE. ACM, pp 215\u2013224. doi: 10.1145\/1806799.1806833","DOI":"10.1145\/1806799.1806833"},{"key":"270_CR23","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-21668-3_13","volume-title":"Computer Aided Verification","author":"Etienne Kneuss","year":"2015","unstructured":"Kneuss E, Koukoutos M, Kuncak V (2015) Deductive program repair. In: Kroening D, Pasareanu CS (eds) CAV, LNCS, vol 9207. Springer, pp 217\u2013233. doi: 10.1007\/978-3-319-21668-3_13"},{"key":"270_CR24","doi-asserted-by":"publisher","unstructured":"Kneuss E, Kuraj I, Kuncak V, Suter P (2013) Synthesis modulo recursive functions. In: Hosking AL, Eugster PT, Lopes CV(eds) OOPSLA. ACM, pp 407\u2013426. doi: 10.1145\/2509136.2509555","DOI":"10.1145\/2509136.2509555"},{"key":"270_CR25","doi-asserted-by":"crossref","unstructured":"Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Computer aided verification. Springer","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"270_CR26","doi-asserted-by":"publisher","unstructured":"Kuncak V, Mayer M, Piskac R, Suter P (2010)Complete functional synthesis. In: Zorn BG, Aiken A (eds) PLDI, pp 316\u2013329. ACM. doi: 10.1145\/1806596.1806632","DOI":"10.1145\/1806596.1806632"},{"issue":"2","key":"270_CR27","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/2076450.2076472","volume":"55","author":"V Kuncak","year":"2012","unstructured":"Kuncak V, Mayer M, Piskac R, Suter P (2012) Software synthesis procedures. CACM 55(2):103\u2013111. doi: 10.1145\/2076450.2076472","journal-title":"CACM"},{"issue":"5\u20136","key":"270_CR28","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s10009-011-0217-7","volume":"15","author":"V Kuncak","year":"2013","unstructured":"Kuncak V, Mayer M, Piskac R, Suter P (2013) Functional synthesis for linear arithmetic and sets. STTT 15(5\u20136):455\u2013474. doi: 10.1007\/s10009-011-0217-7","journal-title":"STTT"},{"key":"270_CR29","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/978-3-319-08867-9_51","volume-title":"Computer Aided Verification","author":"Ravichandhran Madhavan","year":"2014","unstructured":"Madhavan R, Kuncak V (2014) Symbolic resource bound inference for functional programs. In: Biere A, Bloem R (eds) CAV, LNCS, vol 8559. Springer, pp 762\u2013778. doi: 10.1007\/978-3-319-08867-9_51"},{"issue":"1","key":"270_CR30","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna Z, Waldinger RJ (1980) A deductive approach to program synthesis. TOPLAS 2(1):90\u2013121. doi: 10.1145\/357084.357090","journal-title":"TOPLAS"},{"key":"270_CR31","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-14295-6_51","volume-title":"Computer Aided Verification","author":"David Monniaux","year":"2010","unstructured":"Monniaux D (2010) Quantifier elimination by lazy model enumeration. In: Touili T, Cook B, Jackson P (eds) CAV, LNCS, vol 6174. Springer, pp 585\u2013599. doi: 10.1007\/978-3-642-14295-6_51"},{"key":"270_CR32","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"Leonardo de Moura","year":"2007","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2007) Efficient e-matching for SMT solvers. In: F. Pfenning (ed) CADE, LNCS, vol 4603. Springer, pp 183\u2013198. doi: 10.1007\/978-3-540-73595-3_13"},{"issue":"6","key":"270_CR33","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"key":"270_CR34","doi-asserted-by":"publisher","unstructured":"Perelman D, Gulwani S, Grossman D, Provost P (2010) Test-driven synthesis. In: O\u2019Boyle MFP, Pingali K (eds) PLDI. ACM, p\u00a043. doi: 10.1145\/2594291.2594297","DOI":"10.1145\/2594291.2594297"},{"key":"270_CR35","doi-asserted-by":"publisher","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Conference record of the sixteenth annual ACM symposium on principles of programming languages, pp 179\u2013190, Austin, TX, USA, 11\u201313 Jan 1989. doi: 10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"270_CR36","unstructured":"Presburger M (1929) \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Aritmethik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier Congr\u00e8s des Math\u00e9maticiens des Pays slaves, Warsawa, pp 92\u2013101"},{"key":"270_CR37","unstructured":"Raghothaman M., Udupa A (2014) Language to specify syntax-guided synthesis problems. CoRR arXiv:1405.5590"},{"key":"270_CR38","doi-asserted-by":"crossref","unstructured":"Reynolds A, Deters M, Kuncak V, Tinelli C, Barrett CW (2015) Counterexample-guided quantifier instantiation for synthesis in SMT. In: Computer aided verification\u201427th international conference, CAV 2015, Proceedings, Part II, pp 198\u2013216, San Francisco, CA, USA, 18\u201324 July 2015","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"270_CR39","unstructured":"Reynolds A, King T, Kuncak V (2015) An instantiation-based approach for solving quantified linear arithmetic. CoRR arXiv:1510.02642"},{"key":"270_CR40","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-38574-2_26","volume-title":"Automated Deduction \u2013 CADE-24","author":"Andrew Reynolds","year":"2013","unstructured":"Reynolds A, Tinelli C, Goel A, Krsti\u0107 S, Deters M, Barrett C (2013) Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina MP (ed) Proceedings of the 24th international conference on automated deduction, Lake Placid, NY, USA, Lecture notes in computer science, vol 7898. Springer, pp 377\u2013391"},{"key":"270_CR41","doi-asserted-by":"crossref","unstructured":"Reynolds A, Tinelli C, Moura LD (2014) Finding conflicting instances of quantified formulas in SMT. In: Formal methods in computer-aided design (FMCAD)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"270_CR42","unstructured":"Ryzhyk L, Walker A, Keys J, Legg A, Raghunath A, Stumm M, Vij M (2014) User-guided device driver synthesis. In: Flinn J, Levy H (eds) OSDI. USENIX Association, pp 661\u2013676"},{"key":"270_CR43","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-319-21690-4_26","volume-title":"Computer Aided Verification","author":"Shambwaditya Saha","year":"2015","unstructured":"Saha S, Garg P, Madhusudan P (2015) Alchemist: learning guarded affine functions. In: Kroening D, Psreanu CS (eds) Computer aided verification, Lecture notes in computer science, vol 9206, pp 440\u2013446. Springer. doi: 10.1007\/978-3-319-21690-4_26"},{"issue":"4","key":"270_CR44","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1145\/2499368.2451150","volume":"48","author":"E Schkufza","year":"2013","unstructured":"Schkufza E, Sharma R, Aiken A (2013) Stochastic superoptimization. SIGPLAN Not 48(4):305\u2013316. doi: 10.1145\/2499368.2451150","journal-title":"SIGPLAN Not"},{"issue":"5\u20136","key":"270_CR45","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama A (2013) Program sketching. STTT 15(5\u20136):475\u2013495. doi: 10.1007\/s10009-012-0249-7","journal-title":"STTT"},{"key":"270_CR46","doi-asserted-by":"publisher","unstructured":"Solar-Lezama A, Tancau L, Bod\u00edk R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: Shen JP, Martonosi M (eds) ASPLOS. ACM, pp 404\u2013415. doi: 10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"issue":"5\u20136","key":"270_CR47","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava S, Gulwani S, Foster JS (2013) Template-based program verification and program synthesis. STTT 15(5\u20136):497\u2013518. doi: 10.1007\/s10009-012-0223-4","journal-title":"STTT"},{"key":"270_CR48","doi-asserted-by":"crossref","unstructured":"Stump A, Sutcliffe G, Tinelli C (2014) Starexec: a cross-community infrastructure for logic solving. In: Proceedings of the 7th international joint conference on automated reasoning, Lecture notes in artificial intelligence. Springer","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"270_CR49","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-40447-4_2","volume-title":"Lecture Notes in Computer Science","author":"Josef Svenningsson","year":"2013","unstructured":"Svenningsson J, Axelsson E (2012) Combining deep and shallow embedding for EDSL. In: Trends in functional programming\u201413th international symposium, TFP 2012, Revised selected papers, pp 21\u201336, St. Andrews, UK, 12\u201314 June 2012. doi: 10.1007\/978-3-642-40447-4_2"},{"key":"270_CR50","doi-asserted-by":"crossref","unstructured":"Tiwari A, Gasc\u00f3n A, Dutertre B (2015) Program synthesis using dual interpretation. In: Automated deduction\u2014CADE-25\u201425th international conference on automated deduction, Proceedings, Berlin, Germany, 1\u20137 Aug 2015, pp 482\u2013497","DOI":"10.1007\/978-3-319-21401-6_33"},{"key":"270_CR51","doi-asserted-by":"publisher","unstructured":"Udupa A, Raghavan A, Deshmukh JV, Mador-Haim S, Martin MM, Alur R (2013) Transit: specifying protocols with concolic snippets. In: PLDI. ACM, pp 287\u2013296. doi: 10.1145\/2491956.2462174","DOI":"10.1145\/2491956.2462174"},{"key":"270_CR52","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Lecture Notes in Computer Science","author":"Martin Wildmoser","year":"2004","unstructured":"Wildmoser M, Nipkow T (2004) Certifying machine code safety: shallow versus deep embedding. In: Theorem proving in higher order logics, 17th international conference, TPHOLs 2004, Proceedings, pp 305\u2013320, Park City, UT, USA, 14\u201317 Sept 2004. doi: 10.1007\/978-3-540-30142-4_22"},{"issue":"1","key":"270_CR53","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"CM Wintersteiger","year":"2013","unstructured":"Wintersteiger CM, Hamadi Y, De Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42(1):3\u201323","journal-title":"Form Methods Syst Des"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0270-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0270-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0270-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,24]],"date-time":"2022-07-24T07:51:10Z","timestamp":1658649070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0270-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,16]]},"references-count":53,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["270"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0270-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,16]]},"assertion":[{"value":"16 February 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}