{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T19:40:22Z","timestamp":1740944422160,"version":"3.38.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,2,18]],"date-time":"2011-02-18T00:00:00Z","timestamp":1297987200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2011,9]]},"DOI":"10.1007\/s10472-011-9224-3","type":"journal-article","created":{"date-parts":[[2011,2,17]],"date-time":"2011-02-17T14:12:52Z","timestamp":1297951972000},"page":"5-30","source":"Crossref","is-referenced-by-count":10,"title":["Formal testing for separation assurance"],"prefix":"10.1007","volume":"63","author":[{"given":"Dimitra","family":"Giannakopoulou","sequence":"first","affiliation":[]},{"given":"David H.","family":"Bushnell","sequence":"additional","affiliation":[]},{"given":"Johann","family":"Schumann","sequence":"additional","affiliation":[]},{"given":"Heinz","family":"Erzberger","sequence":"additional","affiliation":[]},{"given":"Karen","family":"Heere","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,2,18]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Betin-Can, A., Bultan, T., Lindvall, M., Lux, B., Topp, S.: Application of design for verification with concurrency controllers to air traffic control software. In: ASE 2005: Proceedings of the 20th International Conference on Automated Software Engineering, pp.\u00a014\u201323 (2005)","key":"9224_CR1","DOI":"10.1145\/1101908.1101914"},{"unstructured":"Bishop, C.M.: Pattern Recognition and Machine Learning (Information Science and Statistics). Springer (2006)","key":"9224_CR2"},{"doi-asserted-by":"crossref","unstructured":"Boyapati, R., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp.\u00a0123\u2013133. ACM Press (2002)","key":"9224_CR3","DOI":"10.1145\/566171.566191"},{"key":"9224_CR4","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1613\/jair.62","volume":"2","author":"WL Buntine","year":"1994","unstructured":"Buntine, W.L.: Operations for learning with graphical models. J. Artif. Intell. Res. 2, 159\u2013225 (1994)","journal-title":"J. Artif. Intell. Res."},{"doi-asserted-by":"crossref","unstructured":"Bushnell, D.H., Giannakopoulou, D., Mehlitz, P., Paielli, R., P\u01ces\u01cereanu, C.: Verification and validation of air traffic systems: tactical separation assurance. In: Proc. IEEE Aerospace Conference. IEEE Press (2009)","key":"9224_CR5","DOI":"10.1109\/AERO.2009.4839621"},{"doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS) (2006)","key":"9224_CR6","DOI":"10.1145\/1180405.1180445"},{"unstructured":"Cheeseman, P., Stutz, J.: Bayesian classification (AutoClass): theory and results. In: Fayyad, U.M., Piatetsky-Shapiro, G., Smyth, P., Uthurusamy, R. (eds.) Proc. 2nd Int. Conf. on Knowledge Discovery and Data Mining, pp.\u00a0153\u2013180. AAAI Press (1996)","key":"9224_CR7"},{"unstructured":"The Choco Constraint Solver. http:\/\/choco.sourceforge.net\/ . Accessed February 2011","key":"9224_CR8"},{"unstructured":"Clarke, E., Grumberg O., Peled, D.: Model Checking. MIT Press (2000)","key":"9224_CR9"},{"unstructured":"Codecover\u2014an open-source glass-box testing tool. http:\/\/codecover.org (2009). Accessed February 2011","key":"9224_CR10"},{"issue":"5","key":"9224_CR11","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1109\/52.536462","volume":"13","author":"D Cohen","year":"1996","unstructured":"Cohen, D., Dalal, S., Parelius, J., Patton, G.: The combinatorial design approach to automatic test generation. IEEE Softw. 13(5), 83\u201388 (1996)","journal-title":"IEEE Softw."},{"issue":"0021-8669","key":"9224_CR12","doi-asserted-by":"crossref","first-page":"353","DOI":"10.2514\/1.20586","volume":"45","author":"M Consiglio","year":"2008","unstructured":"Consiglio, M., Carreno, V., Williams, D., Munoz, C.: Conflict prevention and separation assurance method in the small aircraft transportation system. J. Aircr. 45(0021-8669), 353\u2013358 (2008)","journal-title":"J. Aircr."},{"key":"9224_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1111\/j.2517-6161.1977.tb01600.x","volume":"39","author":"AP Dempster","year":"1977","unstructured":"Dempster, A.P., Laird, N.M., Rubin, D.B.: Maximum likelihood from incomplete data via the EM algorithm (with discussion). J. R. Stat. Soc. Ser. B 39, 1\u201338 (1977)","journal-title":"J. R. Stat. Soc. Ser. B"},{"doi-asserted-by":"crossref","unstructured":"Dowek, G., Munoz, C.: Conflict detection and resolution for 1,2,...,N aircraft. In: Proceedings of the 7th AIAA Aviation, Technology, Integration, and Operations Conference (2007)","key":"9224_CR14","DOI":"10.2514\/6.2007-7737"},{"doi-asserted-by":"crossref","unstructured":"Dunietz, I.S., Ehrlich, W.K., Szablak, B.D., Mallows, C.L., Iannino, A.: Applying design of experiments to software testing: experience report. In: ICSE \u201997: Proceedings of the 19th International Conference on Software Engineering, pp.\u00a0205\u2013215 (1997)","key":"9224_CR15","DOI":"10.1145\/253228.253271"},{"issue":"2","key":"9224_CR16","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1243\/09544100JAERO546","volume":"224","author":"H Erzberger","year":"2010","unstructured":"Erzberger, H., Heere, K.: Algorithm and operational concept for resolving short-range conflicts. Proc. Inst. Mech. Eng. G: J. Aerosp. Eng. 224(2), 225\u2013243 (2010)","journal-title":"Proc. Inst. Mech. Eng. G: J. Aerosp. Eng."},{"unstructured":"Erzberger, H., Lauderdale, T.A., Chu, Y.C.: Automated conflict resolution, arrival management and weather avoidance for ATM. In: Proceedings of the 27th International Congress of the Aeronautical Sciences (2010)","key":"9224_CR17"},{"issue":"3","key":"9224_CR18","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1017\/S0956796802004562","volume":"13","author":"B Fischer","year":"2003","unstructured":"Fischer, B., Schumann, J.: AutoBayes: a system for generating data analysis programs from statistical models. J. Funct. Program. 13(3), 483\u2013508 (2003)","journal-title":"J. Funct. Program."},{"doi-asserted-by":"crossref","unstructured":"Fraley, C., Raftery, A.E.: MCLUST: software for model-based clustering, density estimation, and discriminant analysis. Tech. Rep. 415, Department of Statistics, University of Washington (2002)","key":"9224_CR19","DOI":"10.21236\/ADA459792"},{"doi-asserted-by":"crossref","unstructured":"Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: ICSE \u201910: 32nd International Conference on Software Engineering (2010)","key":"9224_CR20","DOI":"10.1145\/1806799.1806835"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: POPL, pp.\u00a047\u201354 (2007)","key":"9224_CR21","DOI":"10.1145\/1190215.1190226"},{"issue":"6","key":"9224_CR22","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1064978.1065036","volume":"40","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. SIGPLAN Notes 40(6), 213\u2013223 (2005)","journal-title":"SIGPLAN Notes"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL, pp.\u00a043\u201356 (2010)","key":"9224_CR23","DOI":"10.1145\/1707801.1706307"},{"issue":"3","key":"9224_CR24","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1002\/stvr.319","volume":"15","author":"M Grindal","year":"2005","unstructured":"Grindal, M., Offutt, J., Andler, S.F.: Combination testing strategies: a survey. Softw. Test. Verif. Reliab. 15(3), 167\u2013199 (2005)","journal-title":"Softw. Test. Verif. Reliab."},{"unstructured":"IASolver. http:\/\/www.cs.brandeis.edu\/\u223ctim\/Applets\/IAsolver.html . Accessed February 2011","key":"9224_CR25"},{"unstructured":"JavaPathfinder. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf . Accessed February 2011","key":"9224_CR26"},{"unstructured":"JUnit. http:\/\/www.junit.org\/ . Accessed February 2011","key":"9224_CR27"},{"issue":"7","key":"9224_CR28","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"9","key":"9224_CR29","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"NG Leveson","year":"1994","unstructured":"Leveson, N.G., Heimdahl, M.P.E., Hildreth, H., Reese, J.D.: Requirements specification for process-control systems. IEEE Trans. Softw. Eng. 20(9), 684\u2013707 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9224_CR30","first-page":"416","volume-title":"ICSE \u201907: Proceedings of the 29th International Conference on Software Engineering","author":"R Majumdar","year":"2007","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: ICSE \u201907: Proceedings of the 29th International Conference on Software Engineering, pp.\u00a0416\u2013426. IEEE Computer Society, Washington, DC (2007)"},{"issue":"2","key":"9224_CR31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.18637\/jss.v004.i02","volume":"4","author":"G McLachlan","year":"1999","unstructured":"McLachlan, G., Peel, D., Basford, K.E., Adams, P.: The EMMIX software for the fitting of mixtures of normal and t-components. Journal Statistical Software 4(2), 1\u201314 (1999)","journal-title":"Journal Statistical Software"},{"unstructured":"Murphy, M.: Octave: a free, high-level language for mathematics. Linux J. 39 (1997)","key":"9224_CR32"},{"unstructured":"Octave. http:\/\/www.gnu.org\/software\/octave (2010)","key":"9224_CR33"},{"key":"9224_CR34","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"C P\u01ces\u01cereanu","year":"2009","unstructured":"P\u01ces\u01cereanu, C., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transf. (STTT) 11, 339\u2013353 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"doi-asserted-by":"crossref","unstructured":"P\u01ces\u01cereanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M.R., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: ISSTA \u201908: Proceedings of the International Symposium on Software Testing and Analysis, pp.\u00a015\u201326. ACM (2008)","key":"9224_CR35","DOI":"10.1145\/1390630.1390635"},{"unstructured":"RTCA. DO-178B: software considerations in airborne systems and equipment certification. http:\/\/www.rtca.org (1992)","key":"9224_CR36"},{"doi-asserted-by":"crossref","unstructured":"Schumann, J., Gundy-Burlet, K., P\u01ces\u01cereanu, C., Menzies, T., Barrett, T.: Software V&V support by parametric analysis of large software simulation systems. In: Proc. IEEE Aerospace. IEEE Press (2009)","key":"9224_CR37","DOI":"10.1109\/AERO.2009.4839618"},{"unstructured":"Schumann, J., Jafari, H., Pressburger, T., Denney, E., Buntine, W., Fischer, B.: AutoBayes program synthesis system users manual. Tech. Rep. NASA\/TM-2008-215366, NASA (2008)","key":"9224_CR38"},{"key":"9224_CR39","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1145\/1081706.1081750","volume-title":"ESEC\/FSE-13: Proceedings of the 10th European Software Engineering Conference","author":"K Sen","year":"2005","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC\/FSE-13: Proceedings of the 10th European Software Engineering Conference, pp.\u00a0263\u2013272. ACM, New York (2005)"},{"unstructured":"T-Vec. http:\/\/www.t-vec.com (2002). Accessed February 2011","key":"9224_CR40"},{"issue":"1","key":"9224_CR41","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1109\/32.979992","volume":"28","author":"K Tai","year":"2002","unstructured":"Tai, K., Lie, Y.: A test generation strategy for pairwise testing. IEEE Trans. Softw. Eng. 28(1), 109\u2013111 (2002)","journal-title":"IEEE Trans. Softw. Eng."},{"doi-asserted-by":"crossref","unstructured":"Tillmann, N., de\u00a0Halleux, J.: Pex: white box test generation for .NET. In: Beckert, B., H\u00e4hnle, R. (eds.) Tests and Proofs. Lecture Notes in Computer Science, vol.\u00a04966, pp.\u00a0134\u2013153. Springer (2008)","key":"9224_CR42","DOI":"10.1007\/978-3-540-79124-9_10"},{"issue":"2","key":"9224_CR43","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"issue":"4","key":"9224_CR44","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1013886.1007526","volume":"29","author":"W Visser","year":"2004","unstructured":"Visser, W., P\u01ces\u01cereanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. SIGSOFT Softw. Eng. Notes 29(4), 97\u2013107 (2004)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"doi-asserted-by":"crossref","unstructured":"Wallace, D.R., Kuhn, D.R.: Failure modes in medical device software: an analysis of 15 years of recall data. Int. J. Reliab. Qual. Saf. Eng. 8(4) (2001)","key":"9224_CR45","DOI":"10.1142\/S021853930100058X"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9224-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-011-9224-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9224-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T18:53:29Z","timestamp":1740941609000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-011-9224-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,2,18]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,9]]}},"alternative-id":["9224"],"URL":"https:\/\/doi.org\/10.1007\/s10472-011-9224-3","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2011,2,18]]}}}