乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T05:38:08Z","timestamp":1648877888651},"reference-count":39,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T00:00:00Z","timestamp":1196467200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":2091,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2007,12]]},"DOI":"10.1016\/j.tcs.2007.07.050","type":"journal-article","created":{"date-parts":[[2007,8,20]],"date-time":"2007-08-20T12:45:21Z","timestamp":1187613921000},"page":"227-242","source":"Crossref","is-referenced-by-count":8,"title":["Verification of Boolean programs with unbounded thread creation"],"prefix":"10.1016","volume":"388","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2007.07.050_b1","series-title":"SPIN 00","first-page":"113","article-title":"Bebop: A symbolic model checker for Boolean programs","volume":"vol. 1885","author":"Ball","year":"2000"},{"key":"10.1016\/j.tcs.2007.07.050_b2","series-title":"SPIN","first-page":"75","article-title":"Symbolic model checking for asynchronous Boolean programs","volume":"vol. 3639","author":"Cook","year":"2005"},{"key":"10.1016\/j.tcs.2007.07.050_b3","series-title":"Proceedings of FMCAD","first-page":"53","article-title":"Over-approximating Boolean programs with unbounded thread creation","author":"Cook","year":"2006"},{"key":"10.1016\/j.tcs.2007.07.050_b4","series-title":"Computer-Aided Verification (CAV)","first-page":"72","article-title":"Construction of abstract state graphs with PVS","volume":"vol. 1254","author":"Graf","year":"1997"},{"key":"10.1016\/j.tcs.2007.07.050_b5","series-title":"Static Analysis (SAS)","first-page":"268","article-title":"Boolean heaps","volume":"vol. 3672","author":"Podelski","year":"2005"},{"issue":"1","key":"10.1016\/j.tcs.2007.07.050_b6","doi-asserted-by":"crossref","DOI":"10.1145\/1182613.1182618","article-title":"Logical characterizations of heap abstractions","volume":"8","author":"Yorsh","year":"2007","journal-title":"ACM Transactions on Computational Logic"},{"issue":"5","key":"10.1016\/j.tcs.2007.07.050_b7","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","article-title":"Counterexample-guided abstraction refinement for symbolic model checking","volume":"50","author":"Clarke","year":"2003","journal-title":"Journal of the ACM"},{"key":"10.1016\/j.tcs.2007.07.050_b8","series-title":"Static Analysis (SAS)","first-page":"1","article-title":"Analysis of multithreaded programs","volume":"vol. 2126","author":"Rinard","year":"2001"},{"issue":"2","key":"10.1016\/j.tcs.2007.07.050_b9","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1145\/349214.349241","article-title":"Context-sensitive synchronization-sensitive analysis is undecidable","volume":"22","author":"Ramalingam","year":"2000","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/j.tcs.2007.07.050_b10","first-page":"89","article-title":"Composition, decomposition and model checking of pushdown processes","volume":"2","author":"Burkart","year":"1995","journal-title":"Nordic Journal of Computing"},{"key":"10.1016\/j.tcs.2007.07.050_b11","series-title":"Computer-Aided Verification (CAV)","first-page":"324","article-title":"A BDD-based model checker for recursive programs","volume":"vol. 2102","author":"Esparza","year":"2001"},{"key":"10.1016\/j.tcs.2007.07.050_b12","series-title":"Model Checking Software (SPIN)","first-page":"104","article-title":"A SAT characterization of Boolean-program correctness","volume":"vol. 2648","author":"Leino","year":"2003"},{"key":"10.1016\/j.tcs.2007.07.050_b13","series-title":"Proceedings of MEMOCODE 2004","first-page":"7","article-title":"Verification of SpecC and Verilog using predicate abstraction","author":"Jain","year":"2004"},{"key":"10.1016\/j.tcs.2007.07.050_b14","series-title":"Computer Aided Verification (CAV)","first-page":"359","article-title":"NuSMV 2: An opensource tool for symbolic model checking","author":"Cimatti","year":"2002"},{"key":"10.1016\/j.tcs.2007.07.050_b15","series-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","first-page":"334","article-title":"Verifying concurrent message-passing C programs with recursive calls","volume":"vol. 3920","author":"Chaki","year":"2006"},{"key":"10.1016\/j.tcs.2007.07.050_b16","series-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","first-page":"93","article-title":"Context-bounded model checking of concurrent software","volume":"vol. 3440","author":"Qadeer","year":"2005"},{"key":"10.1016\/j.tcs.2007.07.050_b17","series-title":"CONCUR 04","first-page":"276","article-title":"Verification by network decomposition","volume":"vol. 3170","author":"Clarke","year":"2004"},{"key":"10.1016\/j.tcs.2007.07.050_b18","series-title":"Computer-Aided Verification (CAV)","first-page":"147","article-title":"Verifying systems with replicated components in mur\u03d5","volume":"vol. 1102","author":"Ip","year":"1996"},{"key":"10.1016\/j.tcs.2007.07.050_b19","series-title":"Verification\u2014Theory and Practice: Proceedings of an International Symposium in Honor of Zohar Manna\u2019s 64th Birthday","first-page":"84","article-title":"TLPVS: A PVS-based LTL verification system","author":"Pnueli","year":"2003"},{"key":"10.1016\/j.tcs.2007.07.050_b20","series-title":"PLDI","first-page":"1","article-title":"Race checking by context inference","author":"Henzinger","year":"2004"},{"key":"10.1016\/j.tcs.2007.07.050_b21","series-title":"SPIN","first-page":"213","article-title":"Thread-modular model checking","volume":"vol. 2648","author":"Flanagan","year":"2003"},{"issue":"3","key":"10.1016\/j.tcs.2007.07.050_b22","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/j.entcs.2005.02.063","article-title":"Reachability analysis of synchronized PA systems","volume":"138","author":"Bouajjani","year":"2005","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/j.tcs.2007.07.050_b23","series-title":"SPIN Model Checking and Software Verification","first-page":"224","article-title":"Model-checking multi-threaded distributed Java programs","volume":"vol. 1885","author":"Stoller","year":"2000"},{"issue":"4","key":"10.1016\/j.tcs.2007.07.050_b24","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","article-title":"Model checking Java programs using Java PathFinder","volume":"2","author":"Havelund","year":"2000","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/j.tcs.2007.07.050_b25","series-title":"POPL","first-page":"27","article-title":"Verifying safety properties of concurrent Java programs using 3-valued logic","author":"Yahav","year":"2001"},{"key":"10.1016\/j.tcs.2007.07.050_b26","series-title":"CONCUR 04","first-page":"1","article-title":"Zing: Exploiting program structure for model checking concurrent software","volume":"vol. 3170","author":"Andrews","year":"2004"},{"key":"10.1016\/j.tcs.2007.07.050_b27","series-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","first-page":"158","article-title":"Parameterized verification of multithreaded software libraries","volume":"vol. 2031","author":"Ball","year":"2001"},{"key":"10.1016\/j.tcs.2007.07.050_b28","series-title":"Principles of Programming Languages (POPL)","first-page":"303","article-title":"On the analysis of interacting pushdown systems","author":"Kahlon","year":"2007"},{"key":"10.1016\/j.tcs.2007.07.050_b29","series-title":"Principles of Programming Languages (POPL)","first-page":"343","article-title":"Model checking and abstraction","author":"Clarke","year":"1992"},{"key":"10.1016\/j.tcs.2007.07.050_b30","series-title":"Computer-Aided Verification (CAV)","first-page":"293","article-title":"Generating finite-state abstractions of reactive systems using decision procedures","volume":"vol. 1427","author":"Col\u00f3n","year":"1998"},{"key":"10.1016\/j.tcs.2007.07.050_b31","unstructured":"T. Ball, S. Rajamani, Boolean programs: A model and process for software analysis, Tech. Rep. 2000-14, Microsoft Research, February 2000"},{"key":"10.1016\/j.tcs.2007.07.050_b32","series-title":"Computer-Aided Verification of Coordinating Processes","author":"Kurshan","year":"1995"},{"key":"10.1016\/j.tcs.2007.07.050_b33","series-title":"Computer-Aided Verification (CAV)","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"Clarke","year":"2000"},{"key":"10.1016\/j.tcs.2007.07.050_b34","series-title":"Computer-Aided Verification (CAV)","first-page":"385","article-title":"The State of SPIN","volume":"vol. 1102","author":"Holzmann","year":"1996"},{"issue":"8","key":"10.1016\/j.tcs.2007.07.050_b35","doi-asserted-by":"crossref","first-page":"1005","DOI":"10.1109\/43.298036","article-title":"Efficient symbolic simulation-based verification using the parametric form of Boolean expressions","volume":"13","author":"Jain","year":"1994","journal-title":"IEEE Transactions on CAD of ICs and Systems"},{"key":"10.1016\/j.tcs.2007.07.050_b36","series-title":"ICCAD","first-page":"78","article-title":"A unified framework for the formal verification of sequential circuits","author":"Coudert","year":"1990"},{"key":"10.1016\/j.tcs.2007.07.050_b37","series-title":"DAC","first-page":"402","article-title":"Formal verification using parametric representations of boolean constraints","author":"Aagaard","year":"1999"},{"key":"10.1016\/j.tcs.2007.07.050_b38","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","article-title":"Predicate abstraction of ANSI-C programs using SAT","volume":"25","author":"Clarke","year":"2004","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/j.tcs.2007.07.050_b39","series-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","first-page":"570","article-title":"SATABS: SAT-based predicate abstraction for ANSI-C","volume":"vol. 3440","author":"Clarke","year":"2005"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397507006202?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397507006202?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,5]],"date-time":"2019-01-05T02:51:16Z","timestamp":1546656676000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397507006202"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":39,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2007,12]]}},"alternative-id":["S0304397507006202"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2007.07.050","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2007,12]]}}}