{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T03:05:52Z","timestamp":1649041552632},"reference-count":27,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3742,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s1571-0661(04)80656-x","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"105-119","source":"Crossref","is-referenced-by-count":5,"title":["Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs"],"prefix":"10.1016","volume":"86","author":[{"given":"Silvio","family":"Ranise","sequence":"first","affiliation":[]},{"given":"David","family":"D\u00e9harbe","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB1","series-title":"\u201cThe B-Book: Assigning Programs to Meanings,\u201d","author":"Abrial","year":"1996"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB2","doi-asserted-by":"crossref","unstructured":"Armando A., S. Ranise and M. Rusinowitch, A rewriting approach to satisfiability procedures, Information and Computation To appear (2003), preprint available at http:\/\/www.loria.fr\/~ranise\/papers.html.","DOI":"10.1016\/S0890-5401(03)00020-8"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB3","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","article-title":"Rewrite-based equational theorem proving with selection and simplification","volume":"4","author":"Bachmair","year":"1994","journal-title":"J. of Logic and Comp"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB4","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02328452","article-title":"Set Theory in First-Order Logic: Clauses for Godel's Axioms","volume":"2","author":"Boyer","year":"1986","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB5","first-page":"83","article-title":"Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic","volume":"11","author":"Boyer","year":"1988","journal-title":"Machine Intelligence"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB6","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1109\/TC.1984.1676408","article-title":"Graph-Based Algorithms for Boolean Function Manipulation","volume":"33","author":"Bryant","year":"1984","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB7","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/371282.371364","article-title":"Processor Verification Using Efficient Reductions of the logic of Uninterpreted Functions to Propositional Logic","volume":"2","author":"Bryant","year":"2001","journal-title":"ACM Trans. on Computational Logic (TOCL)"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB8","unstructured":"Claessen K., R. H\u00e4hnle and J. Maartensson, Verification of Hardware Systems with First-Order Logic, in: In VERIFY'02 (Workshop affiliated to FloC'02, 2002."},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB9","doi-asserted-by":"crossref","unstructured":"Dor N., M. Rodeh and S. Sagiv, Checking Cleanness in Linked Lists, in: Static Analysis Symposium, 2000, pp. 115\u2013134.","DOI":"10.1007\/978-3-540-45099-3_7"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB10","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1145\/322092.322104","article-title":"Assignment commands with array references","volume":"25","author":"Downey","year":"1978","journal-title":"Journal of the Association of Computing Machinery"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB11","series-title":"\u201cA Mathematical Introduction to Logic,\u201d","author":"Enderton","year":"1972"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB12","doi-asserted-by":"crossref","unstructured":"Flanagan C., K. R. Leino, M. Lillibridge, G. Nelson, J. B. Saxe and R. Stata, Extended Static Checking for Java, in: Proc. of the 2002 ACM SIGPLAN Conf. on Prog. Lang. Design and Impl. (PLDI), Berlin, Germany, 2002, pp. 234\u2013245.","DOI":"10.1145\/512529.512558"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB13","doi-asserted-by":"crossref","unstructured":"Fontaine P. and E. P. Gribomont, Using bdds with combinations of theories, in: 9th Intl. Conf. on Logic for Programming and Automated Reasoning (LPAR'2002), 2002.","DOI":"10.1007\/3-540-36078-6_13"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB14","unstructured":"Gribomont, E. P. and P. Fontaine, Decidability of Invariant Validation for Parameterized Systems, in: Proc. of 9th Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), 2003, to appear."},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB15","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1145\/363235.363259","article-title":"An Axiomatic Basis for Computer Programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Comm. ACM"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB16","doi-asserted-by":"crossref","unstructured":"Hong Y., P. Beerel, J. Burch and K. McMillan, Safe bdd minimization using don't cares, in: 34th Design Automation Conference, 1997.","DOI":"10.1109\/DAC.1997.597145"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB17","doi-asserted-by":"crossref","unstructured":"Jackson D. and M. Vaziri, Finding Bugs with a Constraint Solver, in: Proc. of International Symposium on Software Testing and Analysis, Portland, OR, USA, 2000.","DOI":"10.1145\/347324.383378"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB18","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic Execution and Program Testing","volume":"19","author":"King","year":"1976","journal-title":"Comm. ACM"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB19","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF00881842","article-title":"Introduction to the OBDD Algorithm for the ATP Community","volume":"6","author":"Moore","year":"1994","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB20","unstructured":"Nelson G., Techniques for Program Verification, Technical Report CSL-81-10, Xerox, Palo Alto Research Center (1981)."},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB21","doi-asserted-by":"crossref","unstructured":"Nelson G., Verifying Reachability Invariants of Linked Structures, in: Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages (POPL'83), Austin, Texas, USA, 1983, pp. 38\u201347.","DOI":"10.1145\/567067.567073"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB22","series-title":"Hand. of Automated Reasoning","article-title":"Paramodulation-based theorem proving","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB23","doi-asserted-by":"crossref","first-page":"697","DOI":"10.1093\/logcom\/5.6.697","article-title":"Automated Deduction with Shannon Graphs","volume":"5","author":"Posegga","year":"1995","journal-title":"J. of Logic and Computation"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB24","doi-asserted-by":"crossref","unstructured":"Reynolds, J. C., Separation Logic: A Logic for Shared Mutable Data Structures, in: Proc. of the 17th IEEE Symposium on Logic in Computer Science (LICS'02), Copenhagen, Denmark, 2002.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB25","first-page":"21","article-title":"Theorem-proving with Resolution and Superposition","volume":"11","author":"Rusinowitch","year":"1991","journal-title":"JSC"},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB26","unstructured":"Schulz S., E-a brainiac theorem prover, AI Communications (2002)."},{"key":"10.1016\/S1571-0661(04)80656-X_NEWBIB27","series-title":"Hand. of Automated Reasoning","article-title":"Small clause normal form","author":"Weidenbach","year":"2001"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480656X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480656X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T10:53:07Z","timestamp":1549191187000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610480656X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S157106610480656X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80656-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}