{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:02Z","timestamp":1763468162763,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T00:00:00Z","timestamp":1379289600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,9,16]]},"DOI":"10.1145\/2505879.2505901","type":"proceedings-article","created":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T19:57:05Z","timestamp":1379447825000},"page":"193-204","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Theory propagation and rational-trees"],"prefix":"10.1145","author":[{"given":"Ed","family":"Robbins","sequence":"first","affiliation":[{"name":"University of Kent"}]},{"given":"Jacob M.","family":"Howe","sequence":"additional","affiliation":[{"name":"City University London"}]},{"given":"Andy","family":"King","sequence":"additional","affiliation":[{"name":"University of Kent"}]}],"member":"320","published-online":{"date-parts":[[2013,9,16]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Resolution Proof for Look-ahead SAT Solvers","author":"Anoep S.","year":"2006","unstructured":"S. Anoep , E. Drijver , A. Ganga , and M. Kirsten . Resolution Proof for Look-ahead SAT Solvers . 2006 . www.st.ewi.tudelft.nl\/sat\/reports\/resolution.pdf. S. Anoep, E. Drijver, A. Ganga, and M. Kirsten. Resolution Proof for Look-ahead SAT Solvers. 2006. www.st.ewi.tudelft.nl\/sat\/reports\/resolution.pdf."},{"key":"e_1_3_2_1_2_1","volume-title":"Recovery of Variables and Heap Structure in x86 Executables. Technical report","author":"Balakrishnan G.","year":"2005","unstructured":"G. Balakrishnan and T. Reps . Recovery of Variables and Heap Structure in x86 Executables. Technical report , University of Wisconsin , 2005 . G. Balakrishnan and T. Reps. Recovery of Variables and Heap Structure in x86 Executables. Technical report, University of Wisconsin, 2005."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190039"},{"key":"e_1_3_2_1_4_1","first-page":"358","volume-title":"Bylands: Reverse Engineering Safety-critical Systems. In International Conference on Software Maintenance","author":"Bull T.","year":"1995","unstructured":"T. Bull , E. Younger , K. Bennett , and Z. Luo . Bylands: Reverse Engineering Safety-critical Systems. In International Conference on Software Maintenance , pages 358 -- 366 . IEEE Computer Society , 1995 . T. Bull, E. Younger, K. Bennett, and Z. Luo. Bylands: Reverse Engineering Safety-critical Systems. In International Conference on Software Maintenance, pages 358--366. IEEE Computer Society, 1995."},{"key":"e_1_3_2_1_5_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BFb0033845","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"Carlsson M.","year":"1997","unstructured":"M. Carlsson , G. Ottosson , and B. Carlson . An Open-Ended Finite Domain Constraint Solver . In Programming Languages: Implementations, Logics, and Programs , volume 1292 of Lecture Notes in Computer Science , pages 191 -- 206 . Springer , 1997 . M. Carlsson, G. Ottosson, and B. Carlson. An Open-Ended Finite Domain Constraint Solver. In Programming Languages: Implementations, Logics, and Programs, volume 1292 of Lecture Notes in Computer Science, pages 191--206. Springer, 1997."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93585"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755913.1755932"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068407003146"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455820"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_12_1","series-title":"LIPIcs","first-page":"301","volume-title":"ICLP (Technical Communications)","author":"Drabent W.","year":"2012","unstructured":"W. Drabent . Logic + Control : An Example . In ICLP (Technical Communications) , volume 17 of LIPIcs , pages 301 -- 311 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 2012 . W. Drabent. Logic + Control: An Example. In ICLP (Technical Communications), volume 17 of LIPIcs, pages 301--311. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2012."},{"key":"e_1_3_2_1_13_1","first-page":"603","volume-title":"Conference on Computer Communications","author":"Guha B.","year":"1996","unstructured":"B. Guha , C. Davis , and B. Mukherjee . Network Security via Reverse Rngineering of TCP code: Vulnerability Analysis and Proposed Solutions . In Conference on Computer Communications , pages 603 -- 610 . IEEE Computer Society , 1996 . B. Guha, C. Davis, and B. Mukherjee. Network Security via Reverse Rngineering of TCP code: Vulnerability Analysis and Proposed Solutions. In Conference on Computer Communications, pages 603--610. IEEE Computer Society, 1996."},{"key":"e_1_3_2_1_14_1","first-page":"631","volume-title":"Using Attributed Variables in the Implementation of Concurrent and Parallel Logic Programming Systems. In International Conference on Logic Programming","author":"Hermenegildo M.","year":"1995","unstructured":"M. Hermenegildo , D. Cabeza , and M. Carro . Using Attributed Variables in the Implementation of Concurrent and Parallel Logic Programming Systems. In International Conference on Logic Programming , pages 631 -- 645 . MIT Press , 1995 . M. Hermenegildo, D. Cabeza, and M. Carro. Using Attributed Variables in the Implementation of Concurrent and Parallel Logic Programming Systems. In International Conference on Logic Programming, pages 631--645. MIT Press, 1995."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/646448.692447"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/645521.656282"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068402001485"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_13"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.02.024"},{"key":"e_1_3_2_1_20_1","volume-title":"Universit\u00e9 Paris VII","author":"Huet G.","year":"1976","unstructured":"G. Huet . R\u00e9solution d' \u00e9quations dans les langages d'ordre 1, 2,..., \u03c9. PhD thesis , Universit\u00e9 Paris VII , 1976 . G. Huet. R\u00e9solution d'\u00e9quations dans les langages d'ordre 1, 2,..., \u03c9. PhD thesis, Universit\u00e9 Paris VII, 1976."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037057"},{"key":"e_1_3_2_1_22_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1007\/978-3-642-04244-7_37","volume-title":"Constraint Programming","author":"Jaffar J.","year":"2009","unstructured":"J. Jaffar , A. E. Santosa , and R. Voicu . An Interpolation Method for CLP Traversal . In Constraint Programming , volume 5732 of Lecture Notes in Computer Science , pages 454 -- 469 . Springer , 2009 . J. Jaffar, A. E. Santosa, and R. Voicu. An Interpolation Method for CLP Traversal. In Constraint Programming, volume 5732 of Lecture Notes in Computer Science, pages 454--469. Springer, 2009."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531077"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647196.720988"},{"issue":"1","key":"e_1_3_2_1_25_1","first-page":"100","article-title":"Analysis of Executables: Benefits and Challenges (Dagstuhl Seminar 12051)","volume":"2","author":"King A.","year":"2012","unstructured":"A. King , A. Mycroft , T. W. Reps , and A. Simon . Analysis of Executables: Benefits and Challenges (Dagstuhl Seminar 12051) . Dagstuhl Reports , 2 ( 1 ): 100 -- 116 , 2012 . A. King, A. Mycroft, T. W. Reps, and A. Simon. Analysis of Executables: Benefits and Challenges (Dagstuhl Seminar 12051). Dagstuhl Reports, 2(1):100--116, 2012.","journal-title":"Dagstuhl Reports"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/359131.359136"},{"key":"e_1_3_2_1_27_1","volume-title":"Decision Procedures","author":"Kroening D.","year":"2008","unstructured":"D. Kroening and O. Strichman . Decision Procedures . Springer , 2008 . D. Kroening and O. Strichman. Decision Procedures. Springer, 2008."},{"key":"e_1_3_2_1_28_1","volume-title":"TIE: Principled Reverse Engineering of Types in Binary Programs. In Network and Distributed System Security Symposium. The Internet Society","author":"Lee J.","year":"2011","unstructured":"J. Lee , T. Avgerinos , and D. Brumley . TIE: Principled Reverse Engineering of Types in Binary Programs. In Network and Distributed System Security Symposium. The Internet Society , 2011 . J. Lee, T. Avgerinos, and D. Brumley. TIE: Principled Reverse Engineering of Types in Binary Programs. In Network and Distributed System Security Symposium. The Internet Society, 2011."},{"key":"e_1_3_2_1_29_1","series-title":"Lecture Notes in Computer Science","first-page":"341","volume-title":"Constraint Programming","author":"Li C. M.","year":"1997","unstructured":"C. M. Li and Anbulagan. Look-Ahead Versus Look-Back for Satisfiability Problems . In Constraint Programming , volume 1330 of Lecture Notes in Computer Science , pages 341 -- 355 . Springer , 1997 . C. M. Li and Anbulagan. Look-Ahead Versus Look-Back for Satisfiability Problems. In Constraint Programming, volume 1330 of Lecture Notes in Computer Science, pages 341--355. Springer, 1997."},{"key":"e_1_3_2_1_30_1","volume-title":"Network and Distributed System Security Symposium. The Internet Society","author":"Lin Z.","year":"2010","unstructured":"Z. Lin , X. Zhang , and D. Xu . Automatic Reverse Engineering of Data Structures from Binary Execution . In Network and Distributed System Security Symposium. The Internet Society , 2010 . Z. Lin, X. Zhang, and D. Xu. Automatic Reverse Engineering of Data Structures from Binary Execution. In Network and Distributed System Security Symposium. The Internet Society, 2010."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800528"},{"key":"e_1_3_2_1_32_1","first-page":"348","volume-title":"Rational and Infinite Trees. In Logic in Computer Science","author":"Maher M. J.","year":"1988","unstructured":"M. J. Maher . Complete Axiomatizations of the Algebras of Finite , Rational and Infinite Trees. In Logic in Computer Science , pages 348 -- 357 . IEEE Computer Society , 1988 . M. J. Maher. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In Logic in Computer Science, pages 348--357. IEEE Computer Society, 1988."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024569.2024572"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_35_1","volume-title":"European Symposium on Programming","volume":"1576","author":"Mycroft A.","year":"1999","unstructured":"A. Mycroft . Type-Based Decompilation (or Program Reconstruction via Type Reconstruction). In European Symposium on Programming , volume 1576 of Lecture Notes in Computer Science, pages 208--223. Springer , 1999 . A. Mycroft. Type-Based Decompilation (or Program Reconstruction via Type Reconstruction). In European Symposium on Programming, volume 1576 of Lecture Notes in Computer Science, pages 208--223. Springer, 1999."},{"key":"e_1_3_2_1_36_1","series-title":"Lecture Notes in Computer Science","volume-title":"Negation and Control in Logic Programs","author":"Naish L.","year":"1986","unstructured":"L. Naish . Negation and Control in Logic Programs , volume 238 of Lecture Notes in Computer Science . Springer , 1986 . L. Naish. Negation and Control in Logic Programs, volume 238 of Lecture Notes in Computer Science. Springer, 1986."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_33"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292553"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.27"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008725524946"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_23"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/646333.687633"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734434"}],"event":{"name":"PPDP '13: 15th International Symposium on Principles and Practice of Declarative Programming","sponsor":["Universidad Complutense de Madrid","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Madrid Spain","acronym":"PPDP '13"},"container-title":["Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2505879.2505901","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2505879.2505901","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:17Z","timestamp":1750232057000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2505879.2505901"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,16]]},"references-count":44,"alternative-id":["10.1145\/2505879.2505901","10.1145\/2505879"],"URL":"https:\/\/doi.org\/10.1145\/2505879.2505901","relation":{},"subject":[],"published":{"date-parts":[[2013,9,16]]},"assertion":[{"value":"2013-09-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}