{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:27:57Z","timestamp":1725550077940},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540292098"},{"type":"electronic","value":"9783540319696"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11562948_15","type":"book-chapter","created":{"date-parts":[[2005,10,10]],"date-time":"2005-10-10T10:06:40Z","timestamp":1128938800000},"page":"174-186","source":"Crossref","is-referenced-by-count":1,"title":["Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming"],"prefix":"10.1007","author":[{"given":"Tun","family":"Li","sequence":"first","affiliation":[]},{"given":"Yang","family":"Guo","sequence":"additional","affiliation":[]},{"given":"SiKun","family":"Li","sequence":"additional","affiliation":[]},{"given":"GongJie","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"15_CR3","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 457\u2013461. Springer, Heidelberg (2004)"},{"key":"15_CR5","unstructured":"Ball, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research (February 2000)"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/503272.503291","volume-title":"POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 191\u2013202. ACM Press, New York (2002)"},{"key":"15_CR7","first-page":"203","volume-title":"ACM Conference on Programming Language Design and Implementation","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: ACM Conference on Programming Language Design and Implementation, pp. 203\u2013213. ACM Press, New York (2001)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"issue":"6","key":"15_CR10","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. IEEE Transactions on Software Engineering\u00a030(6), 388\u2013402 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-24605-3_7","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 78\u201392. Springer, Heidelberg (2004)"},{"issue":"2-3","key":"15_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design (FMSD)\u00a025(2-3), 105\u2013127 (2004)","journal-title":"Formal Methods in System Design (FMSD)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E., Jain, H., Kroening, D.: Predicate Abstraction and Re-finement Techniques for Verifying Verilog. Technical report, Carnegie Mellon University, CMU-CS-04-139 (June 2004)","DOI":"10.21236\/ADA457877"},{"key":"15_CR14","unstructured":"Clarke, E., Jain, H., Kroening, D.: Verification of SpecC using Predicate Abstraction. MEMOCODE (June 2004)"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: A Survey. The Journal of Logic Programming\u00a019, 20, 503\u2013582 (1994)","journal-title":"The Journal of Logic Programming"},{"issue":"1","key":"15_CR16","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/54.485782","volume":"13","author":"R. Ubar","year":"1996","unstructured":"Ubar, R.: Test synthesis with alternative graphs. IEEE Design & Test of Computers\u00a013(1), 48\u201357 (1996)","journal-title":"IEEE Design & Test of Computers"},{"key":"15_CR17","unstructured":"Tun, L.: Research on techniques of VLSI RT-Level automatic functional vectors generation [Ph.D. Thesis] National University of Defense Technology, ChangSha (2003)"},{"key":"15_CR18","unstructured":"Li, T., Guo, Y., Li, S.: Functional Vectors Generation for RT-Level Verilog Descriptions Based on Path Enumeration and Constraint Logic Programming. To appear Proceedings of 8th Euromicro Conference on Digital System Design, Porto, Portugal (August 2005)"},{"key":"15_CR19","unstructured":"http:\/\/vlsi.colorado.edu\/~vis"},{"key":"15_CR20","unstructured":"Silva, J.M.: BLIF2CNF, sat.inesc-id.pt\/~jpms\/scripts\/bin\/blif2cnf"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of 39th Design Automation Conference (DAC 2001), Las Vegas (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"2002","unstructured":"McMillan, K.: Applying SAT Methods in Unbounded Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"15_CR23","unstructured":"Sun Microsystems. PicoJava technology (1999), http:\/\/www.sun.com\/microelectronics\/communitysource\/picojava\/"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11562948_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:52:14Z","timestamp":1605624734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11562948_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540292098","9783540319696"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11562948_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}