{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T22:40:43Z","timestamp":1789944043177,"version":"4.0.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319465197","type":"print"},{"value":"9783319465203","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46520-3_13","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T10:40:27Z","timestamp":1474454427000},"page":"192-208","source":"Crossref","is-referenced-by-count":7,"title":["Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems"],"prefix":"10.1007","author":[{"given":"Nikola","family":"Bene\u0161","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Demko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samuel","family":"Pastva","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"\u0160afr\u00e1nek","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Arney, D., Pajic, M., Goldman, J.M., Lee, I., Mangharam, R., Sokolsky, O.: Toward patient safety in closed-loop medical device systems. In: ICCPS 2010, pp. 139\u2013148. ACM (2010)","DOI":"10.1145\/1795194.1795214"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Baker, M., Carpenter, B., Shafi, A.: MPJ express: towards thread safe Java HPC. In: IEEE Cluster Computing 2006. IEEE Computer Society (2006)","DOI":"10.1109\/CLUSTR.2006.311890"},{"issue":"3","key":"13_CR3","doi-asserted-by":"crossref","first-page":"693","DOI":"10.1109\/TCBB.2011.110","volume":"9","author":"J Barnat","year":"2012","unstructured":"Barnat, J., Brim, L., Krej\u010d\u00ed, A., Streck, A., \u0160afr\u00e1nek, D., Vejn\u00e1r, M., Vejpustek, T.: On parameter synthesis by parallel model checking. IEEE\/ACM Trans. Comput. Biol. Bioinf. 9(3), 693\u2013705 (2012)","journal-title":"IEEE\/ACM Trans. Comput. Biol. Bioinf."},{"issue":"3","key":"13_CR4","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1093\/bib\/bbp074","volume":"11","author":"J Barnat","year":"2010","unstructured":"Barnat, J., Brim, L., \u0160afr\u00e1nek, D.: High-performance analysis of biological systems dynamics with the divine model checker. Brief. Bioinf. 11(3), 301\u2013312 (2010)","journal-title":"Brief. Bioinf."},{"key":"13_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015)"},{"key":"13_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics)","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer-Verlag New York Inc, Secaucus (2006)"},{"issue":"18","key":"13_CR7","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1093\/bioinformatics\/btq387","volume":"26","author":"G Batt","year":"2010","unstructured":"Batt, G., Page, M., Cantone, I., G\u00f6ssler, G., Monteiro, P., de Jong, H.: Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18), 603\u2013610 (2010)","journal-title":"Bioinformatics"},{"issue":"18","key":"13_CR8","doi-asserted-by":"crossref","first-page":"2415","DOI":"10.1093\/bioinformatics\/btm362","volume":"23","author":"G Batt","year":"2007","unstructured":"Batt, G., Yordanov, B., Weiss, R., Belta, C.: Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23(18), 2415\u20132422 (2007)","journal-title":"Bioinformatics"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-26287-1_2","volume-title":"Hardware and Software: Verification and Testing","author":"S Bogomolov","year":"2015","unstructured":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R.: Abstraction-based parameter synthesis for multiaffine systems. In: Piterman, N., et al. (eds.) HVC 2015. LNCS, vol. 9434, pp. 19\u201335. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26287-1_2"},{"key":"13_CR10","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.ic.2014.01.012","volume":"236","author":"L Brim","year":"2014","unstructured":"Brim, L., Dluho\u0161, P., \u0160afr\u00e1nek, D., Vejpustek, T.: STL*: extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52\u201367 (2014). Special Issue on Hybrid Systems and Biology","journal-title":"Inf. Comput."},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-319-23401-4_21","volume-title":"Computational Methods in Systems Biology","author":"L Brim","year":"2015","unstructured":"Brim, L., \u010ce\u0161ka, M., Demko, M., Pastva, S., \u0160afr\u00e1nek, D.: Parameter synthesis by parallel coloured CTL model checking. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 251\u2013263. Springer, Heidelberg (2015)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-319-26916-0_4","volume-title":"Hybrid Systems Biology","author":"L Brim","year":"2015","unstructured":"Brim, L., Demko, M., Pastva, S., \u0160afr\u00e1nek, D.: High-performance discrete bifurcation analysis for piecewise-affine dynamical systems. In: Abate, A., et al. (eds.) HSB 2015. LNCS, vol. 9271, pp. 58\u201374. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26916-0_4"},{"issue":"1","key":"13_CR13","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s10009-004-0163-8","volume":"7","author":"L Brim","year":"2005","unstructured":"Brim, L., Yorav, K., \u017d\u00eddkov\u00e1, J.: Assumption-based distribution of CTL model checking. STTT 7(1), 61\u201373 (2005)","journal-title":"STTT"},{"issue":"2","key":"13_CR14","first-page":"485","volume":"61","author":"HD Chiang","year":"2016","unstructured":"Chiang, H.D., Wang, T.: On the number and types of unstable equilibria in nonlinear dynamical systems with uniformly-bounded stability regions. IEEE Trans. Autom. Control 61(2), 485\u2013490 (2016)","journal-title":"IEEE Trans. Autom. Control"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Collins, P., Habets, L.C., van Schuppen, J.H., \u010cern\u00e1, I., Fabrikov\u00e1, J., \u0160afr\u00e1nek, D.: Abstraction of biochemical reaction systems on polytopes. In: IFAC World Congress. pp. 14869\u201314875. IFAC (2011)","DOI":"10.3182\/20110828-6-IT-1002.03317"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Dang, T., Donze, A., Maler, O., Shalev, N.: Sensitive state-space exploration. In: IEEE Conference on Decision and Control, pp. 4049\u20134054 (2008)","DOI":"10.1109\/CDC.2008.4739371"},{"issue":"9","key":"13_CR17","doi-asserted-by":"crossref","first-page":"e24246","DOI":"10.1371\/journal.pone.0024246","volume":"6","author":"A Donz\u00e9","year":"2011","unstructured":"Donz\u00e9, A., Fanchon, E., Gattepaille, L.M., Maler, O., Tracqui, P.: Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE 6(9), e24246 (2011)","journal-title":"PLoS ONE"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-3-642-00602-9_12","volume-title":"Hybrid Systems: Computation and Control","author":"A Donz\u00e9","year":"2009","unstructured":"Donz\u00e9, A., Krogh, B., Rajhans, A.: Parameter synthesis for hybrid systems with an application to simulink models. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 165\u2013179. Springer, Heidelberg (2009)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-33386-6_9","volume-title":"Automated Technology for Verification and Analysis","author":"A Donz\u00e9","year":"2012","unstructured":"Donz\u00e9, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 92\u2013106. Springer, Heidelberg (2012)"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Dreossi, T., Dang, T.: Parameter synthesis for polynomial biological models. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, pp. 233\u2013242 (2014)","DOI":"10.1145\/2562059.2562123"},{"issue":"1","key":"13_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1186\/s12934-015-0393-3","volume":"14","author":"P Dvorak","year":"2015","unstructured":"Dvorak, P., Chrast, L., Nikel, P.I., Fedr, R., Soucek, K., Sedlackova, M., Chaloupkova, R., Lorenzo, V., Prokop, Z., Damborsky, J.: Exacerbation of substrate toxicity by IPTG in Escherichia coli BL21(DE3) carrying a synthetic metabolic pathway. Microb. Cell Fact. 14(1), 1\u201315 (2015)","journal-title":"Microb. Cell Fact."},{"issue":"6767","key":"13_CR22","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1038\/35002125","volume":"403","author":"MB Elowitz","year":"2000","unstructured":"Elowitz, M.B., Leibler, S.: A synthetic oscillatory network of transcriptional regulators. Nature 403(6767), 335\u2013338 (2000)","journal-title":"Nature"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: $${\\sf dReal{:}}$$ an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013)"},{"key":"13_CR24","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1038\/35002131","volume":"403","author":"TS Gardner","year":"1999","unstructured":"Gardner, T.S., Cantor, C.R., Collins, J.J.: Construction of a genetic toggle switch in Escherichia coli. Nature 403, 339\u2013342 (1999)","journal-title":"Nature"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/978-3-662-46681-0_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Giacobbe","year":"2015","unstructured":"Giacobbe, M., Guet, C.C., Gupta, A., Henzinger, T.A., Paix\u00e3o, T., Petrov, T.: Model checking gene regulatory networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 469\u2013483. Springer, Heidelberg (2015)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","volume-title":"Computer Aided Verification","author":"R Grosu","year":"2011","unstructured":"Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396\u2013411. Springer, Heidelberg (2011)"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Bioinformatics)","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/11905455_6","volume-title":"Transactions on Computational Systems Biology VII","author":"S Jha","year":"2006","unstructured":"Jha, S., Shyamasundar, R.K.: Adapting biochemical kripke structures for distributed model checking. In: Priami, C., Ing\u00f3lfsd\u00f3ttir, A., Mishra, B., Riis Nielson, H. (eds.) Transactions on Computational Systems Biology VII. LNCS (LNBI), vol. 4230, pp. 107\u2013122. Springer, Heidelberg (2006)"},{"issue":"31","key":"13_CR28","doi-asserted-by":"crossref","first-page":"7668","DOI":"10.1021\/acs.iecr.5b00572","volume":"54","author":"W Li","year":"2015","unstructured":"Li, W., Zhong, L., He, Y., Meng, J., Yao, F., Guo, Y., Xu, C.: Multiple steady-states analysis and unstable operating point stabilization in homogeneous azeotropic distillation with intermediate entrainer. Ind. Eng. Chem. Res. 54(31), 7668\u20137686 (2015)","journal-title":"Ind. Eng. Chem. Res."},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL 2014, pp. 607\u2013618. ACM (2014)","DOI":"10.1145\/2535838.2535857"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/978-3-319-23401-4_16","volume-title":"Computational Methods in Systems Biology","author":"C Madsen","year":"2015","unstructured":"Madsen, C., Shmarov, F., Zuliani, P.: BioPSy: an SMT-based tool for guaranteed parameter set synthesis of biological models. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 182\u2013194. Springer, Heidelberg (2015)"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004)"},{"issue":"113","key":"13_CR32","doi-asserted-by":"crossref","first-page":"20150831","DOI":"10.1098\/rsif.2015.0831","volume":"12","author":"A Milias-Argeitis","year":"2015","unstructured":"Milias-Argeitis, A., Engblom, S., Bauer, P., Khammash, M.: Stochastic focusing coupled with negative feedback enables robust regulation in biochemical reaction networks. J. R. Soc. Interface 12(113), 20150831 (2015)","journal-title":"J. R. Soc. Interface"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Raman, V., Donz\u00e9, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: HSCC 2015, pp. 239\u2013248. ACM (2015)","DOI":"10.1145\/2728606.2728628"},{"issue":"12","key":"13_CR35","doi-asserted-by":"crossref","first-page":"i169","DOI":"10.1093\/bioinformatics\/btp200","volume":"25","author":"A Rizk","year":"2009","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25(12), i169\u2013i178 (2009)","journal-title":"Bioinformatics"},{"issue":"4","key":"13_CR36","doi-asserted-by":"crossref","first-page":"645","DOI":"10.1016\/S0022-2836(03)00506-0","volume":"329","author":"N Rosenfeld","year":"2003","unstructured":"Rosenfeld, N., Alon, U.: Response delays and the structure of transcription networks. J. Mol. Biol. 329(4), 645\u2013654 (2003)","journal-title":"J. Mol. Biol."},{"issue":"10","key":"13_CR37","doi-asserted-by":"crossref","first-page":"1506","DOI":"10.1093\/bioinformatics\/bth110","volume":"20","author":"M Swat","year":"2004","unstructured":"Swat, M., Kel, A., Herzel, H.: Bifurcation analysis of the regulatory modules of the mammalian G1\/S transition. Bioinformatics 20(10), 1506\u20131511 (2004)","journal-title":"Bioinformatics"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46520-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T20:54:54Z","timestamp":1568408094000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46520-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319465197","9783319465203"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46520-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}