{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:53:24Z","timestamp":1742385204014},"reference-count":29,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,11,1]],"date-time":"2001-11-01T00:00:00Z","timestamp":1004572800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4288,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,11]]},"DOI":"10.1016\/s1571-0661(04)80962-9","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"174-196","source":"Crossref","is-referenced-by-count":2,"special_numbering":"C","title":["Model-Checking View-Based Partial Specifications"],"prefix":"10.1016","volume":"45","author":[{"given":"Michael","family":"Huth","sequence":"first","affiliation":[]},{"given":"Shekhar","family":"Pradhan","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB1","first-page":"1","article-title":"Domain theory","volume":"volume 3","author":"Abramsky","year":"1994"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB2","doi-asserted-by":"crossref","unstructured":"G. Bruns and P. Godefroid. Model Checking Partial State Spaces with 3-Valued Temporal Logics. In Proceedings of the 11th Conference on Computer Aided Verification, volume 1633 of Lecture Notes in Computer Science, pages 274\u2013287. Springer Verlag, July 1999.","DOI":"10.1007\/3-540-48683-6_25"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB3","doi-asserted-by":"crossref","unstructured":"G. Bruns and P. Godefroid. Generalized Model Checking: Reasoning about Partial State Spaces. In Proceedings of CONCUR '2000 (11th International Conference on Concurrency Theory), volume 1877 of Lecture Notes in Computer Science, pages 168\u2013182. Springer Verlag, August 2000.","DOI":"10.1007\/3-540-44618-4_14"},{"issue":"1","key":"10.1016\/S1571-0661(04)80962-9_NEWBIB4","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0304-3975(91)90266-5","article-title":"Using powerdomains to generalize relational databases","volume":"91","author":"Buneman","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs. In Proc. 4th ACM Symp. on Principles of Programming Languages, pages 238\u2013252. ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Temporal abstract interpretation. In Conference Record of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 12\u201325, Boston, Mass., January 2000. ACM Press, New York, NY.","DOI":"10.1145\/325694.325699"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB7","doi-asserted-by":"crossref","unstructured":"S. M. Easterbrook and M. Chechik. A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints. In Proceedings, 23rd International Conference on Software Engineering (ICSE-01), Toronto, Canada, May 12-19 2001. IEEE Computer Society Press. To appear.","DOI":"10.1109\/ICSE.2001.919114"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB8","doi-asserted-by":"crossref","unstructured":"P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based Model Checking using Modal Transition Systems. In Proceedings of the International Conference on Theory and Practice of Concurrency, Lecture Notes in Computer Science. Springer Verlag, August 2001. To appear.","DOI":"10.1007\/3-540-44685-0_29"},{"issue":"1","key":"10.1016\/S1571-0661(04)80962-9_NEWBIB9","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","article-title":"Institutions: Abstract model theory for specification and programming","volume":"39","author":"Goguen","year":"1992","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB10","series-title":"Proc. of the 8th Int. Conf. on Algebraic Methodology and Software Technology (AMAST 2000), volume 1816 of Lecture Notes in Computer Science","first-page":"26","article-title":"Distance Functions for Defaults in Reactive Systems","author":"Guerra","year":"2000"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB11","doi-asserted-by":"crossref","unstructured":"M. Huth, R. Jagadeesan, and D. Schmidt. Modal transition systems: a foundation for three-valued program analysis. In D. Sands, editor, Proceedings of the European Symposium on Programming (ESOP'2001), volume 2028 of LNCS, pages 155\u2013169, Geneva, Italy, April 2001. Springer Verlag.","DOI":"10.1007\/3-540-45309-1_11"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB12","unstructured":"M. Huth and S. Pradhan. Aspect-driven Property Verification of Inconsistent System Descriptions. Technical Report KSU-CIS-TR-2001-1, Computing & Information Sciences, Kansas State University, Manhattan, Kansas, May 2001. Extended 12-page abstract sunmitted to FSTTCS 2001."},{"issue":"4","key":"10.1016\/S1571-0661(04)80962-9_NEWBIB13","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/226241.226249","article-title":"Structuring Z Specifications With Views","volume":"4","author":"Jackson","year":"1995","journal-title":"ACM Trans. on Software Engineering and Methodology"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB14","unstructured":"D. Jackson. Alloy: A Lightweight Object Modelling Language. Technical Report TR-797, Laboratory of Computer Science, Massachusetts Institute of Technology, 28 July 2000."},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB15","doi-asserted-by":"crossref","unstructured":"D. Jackson, I. Schechter, and I. Shlyahter. Alcoa: The Alloy Constraint Analyzer. In Proc. Int'l Conf. on Software Engineering 2000 (ICSE 2000), pages 730\u2013733. IEEE Computer Society Press, 2000.","DOI":"10.1145\/337180.337616"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB16","unstructured":"C. B. Jones. Systematic Software Development Using VDM. Prentice-Hall, Upper Saddle River, NJ 07458, USA, 1990."},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB17","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BF01178666","article-title":"A typed logic of partial functions reconstructed classically","volume":"31","author":"Jones","year":"1994","journal-title":"Acta Informatica"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB18","unstructured":"P. Kelb. Model checking and abstraction: a framework preserving both truth and failure information. Technical Report OFFIS, University of Oldenburg, Germany, 1994."},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB19","series-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB20","series-title":"Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science","first-page":"232","article-title":"Modal Specifications","author":"Larsen","year":"1989"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB21","doi-asserted-by":"crossref","unstructured":"K. G. Larsen and B. Thomsen. A Modal Process Logic. In Third Annual Symposium on Logic in Computer Science, pages 203\u2013210. IEEE Computer Society Press, 1988.","DOI":"10.1109\/LICS.1988.5119"},{"issue":"2","key":"10.1016\/S1571-0661(04)80962-9_NEWBIB22","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/S0167-6423(98)00019-7","article-title":"E3: A Logic for Reasoning Equationally in the Presence of Partiality","volume":"34","author":"Morris","year":"1999","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB23","unstructured":"C. Nentwich, W. Emmerich, and A. Finkelstein. xlinkit: links that make sense. Technical report, Department of Computer Science, University College of London, 2001."},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB24","doi-asserted-by":"crossref","unstructured":"B. Nuseibeh and S. M. Easterbrook. The Process of Inconsistency Management: A framework for understanding. In Proceedings of the First International Workshop on the Requirements Engineering Process (REP'99), 2-3 September 1999.","DOI":"10.1109\/DEXA.1999.795194"},{"issue":"10","key":"10.1016\/S1571-0661(04)80962-9_NEWBIB25","doi-asserted-by":"crossref","first-page":"760","DOI":"10.1109\/32.328995","article-title":"A Framework for Expressing the Relationships Between Multiple Views in Requirements Specification","volume":"20","author":"Nuseibeh","year":"1994","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB26","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. of the 18th IEEE Symposium on the Foundations of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB27","doi-asserted-by":"crossref","unstructured":"M. Sagiv, T. Reps, and R. Wilhelm. Parametric Shape Analysis via 3-Valued Logic. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, pages 105\u2013118, January 20-22, San Antonio, Texas 1999.","DOI":"10.1145\/292540.292552"},{"key":"10.1016\/S1571-0661(04)80962-9_NEWBIB28","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0022-0000(78)90048-X","article-title":"Powerdomains","volume":"16","author":"Smyth","year":"1977","journal-title":"Journal of Computer and Systems Science"},{"issue":"3","key":"10.1016\/S1571-0661(04)80962-9_NEWBIB29","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/373243.360206","article-title":"Verifying safety properties of concurrent Java programs using 3-valued logic","volume":"36","author":"Yahav","year":"2001","journal-title":"ACM SIGPLAN Notices"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104809629?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104809629?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T05:55:35Z","timestamp":1549173335000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104809629"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,11]]},"references-count":29,"alternative-id":["S1571066104809629"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80962-9","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,11]]}}}