{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T08:50:52Z","timestamp":1729673452181,"version":"3.28.0"},"reference-count":23,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,7]]},"DOI":"10.1109\/memcod.2010.5558625","type":"proceedings-article","created":{"date-parts":[[2010,8,27]],"date-time":"2010-08-27T14:37:22Z","timestamp":1282919842000},"page":"41-48","source":"Crossref","is-referenced-by-count":2,"title":["A flexible schema for generating explanations in lazy theory propagation"],"prefix":"10.1109","author":[{"given":"Roberto","family":"Bruttomesso","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edgar","family":"Pek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_19"},{"key":"ref11","first-page":"337","article-title":"Z3: An Efficient SMT Solver","author":"de moura","year":"2008","journal-title":"TACAS'08"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"ref13","article-title":"The Yices SMT Solver","author":"dutertre","year":"0","journal-title":"Tool paper"},{"key":"ref14","first-page":"502","article-title":"An Extensible SAT-Solver","author":"e\u00e9n","year":"2003","journal-title":"Proc Theory Applications Satisfiability Testing (SAT)"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.13"},{"key":"ref16","article-title":"Decision procedures an algorithmic point of view","author":"kroening","year":"2008","journal-title":"Theoretical Computer Science"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP: A Search Algorithm for Propositional Satisfiability","volume":"48","author":"marques-silva","year":"1999","journal-title":"IEEE Transactions on Computers"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_33"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"ref4","volume":"185","author":"barrett","year":"2009","journal-title":"Handbook on Satisfiability"},{"key":"ref3","article-title":"A SAT-Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions","author":"audemard","year":"2002","journal-title":"Proc of CADE'02"},{"key":"ref6","first-page":"294","article-title":"The Barcelogic SMT Solver","volume":"5123","author":"bofill","year":"2008","journal-title":"CAV 08"},{"journal-title":"CAV'07","year":"2007","author":"barrett","key":"ref5"},{"key":"ref8","first-page":"299","article-title":"The MathSAT 4 SMT Solver","author":"bruttomesso","year":"2008","journal-title":"CAV"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_21"},{"key":"ref2","first-page":"97","article-title":"SAT-Based Decision Procedures for Temporal Reasoning","author":"armando","year":"1999","journal-title":"ECP"},{"journal-title":"SMT-Comp","year":"0","key":"ref1"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_12"},{"year":"0","key":"ref20"},{"key":"ref22","first-page":"144","article-title":"Lazy Satisfiability Modulo Theories","volume":"3","author":"sebastiani","year":"2007","journal-title":"JSAT"},{"journal-title":"The Satisfiability Modulo Theories Library (SMT-LIB)","year":"2006","author":"ranise","key":"ref21"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_12"}],"event":{"name":"2010 8th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010)","start":{"date-parts":[[2010,7,26]]},"location":"Grenoble, France","end":{"date-parts":[[2010,7,28]]}},"container-title":["Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5550962\/5558619\/05558625.pdf?arnumber=5558625","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T13:11:02Z","timestamp":1497877862000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5558625\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":23,"URL":"https:\/\/doi.org\/10.1109\/memcod.2010.5558625","relation":{},"subject":[],"published":{"date-parts":[[2010,7]]}}}