{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:51:40Z","timestamp":1725558700444},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540205272"},{"type":"electronic","value":"9783540400073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-40007-3_25","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:04:10Z","timestamp":1277496250000},"page":"423-438","source":"Crossref","is-referenced-by-count":1,"title":["A Theory of Hints in Model Checking"],"prefix":"10.1007","author":[{"given":"Markus","family":"Kaltenbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jayadev","family":"Misra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters\u00a021, 181\u2013185 (1985)","journal-title":"Information Processing Letters"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Brace, K.S., Bryant, R.E., Rudell, R.L.: Efficient implementation of a BDD package. In: Proceedings of the 27th ACM\/IEEE Design Automation Conference (1990)","DOI":"10.1145\/123186.123222"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.M.: Representing circuits more efficiently in symbolic model checking. In: Proccedings of the 28th Design Automation Conference 1991, pp. 403\u2013407 (1991)","DOI":"10.1145\/127601.127702"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Proccedings of the 37th Design Automation Conference 2000, pp. 29\u201334 (2000)","DOI":"10.1145\/337292.337306"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computing\u00a0(6) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131. Springer, Heidelberg (1982)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a0(2) (1986)","DOI":"10.1145\/5397.5399"},{"key":"25_CR8","volume-title":"Parallel Program Design, A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design, A Foundation. Addison-Wesley, Reading (1988)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"FME \u201994: Industrial Benefit of Formal Methods","author":"J. Cuellar","year":"1994","unstructured":"Cuellar, J., Wildgruber, I., Barnard, D.: The temporal logic of transitions. In: Naftalin, M., Bertr\u00e1n, M., Denvir, T. (eds.) FME 1994. LNCS, vol.\u00a0873. Springer, Heidelberg (1994)"},{"key":"25_CR10","series-title":"Text and Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Text and Monographs in Computer Science. Springer, Heidelberg (1990)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Jutla, C.S., Knapp, E., Rao, J.R.: A predicate transformer approach to semantics of parallel programs. In: Proceedings of the 8th ACM Symposium on Principles of Distributed Computing (1989)","DOI":"10.1145\/72981.72999"},{"key":"25_CR12","unstructured":"Kaltenbach, M.: Model checking for UNITY. Technical Report TR94-31, The University of Texas at Austin (December 1994)"},{"key":"25_CR13","unstructured":"Kaltenbach, M.: The UV System, User\u2019s Manual, Revision 1.18 (February 1995)"},{"key":"25_CR14","unstructured":"Kaltenbach, M.: Interactive Verification Exploiting Program Design Knowledge: A Model-Checker for UNITY. PhD thesis, The University of Texas at Austin (December 1996)"},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0020-0190(90)90218-M","volume":"33","author":"E. Knapp","year":"1990","unstructured":"Knapp, E.: A predicate transformer for progress. Information Processing Letters\u00a033, 323\u2013330 (1990)","journal-title":"Information Processing Letters"},{"issue":"2","key":"25_CR16","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions of Software Engineering\u00a03(2), 125\u2013143 (1977)","journal-title":"IEEE Transactions of Software Engineering"},{"key":"25_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)"},{"key":"25_CR18","series-title":"International Series in Computer Science","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989)"},{"issue":"2","key":"25_CR19","first-page":"273","volume":"3","author":"J. Misra","year":"1995","unstructured":"Misra, J.: A logic for concurrent programming: Progress. Journal of Computer and Software Engineering\u00a03(2), 273\u2013300 (1995)","journal-title":"Journal of Computer and Software Engineering"},{"issue":"2","key":"25_CR20","first-page":"239","volume":"3","author":"J. Misra","year":"1995","unstructured":"Misra, J.: A logic for concurrent programming: Safety. Journal of Computer and Software Engineering\u00a03(2), 239\u2013272 (1995)","journal-title":"Journal of Computer and Software Engineering"},{"key":"25_CR21","series-title":"Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8528-6","volume-title":"A Discipline of Multiprogramming","author":"J. Misra","year":"2001","unstructured":"Misra, J.: A Discipline of Multiprogramming. Monographs in Computer Science. Springer-Verlag New York Inc, New York (2001), The first chapter is available at http:\/\/www.cs.utexas.edu\/users\/psp\/discipline.ps.gz"},{"key":"25_CR22","series-title":"Professional Computing Series","volume-title":"Tcl and the Tk toolkit","author":"J.K. Ousterhout","year":"1994","unstructured":"Ousterhout, J.K.: Tcl and the Tk toolkit. Professional Computing Series. Addison-Wesley, Reading (1994)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods at the Crossroads. From Panacea to Foundational Support"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40007-3_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T12:45:22Z","timestamp":1559220322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40007-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540205272","9783540400073"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40007-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}