{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:43:35Z","timestamp":1777347815486,"version":"3.51.4"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,6,3]],"date-time":"2011-06-03T00:00:00Z","timestamp":1307059200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,2]]},"DOI":"10.1007\/s10009-011-0204-z","type":"journal-article","created":{"date-parts":[[2011,6,3]],"date-time":"2011-06-03T04:13:12Z","timestamp":1307074392000},"page":"95-108","source":"Crossref","is-referenced-by-count":2,"title":["Selection of formal verification heuristics for parallel execution"],"prefix":"10.1007","volume":"14","author":[{"given":"Georgia Penido","family":"Safe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"suffix":"Jr.","given":"Claudionor","family":"Coelho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luiz Filipe M.","family":"Vieira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Celina Gomes","family":"Do Val","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jose Augusto","family":"Nacif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonio Otavio","family":"Fernandes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,6,3]]},"reference":[{"key":"204_CR1","doi-asserted-by":"crossref","unstructured":"Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L.: An analysis of SAT-based model checking techniques in an industrial environment. In: CHARME: Correct Hardware Design and Verification Methods, pp. 254\u2013268 (2005)","DOI":"10.1007\/11560548_20"},{"key":"204_CR2","doi-asserted-by":"crossref","unstructured":"Amla, N., Kurshan, R.P., McMillan, K.L., Medel, R.: Experimental analysis of different techniques for bounded model checking. In: TACAS: Tools and Algorithms for the Construction and Analysis of Systems, pp. 34\u201348 (2003)","DOI":"10.1007\/3-540-36577-X_4"},{"key":"204_CR3","unstructured":"Bailey, B.: A new vision of scalable verification. http:\/\/www.eetimes.com\/news\/design\/features\/showArticle.jhtml?articleID=18400907 (2004)"},{"key":"204_CR4","doi-asserted-by":"crossref","unstructured":"Cherry, G.A., Qin, S.J.: Multiblock principal component analysis based on a combined index for semiconductor fault detection and diagnosis. In: IEEE Transactions on Semiconductor Manufacturing, vol. 19, pp. 159\u2013172 (2006)","DOI":"10.1109\/TSM.2006.873524"},{"key":"204_CR5","volume-title":"Applied Multiple Regression\/Correlation Analysis for the Behavioral Sciences","author":"J. Cohen","year":"2003","unstructured":"Cohen J., Cohen P., West S.G., Aiken L.S.: Applied Multiple Regression\/Correlation Analysis for the Behavioral Sciences. Lawrence, Erlbaum Associate Publishers, Hillsdale (2003)"},{"key":"204_CR6","doi-asserted-by":"crossref","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Conference on Theory and Applications of Satisfiability Testing, SAT. Lecture Notes in Computer Science, vol. 2919, pp. 502\u2013518. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"204_CR7","volume-title":"Modern Portfolio Theory and Investment Analysis","author":"E.J. Elton","year":"1995","unstructured":"Elton E.J., Gruber M.J.: Modern Portfolio Theory and Investment Analysis. Wiley, New York (1995)"},{"key":"204_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-69167-1","volume-title":"SAT-Based Scalable Formal Verification Solutions","author":"M. Ganai","year":"2007","unstructured":"Ganai M., Gupta A.: SAT-Based Scalable Formal Verification Solutions. Springer, New York (2007)"},{"issue":"12","key":"204_CR9","doi-asserted-by":"publisher","first-page":"1549","DOI":"10.1016\/j.dam.2006.10.007","volume":"155","author":"E. Goldberg","year":"2007","unstructured":"Goldberg E., Novikov Y.: Berkmin: a fast and robust SAT-solver. Discrete Appl. Math. 155(12), 1549\u20131561 (2007)","journal-title":"Discrete Appl. Math."},{"key":"204_CR10","doi-asserted-by":"crossref","unstructured":"Goldstein, L.H., Thigpen, E.L.: SCOAP: Sandia controllability\/observability analysis program. In: 25 Years of DAC: Papers on Twenty-Five Years of Electronic Design Automation, pp. 397\u2013403. ACM, New York (1988)","DOI":"10.1145\/62882.62929"},{"key":"204_CR11","volume-title":"The Elements of Statistical Learning. Springer Series in Statistics","author":"T. Hastie","year":"2001","unstructured":"Hastie T., Tibshirani R., Friedman J.: The Elements of Statistical Learning. Springer Series in Statistics. Springer, New York (2001)"},{"key":"204_CR12","unstructured":"Hum, R.: Static verification needs a parallel approach. http:\/\/www.eetimes.com\/news\/design\/columns\/eda\/showArticle.jhtml?articleID=21800552 (2004)"},{"key":"204_CR13","doi-asserted-by":"crossref","unstructured":"Hutter, F., Babic, D., Hoos, H.H., Hu, A.J.: Boosting verification by automatic tuning of decision procedures. In: FMCAD: Formal Methods in Computer Aided Design, pp. 27\u201334. IEEE Computer Society, Washington, DC (2007)","DOI":"10.1109\/FAMCAD.2007.9"},{"key":"204_CR14","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva J.P., Sakallah K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"204_CR15","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: CAV: Computer-Aided Verification, pp. 250\u2013264 (2002)","DOI":"10.1007\/3-540-45657-0_19"},{"key":"204_CR16","doi-asserted-by":"crossref","unstructured":"Mcmillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: TACAS: Tools and Algorithms for the Construction and Analysis of Systems, pp. 2\u201317. Springer, Berlin (2003)","DOI":"10.1007\/3-540-36577-X_2"},{"key":"204_CR17","unstructured":"Qinghua, P.H.: Fault detection using principal component based k-nearest-neighbor rule. In: AIChe: American Institute of Chemical Engineers\u2014Annual Meeting, Salt Lake City (2007)"},{"key":"204_CR18","unstructured":"Smith, L.I.: A tutorial on principal component analysis. http:\/\/csnet.otago.ac.nz\/cosc453\/student_tutorials\/principal_components.pdf (2002)"},{"key":"204_CR19","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 2.2.0 (1998)"},{"key":"204_CR20","volume-title":"Constrained-Based Verification","author":"J. Yuan","year":"2006","unstructured":"Yuan J., Pixley C., Aziz A.: Constrained-Based Verification. Springer, Berlin (2006)"},{"key":"204_CR21","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: an efficient propositional prover. In: CADE: International Conference on Automated Deduction, pp. 272\u2013275 (1997)","DOI":"10.1007\/3-540-63104-6_28"},{"key":"204_CR22","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: IEEE\/ACM International Conference on Computer-Aided Design, pp. 279\u2013285. IEEE Press, New York (2001)","DOI":"10.1145\/774572.774637"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0204-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0204-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0204-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0204-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T13:14:35Z","timestamp":1637759675000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0204-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6,3]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["204"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0204-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,6,3]]}}}