{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:46:01Z","timestamp":1755837961920},"reference-count":28,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/ase.2003.1240300","type":"proceedings-article","created":{"date-parts":[[2004,1,24]],"date-time":"2004-01-24T04:33:03Z","timestamp":1074918783000},"page":"116-127","source":"Crossref","is-referenced-by-count":55,"title":["Automated environment generation for software model checking"],"prefix":"10.1109","author":[{"given":"O.","family":"Tkachuk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.B.","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.S.","family":"Pasareanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2001.919092"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/288195.288307"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9128(199711)9:11<1293::AID-CPE340>3.0.CO;2-J"},{"key":"ref13","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44829-2_14","article-title":"Thread modular model checking","author":"flanagan","year":"2003","journal-title":"Model Checking Software (LNCS 2648)"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2002.1114984"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"journal-title":"The Temporal Logic of Reactive and Concurrent Systems Specification","year":"1991","author":"manna","key":"ref17"},{"journal-title":"Communication and Concurrecny","year":"1989","author":"milner","key":"ref18"},{"key":"ref19","doi-asserted-by":"crossref","DOI":"10.1145\/337180.337364","article-title":"Verification of time partitioning in the DEOS real-time scheduling kernel","author":"penix","year":"2000","journal-title":"Proceedings of the 22nd international conference on Software engineering"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2000.873645"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"ref27","article-title":"Soot - a Java optimization framework","author":"valle-rai","year":"1999","journal-title":"Proceedings of CASCON '99"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/253228.253275"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277754"},{"key":"ref5","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36577-X_24","article-title":"Learning assumptions for compositional verification","author":"cobleigh","year":"2003","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems 9th International conference (LNCS 2619)"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/271771.271778"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2001.919196"},{"journal-title":"Compilers Principles Techniques and Tools","year":"1985","author":"aho","key":"ref1"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s100090200075"},{"key":"ref20","article-title":"DEOS kernel: Environment modeling using LTL assumptions","author":"p?s?reanu","year":"2000","journal-title":"Technical Report Technical Report NASA-ARC-IC-2000-196"},{"key":"ref22","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48234-2_14","article-title":"Assume-guarantee model checking of software: A comparative case study","author":"p?s?reanu","year":"1999","journal-title":"Theoretical and Applied Aspects of SPIN Model Checking (LNCS 1680)"},{"journal-title":"Abstraction and Modular Reasoning for the Verification of Software","year":"2001","author":"p?s?reanu","key":"ref21"},{"key":"ref24","doi-asserted-by":"crossref","DOI":"10.1145\/940071.940097","article-title":"Adapting side effects analysis for modular program model checking","author":"tkachuk","year":"2003"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566179"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940097"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2002.1052929"}],"event":{"name":"18th IEEE International Conference on Automated Software Engineering","acronym":"ASE-03","location":"Montreal, Que., Canada"},"container-title":["18th IEEE International Conference on Automated Software Engineering, 2003. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8780\/27811\/01240300.pdf?arnumber=1240300","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,9]],"date-time":"2018-04-09T04:59:16Z","timestamp":1523249956000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1240300\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/ase.2003.1240300","relation":{},"subject":[]}}