{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:27:02Z","timestamp":1720625222072},"reference-count":31,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/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":3011,"URL":"https:\/\/2.zoppoz.workers.dev:443\/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":[[2005,5]]},"DOI":"10.1016\/j.entcs.2004.08.061","type":"journal-article","created":{"date-parts":[[2005,5,18]],"date-time":"2005-05-18T13:23:08Z","timestamp":1116422588000},"page":"119-137","source":"Crossref","is-referenced-by-count":17,"special_numbering":"C","title":["Efficient Proof Engines for Bounded Model Checking of Hybrid Systems"],"prefix":"10.1016","volume":"133","author":[{"given":"Martin","family":"Fr\u00e4nzle","sequence":"first","affiliation":[]},{"given":"Christian","family":"Herde","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2004.08.061_bib001","unstructured":"E. \u00c1brah\u00e1m, B. Becker, F. Klaedtke, and M. Steffen. Optimizing bounded model checking for linear hybrid systems. To be submitted to VMCAI '05"},{"key":"10.1016\/j.entcs.2004.08.061_bib002","doi-asserted-by":"crossref","unstructured":"F.A. Aloul, A. Ramani, I.L. Markov, and K.A. Sakallah. Generic ILP versus specialized 0-1 ILP: An update. In Proc. ACM\/IEEE Intl. Conf. Comp.-Aided Design (ICCAD), pages 450\u2013457, Nov. 2002","DOI":"10.1145\/774572.774638"},{"key":"10.1016\/j.entcs.2004.08.061_bib003","series-title":"Proc. of the 18th International Conference on Automated Deduction","first-page":"193","article-title":"A SAT-based approach for solving formulas over boolean and linear mathematical propositions","volume":"volume 2392","author":"Audemard","year":"2002"},{"issue":"4","key":"10.1016\/j.entcs.2004.08.061_bib004","article-title":"Verifying industrial hybrid systems with MathSAT","volume":"89","author":"Audemard","year":"2004","journal-title":"ENTCS"},{"key":"10.1016\/j.entcs.2004.08.061_bib005","unstructured":"L. Baptista, I. Lynce, and J. Marques-Silva. Complete search restart strategies for satisfiability. In Proc. of the IJCAI'01 Workshop on Stochastic Search Algorithms (IJCAI-SSA), August 2001"},{"key":"10.1016\/j.entcs.2004.08.061_bib006","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and A. Stump. Checking satisfiability of first-order formulas by incremental translation to SAT. In 14th International Conference on Computer-Aided Verification, 2002","DOI":"10.1007\/3-540-45657-0_18"},{"key":"10.1016\/j.entcs.2004.08.061_bib007","unstructured":"P. Barth. A Davis-Putnam based enumeration algorithm for linear pseudo-boolean optimization. Technical Report MPI-I-95-2-003, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, 1995"},{"key":"10.1016\/j.entcs.2004.08.061_bib008","series-title":"Hybrid Systems: Computation and Control","first-page":"31","article-title":"Verification of hybrid systems via mathematical programming","volume":"volume 1569","author":"Bemporad","year":"1999"},{"key":"10.1016\/j.entcs.2004.08.061_bib009","series-title":"TACAS'99","article-title":"Symbolic model checking without BDDs","volume":"volume 1579","author":"Biere","year":"1999"},{"issue":"2","key":"10.1016\/j.entcs.2004.08.061_bib010","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1287\/ijoc.9.2.164","article-title":"Finding a useful subset of constraints for analysis in an infeasible linear program","volume":"9","author":"Chinneck","year":"1997","journal-title":"INFORMS Journal on Computing"},{"issue":"2","key":"10.1016\/j.entcs.2004.08.061_bib011","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","article-title":"Locating minimal infeasible constraint sets in linear programs","volume":"3","author":"Chinneck","year":"1991","journal-title":"ORSA Journal on Computing"},{"key":"10.1016\/j.entcs.2004.08.061_bib012","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem proving","volume":"5","author":"Davis","year":"1962","journal-title":"Communications of the ACM"},{"key":"10.1016\/j.entcs.2004.08.061_bib013","series-title":"2nd International Joint Conference on Automated Reasoning","first-page":"218","article-title":"The ICS decision procedures for embedded deduction","volume":"volume 3097","author":"de Moura","year":"2004"},{"key":"10.1016\/j.entcs.2004.08.061_bib014","series-title":"Proceedings of CAV'04","article-title":"An experimental evaluation of ground decision procedures","author":"de Moura","year":"2004"},{"key":"10.1016\/j.entcs.2004.08.061_bib015","unstructured":"L. de Moura, H. Rue\u00df, J. Rushby, and N. Shankar. Embedded deduction with ICS. In B. Martin, editor, HCSS'03\u2014High Confidence Software and Systems Conference, Baltimore, MD, 1-3 April 2003"},{"key":"10.1016\/j.entcs.2004.08.061_bib016","series-title":"Logic for Programming, Artificial Intelligence, and Reasoning","article-title":"Efficient SAT engines for concise logics: Accelerating proof search for zero-one linear constraint systems","volume":"volume 2850","author":"Fr\u00e4nzle","year":"2003"},{"key":"10.1016\/j.entcs.2004.08.061_bib017","series-title":"Compass '95: 10th Annual Conference on Computer Assurance","first-page":"57","article-title":"The safety guaranteeing system at station hoorn-kersenboogerd","author":"Groote","year":"1995"},{"key":"10.1016\/j.entcs.2004.08.061_bib018","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/69610.357988","article-title":"Predicative programming","volume":"27","author":"Hehner","year":"1984","journal-title":"Communications of the ACM"},{"key":"10.1016\/j.entcs.2004.08.061_bib019","series-title":"16th Annual IEEE Real-time Systems Symposium","first-page":"56","article-title":"HyTech: The next generation","author":"Henzinger","year":"1995"},{"key":"10.1016\/j.entcs.2004.08.061_bib020","series-title":"Proceedings of the Twenty-Seventh Annual ACM Symposium on the Theory of Computing","first-page":"373","article-title":"What's decidable about hybrid automata","author":"Henzinger","year":"1995"},{"key":"10.1016\/j.entcs.2004.08.061_bib021","series-title":"Preliminary Proceeding of BMC'04","article-title":"An incremental algorithm to check satisfiability for bounded model checking","author":"Jin","year":"2004"},{"key":"10.1016\/j.entcs.2004.08.061_bib022","doi-asserted-by":"crossref","unstructured":"J.P. Marques-Silva. The impact of branching heuristics in propositional satisfiability algorithms. In Proc. of the 9th Portuguese Conference on Artificial Intelligence (EPIA), Sept. 1999","DOI":"10.1007\/3-540-48159-1_5"},{"issue":"5","key":"10.1016\/j.entcs.2004.08.061_bib023","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":"10.1016\/j.entcs.2004.08.061_bib024","series-title":"Proc. of the 38th Design Automation Conference","article-title":"Chaff: Engineering an Efficient SAT Solver","author":"Moskewicz","year":"2001"},{"key":"10.1016\/j.entcs.2004.08.061_bib025","article-title":"Computing small clause normal forms","author":"Nonnengart","year":"1999"},{"key":"10.1016\/j.entcs.2004.08.061_bib026","series-title":"Computer Aided Verification","first-page":"480","article-title":"Tuning SAT checkers for bounded model checking","volume":"volume 1855","author":"Shtrichman","year":"2000"},{"key":"10.1016\/j.entcs.2004.08.061_bib027","series-title":"Studies in Constructive Mathematics and Mathematical Logics","article-title":"On the complexity of derivations in propositional calculus","author":"Tseitin","year":"1968"},{"issue":"2","key":"10.1016\/j.entcs.2004.08.061_bib028","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","article-title":"A linear-time transformation of linear inequalities into conjunctive normal form","volume":"68","author":"Warners","year":"1998","journal-title":"Information Processing Letters"},{"key":"10.1016\/j.entcs.2004.08.061_bib029","series-title":"Proc. of the Design Automation Conference","first-page":"542","article-title":"SATIRE: A new incremental satisfiability engine","author":"Whittemore","year":"2001"},{"key":"10.1016\/j.entcs.2004.08.061_bib030","series-title":"Proc. 16th International Joint Conference on i Artificial Intelligence","first-page":"310","article-title":"The LPSAT engine & its application to resource planning","author":"Wolfman","year":"1999"},{"key":"10.1016\/j.entcs.2004.08.061_bib031","series-title":"Proc. of the International Conference on Computer-Aided Design","first-page":"279","article-title":"Efficient conflict driven learning in a Boolean satisfiability solver","author":"Zhang","year":"2001"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S1571066105050279?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S1571066105050279?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T10:55:03Z","timestamp":1586256903000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105050279"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":31,"alternative-id":["S1571066105050279"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.entcs.2004.08.061","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2005,5]]}}}