{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:07:34Z","timestamp":1751983654222},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672821"},{"type":"electronic","value":"9783540464198"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_26","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T19:17:25Z","timestamp":1186600645000},"page":"378-395","source":"Crossref","is-referenced-by-count":17,"title":["Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking"],"prefix":"10.1007","author":[{"given":"Ramesh","family":"Bharadwaj","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Sims","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"26_CR1","series-title":"Technical Report","volume-title":"Software requirements for the A-7E aircraft","author":"T. A. Alspaugh","year":"1992","unstructured":"T. A. Alspaugh et al. Software requirements for the A-7E aircraft. Technical Report NRL-9194, Naval Research Laboratory, Wash., DC, 1992. 387"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"R. J. Anderson, P. Beame, et al. Model checking large software specifications. In Proc. Fourth ACM FSE, October 1996. 380","DOI":"10.1145\/239098.239127"},{"key":"26_CR3","unstructured":"M. Archer, C. Heitmeyer, and S. Sims. TAME: A PVS interface to simplify proofs for automata models. In Proc. User Interfaces for Theorem Provers, Eindhoven, Netherlands, July 1998. Eindhoven University CS Technical Report. 380, 387"},{"key":"26_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods In Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In Formal Methods In Computer-Aided Design, volume 1166 of LNCS, pages 187\u2013201, November 1996. 380"},{"key":"26_CR5","unstructured":"S. Bensalem and Y. Lakhnech. Automatic Generation of Invariants. Formal Methods in Systems Design, July 1998. 379, 380"},{"key":"26_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Conference on Computer Aided Verification CAV\u201996","author":"S. Bensalem","year":"1996","unstructured":"S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. In Conference on Computer Aided Verification CAV\u201996, LNCS 1102, July 1996. 379, 380"},{"key":"26_CR7","unstructured":"R. Bharadwaj and C. Heitmeyer. Applying the SCR requirements method to a simple autopilot. In Proc. Fourth NASA Langley Formal Methods Workshop (LFM97), NASA Langley Research Center, September 1997. 387"},{"key":"26_CR8","unstructured":"R. Bharadwaj and C. Heitmeyer. Verifying SCR requirements specifications using state exploration. In 1 st ACM Workshop on Autom. Analysis of Software, 1997. 383"},{"key":"26_CR9","unstructured":"R. Bharadwaj and C. Heitmeyer. Model checking complete requirements specifications using abstraction. Journal of Automated Software Eng., January 1999. 378, 379, 380, 383, 387, 390, 393"},{"key":"26_CR10","unstructured":"R. Bharadwaj and S. Sims. Salsa: Combining decision procedures for fullyautomatic verification. Technical report, Naval Research Laboratory, To appear. 382, 384, 386"},{"key":"26_CR11","unstructured":"N. Bjorner, A. Browne, M. Colon, B. Finkbeiner, Z. Manna, H. Sipma, and T. Uribe. Verifying temporal properties of reactive systems: A step tutorial. Formal Methods in System Design, 1999. 379, 380"},{"key":"26_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Trees and Algebra in Programming-CAAP","author":"A. Boudet","year":"1996","unstructured":"A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In Trees and Algebra in Programming-CAAP, LNCS 1059, 1996. 380, 385"},{"key":"26_CR13","unstructured":"J. R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congress Logic, Methodology, and Philosophy of Science, pages 1\u201311. Stanford University Press, 1960. 385"},{"key":"26_CR14","series-title":"Technical Report","volume-title":"Verifying systems with integer constraints and boolean predicates: A composite approach","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Gerber, and C. League. Verifying systems with integer constraints and boolean predicates: A composite approach. Technical Report UMIACS-TR-97-62, University of Maryland, College Park, MD, August 1997. 380"},{"key":"26_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-63166-6_32","volume-title":"Computer Aided Verification","author":"W. Chan","year":"1997","unstructured":"W. Chan, R. Anderson, P. Beame, and D. Notkin. Combining constraint solving with symbolic model checking for a class of systems with non-linear constraints. In Computer Aided Verification, LNCS, pages 316\u2013327, 1997. 380"},{"issue":"7","key":"26_CR16","first-page":"380","volume":"24","author":"William Chan","year":"1998","unstructured":"William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, and Jon D. Reese. Model checking large software specifications. IEEE Trans. on Softw. Eng., 24(7), July 1998. 380","journal-title":"IEEE Trans. on Softw. Eng."},{"issue":"2","key":"26_CR17","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. on Prog. Lang. and Systems, 8(2):244\u2013263, April 1986. 378","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"key":"26_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028773","volume-title":"Computer Aided Verification, CAV\u2019 98","author":"J. Elgaard","year":"1998","unstructured":"J. Elgaard, N. Klarlund, and A. Moller. Mona 1.x: new techniques for ws1s and ws2s. In Computer Aided Verification, CAV\u2019 98, LNCS 1427, 1998. 380"},{"key":"26_CR19","unstructured":"Fischer and Rabin. Super-exponential complexity of Presburger arithmetic. In Complexity of Computation: Proceedings of a Symposium in Applied Mathematics of the American Mathematical Society and the Society for Industrial and Applied Mathematics, 1974. 384"},{"key":"26_CR20","unstructured":"M.R. Garey and D.S. Johnson. Computers and Intractability: A guide to the theory of NP-Completeness. W.H. Freeman and Company, 1979. 384"},{"key":"26_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Conference on Computer Aided Verification CAV\u201996","author":"S. Graf","year":"1996","unstructured":"S. Graf and H. Saidi. Verifying invariants using theorem proving. In Conference on Computer Aided Verification CAV\u201996, LNCS 1102, Springer Verlag, 1996. 380"},{"key":"26_CR22","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C. Heitmeyer","year":"1998","unstructured":"C. Heitmeyer, J. Kirby, B. Labaw, M. Archer, and R. Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering, 24:927\u2013947, November 1998. 379, 380, 383, 387","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer, J. Kirby, B. Labaw, and R. Bharadwaj. SCR*: A toolset for specifying and analyzing software requirements. In Proc. Computer-Aided Verification, 10th Annual Conf. (CAV\u201998), Vancouver, Canada, June 1998. 379, 380, 387","DOI":"10.21236\/ADA465334"},{"issue":"3","key":"26_CR24","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C. L. Heitmeyer","year":"1996","unstructured":"C. L. Heitmeyer, R. D. Jeffords, and B. G. Labaw. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5(3):231\u2013261, July 1996. 379, 381, 387","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"issue":"5","key":"26_CR25","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Trans. on Softw. Eng., 23(5):279\u2013295, May 1997. 380, 389","journal-title":"IEEE Trans. on Softw. Eng."},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"R. Jeffords and C. Heitmeyer. Automatic generation of state invariants from requirements specifications. In Proc. Sixth ACM SIGSOFT Symp. on Foundations of Software Engineering, November 1998. 379, 389","DOI":"10.1145\/288195.288218"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"J. Kirby, Jr., M. Archer, and C. Heitmeyer. SCR: A practical approach to building a high assurance COMSEC system. In Proceedings of the 15th Annual Computer Security Applications Conference (ACSAC\u2019 99), December 1999. 387","DOI":"10.1109\/CSAC.1999.816018"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. 380, 384, 389","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"2","key":"26_CR29","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, 1979. 380","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"26_CR30","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995. 380","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BFb0035388","volume-title":"Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201997)","author":"P. Kelb","year":"1997","unstructured":"P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. Mosel: A flexible toolset for monadic second-order logic. In Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201997), volume 1217 of (LNCS), pages 183\u2013202, Heidelberg, Germany, March 1997. Springer-Verlag. 380"},{"key":"26_CR32","doi-asserted-by":"crossref","unstructured":"Y. Lakhnech S. Bensalem and S. Owre. InVeSt: A tool for the verification of invariants. In Proc. Computer-Aided Verification, 10th Annual Conf. (CAV\u201998), Vancouver, Canada, June 1998. 380","DOI":"10.1007\/BFb0028771"},{"issue":"1","key":"26_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"Robert E. Shostak. Deciding combinations of theories. JACM, 31(1):1\u201312, January 1984. 380","journal-title":"JACM"},{"key":"26_CR34","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification-10 th Int\u2019l. Conference","author":"P. Wolper","year":"1998","unstructured":"P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In Computer Aided Verification-10 th Int\u2019l. Conference, LNCS 1427, 1998. 380, 385"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T17:07:28Z","timestamp":1556730448000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}