{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:45:08Z","timestamp":1725763508502},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319039978"},{"type":"electronic","value":"9783319039985"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03998-5_17","type":"book-chapter","created":{"date-parts":[[2013,12,12]],"date-time":"2013-12-12T08:10:42Z","timestamp":1386835842000},"page":"332-354","source":"Crossref","is-referenced-by-count":0,"title":["Specializations in Symbolic Verification"],"prefix":"10.1007","author":[{"given":"Vladimir","family":"Peschanenko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Guba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Shushpanov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Symbolic Modeling, \n                    \n                      http:\/\/en.wikipedia.org\/wiki\/Model_checking"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-44616-3_18","volume-title":"Recent Trends in Algebraic Development Techniques","author":"A. Letichevsky","year":"2000","unstructured":"Letichevsky, A., Gilbert, D.: A Model for Interaction of Agents and Environments. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 311\u2013328. Springer, Heidelberg (2000)"},{"key":"17_CR3","series-title":"NATO Science Series II. Mathematics, Physics and Chemistry","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/1-4020-3817-8_10","volume-title":"Structural Theory of Automata, Semigroups, and Universal Algebra","author":"A. Letichevsky","year":"2005","unstructured":"Letichevsky, A.: Algebra of Behavior Transformations and its Applications. In: Kudryavtsev, V.B., Rosenberg, I.G. (eds.) Structural Theory of Automata, Semigroups, and Universal Algebra. NATO Science Series II. Mathematics, Physics and Chemistry, vol.\u00a0207, pp. 241\u2013272. Springer, Heidelberg (2005)"},{"key":"17_CR4","unstructured":"Letichevsky, A., Kapitonova, J., Kotlyarov, V., Letichevsky Jr., A., Nikitchenko, N., Volkov, V., Weigert, T.: Insertion Modeling in Distributed System Design. Problems of Programming\u00a0(4), 13\u201339 (2008)"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Letichevsky, A., Kapitonova, J., Volkov, V., Letichevsky Jr., A., Baranov, S., Kotlyarov, V., Weigert, T.: System Specification with Basic Protocols. Cybernetics and System Analysis\u00a0(4), 3\u201321 (2005)","DOI":"10.1007\/s10559-005-0083-y"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Letichevsky, A.A., Godlevsky, A.B., Letichevsky Jr., A.A., Potienko, S.V., Peschanenko, V.S.: Properties of Predicate Transformer of VRS System. Cybernetics and System Analyses\u00a0(4), 3\u201316 (2010)","DOI":"10.1007\/s10559-010-9229-7"},{"key":"17_CR7","unstructured":"Letichevsky, A., Kapitonova, J., Letichevsky Jr., A., Volkov, V., Baranov, S., Kotlyarov, V., Weigert, T.: Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications. In: ISSRE 2004, WITUL (Workshop on Integrated reliability with Telecommunications and UML Languages), Rennes (November 4, 2005)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-29709-0_23","volume-title":"Perspectives of Systems Informatics","author":"A.A. Letichevsky","year":"2012","unstructured":"Letichevsky, A.A., Letychevskyi, O.A., Peschanenko, V.S.: Insertion Modeling System. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol.\u00a07162, pp. 262\u2013273. Springer, Heidelberg (2012)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer Aided Verification","author":"M. Bofill","year":"2008","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The Barcelogic SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 294\u2013298. Springer, Heidelberg (2008)"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some Progress in Satisfiability Checking for Difference Logic. In: Proc. FORMATS-FTRTFT (2004)","DOI":"10.1007\/978-3-540-30206-3_19"},{"key":"17_CR14","unstructured":"D\u00e9harbe, D., Ranise, S.: Bdd-Driven First-Order Satisfiability Procedures (extended version). Research report 4630, LORIA (2002)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 317\u2013333. Springer, Heidelberg (2005)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/11691372_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.K. Ganai","year":"2006","unstructured":"Ganai, M.K., Talupur, M., Gupta, A.: SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 135\u2013150. Springer, Heidelberg (2006)"},{"key":"17_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P.G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 195\u2013210. Springer, Heidelberg (2002)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"17_CR20","series-title":"Lecture Notes in Artificial Intelligence","first-page":"322","volume-title":"CADE 2003","author":"C. Walther","year":"2003","unstructured":"Walther, C., Schweitzer, S.: About veriFun. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 322\u2013327. Springer, Heidelberg (2003)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 457\u2013461. Springer, Heidelberg (2004)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","first-page":"3","volume-title":"HVC 2010","author":"C. Barrett","year":"2010","unstructured":"Barrett, C., de Moura, L., Ranise, S., Stump, A., Tinelli, C.: The SMT-LIB Initiative and the Rise of SMT (HVC 2010 Award Talk). In: Raz, O. (ed.) HVC 2010. LNCS, vol.\u00a06504, pp. 3\u20133. Springer, Heidelberg (2010)"},{"key":"17_CR24","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1613\/jair.2861","volume":"36","author":"F. Hutter","year":"2009","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K., Stuetzle, T.: ParamILS: an Automatic Algorithm Configuration Framework. JAIR\u00a036, 267\u2013306 (2009)","journal-title":"JAIR"},{"key":"17_CR25","unstructured":"Peschanenko, V.S., Guba, A.A., Shushpanov, C.I.: Mixed Concrete-Symbolic Predicate Transformer. Bulletin of Taras Shevchenko National University of Kyiv, Series Physics & Mathematics\u00a02 (2013) (in press)"},{"key":"17_CR26","first-page":"825","volume":"185","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability Modulo Theories. Frontiers in Artificial Intelligence and Applications\u00a0185, 825\u2013885 (2009)","journal-title":"Frontiers in Artificial Intelligence and Applications"},{"key":"17_CR27","first-page":"91","volume":"4","author":"A.B. Godlevsky","year":"2010","unstructured":"Godlevsky, A.B.: Predicate Transformers in the Context of Symbolic Modeling of Transition Systems. Cybernetics and System Analysis\u00a04, 91\u201399 (2010)","journal-title":"Cybernetics and System Analysis"},{"key":"17_CR28","unstructured":"Satisfiability Modulo Theories Competition (SMT-COMP), \n                    \n                      http:\/\/smtcomp.sourceforge.net"},{"key":"17_CR29","unstructured":"The Satisfiability Modulo Theories Library, \n                    \n                      http:\/\/www.smtlib.org\/"}],"container-title":["Communications in Computer and Information Science","Information and Communication Technologies in Education, Research, and Industrial Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03998-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T11:00:56Z","timestamp":1558782056000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03998-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319039978","9783319039985"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03998-5_17","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2013]]}}}