{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:32:43Z","timestamp":1725485563257},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_13","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T22:48:36Z","timestamp":1180651716000},"page":"190-201","source":"Crossref","is-referenced-by-count":7,"title":["Using BDDs with Combinations of Theories"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Fontaine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E. Pascal","family":"Gribomont","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"13_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"W. Ackermann. Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954."},{"key":"13_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45988-X_11","volume-title":"Frontiers of Combining Systems (FROCOS)","author":"C. W. Barrett","year":"2002","unstructured":"C. W. Barrett, D. L. Dill, and A. Stump. A generalization of Shostak\u2019s method for combining decision procedures. In Frontiers of Combining Systems (FROCOS), volume 2309 of Lecture Notes in Computer Science. Springer-Verlag, 2002."},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"N. S. Bj\u00f8rner, Z. Manna, H. B. Sipma, and T. E. Uribe. Deductive verification of real-time systems using STeP. TCS: Theoretical Computer Science, 253, 2001.","DOI":"10.1016\/S0304-3975(00)00088-8"},{"issue":"8","key":"13_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677\u2013691, Aug. 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"13_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-63166-6_32","volume-title":"Proc. 9th Conf. Computer Aided Verification","author":"W. Chan","year":"1997","unstructured":"W. Chan, R. Anderson, P. Beame, and D. Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In Proc. 9th Conf. Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 316\u2013327. Springer-Verlag, 1997."},{"key":"13_CR6","volume-title":"Parallel Program Design","author":"K. M. Chandy","year":"1988","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design. Addison-Wesley, Reading, Massachusetts, 1988."},{"key":"13_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-61511-3_107","volume-title":"Proc. 13th Int. Conf. on Automated Deduction","author":"D. Cyrluk","year":"1996","unstructured":"D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak\u2019s decision procedure for combinations of theories. In Proc. 13th Int. Conf. on Automated Deduction, volume 1104 of Lecture Notes in Computer Science, pages 463\u2013477, New Brunswick, NJ, 1996. Springer-Verlag."},{"key":"13_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Proc. 13th Conf. Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"J.-C. Filli\u00e2tre, S. Owre, H. Rue\u00df, and N. Shankar. ICS: integrated canonizer and solver. In Proc. 13th Conf. Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 246\u2013249. Springer-Verlag, 2001."},{"key":"13_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0028749","volume-title":"Proc. 10th Conf. Computer Aided Verification","author":"A. Goel","year":"1998","unstructured":"A. Goel, K. Sajid, H. Zhou, A. Aziz, and V. Singhal. BDD based procedures for a theory of equality with uninterpreted functions. In Proc. 10th Conf. Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 244\u2013255. Springer-Verlag, 1998."},{"key":"13_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-58156-1_36","volume-title":"Proc. 12th Conf. on Automated Deduction","author":"J. Goubault","year":"1994","unstructured":"J. Goubault. Proving with BDDs and control of information. In Proc. 12th Conf. on Automated Deduction, volume 814 of Lecture Notes in Computer Science, pages 499\u2013513. Springer-Verlag, 1994."},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/3-540-60045-0_41","volume-title":"Proc. 7th Conf. on Computer Aided Verification","author":"E. P. Gribomont","year":"1995","unstructured":"E. P. Gribomont and D. Rossetto. CAVEAT: technique and tool for Computer Aided VErification And Transformation. In Proc. 7th Conf. on Computer Aided Verification, volume 939 of Lecture Notes in Computer Science, pages 70\u201383, Liege, Belgium, 1995. Springer-Verlag."},{"key":"13_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-48660-7_18","volume-title":"Proc. 16th Int. Conf. on Automated Deduction","author":"E. P. Gribomont","year":"1999","unstructured":"E. P. Gribomont and N. Salloum. Using OBDD\u2019s for the validation of Skolem verification conditions. In Proc. 16th Int. Conf. on Automated Deduction, volume 1632 of Lecture Notes in Computer Science, pages 222\u2013226, Trento, Italy, 1999. Springer-Verlag."},{"key":"13_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-44404-1_11","volume-title":"Logic Programming and Automated Reasoning","author":"J. F. Groote","year":"2000","unstructured":"J. F. Groote and J. van de Pol. Equational binary decision diagrams. In Logic Programming and Automated Reasoning, volume 1955 of Lecture Notes in Computer Science, pages 161\u2013178. Springer-Verlag, 2000."},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer and N. A. Lynch. The generalized railroad crossing \u2014 a case study in formal verification of real-time systems. In Proceedings 15th IEEE Real-Time Systems Symposium, San Juan, Puerto Rico, pages 120\u2013131, Dec. 1994.","DOI":"10.1109\/REAL.1994.342724"},{"key":"13_CR15","unstructured":"The Li\u00e8ge Automata-based Symbolic Handler (LASH). Available at http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/ ."},{"key":"13_CR16","unstructured":"J. R. Levitt. Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University, December 1998."},{"key":"13_CR17","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"N. Lynch. Distributed Algorithms. Morgan Kaufmann, San Francisco, CS, 1996."},{"key":"13_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-48168-0_9","volume-title":"Computer Science Logic","author":"J. M\u00f8ller","year":"1999","unstructured":"J. M\u00f8ller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 111\u2013125. Springer-Verlag, 1999."},{"issue":"2","key":"13_CR19","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplifications by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, Oct. 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"13_CR20","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356\u2013364, 1980.","journal-title":"Journal of the ACM"},{"issue":"6","key":"13_CR21","doi-asserted-by":"crossref","first-page":"697","DOI":"10.1093\/logcom\/5.6.697","volume":"5","author":"J. Posegga","year":"1995","unstructured":"J. Posegga and P. H. Schmitt. Automated deduction with shannon graphs. Journal of Logic and Computation, 5(6):697\u2013729, Dec. 1995.","journal-title":"Journal of Logic and Computation"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"H. Rue\u00df and N. Shankar. Deconstructing shostak. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS-01), pages 19\u201328, Los Alamitos, CA, 2001. IEEE Computer Society.","DOI":"10.1109\/LICS.2001.932479"},{"issue":"1","key":"13_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"R. E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1\u201312, Jan. 1984.","journal-title":"Journal of the ACM"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"C. Tinelli and M. T. Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In F. Baader and K. U. Schulz, editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop (Munich, Germany), pages 103\u2013120. Kluwer Academic Publishers, 1996.","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"13_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"P. Wolper and B. Boigelot. On the construction of automata from linear arithmetic constraints. In Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science, pages 1\u201319, Berlin, March 2000. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:17:54Z","timestamp":1556450274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}