{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T22:46:56Z","timestamp":1768258016661,"version":"3.49.0"},"publisher-location":"Cham","reference-count":79,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_25","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"831-870","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Symbolic Trajectory Evaluation"],"prefix":"10.1007","author":[{"given":"Tom","family":"Melham","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"25_CR1","series-title":"LNCS","first-page":"263","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"M.D. Aagaard","year":"2000","unstructured":"Aagaard, M.D., Jones, R.B., Melham, T.F., O\u2019Leary, J.W., Seger, C.J.H.: A methodology for large-scale hardware verification. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol.\u00a01954, pp.\u00a0263\u2013282. Springer, Heidelberg (2000)"},{"key":"25_CR2","first-page":"538","volume-title":"Design Automation Conf. (DAC)","author":"M.D. Aagaard","year":"1998","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Combining theorem proving and trajectory evaluation in an industrial environment. In: Design Automation Conf. (DAC), pp.\u00a0538\u2013541. IEEE, Piscataway (1998)"},{"key":"25_CR3","first-page":"402","volume-title":"Design Automation Conf. (DAC)","author":"M.D. Aagaard","year":"1999","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Formal verification using parametric representations of Boolean constraints. In: Design Automation Conf. (DAC), pp.\u00a0402\u2013407. ACM, New York (1999)"},{"key":"25_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-48256-3_22","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs)","author":"M.D. Aagaard","year":"1999","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Lifted-FL: a pragmatic implementation of combined model checking and theorem proving. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol.\u00a01690, pp.\u00a0323\u2013340. Springer, Heidelberg (1999)"},{"key":"25_CR5","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1109\/FAMCAD.2007.27","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"S. Adams","year":"2007","unstructured":"Adams, S., Bj\u00f6rk, M., Melham, T., Seger, C.J.: Automatic abstraction in symbolic trajectory evaluation. In: Baumgartner, J., Sheeran, M. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0127\u2013135. IEEE, Piscataway (2007)"},{"key":"25_CR6","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T. Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. Int. J. Softw. Tools Technol. Transf. 5, 49\u201358 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"25_CR7","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/196244.196575","volume-title":"Design Automation Conf. (DAC)","author":"D.L. Beatty","year":"1994","unstructured":"Beatty, D.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: Design Automation Conf. (DAC), pp.\u00a0596\u2013602. ACM, New York (1994)"},{"issue":"2","key":"25_CR8","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Form. Methods Syst. Des. 18(2), 141\u2013162 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"25_CR9","unstructured":"Berkeley Logic Synthesis and Verification Group: ABC: a system for sequential synthesis and verification. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1109\/HLDVT.2001.972820","volume-title":"High-Level Design Validation and Test Workshop","author":"J. Bhadra","year":"2001","unstructured":"Bhadra, J., Martin, A., Abraham, J., Abadir, M.: A language formalism for verification of PowerPC custom memories using compositions of abstract specifications. In: High-Level Design Validation and Test Workshop, pp.\u00a0134\u2013141. IEEE, Piscataway (2001)"},{"key":"25_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/3-540-44798-9_30","volume-title":"Correct Hardware Design and Verification Methods (CHARME)","author":"J. Bhadra","year":"2001","unstructured":"Bhadra, J., Martin, A.K., Abraham, J.A., Abadir, M.S.: Using abstract specifications to verify PowerPC custom memories by symbolic trajectory evaluation. In: Correct Hardware Design and Verification Methods (CHARME). LNCS, vol.\u00a01690, pp.\u00a0386\u2013402. Springer, Heidelberg (2001)"},{"key":"25_CR12","volume-title":"Introduction to Functional Programming using Haskell","author":"R. Bird","year":"1998","unstructured":"Bird, R.: Introduction to Functional Programming using Haskell, 2nd edn. Prentice Hall, New York (1998)","edition":"2"},{"issue":"1","key":"25_CR13","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1109\/43.62795","volume":"10","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E.: Formal verification of memory circuits by switch-level simulation. Trans. Comput.-Aided Des. Integr. Circuits Syst. 10(1), 94\u2013102 (1991)","journal-title":"Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"issue":"2","key":"25_CR14","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/103516.103519","volume":"38","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E.: A methodology for hardware verification based on logic simulation. J. ACM 38(2), 299\u2013328 (1991)","journal-title":"J. ACM"},{"key":"25_CR15","first-page":"9","volume-title":"Design Automation Conf. (DAC)","author":"R.E. Bryant","year":"1987","unstructured":"Bryant, R.E., Beatty, D., Brace, K., Cho, K., Sheffler, T.: COSMOS: a compiled simulator for MOS circuits. In: Design Automation Conf. (DAC), pp.\u00a09\u201316. ACM, New York (1987)"},{"key":"25_CR16","first-page":"297","volume-title":"Design Automation Conf. (DAC)","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E., Beatty, D.E., Seger, C.J.H.: Formal hardware verification by symbolic ternary trajectory evaluation. In: Design Automation Conf. (DAC), pp.\u00a0297\u2013402. IEEE, Piscataway (1991)"},{"key":"25_CR17","first-page":"43","volume-title":"From HDL Descriptions to Guaranteed Correct Circuit Designs","author":"A. Camilleri","year":"1987","unstructured":"Camilleri, A., Gordon, M., Melham, T.: Hardware verification using higher-order logic. In: Borrione, D. (ed.) From HDL Descriptions to Guaranteed Correct Circuit Designs, pp.\u00a043\u201367. North-Holland, Amsterdam (1987)"},{"key":"25_CR18","series-title":"LNCS","first-page":"233","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"H. Chockler","year":"2008","unstructured":"Chockler, H., Grumberg, O., Yadgar, A.: Efficient automatic STE refinement using responsibility. In: Ramakrishnan, R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04963, pp.\u00a0233\u2013248. Springer, Heidelberg (2008)"},{"key":"25_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-48683-6_19","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"C.T. Chou","year":"1999","unstructured":"Chou, C.T.: The mathematical foundation of symbolic trajectory evaluation. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01633, pp.\u00a0196\u2013207. Springer, Heidelberg (1999)"},{"key":"25_CR20","series-title":"LNCS","first-page":"56","volume-title":"International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM)","author":"K. Claessen","year":"2006","unstructured":"Claessen, K., Roorda, J.W.: An introduction to symbolic trajectory evaluation. In: International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM). LNCS, vol.\u00a03965, pp.\u00a056\u201377. Springer, Heidelberg (2006)"},{"issue":"2","key":"25_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-5(2:1)2009","volume":"5","author":"K. Claessen","year":"2009","unstructured":"Claessen, K., Roorda, J.W.: A faithful semantics for generalised symbolic trajectory evaluation. Log. Methods Comput. Sci. 5(2), 1\u201332 (2009)","journal-title":"Log. Methods Comput. Sci."},{"key":"25_CR22","first-page":"343","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"E.M. Clarke","year":"1992","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0343\u2013354. ACM, New York (1992)"},{"key":"25_CR23","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"25_CR24","volume-title":"Introduction to Lattices and Order","author":"B.A. Davey","year":"1990","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"key":"25_CR25","unstructured":"Een, N.: ABC\/ZZ. https:\/\/bitbucket.org\/niklaseen\/abc-zz"},{"key":"25_CR26","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/FAMCAD.2007.38","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"A. Flaisher","year":"2007","unstructured":"Flaisher, A., Gluska, A., Singerman, E.: Case study: integrating FV and DV in the verification of the Intel Core 2 Duo microprocessor. In: Baumgartner, J., Sheeran, M. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0192\u2013195. IEEE, Piscataway (2007)"},{"key":"25_CR27","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"25_CR28","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11804192_11","volume-title":"Formal Methods for Components and Objects","author":"O. Grumberg","year":"2006","unstructured":"Grumberg, O.: Abstraction and refinement in model checking. In: de Boer, F., Bonsangue, M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects. LNCS, vol.\u00a04111, pp.\u00a0219\u2013242. Springer, Heidelberg (2006)"},{"key":"25_CR29","volume-title":"Naive Set Theory","author":"P.R. Halmos","year":"1987","unstructured":"Halmos, P.R.: Naive Set Theory. Springer, Heidelberg (1987)"},{"key":"25_CR30","unstructured":"Hazelhurst, S.: Compositional model checking of partially ordered state spaces. Technical report 96-02, Department of Computer Science, University of British, Columbia (1996)"},{"issue":"4","key":"25_CR31","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1109\/43.372367","volume":"14","author":"S. Hazelhurst","year":"1995","unstructured":"Hazelhurst, S., Seger, C.J.H.: A simple theorem prover based on symbolic trajectory evaluation and BDDs. Trans. Comput.-Aided Des. Integr. Circuits Syst. 14(4), 413\u2013422 (1995)","journal-title":"Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"25_CR32","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-63475-4_1","volume-title":"Formal Hardware Verification","author":"S. Hazelhurst","year":"1997","unstructured":"Hazelhurst, S., Seger, C.J.H.: Symbolic trajectory evaluation. In: Kropf, T. (ed.) Formal Hardware Verification, pp.\u00a03\u201378. Springer, Heidelberg (1997). Chap.\u00a01"},{"issue":"3","key":"25_CR33","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/PGEC.1963.263531","volume":"EC-12","author":"L. Hellerman","year":"1963","unstructured":"Hellerman, L.: A catalog of three-variable or-invert and and-invert logical circuits. Trans. Electron. Comput. EC-12(3), 198\u2013223 (1963)","journal-title":"Trans. Electron. Comput."},{"key":"25_CR34","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-1-4419-1539-9_3","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"W.A. Hunt Jr.","year":"2010","unstructured":"Hunt, W.A. Jr., Swords, S., Davis, J., Slobodova, A.: Use of formal verification at Centaur Technology. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp.\u00a065\u201388. Springer, Heidelberg (2010)"},{"key":"25_CR35","unstructured":"Jain, A.: Formal hardware verification by symbolic trajectory evaluation. Ph.D. thesis, Carnegie Mellon University (1997)"},{"issue":"11","key":"25_CR36","doi-asserted-by":"publisher","first-page":"1005","DOI":"10.1109\/43.298036","volume":"13","author":"P. Jain","year":"1994","unstructured":"Jain, P., Gopalakrishnan, G.: Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. Trans. Comput.-Aided Des. Integr. Circuits Syst. 13(11), 1005\u20131015 (1994)","journal-title":"Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"25_CR37","unstructured":"Jones, R.B.: Applications of symbolic simulation to the formal verification of microprocessors. Ph.D. thesis, Department of Electrical Engineering, Stanford University (1999)"},{"issue":"4","key":"25_CR38","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1109\/54.936245","volume":"18","author":"R.B. Jones","year":"2001","unstructured":"Jones, R.B., O\u2019Leary, J.W., Seger, C.J.H., Aagaard, M.D., Melham, T.F.: Practical formal verification in microprocessor design. IEEE Des. Test Comput. 18(4), 16\u201325 (2001)","journal-title":"IEEE Des. Test Comput."},{"key":"25_CR39","first-page":"469","volume-title":"Design Automation Conf. (DAC)","author":"J. Joyce","year":"1993","unstructured":"Joyce, J., Seger, C.J.: Linking BDD-based symbolic evaluation to interactive theorem-proving. In: Design Automation Conf. (DAC), pp.\u00a0469\u2013474. IEEE, Piscataway (1993)"},{"key":"25_CR40","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11513988_19","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Kaivola","year":"2005","unstructured":"Kaivola, R.: Formal verification of Pentium\u00ae 4 components with symbolic simulation and inductive invariants. In: Etessami, K., Rajamani, S.K. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03576, pp.\u00a0170\u2013184. Springer, Heidelberg (2005)"},{"key":"25_CR41","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-02658-4_32","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Kaivola","year":"2009","unstructured":"Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodova, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing testing with formal verification in Intel Core i7 processor execution engine validation. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, pp.\u00a0414\u2013429. Springer, Heidelberg (2009)"},{"issue":"3","key":"25_CR42","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s10009-002-0081-6","volume":"4","author":"R. Kaivola","year":"2003","unstructured":"Kaivola, R., Kohatsu, K.R.: Proof engineering in the large: formal verification of Pentium 4 floating-point divider. Int. J. Softw. Tools Technol. Transf. 4(3), 323\u2013334 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"25_CR43","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common Lisp. Trans. Softw. Eng. 23(4), 203\u2013213 (1997)","journal-title":"Trans. Softw. Eng."},{"key":"25_CR44","first-page":"108","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"Z. Khasidashvili","year":"2009","unstructured":"Khasidashvili, Z., Gavrielov, G., Melham, T.: Assume-guarantee validation for STE properties within an SVA environment. In: Biere, A., Pixley, C. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0108\u2013115. IEEE, Piscataway (2009)"},{"issue":"4","key":"25_CR45","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/54.895007","volume":"17","author":"N. Krishnamurthy","year":"2000","unstructured":"Krishnamurthy, N., Martin, A.K., Abadir, M.S., Abraham, J.A.: Validating PowerPC custom memories. IEEE Des. Test Comput. 17(4), 61\u201376 (2000)","journal-title":"IEEE Des. Test Comput."},{"key":"25_CR46","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569845","volume-title":"Higher Order Logic and Hardware Verification","author":"T. Melham","year":"1993","unstructured":"Melham, T.: Higher Order Logic and Hardware Verification. Cambridge University Press, Cambridge (1993)"},{"key":"25_CR47","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-36126-X_1","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"T.F. Melham","year":"2002","unstructured":"Melham, T.F., Jones, R.B.: Abstraction by symbolic indexing transformations. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol.\u00a02517, pp.\u00a01\u201318. Springer, Heidelberg (2002)"},{"key":"25_CR48","first-page":"161","volume-title":"Design Automation Conf. (DAC)","author":"K.L. Nelson","year":"1997","unstructured":"Nelson, K.L., Jain, A., Bryant, R.E.: Formal verification of a superscalar execution unit. In: Design Automation Conf. (DAC), pp.\u00a0161\u2013166. ACM, New York (1997)"},{"key":"25_CR49","first-page":"409","volume-title":"Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD)","author":"K. Ng","year":"2004","unstructured":"Ng, K., Hu, A.J., Yang, J.: Generating monitor circuits for simulation-friendly GSTE assertion graphs. In: Grochowski, E., Dillinger, T. (eds.) Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD), pp.\u00a0409\u2013416. IEEE, Piscataway (2004)"},{"issue":"11","key":"25_CR50","doi-asserted-by":"publisher","first-page":"2068","DOI":"10.1109\/TCAD.2008.2006092","volume":"27","author":"M.D. Nguyen","year":"2008","unstructured":"Nguyen, M.D., Thalmaier, M., Wedler, M., Bormann, J., Stoffel, D., Kunz, W.: Unbounded protocol compliance verification using interval property checking with invariants. Trans. Comput.-Aided Des. Integr. Circuits Syst. 27(11), 2068\u20132082 (2008)","journal-title":"Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"25_CR51","first-page":"97","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"J. O\u2019Leary","year":"2013","unstructured":"O\u2019Leary, J., Kaivola, R., Melham, T.: Relational STE and theorem proving for formal verification of industrial circuit designs. In: Jobstmann, B., Ray, S. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a097\u2013104. IEEE, Piscataway (2013)"},{"key":"25_CR52","first-page":"167","volume-title":"Design Automation Conf. (DAC)","author":"M. Pandey","year":"1997","unstructured":"Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. In: Design Automation Conf. (DAC), pp.\u00a0167\u2013172. ACM, New York (1997)"},{"key":"25_CR53","doi-asserted-by":"crossref","unstructured":"Roorda, J.W.: Semantics, decision procedures, and abstraction refinement for symbolic trajectory evaluation. Ph.D. thesis, Chalmers University of Technology and G\u00f6teborg Universty (2006)","DOI":"10.1007\/11817963_19"},{"key":"25_CR54","series-title":"LNCS","first-page":"555","volume-title":"International Computer Science Symposium in Russia (CSR)","author":"J.W. Roorda","year":"2006","unstructured":"Roorda, J.W., Claessen, K.: Explaining symbolic trajectory evaluation by giving it a faithful semantics. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) International Computer Science Symposium in Russia (CSR). LNCS, vol.\u00a03967, pp.\u00a0555\u2013566. Springer, Heidelberg (2006)"},{"key":"25_CR55","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/11817963_19","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"J.W. Roorda","year":"2006","unstructured":"Roorda, J.W., Claessen, K.: SAT-based assistance in abstraction refinement for symbolic trajectory evaluation. In: Intl. Conf. on Computer-Aided Verification (CAV), pp.\u00a0175\u2013189. Springer, Heidelberg (2006)"},{"key":"25_CR56","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"M. Ryan","year":"1992","unstructured":"Ryan, M., Sadler, M.: Valuation systems and consequent relations. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol.\u00a01, pp.\u00a01\u201378. Oxford University Press, Oxford (1992). Chap.\u00a01"},{"key":"25_CR57","unstructured":"Santarini, M.: Synopsys extends formal reach with InnoLogic acquisition. EE Times (2003). www.eetimes.com\/document.asp?doc_id=1216962"},{"key":"25_CR58","first-page":"1","volume-title":"Design Automation Conf. (DAC)","author":"T. Schubert","year":"2003","unstructured":"Schubert, T.: High level formal verification of next-generation microprocessors. In: Design Automation Conf. (DAC), pp.\u00a01\u20136. ACM, New York (2003)"},{"issue":"2","key":"25_CR59","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s10703-007-0036-3","volume":"31","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani, R., Singerman, E., Tonetta, S., Vardi, M.Y.: GSTE is partitioned model checking. Form. Methods Syst. Des. 31(2), 177\u2013196 (2007)","journal-title":"Form. Methods Syst. Des."},{"key":"25_CR60","series-title":"LNCS","first-page":"389","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani, R., Tonetta, S., Vardi, M.: Property-driven partitioning for abstraction refinement. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04424, pp.\u00a0389\u2013404. Springer, Heidelberg (2007)"},{"key":"25_CR61","unstructured":"Seger, C.J., Joyce, J.: A mathematically precise two-level formal hardware verification methodology. Report 92-34, Department of Computer Science, University of British, Columbia (1992)"},{"key":"25_CR62","unstructured":"Seger, C.J.H.: Voss\u2014a formal hardware verification system: user\u2019s guide. Tech. Rep. TR-93-45, University of British Columbia, Department of Computer Science (1993)"},{"key":"25_CR63","unstructured":"Seger, C.J.H.: Personal communication (2014)"},{"issue":"2","key":"25_CR64","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.J.H. Seger","year":"1995","unstructured":"Seger, C.J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Form. Methods Syst. Des. 6(2), 147\u2013189 (1995)","journal-title":"Form. Methods Syst. Des."},{"issue":"9","key":"25_CR65","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"C.J.H. Seger","year":"2005","unstructured":"Seger, C.J.H., Jones, R.B., O\u2019Leary, J.W., Melham, T., Aagaard, M.D., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. Trans. Comput.-Aided Des. Integr. Circuits Syst. 24(9), 1381\u20131405 (2005)","journal-title":"Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"25_CR66","first-page":"89","volume-title":"International Conference on Formal Methods and Models for Codesign","author":"A. Slobodov\u00e1","year":"2011","unstructured":"Slobodov\u00e1, A., Davis, J., Swords, S., Hunt, W.: A flexible formal verification framework for industrial scale validation. In: International Conference on Formal Methods and Models for Codesign, pp.\u00a089\u201397. IEEE, Piscataway (2011)"},{"key":"25_CR67","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1109\/FAMCAD.2007.36","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"E. Smith","year":"2007","unstructured":"Smith, E.: A logic for GSTE. In: Baumgartner, J., Sheeran, M. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0119\u2013126. IEEE, Piscataway (2007)"},{"key":"25_CR68","unstructured":"Smith, E.: Specifying properties for generalized symbolic trajectory evaluation. Ph.D. thesis, University of Oxford (2008)"},{"key":"25_CR69","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/11817963_20","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Tzoref","year":"2006","unstructured":"Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0190\u2013204. Springer, Heidelberg (2006)"},{"key":"25_CR70","series-title":"LNCS","first-page":"136","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M.N. Velev","year":"1998","unstructured":"Velev, M.N., Bryant, R.E.: Efficient modeling of memory arrays in symbolic ternary simulation. In: Steffen, B. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01384, pp.\u00a0136\u2013150. Springer, Heidelberg (1998)"},{"key":"25_CR71","first-page":"534","volume-title":"Design Automation Conf. (DAC)","author":"L.C. Wang","year":"1998","unstructured":"Wang, L.C., Abadir, M.S., Krishnamurthy, N.: Automatic generation of assertions for formal verification of PowerPC microprocessor arrays using symbolic trajectory evaluation. In: Design Automation Conf. (DAC), pp.\u00a0534\u2013537. IEEE, Piscataway (1998)"},{"key":"25_CR72","first-page":"930","volume-title":"International Conference on ASIC (ASICON)","author":"J. Yang","year":"2005","unstructured":"Yang, J., Ghughal, R., Tiemeyer, A.: Industrial scale formal verification using concurrent GSTE. In: Tang, T.A., Huang, Y. (eds.) International Conference on ASIC (ASICON), pp.\u00a0930\u2013933. IEEE, Piscataway (2005)"},{"key":"25_CR73","first-page":"534","volume-title":"International Conference on Computer Aided Design (ICCAD)","author":"J. Yang","year":"2002","unstructured":"Yang, J., Goel, A.: GSTE through a case study. In: Pileggi, L., Kuelmann, A. (eds.) International Conference on Computer Aided Design (ICCAD), pp.\u00a0534\u2013541. ACM, New York (2002)"},{"key":"25_CR74","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/3-540-36126-X_5","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"J. Yang","year":"2002","unstructured":"Yang, J., Seger, C.H.: Generalized symbolic trajectory evaluation\u2014abstraction in action. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol.\u00a02517, pp.\u00a070\u201387. Springer, Heidelberg (2002)"},{"key":"25_CR75","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-27813-9_17","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"J. Yang","year":"2004","unstructured":"Yang, J., Seger, C.J.: Compositional specification and model checking in GSTE. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03114, pp.\u00a0216\u2013228. Springer, Heidelberg (2004)"},{"key":"25_CR76","unstructured":"Yang, J., Seger, C.J.H.: Generalized symbolic trajectory evaluation. Tech. rep., Intel Strategic CAD Labs (2000)"},{"issue":"3","key":"25_CR77","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1109\/TVLSI.2003.812320","volume":"11","author":"J. Yang","year":"2003","unstructured":"Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. Trans. Very Large Scale Integr. (VLSI) Syst. 11(3), 345\u2013353 (2003)","journal-title":"Trans. Very Large Scale Integr. (VLSI) Syst."},{"key":"25_CR78","unstructured":"Zhong, J.X.: Circuit simulation using encoding of repetitive subcircuits (2001). US Patent Number 6,865,525"},{"key":"25_CR79","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/3-540-58179-0_62","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"Z. Zhu","year":"1994","unstructured":"Zhu, Z., Seger, C.J.: The completeness of a hardware inference system. In: Dill, D.L. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0818, pp.\u00a0286\u2013298. Springer, Heidelberg (1994)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T05:45:19Z","timestamp":1571377519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":79,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_25","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}