{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:31:01Z","timestamp":1773192661796,"version":"3.50.1"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,3,1]],"date-time":"2005-03-01T00:00:00Z","timestamp":1109635200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2005,3]]},"DOI":"10.1007\/s10703-005-1490-4","type":"journal-article","created":{"date-parts":[[2005,8,25]],"date-time":"2005-08-25T10:33:31Z","timestamp":1124966011000},"page":"103-135","source":"Crossref","is-referenced-by-count":21,"title":["Verifying Time Partitioning in the DEOS Scheduling Kernel"],"prefix":"10.1007","volume":"26","author":[{"given":"John","family":"Penix","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"SeungJoon","family":"Park","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corina","family":"Pasareanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Engstrom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aaron","family":"Larson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicholas","family":"Weininger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1490_CR1","doi-asserted-by":"crossref","unstructured":"R. Allen, D. Garlan, and J. Ivers, \u201cFormal modeling and analysis of the HLA component integration standard,\u201d in Proc. 6th SIGSOFT FSE, Lake Buena Vista, Florida, November 1998. ACM.","DOI":"10.1145\/288195.288251"},{"issue":"1","key":"1490_CR2","first-page":"24","volume":"19","author":"J. M. Atlee","year":"1993","unstructured":"J. M. Atlee and J. Gannon, \u201cState-based model checking of event-driven systems requirements,\u201d IEEE TSE, Vol. 19, No. 1, pp. 24\u201340, 1993.","journal-title":"IEEE TSE"},{"key":"1490_CR3","doi-asserted-by":"crossref","unstructured":"T. Ball, A. Podelski, and S. Rajamani, \u201cBoolean and cartesian abstractions for model checking C programs,\u201d in Proc. of TACAS 2001, Volume 2031 of LNCS, Genova, Italy, Springer-Verlag, April 2001.","DOI":"10.1007\/3-540-45319-9_19"},{"key":"1490_CR4","doi-asserted-by":"crossref","unstructured":"T. Ball, A. Podelski, and S. K. Rajamani, \u201cRelative completeness of abstraction refinement for software model checking,\u201d in Proc. of TACAS 2002., Volume 2280 of LNCS, Grenoble, France, Springer-Verlag, April 2002.","DOI":"10.1007\/3-540-46002-0_12"},{"key":"1490_CR5","doi-asserted-by":"crossref","unstructured":"T. Ball and S. Rajamani, \u201cBebop: A symbolic Model Checker for Boolean Programs,\u201d in Proc. 7th International SPIN Workshop, Volume 1885 of LNCS, Stanford University, California, USA, Springer-Verlag, August 2000.","DOI":"10.1007\/10722468_7"},{"key":"1490_CR6","volume-title":"Software Testing Techniques","author":"B. Beizer","year":"1990","unstructured":"B. Beizer, Software Testing Techniques, 2nd ed, Van Nostrand Reinhold, New York, 1990.","edition":"2"},{"key":"1490_CR7","unstructured":"B. Boehm, Software Engineering Economics. Prentice Hall, 1981."},{"key":"1490_CR8","unstructured":"G. Booch, J. Rumbaugh, and I. Jacobson, The unified modeling language user guide. Addison-Wesley, 1998."},{"key":"1490_CR9","doi-asserted-by":"crossref","unstructured":"D. Bosnacki and D. Dams, \u201cIntegrating real time into Spin: A prototype implementation,\u201d in Proc. FORTE\/PSTV XVIII, Kluwer, 1998, pp. 423\u2013439.","DOI":"10.1007\/978-0-387-35394-4_26"},{"key":"1490_CR10","doi-asserted-by":"crossref","unstructured":"E. Brinksma and A. Mader, \u201cVerification and optimization of a PLC control schedule,\u201d in Proc. 7th SPIN Workshop, Springer-Verlag, 2000, pp. 73\u201392.","DOI":"10.1007\/10722468_5"},{"key":"1490_CR11","unstructured":"B. Bruegge and A. H. Dutoit, \u201cObject-oriented software engineering: Conquering complex and changing systems.\u201d Prentice Hall, 2000."},{"issue":"1","key":"1490_CR12","first-page":"3","volume":"19","author":"R. W. Butler","year":"1993","unstructured":"R. W. Butler and G. B. Finelli, \u201cThe infeasibility of quantifying the reliability of life-critical real-time software,\u201d IEEE TSE, Vol. 19, No. 1, pp. 3\u201312, 1993.","journal-title":"IEEE TSE"},{"key":"1490_CR13","unstructured":"J. Falk C. Kaner and H.Q. Nguyen, Testing computer Software, 2nd ed, Wiley, 1993."},{"key":"1490_CR14","doi-asserted-by":"crossref","unstructured":"W. Chan, R. Andersen, P. Beame, D. Jones, D. Notkin, and W. Warner, \u201cDecoupling synchronization from local control for efficient symbolic model checking of statecharts,\u201d in Proc. 21st International Conference on Software Engineering, ACM Press: Los Angeles, May 1999, pp. 142\u2013151.","DOI":"10.1145\/302405.302460"},{"issue":"7","key":"1490_CR15","first-page":"498","volume":"24","author":"W. Chan","year":"1998","unstructured":"W. Chan, R. J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. D. Reese, \u201cModel checking large software specifications,\u201d IEEE TSE, Vol. 24, No. 7, pp. 498\u2013520, 1998.","journal-title":"IEEE TSE"},{"key":"1490_CR16","doi-asserted-by":"crossref","unstructured":"J.J. Chilenski and S.P. Miller, \u201cApplicability of modied condition\/decision coverage to software testing,\u201d Software Engineering Journal, Vol. 9, No. 5, 1994.","DOI":"10.1049\/sej.1994.0025"},{"key":"1490_CR17","doi-asserted-by":"crossref","unstructured":"E. Clarke, A. Gupta, J. Kukula, and O. Strichman, \u201cSAT based abstraction-refinement using ILP and machine learning techniques,\u201d in Proc. 14th Conference on Computer-Aided Verification, LNCS. Springer-Verlag, July 2002.","DOI":"10.1007\/3-540-45657-0_20"},{"issue":"2","key":"1490_CR18","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla, \u201cAutomatic verification of finite-state concurrent systems using temporal logic specifications,\u201d ACM Trans. on Programming Languages and Systems, Vol. 8, No. 2, pp. 244\u2013263, 1986.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"1490_CR19","doi-asserted-by":"crossref","unstructured":"J. M. Cobleigh, D. Giannakopoulou, and C. S. P\u0103s\u0103reanu, \u201cLearning assumptions for compositional verification,\u201d in Proc. of TACAS 2003, volume 2619 of LNCS, Springer-Verlag, April 2003.","DOI":"10.1007\/3-540-36577-X_24"},{"key":"1490_CR20","doi-asserted-by":"crossref","unstructured":"M. Col\u00f3n and T. Uribe, Generating finite-state abstractions of reactive systems using decision procedures,\u201d in Proc. 10th Conference on Computer-Aided Verification, volume 1427 of LNCS, Springer-Verlag, July 1998.","DOI":"10.1007\/BFb0028753"},{"key":"1490_CR21","doi-asserted-by":"crossref","unstructured":"J. Corbett, \u201cConstructing compact models of concurrent Java programs,\u201d in M. Young, (ed.), Proc. Intl. Symposium on Software Testing and Analysis, Software Engineering Notes, SIGSOFT, ACM, March 1998, pp. 1\u201310.","DOI":"10.1145\/271771.271778"},{"key":"1490_CR22","doi-asserted-by":"crossref","unstructured":"J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng, \u201cBandera : Extracting finite-state models from Java source code,\u201d in Proc. 22nd Intl. Conf. on Software Engineering. ACM Press, June 2000.","DOI":"10.1145\/337180.337234"},{"key":"1490_CR23","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, \u201cComparing the Galois connection and widening\/narrowing approaches to abstract interpretation,\u201d in M. Bruynooghe and M. Wirsing, (eds.), Proc. Fourth International Symposium on Programming Language Implementation and Logic Programming, volume 631 of LNCS, Leuven, Belgium, 1992. Springer-Verlag, pp. 269\u2013295.","DOI":"10.1007\/3-540-55844-6_142"},{"key":"1490_CR24","doi-asserted-by":"crossref","unstructured":"Z. Dang and R. Kemmerer, \u201cUsing the astral model checker to analyze mobile IP,\u201d in Proc. IEEE 21st International Conference on Software Engineering, Los Angeles, May 1999. ACM Press, pp. 132\u2013 141.","DOI":"10.1145\/302405.302459"},{"key":"1490_CR25","doi-asserted-by":"crossref","unstructured":"S. Das, D. Dill, and S. Park, \u201cExperience with predicate abstraction,\u201d in Proc. International Conference on Conputer-aided Verification (CAV\u201999), volume 1633 of LNCS, Springer-Verlag, 1999, pp. 160\u2013171.","DOI":"10.1007\/3-540-48683-6_16"},{"issue":"7","key":"1490_CR26","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. Demartini","year":"1999","unstructured":"C. Demartini, R. Iosif, and R. Sist, \u201cA deadlock detection tool for concurrent Java programs,\u201d Software Practice and Experience, Vol. 29. No. (7), pp. 577\u2013603, 1999.","journal-title":"Software Practice and Experience"},{"key":"1490_CR27","doi-asserted-by":"crossref","unstructured":"C. Demartini, R. Iosif, and R. Sisto, \u201cdSPIN: A dynamic extension of SPIN,\u201d in Proc. 6th SPIN Workshop, volume 1680 of LNCS, Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48234-2_20"},{"key":"1490_CR28","doi-asserted-by":"crossref","unstructured":"N. Dor, M. Rodeh, and S. Sagiv, \u201cDetecting memory errors via static pointer analysis (preliminary experience),\u201d in Workshop on Program Analysis For Software Tools and Engineering, ACM, 1998, pp. 27\u201334.","DOI":"10.1145\/277631.277637"},{"key":"1490_CR29","unstructured":"M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, and H. Zheng, \u201cTool-supported program abstraction for finite-state verification,\u201d in Proc. 23rd International Conference on Software Engineering, Toronto, Cananda., ACM Press, May 2001."},{"key":"1490_CR30","doi-asserted-by":"crossref","unstructured":"M. Dwyer and C. Pasareanu, \u201cFilter-based model checking of partial systems,\u201d in Proc. 6th ACM SIGSOFT FSE, ACM SIGSOFT, November 1998.","DOI":"10.1145\/288195.288307"},{"key":"1490_CR31","doi-asserted-by":"crossref","unstructured":"D. Evans, \u201cStatic detection of dynamic memory errors,\u201d in Conference on Programming Language Design and Implementation, ACM, 1996, pp. 44\u201353.","DOI":"10.1145\/231379.231389"},{"key":"1490_CR32","doi-asserted-by":"crossref","unstructured":"P. Godefroid, \u201cModel checking for programming languages using Verisoft,\u201d in Symp. on Principles of Programming Languages, ACM, 1997, pp. 174\u2013186.","DOI":"10.1145\/263699.263717"},{"key":"1490_CR33","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi, \u201cConstruction of abstract state graphs with PVS,\u201d in Proc. 9th International Conference on Computer Aided Vericifaction, volume 1254 of LNCS, Springer-Verlag, 1997, pp. 174\u2013186.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"1490_CR34","doi-asserted-by":"crossref","unstructured":"A. Groce and W. Visser, \u201cModel checking Java programs using structural heuristics,\u201d in Proc. Intl. Symp. on Software Testing and Analysis. ACM Press, July 2002.","DOI":"10.1145\/566172.566175"},{"key":"1490_CR35","unstructured":"K. Havelund, M. Lowry, S. Park, C. Pecheur, J. Penix, W. Visser, and J. L. White, \u201cFormal analysis of the remote agent before and after flight,\u201d in 5th NASA Langley Formal Methods Workshop. NASA, 2000."},{"key":"1490_CR36","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger, \u201cModel checking Java programs using Java PathFinder,\u201d Intl. Journal on Software Tools for Technology Transfer, 1999.","DOI":"10.1007\/s100090050043"},{"key":"1490_CR37","unstructured":"K. J. Hayhurst, C. A. Dorsey, J. C. Knight, N. G. Leveson, and G. F. McCormick, \u201cStreamlining software aspects of certification: Report on the SSAC survey,\u201d Technical Report NASA\/TM-1999-209519, NASA Langley Research Center, 1999."},{"issue":"11","key":"1490_CR38","first-page":"927","volume":"24","author":"C. Heitmeyer","year":"1998","unstructured":"C. Heitmeyer, \u201cUsing abstraction and model checking to detect safety violations in requirements specifications,\u201d IEEE TSE, Vol. 24, No. 11, pp. 927\u2013948, 1998.","journal-title":"IEEE TSE"},{"key":"1490_CR39","doi-asserted-by":"crossref","unstructured":"T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, \u201cLazy abstraction,\u201d in Proc. Symp. on Principles of Programming Languages, ACM, 2002, pp. 179\u2013190","DOI":"10.1145\/503272.503279"},{"issue":"5","key":"1490_CR40","first-page":"279","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann, \u201cThe model checker SPIN,\u201d IEEE TSE, Vol. 23, No. 5, pp. 279\u2013295, 1997.","journal-title":"IEEE TSE"},{"issue":"4","key":"1490_CR41","first-page":"364","volume":"28","author":"G. J. Holzmann","year":"2002","unstructured":"G. J. Holzmann and M. H. Smith, \u201cAn automated verification method for distributed systems software based on model extraction,\u201d IEEE TSE, Vol. 28, No. 4, pp. 364\u2013377, 2002.","journal-title":"IEEE TSE"},{"key":"1490_CR42","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann, \u201cLogic verification of ansi-c code with spin,\u201d in Proc. 7th International SPIN Workshop, volume 1885 of LNCS, Springer Verlag, Sep. 2000, pp. 131\u2013147.","DOI":"10.1007\/10722468_8"},{"key":"1490_CR43","unstructured":"G. Hwang, K. Tai, and T. Hunag, \u201cReachability testing: An approach to testing concurrent software,\u201d Journal of Software Engineering and Knowledge Engineering, Vol. 5, No. 4, December 1995."},{"key":"1490_CR44","doi-asserted-by":"crossref","unstructured":"D. Jackson and M. Vaziri, \u201cFinding bugs with a constraint solver,\u201d in Mary Jean Harrold, (ed.), Proc. International Symposium on Software Testing and Analysis, Software Engineering Notes, Portland, Oregon, August 2000, pp. 14\u201325, ACM Press.","DOI":"10.1145\/347324.383378"},{"key":"1490_CR45","unstructured":"JPL Special Review Board, Report on the loss of the Mars Polar Lander and Deep Space 2 missions, March 2000."},{"key":"1490_CR46","doi-asserted-by":"crossref","unstructured":"S. Khurshid, C. S. P\u0103s\u0103reanu, and W. Visser, \u201cGeneralized symbolic execution for model checking and testing,\u201d in Proc. of TACAS 2003, volume 2619 of LNCS, Springer-Verlag, April 2003.","DOI":"10.1007\/3-540-36577-X_40"},{"key":"1490_CR47","unstructured":"R. Lutz, \u201cAnalyzing software requirements errors in safety-critcal embedded systems, in Proc. IEEE International Symposium on Requirements Engineering, IEEE Computer Society, January 1993."},{"key":"1490_CR48","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"1490_CR49","doi-asserted-by":"crossref","unstructured":"G. Naumovich, G. S. Avrunin, and L. A. Clarke, \u201cData flow analysis for checking properties of concurrent Java programs,\u201d in Proc. 21st International Conference on Software Engineering, ACM Press, May 1999, pp. 399\u2013410.","DOI":"10.1145\/302405.302663"},{"key":"1490_CR50","doi-asserted-by":"crossref","unstructured":"J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger, \u201cVerification of time partitioning in the deos scheduler kernel,\u201d in Proc. 22nd International Conference on Software Engineering, ACM Press, June 2000.","DOI":"10.1145\/337180.337364"},{"key":"1490_CR51","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u201cThe Temporal Logic of Programs,\u201d in 18th annual IEEE-CS Symposium on Foundations of Computer Science, pp. 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"1490_CR52","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u201cIn transition from global to modular temporal reasoning about programs,\u201d in K. Apt (ed.), Logic and Models of Concurrent Systems, vol. 13, New York, Springer, pp. 123\u2013144, 1984.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"1490_CR53","unstructured":"PolySpace. http:\/\/www.polyspace.com."},{"key":"1490_CR54","doi-asserted-by":"crossref","unstructured":"C. P\u0103s\u0103reanu, M. Dwyer, and M. Huth, \u201cAssume-guarantee model checking of software: A comparative case study,\u201d in Proc. 6th SPIN Workshop, volume 1680 of LNCS, Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48234-2_14"},{"key":"1490_CR55","doi-asserted-by":"crossref","unstructured":"C.S. P\u0103s\u0103reanu, M.B. Dwyer, and W. Visser, \u201cFinding feasible counter-examples when model checking abstracted Java programs,\u201d in Proc. of TACAS 2001, volume 2031 of LNCS, Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45319-9_20"},{"key":"1490_CR56","doi-asserted-by":"crossref","unstructured":"J.P. Queille and J. Sifakis, \u201cSpecification and Verification of Concurrent Systems in CESAR,\u201d in International Symposium on Programming, volume 137 of LNCS. Springer-Verlag, 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"1490_CR57","doi-asserted-by":"crossref","unstructured":"Robby, M. B. Dwyer, and J. Hatcliff, \u201cBogor: an extensible and highly-modular software model checking framework,\u201d in ESEC 9\/FSE 10, Sep. 2003, pp. 267\u2013276.","DOI":"10.1145\/940071.940107"},{"key":"1490_CR58","unstructured":"RTCA Special Committee 167, \u201cSoftware considerations in airborne systems and equipment certification,\u201d Technical Report DO-178B, RTCA, Inc., dec 1992."},{"key":"1490_CR59","unstructured":"J. Rushby, \u201cPartitioning for safety and security: Requirements, mechanisms, and assurance,\u201d NASA Contractor Report CR-1999-209347, NASA Langley Research Center, June 1999. Also to be issued by the FAA."},{"key":"1490_CR60","doi-asserted-by":"crossref","unstructured":"H. Saidi, \u201cModular and Incremental Analysis of Concurrent Software Systems,\u201d in Proc. 14th IEEE International Conference on Automated Software Engineering, IEEE Computer Society, October 1999, pp. 92\u2013101.","DOI":"10.1109\/ASE.1999.802128"},{"key":"1490_CR61","doi-asserted-by":"crossref","unstructured":"H. Saidi and N. Shankar, \u201cAbstract and model check while you prove,\u201d in Proc. 11th Conference on Computer-Aided Verification, volume 1633 of LNCS, Springer-Verlag, July 1999, pp. 443\u2013454.","DOI":"10.1007\/3-540-48683-6_38"},{"key":"1490_CR62","doi-asserted-by":"crossref","unstructured":"Sha, Klein, and J. Goodenough, \u201cRate monotonic anaysis for real-time systems,\u201d Foundations of Real-Time Computing, pp. 129\u2013155, 1991.","DOI":"10.21236\/ADA235641"},{"key":"1490_CR63","unstructured":"G.S. Shedler, \u201cRegenerative Stochastic Simulation,\u201d Academic Press, 1993."},{"key":"1490_CR64","unstructured":"Microsoft Spec and Check Workshop, 2001, http:\/\/research.microsoft.com\/specncheck\/."},{"key":"1490_CR65","doi-asserted-by":"crossref","unstructured":"S. D. Stoller, \u201cModel-checking multi-threaded distributed Java programs,\u201d in SPIN Model Checking and Software Verification, volume 1885 of LNCS, Springer-Verlag, August 2000, pp. 224\u2013244.","DOI":"10.1007\/10722468_14"},{"key":"1490_CR66","doi-asserted-by":"crossref","unstructured":"S. Tripakis and C. Courcoubetis, \u201cExtending Promela and Spin for real time,\u201d in Proc. of TACAS 1996, volume LNCS 1055. Springer, 1998.","DOI":"10.1007\/3-540-61042-1_53"},{"key":"1490_CR67","doi-asserted-by":"crossref","unstructured":"M. Vardi, \u201cAn automata-theoretic approach to linear temporal logic,\u201d in F. Moller and G. Birtwistle (eds.), Logics for Concurrency, LNCS, 1043, Springer Verlag, 1996, pp. 238\u2013266.","DOI":"10.1007\/3-540-60915-6_6"},{"key":"1490_CR68","doi-asserted-by":"crossref","unstructured":"W. Visser, K. Havelund, G. Brat, and S. Park, \u201cModel checking programs,\u201d in Proc. 14th IEEE International Automated Software Engineering Conference, IEEE Computer Society, September 2000.","DOI":"10.1109\/ASE.2000.873645"},{"key":"1490_CR69","doi-asserted-by":"crossref","unstructured":"W. Visser, S. Park, and J. Penix, \u201cUsing predicate abstraction to reduce objected-oriented programs for model checking,\u201d in Mats P. E. Heimdahl (ed.), Proc. Third ACM Workshop on Formal Methods in Software Practice, Portland, Oregon, ACM Press, August 2000, pp. 3\u201312.","DOI":"10.1145\/349360.351125"},{"key":"1490_CR70","doi-asserted-by":"crossref","unstructured":"C. D. Yang, A. L. Souter, and L. L. Pollock, \u201cAll-du-path coverage for parallel programs,\u201d in International Symposium on Software Testing and Analysis, ACM Press, 1998, pp. 153\u2013162.","DOI":"10.1145\/271771.271804"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-1490-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-005-1490-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-1490-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T06:16:11Z","timestamp":1586412971000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-005-1490-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,3]]},"references-count":70,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,3]]}},"alternative-id":["1490"],"URL":"https:\/\/doi.org\/10.1007\/s10703-005-1490-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,3]]}}}