{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,15]],"date-time":"2024-12-15T17:10:08Z","timestamp":1734282608096,"version":"3.30.2"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,12,18]],"date-time":"2002-12-18T00:00:00Z","timestamp":1040169600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2003,11]]},"DOI":"10.1007\/s10009-002-0091-4","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T15:40:18Z","timestamp":1079797218000},"page":"15-33","source":"Crossref","is-referenced-by-count":14,"title":["A symbolic manipulator for automated verification of reactive systems with heterogeneous data types"],"prefix":"10.1007","volume":"5","author":[{"given":"Tuba","family":"Yavuz-Kahveci","sequence":"first","affiliation":[]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,18]]},"reference":[{"key":"91_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"Alur,","year":"3","unstructured":"Alur, R., Henzinger, T.A., Ho, P.: Automatic symbolic verification of embedded systems. IEEE Trans Software Eng 22(3): 181\u2013201, 1996","journal-title":"IEEE Trans Software Eng"},{"unstructured":"Andrews, G.R.: Concurrent programming: principles and practice. Benjamin\/Cummings, Redwood City, Calif., USA, 1991","key":"91_CR2"},{"doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.H.: Symbolic model checking: 1020 states and beyond. In: Proc. 5th Annual IEEE Symposium on Logic in Computer Science, pp. 428\u2013439, January 1990","key":"91_CR3","DOI":"10.1109\/LICS.1990.113767"},{"doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., League, C.: Verifying systems with integer constraints and Boolean predicates: a composite approach. In: Proc. 1998 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 113\u2013123, March 1998","key":"91_CR4","DOI":"10.1145\/271771.271799"},{"unstructured":"Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Rueb, H., Rushby, J., Rusu, V., Saidi, H., Shankar, N., Singerman, E., Tiwari, A.: An overview of SAL. In: Proc. 5th Langley Formal Methods Workshop, June 2000","key":"91_CR5"},{"key":"91_CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/332740.332746","volume":"9","author":"Bultan,","year":"1","unstructured":"Bultan, T., Gerber, R., League, C.: Composite model checking: verification with type-specific symbolic representations. ACM Trans Software Eng Methodol 9(1): 3\u201350, 2000","journal-title":"ACM Trans Software Eng Methodol"},{"doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic. In: Grumberg, O., (ed.), Proc. 9th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1254. Springer, Berlin Heidelberg New York, 1997, pp. 400\u2013411","key":"91_CR7","DOI":"10.1007\/3-540-63166-6_39"},{"key":"91_CR8","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"Bultan,","year":"4","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Trans Program Lang Syst 21(4): 747\u2013789, 1999","journal-title":"ACM Trans Program Lang Syst"},{"doi-asserted-by":"crossref","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Proc. 10th International Conference for Computer-Aided Verification (CAV\u201998), 1998","key":"91_CR9","DOI":"10.1007\/BFb0028755"},{"key":"91_CR10","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"Ball,","year":"1","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. J Softw Tools Technol Transfer 5(1): 49\u201358, 2003","journal-title":"J Softw Tools Technol Transfer"},{"key":"91_CR11","first-page":"677","volume":"35","author":"Bryant,","year":"8","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput 35(8): 677\u2013691, 1986","journal-title":"IEEE Trans Comput"},{"doi-asserted-by":"crossref","unstructured":"Bharadwaj, R., Sims, S.: Salsa: combining constraint solvers with BDDs for automatic invariant checking. In: Graf, S., Schwartzbach, M., (eds.), Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 1254. Springer, Berlin Heidelberg New York, 2000, pp. 378\u2013394","key":"91_CR12","DOI":"10.1007\/3-540-46419-0_26"},{"doi-asserted-by":"crossref","unstructured":"Bultan, T., Yavuz-Kahveci, T.: Action Language Verifier. In: Proc. 6th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001","key":"91_CR13","DOI":"10.1109\/ASE.2001.989834"},{"key":"91_CR14","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"Chan,","year":"7","unstructured":"Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. IEEE Trans Software Eng 24(7): 498\u2013520, 1998","journal-title":"IEEE Trans Software Eng"},{"doi-asserted-by":"crossref","unstructured":"Chan, W., Anderson, R.J., Beame, P., Notkin, D.: Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In: Grumberg, O., (ed.), Proc. 9th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1254. Springer, Berlin Heidelberg New York, 1997, pp. 316\u2013327","key":"91_CR15","DOI":"10.1007\/3-540-63166-6_32"},{"doi-asserted-by":"crossref","unstructured":"Courtois, P.J., Parnas, D.L.: Documentation for safety critical software. In: Proc. 15th International Conference on Software Engineering, pp. 315\u2013323, May 1993","key":"91_CR16","DOI":"10.1109\/ICSE.1993.346033"},{"unstructured":"CUDD : CU decision diagram package, http:\/\/vlsi.colorado.edu\/\u223cfabio\/cudd\/","key":"91_CR17"},{"doi-asserted-by":"crossref","unstructured":"Delzanno, G., Bultan, T.: Constraint-based verification of client server protocols. In: Proc. 7th International Conference on Principles and Practice of Constraint Programming (CP 2001), 2001","key":"91_CR18","DOI":"10.1007\/3-540-45578-7_20"},{"key":"91_CR19","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","volume":"3","author":"Delzanno,","year":"3","unstructured":"Delzanno, G., Podelski, A.: Constraint-based deductive model checking. J Softw Tools Technol Transfer 3(3): 250\u2013270, 2001","journal-title":"J Softw Tools Technol Transfer"},{"unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: elements of reusable object-oriented software. Addison-Wesley, Reading, Mass., USA, 1994","key":"91_CR20"},{"doi-asserted-by":"crossref","unstructured":"Halbwachs, N.: Delay analysis in synchronous programs. In: C. Courcoubetis, (ed.), Proc. Computer Aided Verification, Lecture Notes in Computer Science, vol. 697. Springer, Berlin Heidelberg New York, 1993, pp. 333\u2013346","key":"91_CR21","DOI":"10.1007\/3-540-56922-7_28"},{"doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Raymond, P., Proy, Y.: Verification of linear hybrid systems by means of convex approximations. In: LeCharlier, B., (ed.), Proc. International Symposium on Static Analysis, Lecture Notes in Computer Science, vol. 864. Springer, Berlin Heidelberg New York, 1994","key":"91_CR22","DOI":"10.1007\/3-540-58485-4_43"},{"unstructured":"Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The Omega Library interface guide. Technical Report CS-TR-3445, Department of Computer Science, University of Maryland, College Park, March 1995","key":"91_CR23"},{"doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking. Kluwer Academic, Boston, Mass., USA, 1993","key":"91_CR24","DOI":"10.1007\/978-1-4615-3190-6"},{"unstructured":"The Omega project, http:\/\/www.cs.umd.edu\/projects\/omega\/","key":"91_CR25"},{"doi-asserted-by":"crossref","unstructured":"Saidi, H.: Model checking guided abstraction and analysis. In: Proc. Statica Analysis Symposium, Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, 2000","key":"91_CR26","DOI":"10.1007\/978-3-540-45099-3_20"},{"key":"91_CR27","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/BF01530796","volume":"8","author":"Srivastava,","year":"1993","unstructured":"Srivastava, D.: Subsumption and indexing in constraint query languages with linear arithmetic constraints. Ann Math Artif Intel 8: 315\u2013343, 1993","journal-title":"Ann Math Artif Intel"},{"doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Heuristics for efficient manipulation of composite constraints. In: Proc. 4th International Workshop on Frontiers of Combining Systems (FroCoS 2002), 2002","key":"91_CR28","DOI":"10.1007\/3-540-45988-X_6"},{"doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci, T., Tuncer, M., Bultan, T.: Composite symbolic library. In: Proc. 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 2031. Springer, Berlin Heidelberg New York, 2001","key":"91_CR29","DOI":"10.1007\/3-540-45319-9_5"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0091-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-002-0091-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0091-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,15]],"date-time":"2024-12-15T16:38:38Z","timestamp":1734280718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-002-0091-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12,18]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["91"],"URL":"https:\/\/doi.org\/10.1007\/s10009-002-0091-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2002,12,18]]}}}