{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T13:59:09Z","timestamp":1760623149247,"version":"3.37.3"},"reference-count":92,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T00:00:00Z","timestamp":1575244800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T00:00:00Z","timestamp":1575244800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004189","name":"Max-Planck-Gesellschaft","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004189","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["W1255-N23"],"award-info":[{"award-number":["W1255-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2021,4]]},"DOI":"10.1007\/s00236-019-00357-3","type":"journal-article","created":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T16:42:29Z","timestamp":1575304949000},"page":"57-93","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A formal methods approach to predicting new features of the eukaryotic vesicle traffic system"],"prefix":"10.1007","volume":"58","author":[{"given":"Arnab","family":"Bhattacharyya","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1038-3602","authenticated-orcid":false,"given":"Ashutosh","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"Lakshmanan","family":"Kuppusamy","sequence":"additional","affiliation":[]},{"given":"Somya","family":"Mani","sequence":"additional","affiliation":[]},{"given":"Ankit","family":"Shukla","sequence":"additional","affiliation":[]},{"given":"Mandayam","family":"Srivas","sequence":"additional","affiliation":[]},{"given":"Mukund","family":"Thattai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,12,2]]},"reference":[{"key":"357_CR1","unstructured":"Alberts, B., Johnson, A., Lewis, J., Walter, P., Raff, M., Roberts, K.: Molecular biology of the cell 4th edition: international student edition. Routledge (2002). https:\/\/books.google.at\/books?id=ozigkQEACAAJ"},{"key":"357_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: 2013 Formal Methods in Computer-Aided Design, IEEE, pp. 1\u20138 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"issue":"8","key":"357_CR3","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1038\/nrm.2016.65","volume":"17","author":"RW Baker","year":"2016","unstructured":"Baker, R.W., Hughson, F.M.: Chaperoning snare assembly and disassembly. Nat. Rev. Mol. Cell Biol. 17(8), 465 (2016)","journal-title":"Nat. Rev. Mol. Cell Biol."},{"key":"357_CR4","doi-asserted-by":"crossref","unstructured":"Barlow, L., Dacks, J.: Seeing the endomembrane system for the trees: evolutionary analysis highlights the importance of plants as models for eukaryotic membrane-trafficking. In: Seminars in cell & developmental biology. Elsevier (2017)","DOI":"10.1016\/j.semcdb.2017.09.027"},{"key":"357_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"357_CR6","first-page":"133","volume":"5","author":"M Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: Qbf-based formal verification: experience and perspectives. J. Satisf. Boolean Model. Comput. 5, 133\u2013191 (2008)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"9","key":"357_CR7","doi-asserted-by":"crossref","first-page":"18670","DOI":"10.3390\/ijms140918670","volume":"14","author":"MG Bexiga","year":"2013","unstructured":"Bexiga, M.G., Simpson, J.C.: Human diseases associated with form and function of the golgi complex. Int. J. Mol. Sci. 14(9), 18670\u201318681 (2013)","journal-title":"Int. J. Mol. Sci."},{"key":"357_CR8","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 193\u2013207. Springer (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"357_CR9","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using sat procedures instead of bdds. In: Proceedings of the 36th Annual ACM\/IEEE Design Automation Conference, pp. 317\u2013320. ACM (1999)","DOI":"10.1145\/309847.309942"},{"key":"357_CR10","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"357_CR11","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS press, Amsterdam (2009)"},{"key":"357_CR12","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T.: Conflict-driven clause learning sat solvers. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pp. 131\u2013153 (2009)"},{"key":"357_CR13","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: International Conference on Computer Aided Verification, pp. 454\u2013464. Springer (2001)","DOI":"10.1007\/3-540-44585-4_44"},{"issue":"3","key":"357_CR14","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1016\/0092-8674(84)90458-6","volume":"39","author":"WA Braell","year":"1984","unstructured":"Braell, W.A., Balch, W.E., Dobbertin, D.C., Rothman, J.E.: The glycoprotein that is transported between successive compartments of the golgi in a cell-free system resides in stacks of cisternae. Cell 39(3), 511\u2013524 (1984)","journal-title":"Cell"},{"key":"357_CR15","first-page":"735","volume":"185","author":"HK B\u00fcning","year":"2009","unstructured":"B\u00fcning, H.K., Bubeck, U.: Theory of quantified boolean formulas. Handb. Satisf. 185, 735\u2013760 (2009)","journal-title":"Handb. Satisf."},{"issue":"1","key":"357_CR16","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1046\/j.1600-0854.2003.00151.x","volume":"5","author":"L Burri","year":"2004","unstructured":"Burri, L., Lithgow, T.: A complete set of snares in yeast. Traffic 5(1), 45\u201352 (2004)","journal-title":"Traffic"},{"key":"357_CR17","doi-asserted-by":"crossref","unstructured":"Cardelli, L., \u010ce\u0161ka, M., Fr\u00e4nzle, M., Kwiatkowska, M., Laurenti, L., Paoletti, N., Whitby, M.: Syntax-guided optimal synthesis for chemical reaction networks. In: International Conference on Computer Aided Verification, pp. 375\u2013395. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_20"},{"issue":"6","key":"357_CR18","doi-asserted-by":"crossref","first-page":"S6","DOI":"10.1186\/1471-2105-9-S6-S6","volume":"9","author":"G Chin","year":"2008","unstructured":"Chin, G., Chavarria, D.G., Nakamura, G.C., Sofia, H.J.: Biographe: high-performance bionetwork analysis using the biological graph environment. BMC Bioinf. 9(6), S6 (2008)","journal-title":"BMC Bioinf."},{"key":"357_CR19","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS, pp. 168\u2013176. Springer (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"issue":"22","key":"357_CR20","doi-asserted-by":"crossref","first-page":"3595","DOI":"10.1091\/mbc.e14-07-1240","volume":"25","author":"E Cocucci","year":"2014","unstructured":"Cocucci, E., Gaudin, R., Kirchhausen, T.: Dynamin recruitment and membrane scission at the neck of a clathrin-coated pit. Mol. Biol. Cell 25(22), 3595\u20133609 (2014)","journal-title":"Mol. Biol. Cell"},{"key":"357_CR21","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151\u2013158. ACM (1971)","DOI":"10.1145\/800157.805047"},{"key":"357_CR22","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bjorner, N.: Z3: An efficient smt solver. In: TACAS, LNCS, vol. 4963, pp. 337\u2013340. Springer Berlin Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"357_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Efficient e-matching for SMT solvers. In: Automated Deduction\u2014CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17\u201320, 2007, Proceedings, vol. 4603, pp. 183\u2013198. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"issue":"17","key":"357_CR24","doi-asserted-by":"crossref","first-page":"2977","DOI":"10.1242\/jcs.013250","volume":"120","author":"JB Dacks","year":"2007","unstructured":"Dacks, J.B., Field, M.C.: Evolution of the eukaryotic membrane-trafficking system: origin, tempo and mode. J. Cell Sci. 120(17), 2977\u20132985 (2007)","journal-title":"J. Cell Sci."},{"issue":"13","key":"357_CR25","doi-asserted-by":"crossref","first-page":"1597","DOI":"10.1007\/s00018-007-6557-5","volume":"64","author":"B Davletov","year":"2007","unstructured":"Davletov, B., Connell, E., Darios, F.: Regulation of snare fusion machinery by fatty acids. Cell. Mol. Life Sci. 64(13), 1597\u20131608 (2007)","journal-title":"Cell. Mol. Life Sci."},{"key":"357_CR26","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"357_CR27","first-page":"Jbc-M109","volume":"285","author":"J Di Giovanni","year":"2010","unstructured":"Di Giovanni, J., Iborra, C., Maulet, Y., L\u00e9v\u00eaque, C., El Far, O., Seagar, M.: Calcium-dependent regulation of snare-mediated membrane fusion by calmodulin. J. Biol. Chem. 285, Jbc-M109 (2010)","journal-title":"J. Biol. Chem."},{"issue":"6188","key":"357_CR28","doi-asserted-by":"crossref","first-page":"1156","DOI":"10.1126\/science.1248882","volume":"344","author":"SJ Dunn","year":"2014","unstructured":"Dunn, S.J., Martello, G., Yordanov, B., Emmott, S., Smith, A.: Defining an essential transcription factor program for naive pluripotency. Science 344(6188), 1156\u20131160 (2014)","journal-title":"Science"},{"issue":"6","key":"357_CR29","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.tcb.2013.01.005","volume":"23","author":"M Faini","year":"2013","unstructured":"Faini, M., Beck, R., Wieland, F.T., Briggs, J.A.: Vesicle coats: structure, function, and general principles of assembly. Trends Cell Biol. 23(6), 279\u2013288 (2013)","journal-title":"Trends Cell Biol."},{"key":"357_CR30","doi-asserted-by":"crossref","unstructured":"Fisher, J., K\u00f6ksal, A.S., Piterman, N., Woodhouse, S.: Synthesising executable gene regulatory networks from single-cell gene expression data. In: International Conference on Computer Aided Verification, pp. 544\u2013560. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_38"},{"issue":"3","key":"357_CR31","doi-asserted-by":"crossref","first-page":"697","DOI":"10.1083\/jcb.90.3.697","volume":"90","author":"E Fries","year":"1981","unstructured":"Fries, E., Rothman, J.E.: Transient activity of golgi-like membranes as donors of vesicular stomatitis viral glycoprotein in vitro. J. Cell Biol. 90(3), 697\u2013704 (1981)","journal-title":"J. Cell Biol."},{"key":"357_CR32","doi-asserted-by":"crossref","first-page":"4277","DOI":"10.1038\/srep04277","volume":"4","author":"N Furukawa","year":"2014","unstructured":"Furukawa, N., Mima, J.: Multiple and distinct strategies of yeast snares to confer the specificity of membrane fusion. Sci. Rep. 4, 4277 (2014)","journal-title":"Sci. Rep."},{"key":"357_CR33","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Guet, C.C., Gupta, A., Henzinger, T.A., Paixao, T., Petrov, T.: Model checking gene regulatory networks. In: TACAS (2015)","DOI":"10.1007\/978-3-662-46681-0_47"},{"issue":"9","key":"357_CR34","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1136\/jmg.2007.050294","volume":"44","author":"P Gissen","year":"2007","unstructured":"Gissen, P., Maher, E.R.: Cargos and genes: insights into vesicular transport from inherited human disease. J. Med. Genet. 44(9), 545\u2013555 (2007)","journal-title":"J. Med. Genet."},{"key":"357_CR35","unstructured":"Goldberg, E.I., Prasad, M.R., Brayton, R.K.: Using sat for combinational equivalence checking. In: Design, Automation and Test in Europe, 2001. Conference and Exhibition 2001. Proceedings, pp. 114\u2013121. IEEE (2001)"},{"key":"357_CR36","unstructured":"Gomes, C.P., Selman, B., McAloon, K., Tretkoff, C.: Randomization in backtrack search: exploiting heavy-tailed profiles for solving hard scheduling problems. In: AIPS, pp. 208\u2013213 (1998)"},{"issue":"12","key":"357_CR37","doi-asserted-by":"crossref","first-page":"1071","DOI":"10.1016\/j.ijpara.2012.09.009","volume":"42","author":"MJ Gubbels","year":"2012","unstructured":"Gubbels, M.J., Duraisingh, M.T.: Evolution of apicomplexan secretory organelles. Int. J. Parasitol. 42(12), 1071\u20131081 (2012)","journal-title":"Int. J. Parasitol."},{"key":"357_CR38","doi-asserted-by":"crossref","unstructured":"Guerra, J., Lynce, I.: Reasoning over biological networks using maximum satisfiability. In: PPCP, pp. 941\u2013956. Springer (2012)","DOI":"10.1007\/978-3-642-33558-7_67"},{"key":"357_CR39","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011, pp. 317\u2013330. ACM (2011)","DOI":"10.1145\/1925844.1926423"},{"key":"357_CR40","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-319-99429-1_6","volume-title":"Computational Methods in Systems Biology","author":"A Gupta","year":"2018","unstructured":"Gupta, A., Mani, S., Shukla, A.: Synthesis for vesicle traffic systems. In: \u010ce\u0161ka, M., \u0160afr\u00e1nek, D. (eds.) Computational Methods in Systems Biology, pp. 93\u2013110. Springer, Cham (2018)"},{"key":"357_CR41","unstructured":"Gupta, A., Shukla, A., Srivas, M., Thattai, M.: Smt solving for vesicle traffic systems in cells. In: SASB (2017)"},{"issue":"3","key":"357_CR42","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1194\/jlr.M800360-JLR200","volume":"50","author":"Y He","year":"2009","unstructured":"He, Y., Linder, M.E.: Differential palmitoylation of the endosomal snares syntaxin 7 and syntaxin 8. J. Lipid Res. 50(3), 398\u2013404 (2009)","journal-title":"J. Lipid Res."},{"key":"357_CR43","doi-asserted-by":"crossref","unstructured":"Heule, M., Verwer, S.: Exact dfa identification using sat solvers. Grammatical inference: theoretical results and applications pp. 66\u201379 (2010)","DOI":"10.1007\/978-3-642-15488-1_7"},{"issue":"12","key":"357_CR44","doi-asserted-by":"crossref","first-page":"5593","DOI":"10.1091\/mbc.e04-06-0468","volume":"15","author":"J Hirst","year":"2004","unstructured":"Hirst, J., Miller, S.E., Taylor, M.J., von Mollard, G.F., Robinson, M.S.: Epsinr is an adaptor for the snare protein vti1b. Mol. Biol. Cell 15(12), 5593\u20135602 (2004)","journal-title":"Mol. Biol. Cell"},{"key":"357_CR45","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/S0091-679X(08)00802-9","volume":"90","author":"BP Jena","year":"2008","unstructured":"Jena, B.P.: Intracellular organelle dynamics at nm resolution. Methods Cell Biol. 90, 19\u201337 (2008)","journal-title":"Methods Cell Biol."},{"issue":"3","key":"357_CR46","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.entcs.2006.12.022","volume":"174","author":"T Jussila","year":"2007","unstructured":"Jussila, T., Biere, A.: Compressing bmc encodings with qbf. Electron. Notes Theor. Comput. Sci. 174(3), 45\u201356 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"23","key":"357_CR47","doi-asserted-by":"crossref","first-page":"3872","DOI":"10.1016\/j.febslet.2009.10.066","volume":"583","author":"RA Kahn","year":"2009","unstructured":"Kahn, R.A.: Toward a model for arf gtpases as regulators of traffic at the golgi. FEBS Lett. 583(23), 3872\u20133879 (2009)","journal-title":"FEBS Lett."},{"key":"357_CR48","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: Proceedings of the National Conference on Artificial Intelligence, pp. 1194\u20131201 (1996)"},{"key":"357_CR49","doi-asserted-by":"publisher","unstructured":"Koksal, A.S., Pu, Y., Srivastava, S., Bodik, R., Fisher, J., Piterman, N.: Synthesis of biological models from mutation experiments. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, pp. 469\u2013482. ACM, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2429069.2429125","DOI":"10.1145\/2429069.2429125"},{"key":"357_CR50","volume-title":"Molecular Cell Biology","author":"H Lodish","year":"2008","unstructured":"Lodish, H., Darnell, J.E., Berk, A., Kaiser, C.A., Krieger, M., Scott, M.P., Bretscher, A., Ploegh, H., Matsudaira, P., et al.: Molecular Cell Biology. Macmillan, Basingtoke (2008)"},{"key":"357_CR51","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. J. Satisf. Boolean Model. Comput. 7, 71\u201376 (2010)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"2","key":"357_CR52","doi-asserted-by":"crossref","first-page":"e8906","DOI":"10.1371\/journal.pone.0008906","volume":"5","author":"K Mangla","year":"2010","unstructured":"Mangla, K., Dill, D.L., Horowitz, M.A.: Timing robustness in the budding and fission yeast cell cycles. PLoS One 5(2), e8906 (2010)","journal-title":"PLoS One"},{"key":"357_CR53","doi-asserted-by":"crossref","first-page":"e16,231","DOI":"10.7554\/eLife.16231","volume":"5","author":"S Mani","year":"2016","unstructured":"Mani, S., Thattai, M.: Stacking the odds for golgi cisternal maturation. Elife 5, e16,231 (2016)","journal-title":"Elife"},{"issue":"6801","key":"357_CR54","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1038\/35025000","volume":"407","author":"JA McNew","year":"2000","unstructured":"McNew, J.A., Parlati, F., Fukuda, R., Johnston, R.J., Paz, K., Paumet, F., S\u00f6llner, T.H., Rothman, J.E.: Compartmental specificity of cellular membrane fusion encoded in snare proteins. Nature 407(6801), 153 (2000)","journal-title":"Nature"},{"issue":"15","key":"357_CR55","doi-asserted-by":"crossref","first-page":"2031","DOI":"10.1038\/emboj.2008.139","volume":"27","author":"J Mima","year":"2008","unstructured":"Mima, J., Hickey, C.M., Xu, H., Jun, Y., Wickner, W.: Reconstituted membrane fusion requires regulatory lipids, snares and synergistic snare chaperones. EMBO J. 27(15), 2031\u20132042 (2008)","journal-title":"EMBO J."},{"issue":"4","key":"357_CR56","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1016\/j.chembiol.2013.03.009","volume":"20","author":"K Mishev","year":"2013","unstructured":"Mishev, K., Dejonghe, W., Russinova, E.: Small molecules for dissecting endomembrane trafficking: a cross-systems view. Chem. Biol. 20(4), 475\u2013486 (2013)","journal-title":"Chem. Biol."},{"issue":"1\u20132","key":"357_CR57","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1080\/21541248.2016.1276999","volume":"9","author":"MP M\u00fcller","year":"2018","unstructured":"M\u00fcller, M.P., Goody, R.S.: Molecular control of rab activity by gefs, gaps and gdi. Small GTPases 9(1\u20132), 5\u201321 (2018)","journal-title":"Small GTPases"},{"issue":"6","key":"357_CR58","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1038\/ncb0604-469","volume":"6","author":"S Munro","year":"2004","unstructured":"Munro, S.: Organelle identity and the organization of membrane traffic. Nat. Cell Biol. 6(6), 469\u2013472 (2004)","journal-title":"Nat. Cell Biol."},{"key":"357_CR59","doi-asserted-by":"crossref","first-page":"jbc-M114","DOI":"10.1074\/jbc.M114.548297","volume":"289","author":"K Nakatsukasa","year":"2014","unstructured":"Nakatsukasa, K., Kanada, A., Matsuzaki, M., Byrne, S.D., Okumura, F., Kamura, T.: The nutrient stress-induced small gtpase rab5 contributes to the activation of vesicle trafficking and vacuolar activity. J. Biol. Chem. 289, jbc-M114 (2014)","journal-title":"J. Biol. Chem."},{"key":"357_CR60","doi-asserted-by":"crossref","unstructured":"Nickel, W., Rabouille, C.: Unconventional protein secretion: Diversity and consensus. In: Seminars in cell & developmental biology. Elsevier (2018)","DOI":"10.1016\/j.semcdb.2018.03.007"},{"issue":"6","key":"357_CR61","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving sat and sat modulo theories: from an abstract davis-putnam-logemann-loveland procedure to dpll (t). J. ACM (JACM) 53(6), 937\u2013977 (2006)","journal-title":"J. ACM (JACM)"},{"issue":"7","key":"357_CR62","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1016\/j.tcb.2015.02.005","volume":"25","author":"JE Paczkowski","year":"2015","unstructured":"Paczkowski, J.E., Richardson, B.C., Fromme, J.C.: Cargo adaptors: structures illuminate mechanisms regulating vesicle biogenesis. Trends Cell Biol. 25(7), 408\u2013416 (2015)","journal-title":"Trends Cell Biol."},{"key":"357_CR63","doi-asserted-by":"crossref","unstructured":"Paoletti, N., Yordanov, B., Hamadi, Y., Wintersteiger, C.M., Kugler, H.: Analyzing and synthesizing genomic logic functions. In: International Conference on Computer Aided Verification, pp. 343\u2013357. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_23"},{"issue":"2","key":"357_CR64","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/s00018-003-3353-8","volume":"61","author":"R Polishchuk","year":"2004","unstructured":"Polishchuk, R., Mironov, A.: Structural aspects of golgi function. Cell. Mol. Life Sci. CMLS 61(2), 146\u2013158 (2004)","journal-title":"Cell. Mol. Life Sci. CMLS"},{"issue":"21","key":"357_CR65","doi-asserted-by":"crossref","first-page":"3971","DOI":"10.1242\/jcs.185702","volume":"129","author":"C Progida","year":"2016","unstructured":"Progida, C., Bakke, O.: Bidirectional traffic between the golgi and the endosomes-machineries and regulation. J. Cell Sci. 129(21), 3971\u20133982 (2016)","journal-title":"J. Cell Sci."},{"key":"357_CR66","unstructured":"Qbflib.org: QDIMACS standard ver. 1.1. (2018). http:\/\/www.qbflib.org\/qdimacs.html"},{"issue":"25","key":"357_CR67","doi-asserted-by":"crossref","first-page":"4532","DOI":"10.1091\/mbc.E14-10-1433","volume":"26","author":"E Richardson","year":"2015","unstructured":"Richardson, E., Zerr, K., Tsaousis, A., Dorrell, R.G., Dacks, J.B.: Evolutionary cell biology: functional insight from \u201cendless forms most beautiful\u201d. Mol. Biol. Cell 26(25), 4532\u20134538 (2015)","journal-title":"Mol. Biol. Cell"},{"issue":"5","key":"357_CR68","doi-asserted-by":"crossref","first-page":"735","DOI":"10.1016\/j.cell.2005.06.043","volume":"122","author":"J Rink","year":"2005","unstructured":"Rink, J., Ghigo, E., Kalaidzidis, Y., Zerial, M.: Rab conversion as a mechanism of progression from early to late endosomes. Cell 122(5), 735\u2013749 (2005)","journal-title":"Cell"},{"issue":"5","key":"357_CR69","doi-asserted-by":"crossref","first-page":"281","DOI":"10.2307\/2303897","volume":"46","author":"HE Robbins","year":"1939","unstructured":"Robbins, H.E.: A theorem on graphs, with an application to a problem of traffic control. Am. Math. Mon. 46(5), 281\u2013283 (1939)","journal-title":"Am. Math. Mon."},{"key":"357_CR70","doi-asserted-by":"crossref","unstructured":"Rosenblueth, D.A., Mu\u00f1oz, S., Carrillo, M., Azpeitia, E.: Inference of boolean networks from gene interaction graphs using a sat solver. In: ICACB, pp. 235\u2013246. Springer (2014)","DOI":"10.1007\/978-3-319-07953-0_19"},{"issue":"10","key":"357_CR71","doi-asserted-by":"crossref","first-page":"1059","DOI":"10.1038\/nm770","volume":"8","author":"JE Rothman","year":"2002","unstructured":"Rothman, J.E.: The machinery and principles of vesicle transport in the cell. Nat. Med. 8(10), 1059\u20131063 (2002)","journal-title":"Nat. Med."},{"issue":"2","key":"357_CR72","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"WJ Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177\u2013192 (1970)","journal-title":"J. Comput. Syst. Sci."},{"key":"357_CR73","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.biosystems.2016.03.012","volume":"146","author":"Y Shavit","year":"2016","unstructured":"Shavit, Y., Yordanov, B., Dunn, S.J., Wintersteiger, C.M., Otani, T., Hamadi, Y., Livesey, F.J., Kugler, H.: Automated synthesis and analysis of switching gene regulatory networks. Biosystems 146, 26\u201334 (2016)","journal-title":"Biosystems"},{"issue":"5","key":"357_CR74","doi-asserted-by":"crossref","first-page":"1160","DOI":"10.1016\/j.cell.2014.03.050","volume":"157","author":"H Shimizu","year":"2014","unstructured":"Shimizu, H., Woodcock, S.A., Wilkin, M.B., Trubenov\u00e1, B., Monk, N.A., Baron, M.: Compensatory flux changes within an endocytic trafficking network maintain thermal robustness of notch signaling. Cell 157(5), 1160\u20131174 (2014)","journal-title":"Cell"},{"issue":"7","key":"357_CR75","doi-asserted-by":"crossref","first-page":"e0180,692","DOI":"10.1371\/journal.pone.0180692","volume":"12","author":"A Shukla","year":"2017","unstructured":"Shukla, A., Bhattacharyya, A., Kuppusamy, L., Srivas, M., Thattai, M.: Discovering vesicle traffic network constraints by model checking. PloS one 12(7), e0180,692 (2017)","journal-title":"PloS one"},{"key":"357_CR76","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A.: The sketching approach to program synthesis. In: Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14\u201316, 2009. Proceedings, pp. 4\u201313. Springer (2009)","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"357_CR77","first-page":"28","volume":"2016","author":"M Soos","year":"2016","unstructured":"Soos, M.: The cryptominisat 5 set of solvers at sat competition 2016. SAT Compet. 2016, 28 (2016)","journal-title":"SAT Compet."},{"issue":"53","key":"357_CR78","first-page":"1","volume":"2005","author":"N Sorensson","year":"2005","unstructured":"Sorensson, N., Een, N.: Minisat v1. 13-a sat solver with conflict-clause minimization. SAT 2005(53), 1\u20132 (2005)","journal-title":"SAT"},{"issue":"8","key":"357_CR79","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1038\/nrm2728","volume":"10","author":"H Stenmark","year":"2009","unstructured":"Stenmark, H.: Rab gtpases as coordinators of vesicle traffic. Nat. Rev. Mol. Cell Biol. 10(8), 513\u2013525 (2009)","journal-title":"Nat. Rev. Mol. Cell Biol."},{"issue":"9","key":"357_CR80","doi-asserted-by":"crossref","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P Stephan","year":"1996","unstructured":"Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Combinational test generation using satisfiability. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 15(9), 1167\u20131176 (1996)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"357_CR81","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time (preliminary report). In: Proceedings of the Fifth Annual ACM Symposium on Theory of Computing, pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"issue":"7","key":"357_CR82","doi-asserted-by":"crossref","first-page":"1375","DOI":"10.1681\/ASN.2013080883","volume":"25","author":"EH Stoops","year":"2014","unstructured":"Stoops, E.H., Caplan, M.J.: Trafficking to the apical and basolateral membranes in polarized epithelial cells. J. Am. Soc. Nephrol. 25(7), 1375\u20131386 (2014)","journal-title":"J. Am. Soc. Nephrol."},{"issue":"6","key":"357_CR83","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1016\/j.tcb.2013.01.008","volume":"23","author":"D Tang","year":"2013","unstructured":"Tang, D., Wang, Y.: Cell cycle regulation of golgi membrane dynamics. Trends Cell Biol. 23(6), 296\u2013304 (2013)","journal-title":"Trends Cell Biol."},{"issue":"2","key":"357_CR84","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"MN Velev","year":"2003","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors. J. Symb. Comput. 35(2), 73\u2013106 (2003)","journal-title":"J. Symb. Comput."},{"issue":"6","key":"357_CR85","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1016\/S0092-8674(00)81404-X","volume":"92","author":"T Weber","year":"1998","unstructured":"Weber, T., Zemelman, B.V., McNew, J.A., Westermann, B., Gmachl, M., Parlati, F., S\u00f6llner, T.H., Rothman, J.E.: Snarepins: minimal machinery for membrane fusion. Cell 92(6), 759\u2013772 (1998)","journal-title":"Cell"},{"issue":"5","key":"357_CR86","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1111\/tra.12560","volume":"19","author":"U Weill","year":"2018","unstructured":"Weill, U., Arakel, E.C., Goldmann, O., Golan, M., Chuartzman, S., Munro, S., Schwappach, B., Schuldiner, M.: Toolbox: creating a systematic database of secretory pathway proteins uncovers new cargo for copi. Traffic 19(5), 370\u2013379 (2018)","journal-title":"Traffic"},{"key":"357_CR87","doi-asserted-by":"crossref","unstructured":"Wells, W.A.: The discovery of synaptic vesicles (2005)","DOI":"10.1083\/jcb1681fta2"},{"issue":"8","key":"357_CR88","doi-asserted-by":"crossref","first-page":"R397","DOI":"10.1016\/j.cub.2018.01.005","volume":"28","author":"TY Yoon","year":"2018","unstructured":"Yoon, T.Y., Munson, M.: Snare complex assembly and disassembly. Curr. Biol. 28(8), R397\u2013R401 (2018)","journal-title":"Curr. Biol."},{"key":"357_CR89","doi-asserted-by":"crossref","first-page":"16,010","DOI":"10.1038\/npjsba.2016.10","volume":"2","author":"B Yordanov","year":"2016","unstructured":"Yordanov, B., Dunn, S.J., Kugler, H., Smith, A., Martello, G., Emmott, S.: A method to identify and analyze biological programs through automated reasoning. NPJ Syst. Biol. Appl. 2, 16,010 (2016)","journal-title":"NPJ Syst. Biol. Appl."},{"key":"357_CR90","doi-asserted-by":"crossref","unstructured":"Yordanov, B., Wintersteiger, C.M., Hamadi, Y., Kugler, H.: Smt-based analysis of biological computation. In: NASA Formal Methods Symposium, pp. 78\u201392. Springer (2013)","DOI":"10.1007\/978-3-642-38088-4_6"},{"issue":"2","key":"357_CR91","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1038\/35052055","volume":"2","author":"M Zerial","year":"2001","unstructured":"Zerial, M., McBride, H.: Rab proteins as membrane organizers. Nat. Rev. Mol. Cell Biol. 2(2), 107 (2001)","journal-title":"Nat. Rev. Mol. Cell Biol."},{"issue":"11","key":"357_CR92","doi-asserted-by":"crossref","first-page":"1995","DOI":"10.1091\/mbc.E14-10-1481","volume":"26","author":"K Zhou","year":"2015","unstructured":"Zhou, K., Sumigray, K.D., Lechler, T.: The arp2\/3 complex has essential roles in vesicle trafficking and transcytosis in the mammalian small intestine. Mol. Biol. Cell 26(11), 1995\u20132004 (2015)","journal-title":"Mol. Biol. Cell"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00357-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-019-00357-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00357-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,28]],"date-time":"2024-07-28T00:26:27Z","timestamp":1722126387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-019-00357-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,2]]},"references-count":92,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["357"],"URL":"https:\/\/doi.org\/10.1007\/s00236-019-00357-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2019,12,2]]},"assertion":[{"value":"16 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 November 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 December 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}