{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T05:27:01Z","timestamp":1737523621121,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540661320"},{"type":"electronic","value":"9783540487456"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48745-x_24","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T08:12:59Z","timestamp":1193472779000},"page":"404-423","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Intuition \u2014 ILF Checks DAWN Proofs"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Baar","sequence":"first","affiliation":[]},{"given":"Ekkart","family":"Kindler","sequence":"additional","affiliation":[]},{"given":"Hagen","family":"V\u00f6lzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,18]]},"reference":[{"key":"24_CR1","unstructured":"T. Baar, B. Fischer, and D. Fuchs. Integrating Deductional Techniques in a Software Reuse Application. In: Journal of Universal Computer Science 1999."},{"key":"24_CR2","volume-title":"Informatik-Bericht","author":"T. Baar","year":"1999","unstructured":"T. Baar, E. Kindler, H. V\u00f6lzer. Verifying Intuition \u2014 ILF checks DAWN proofs. Informatik-Bericht 119, Humboldt-Universit\u00e4t zu Berlin, March 1999."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Furbach. Protein: A prover with a theory extension interface. In Proc. CADE-12, pp. 769\u2013773. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_57"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"E. Best and C. Fern\u00e1ndez. Nonsequential Processes, EATCS Monographs on Theoretical Computer Science 13. Springer-Verlag, 1988.","DOI":"10.1007\/978-3-642-73483-0"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot. Methods and logics for proving programs. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 841\u2013993. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50020-2"},{"key":"24_CR7","first-page":"383","volume":"2","author":"B. I. Dahn","year":"1998","unstructured":"B. I. Dahn and J. Denzinger. Cooperating theorem provers. In Automated Deduction \u2014 A Basis for Applications, Volume 2, pp. 383\u2013416. Kluwer Academic Publishers, 1998.","journal-title":"Automated Deduction \u2014 A Basis for Applications"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"B. I. Dahn, J. Gehne, T. Honigmann, and A. Wolf. Integration of automated and interactive theorem proving in Ilf. In Proc. CADE-14, pp. 55\u201360. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_7"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"J. Desel and E. Kindler. Proving correctness of distributed algorithms using highlevel Petri nets \u2014 a case study. In Proc. CSD 1998, pp. 177\u2013186, Fukushima, Japan, Mar. 1998. IEEE Computer Society Press.","DOI":"10.1109\/CSD.1998.657550"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"C. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent developments (system abstract). In CADE-12, pp. 778\u2013782. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_59"},{"issue":"10","key":"24_CR11","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. Hoare","year":"1969","unstructured":"C. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576\u2013583, Oct. 1969.","journal-title":"Communications of the ACM"},{"key":"24_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BFb0052094","volume-title":"Foundations of Computer Science: Potential \u2014 Theory \u2014 Cognition","author":"E. Kindler","year":"1997","unstructured":"E. Kindler and W. Reisig. Verification of distributed algorithms with algebraic Petri nets. In C. Freksa, M. Jantzen, and R. Valk (eds.), Foundations of Computer Science: Potential \u2014 Theory \u2014 Cognition, LNCS 1337, pp. 261\u2013270. Springer, 1997."},{"key":"24_CR13","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/BF01211299","volume":"9","author":"E. Kindler","year":"1997","unstructured":"E. Kindler, W. Reisig, H. V\u00f6lzer, and R. Walter. Petri net based verification of distributed algorithms: An example. Formal Aspects of Comp., 9:409\u2013424, 1997.","journal-title":"Formal Aspects of Comp."},{"key":"24_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/3-540-69108-1_19","volume-title":"Application and Theory of Petri Nets 1998, 19th International Conference","author":"E. Kindler","year":"1998","unstructured":"E. Kindler and H. V\u00f6lzer. Flexibility in algebraic nets. In J. Desel and M. Silva (eds.), Application and Theory of Petri Nets 1998, 19 th International Conference, LNCS 1420, pp. 345\u2013364. Springer-Verlag, June 1998."},{"key":"24_CR15","unstructured":"L. Lamport. The temporal logic of actions. SRC Research Report 79, Digital Equipment Corporation, Systems Research Center, Dec. 1991."},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In 10 th Annual Symposium on Principles of Programming Languages. ACM, Jan. 1983.","DOI":"10.1145\/567067.567082"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems \u2014; Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. A temporal proof methodology for reactive systems. In M. Broy (ed.), Program Design Calculi, Springer, pp. 287\u2013323, 1992.","DOI":"10.1007\/978-3-662-02880-3_10"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"W. McCune. OTTER 2.0: Recent developments (system abstract). In Proc. CADE-10, pp. 663\u2013664. Springer, 1990.","DOI":"10.1007\/3-540-52885-7_131"},{"issue":"3","key":"24_CR20","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. Prog. Lang. Syst., 4(3):455\u2013495, July 1982.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"W. Reisig. Elements of Distributed Algorithms\u2014; Modeling and Analysis with Petri Nets. Springer, 1998.","DOI":"10.1007\/978-3-662-03687-7"},{"key":"24_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/3-540-65307-4_52","volume-title":"Lectures on Petri Nets II: Applications","author":"W. Reisig","year":"1998","unstructured":"W. Reisig, E. Kindler, T. Vesper, H. V\u00f6lzer, and R. Walter. Distributed algorithms for networks of agents. In W. Reisig and G. Rozenberg (eds.), Lectures on Petri Nets II: Applications, LNCS 1492, pp. 331\u2013385. Springer, 1998."},{"key":"24_CR23","unstructured":"S. Unger. Automatisches \u00dcberpr\u00fcfen von DAWN-Beweisen. Diploma thesis, Humboldt-Universit\u00e4t zu Berlin, April 1999, forthcoming."},{"key":"24_CR24","unstructured":"M. Weber, R. Walter, H. V\u00f6lzer, T. Vesper, W. Reisig, S. Peuker, E. Kindler, J. Freiheit, and J. Desel. DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen. Informatik-Bericht 88, Humboldt-Universit\u00e4t zu Berlin, Dec. 1997."},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Gaede, and G. Rock. Spass & Flotter, version 0.42. In CADE-13, pp. 141\u2013145. Springer, 1996.","DOI":"10.1007\/3-540-61511-3_75"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets 1999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48745-X_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:25:48Z","timestamp":1737501948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48745-X_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540661320","9783540487456"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-48745-x_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}