{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:55:23Z","timestamp":1773194123657,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540412199","type":"print"},{"value":"9783540409229","type":"electronic"}],"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-40922-x_8","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T04:41:36Z","timestamp":1196311296000},"page":"127-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":304,"title":["Checking Safety Properties Using Induction and a SAT-Solver"],"prefix":"10.1007","author":[{"given":"Mary","family":"Sheeran","sequence":"first","affiliation":[]},{"given":"Satnam","family":"Singh","sequence":"additional","affiliation":[]},{"given":"Gunnar","family":"St\u00e5lmarck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Symbolic Reachability Analysis based on SAT solvers","author":"P. A. Abdulla","year":"2000","unstructured":"P. A. Abdulla, P. Bjesse and N. E\u00e9n: Symbolic Reachability Analysis based on SAT solvers, In Proc. Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201900, LNCS, Springer-Verlag, 2000."},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.21236\/ADA360973","volume-title":"Symbolic Model Checking without BDDs","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E.M. Clarke and Y. Zhu: Symbolic Model Checking without BDDs. In Proc. Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201999, number 1579, LNCS, Springer-Verlag, 1999."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, M. Fujita and Y. Zhu: Symbolic model checking using sat procedures instead of BDDs. Design Automation Conference, DAC\u201999, IEEE Press, 1999.","DOI":"10.1145\/309847.309942"},{"key":"8_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.21236\/ADA360973","volume-title":"Verifying Safety Properties of a PowerPC Microprocessor Using Symbolic Model Checking without BDDs","author":"A. Biere","year":"1999","unstructured":"A. Biere, E.M. Clarke, R. Raimi and Y. Zhu: Verifying Safety Properties of a PowerPC Microprocessor Using Symbolic Model Checking without BDDs. In Proc. Int. Conf. on Computer-Aided Verification, CAV\u201999, LNCS, Springer-Verlag, 1999."},{"key":"8_CR5","series-title":"Lect Notes Comput Sci","volume-title":"SAT-based Verification without State Space Traversal","author":"P. Bjesse","year":"2000","unstructured":"P. Bjesse, K. Claessen: SAT-based Verification without State Space Traversal. In Proc. Int. Conf. on Formal Methods in Computer Aided Design of Electronic Circuits, FMCAD\u201900, LNCS, Springer-Verlag, 2000."},{"key":"8_CR6","unstructured":"E. Clarke, O. Grumberg and D. Peled: Model Checking, MIT Press, 1999."},{"key":"8_CR7","unstructured":"W.J. Fokkink and P.R. Hollingshead: Verification of Interlockings: From Control Tables to Ladder Logic Diagrams, in (J.F. Groote, S.P. Luttik and J.J. van Wamel, eds) Proc. 3rd Workshop on Formal Methods for Industrial Critical Systems, FMICS\u201998, Amsterdam, 1998."},{"key":"8_CR8","unstructured":"D. Deharbe and A. Martins Moreira: Using Induction and BDDs to Model Check Invariants, In H. Li and D. Probst, editors, Advances in Hardware Design and Verification, IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods: CHARME\u201997, Chapman and Hall, 1997"},{"key":"8_CR9","first-page":"27","volume":"6","author":"C.J. Lillieroth","year":"1999","unstructured":"C.J. Lillieroth and S. Singh: Formal Verification of FPGA Cores. Nordic Journal of Computing 6, 27\u201347, 1999.","journal-title":"Nordic Journal of Computing"},{"key":"8_CR10","volume-title":"Formal Modelling and Automatic Verification of Lustre Programs Using NP-Tools","author":"M. Ljung","year":"1999","unstructured":"M. Ljung: Formal Modelling and Automatic Verification of Lustre Programs Using NP-Tools, Master\u2019s thesis, Prover Technology AB and Department of Teleinformatics, KTH, Stockholm, 1999."},{"key":"8_CR11","doi-asserted-by":"crossref","first-page":"1","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 proof procedure for propositionallogic. Formal Methods in System Design, 16:1, January 2000.","journal-title":"Formal Methods in System Design"},{"key":"8_CR12","unstructured":"M. Sheeran and G. St\u00e5lmarck: Checking safety properties using induction and boolean satisfiability. Appendix to deliverable d20.2, EU project CRISYS, 1999."},{"key":"8_CR13","series-title":"Lect Notes Comput Sci","volume-title":"St\u00e5lmarck\u2019s Method and QBF Solving","author":"G. St\u00e5lmarck","year":"1999","unstructured":"G. St\u00e5lmarck: St\u00e5lmarck\u2019s Method and QBF Solving. In Proc. Int. Conf. on Computer-Aided Verification, CAV\u201999, LNCS, Springer-Verlag, 1999."},{"key":"8_CR14","unstructured":"Xilinx: Xilinx IP Center, \n                    http:\/\/www.xilinx.com\/ipcenter\n                    \n                  ."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T10:11:17Z","timestamp":1580292677000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}