{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,14]],"date-time":"2025-11-14T07:26:21Z","timestamp":1763105181988,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672821"},{"type":"electronic","value":"9783540464198"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_28","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"411-425","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":59,"title":["Symbolic Reachability Analysis Based on SAT-Solvers"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Per","family":"Bjesse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niklas","family":"E\u00e9n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"H. R. Andersen and H. Hulgaard. Boolean expression diagrams. In Proc. 12th IEEE Int. Symp. on Logic in Computer Science, pages 88\u201398, 1997. 413, 424","DOI":"10.1109\/LICS.1997.614938"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"BCC+99._A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conference (DAC\u201999), 1999. 412","DOI":"10.1145\/309847.309942"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS\u2019 98, 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 1999. 412","DOI":"10.21236\/ADA360973"},{"key":"28_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142\u2013170, 1992. 411","journal-title":"Information and Computation"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"A. Biere, E. M. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC[tm] microprocessor using symbolic model checking without BDDs. In Proc. 11th Int. Conf. on Computer Aided Verification, 1999. 412","DOI":"10.1007\/3-540-48683-6_8"},{"key":"28_CR6","unstructured":"P. Bjesse. Symbolic model checking with sets of states represented as formulas. Technical Report CS-1999-100, Department of Computer Science, Chalmers technical university, March 1999. 412, 424"},{"key":"28_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/3-540-63166-6_3","volume-title":"Proc. 9th Int. Conf. on Computer Aided Verification","author":"A. Bor\u00e4lv","year":"1997","unstructured":"A. Bor\u00e4lv. The industrial success of verification tools based on St\u00e5lmarck\u2019s method. In Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 7\u201310, 1997. 412"},{"issue":"4","key":"28_CR8","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/s001650050021","volume":"10","author":"A. Bor\u00e4lv","year":"1998","unstructured":"A. Bor\u00e4lv. Case study: Formal verification of a computerized railway interlocking. Formal Aspects of Computing, 10(4):338\u2013360, 1998. 412","journal-title":"Formal Aspects of Computing"},{"issue":"8","key":"28_CR9","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8):677\u2013691, Aug. 1986. 411","journal-title":"IEEE Trans. on Computers"},{"issue":"2","key":"28_CR10","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.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 8(2):244\u2013263, April 1986. 411","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"28_CR11","unstructured":"N. E\u00e9n. Symbolic reachability analysis based on SAT-solvers. Master\u2019s thesis, Dept. of Computer Systems, Uppsala university, 1999. 412, 420"},{"key":"28_CR12","unstructured":"J.F. Groote, S.F.M. van Vlijmen, and J.W.C. Koorn. The safety guaranteeing system at station Hoorn-Kersenboogerd. In COMPASS\u201995, 1995. 412"},{"key":"28_CR13","unstructured":"H. Hulgaard, P.F. Williams, and H.R. Andersen. Combinational logic-level verification using boolean expression diagrams. In 3rd International Workshop on Applications of the Reed-Muller Expansion in Circuit Design, 1997. 413, 424"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. 411","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"28_CR15","unstructured":"C. Papadimitriou. Computational complexity. Addison-Wesley, 1994. 412"},{"key":"28_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"5th International Symposium on Programming, Turin","author":"J.P. Queille","year":"1982","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In 5th International Symposium on Programming, Turin, volume 137 of Lecture Notes in Computer Science, pages 337\u2013352. Springer Verlag, 1982. 411"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"G. St\u00e5lmarck and M. S\u00e4flund. Modelling and verifying systems and software in propositional logic. In SAFECOMP\u201990, pages 31\u201336. Pergamon Press, 1990. 412","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"issue":"1","key":"28_CR18","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M. Sheeran","year":"2000","unstructured":"M. Sheeran and G. St\u00e5lmarck. A tutorial on St\u00e5lmarck\u2019s method of propositional proof. Formal Methods In System Design, 16(1), 2000. 412","journal-title":"Formal Methods In System Design"},{"key":"28_CR19","unstructured":"G. St\u00e5lmarck. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula. Swedish Patent No. 467 076 (approved 1992), US patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995). 412"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: an efficient propositional prover. In Proc. Int. Conference om Automated Deduction (CADE\u201997), volume 1249 of LNAI, pages 272\u2013275. Springer Verlag, 1997. 412","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T06:00:38Z","timestamp":1737352838000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"1 June 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}