{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T17:04:20Z","timestamp":1693674260754},"reference-count":75,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,8,30]],"date-time":"2012-08-30T00:00:00Z","timestamp":1346284800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10817-012-9258-1","type":"journal-article","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T15:59:57Z","timestamp":1346255997000},"page":"241-280","source":"Crossref","is-referenced-by-count":7,"title":["Specification and Verification of Concurrent Programs Through Refinements"],"prefix":"10.1007","volume":"51","author":[{"given":"Sandip","family":"Ray","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"Sumners","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,8,30]]},"reference":[{"issue":"2","key":"9258_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comp. Sci. 82(2), 253\u2013284 (1991)","journal-title":"Theor. Comp. Sci."},{"key":"9258_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"9258_CR3","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/s00224-001-0004-z","volume":"34","author":"NS Arora","year":"2001","unstructured":"Arora, N.S., Blumofe, R.D., Plaxton, C.G.: Thread scheduling in multiprogramming multiprocessors. Theory Comput. Syst. 34, 115\u2013144 (2001)","journal-title":"Theory Comput. Syst."},{"key":"9258_CR4","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/301308.301328","volume-title":"Proceedings of 18th ACM Symposium on Principles of Distributed Computing (PODC 1999)","author":"P Attie","year":"1999","unstructured":"Attie, P.: Liveness-preserving simulation relations. In: Welch, J. (ed.) Proceedings of 18th ACM Symposium on Principles of Distributed Computing (PODC 1999), pp. 63\u201372. ACM Press, New York (1999)"},{"key":"9258_CR5","series-title":"LNCS","first-page":"103","volume-title":"Proceedings of the 8th International SPIN Workshop on Model Checking of Software","author":"T Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) Proceedings of the 8th International SPIN Workshop on Model Checking of Software. LNCS, vol. 2057, pp.\u00a0103\u2013122. Springer, New York (2001)"},{"issue":"5","key":"9258_CR6","doi-asserted-by":"crossref","first-page":"720","DOI":"10.1145\/324133.324234","volume":"46","author":"RD Blumofe","year":"1999","unstructured":"Blumofe, R.D., Leiserson, C.E.: Scheduling multithreaded computations by work stealing. J. ACM 46(5), 720\u2013748 (1999)","journal-title":"J. ACM"},{"key":"9258_CR7","unstructured":"Blumofe, R.D., Plaxton, C.G., Ray, S.: Verification of a concurrent deque implementation. Technical report TR-99-11, Department of Computer Sciences, The University of Texas at Austin (1999)"},{"key":"9258_CR8","volume-title":"A Computational Logic Handbook","author":"RS Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, New York (1988)"},{"key":"9258_CR9","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/B978-0-12-450010-5.50007-4","volume-title":"Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy","author":"RS Boyer","year":"1991","unstructured":"Boyer, R.S., Goldshlag, D., Kaufmann, M., Moore, J.S.: Functional instantiation in first order logic. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 7\u201326. Academic, New York (1991)"},{"key":"9258_CR10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Proceedings of the 8th International Conference on Computer-Aided Verification (CAV 1996)","author":"RK Brayton","year":"1996","unstructured":"Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A.L., Somenzi, F., Aziz, A., Cheng, S., Edwards, S.A., Khatri, S.P., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: a system for verification and synthesis. In: Alur, R., Henzinger, T. (eds.) Proceedings of the 8th International Conference on Computer-Aided Verification (CAV 1996). LNCS, vol. 1102, pp. 428\u2013432. Springer, New York (1996)"},{"key":"9258_CR11","first-page":"31","volume-title":"Proceedings of the 1997 International Conference on Computer Design: VLSI in Computers & Processors (ICCD 1997), pp. 31\u201336, Austin, TX (1997)","author":"B Brock","year":"1997","unstructured":"Brock, B., Hunt, W.A., Jr.: Formally specifying and mechanically verifying programs for the motorola complex arithmetic processor DSP. In: Proceedings of the 1997 International Conference on Computer Design: VLSI in Computers & Processors (ICCD 1997), pp. 31\u201336, Austin, TX (1997). IEEE Computer Society Press, Los Alamitos"},{"key":"9258_CR12","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1145\/1024393.1024421","volume-title":"Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2004)","author":"G Bronevetsky","year":"2004","unstructured":"Bronevetsky, G., Marques, D., Pingali, K., Szwed, P., Schulz, M.: Application-level checkpointing for shared memory programs. In: Mukherjee, S., McKinley, K. (eds.) Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2004), pp. 235\u2013247. ACM Press, New York (2004)"},{"key":"9258_CR13","unstructured":"Cantor, G.: Contributions to the Founding of the Theory of Transfinite Numbers. Dover, New York (1952, Translated by P.E.B. Jourdain)"},{"issue":"1","key":"9258_CR14","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/214451.214456","volume":"3","author":"KM Chandy","year":"1985","unstructured":"Chandy, K.M., Lamport, L.: Distributed snapshots: determining global states of distributed systems. ACM Trans Comput Syst 3(1), 63\u201375 (1985)","journal-title":"ACM Trans Comput Syst"},{"issue":"4","key":"9258_CR15","doi-asserted-by":"crossref","first-page":"632","DOI":"10.1145\/1780.1804","volume":"6","author":"KM Chandy","year":"1984","unstructured":"Chandy, K.M., Misra, J.: The drinking philosopher\u2019s problem. ACM Trans. Program. Lang. Syst. (ACM TOPLAS) 6(4), 632\u2013646 (1984)","journal-title":"ACM Trans. Program. Lang. Syst. (ACM TOPLAS)"},{"key":"9258_CR16","volume-title":"Parallel Program Design: A Foundation","author":"KM Chandy","year":"1990","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Cambridge (1990)"},{"key":"9258_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-642-14203-1_12","volume-title":"5th International Joint Conference on Automated Reasoning (IJCAR 2010)","author":"K Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA+ proof system. In: Giesl, J., H\u00e4hnle, R. (eds.) 5th International Joint Conference on Automated Reasoning (IJCAR 2010). LNCS, no. 6173, pp. 142\u2013148. Springer, New York (2010)"},{"key":"9258_CR18","volume-title":"Model-Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model-Checking. MIT Press, Cambridge (2000)"},{"key":"9258_CR19","unstructured":"Davis, J.: Finite set theory based on fully ordered lists. In: Kaufmann, M., Moore, J.S. (eds.) 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004) (2004)"},{"issue":"2","key":"9258_CR20","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"EW Dijkstra","year":"1971","unstructured":"Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Inform. 1(2), 115\u2013138 (1971)","journal-title":"Acta Inform."},{"key":"9258_CR21","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/174675.174673","volume-title":"21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1994)","author":"D Doligez","year":"1994","unstructured":"Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1994), pp. 70\u201383. ACM Press, New York (1994)"},{"key":"9258_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Proceedings of the 12th International Conference on Correct Hardware Design and Verification Methods (CHARME 2003)","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D. (ed.) Proceedings of the 12th International Conference on Correct Hardware Design and Verification Methods (CHARME 2003). LNCS, vol. 2860, pp. 247\u2013262. Springer, New York (2003)"},{"key":"9258_CR23","first-page":"84","volume-title":"Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995)","author":"EA Emerson","year":"1995","unstructured":"Emerson, E.A., Namjoshi, K.: Reasoning about rings. In: Ernst, M. (ed.) Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995), pp. 84\u201395. ACM Press, New York (1995)"},{"key":"9258_CR24","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/BFb0024653","volume-title":"Industrial-Strength Formal Methods, 1st International Symposium of Formal Methods Europe","author":"K Engelhardt","year":"1993","unstructured":"Engelhardt, K., de\u00a0Roever, W.P.: Generalizing Abadi & Lamport\u2019s method to solve a problem posed by Pnueli. In: Woodcock, J., Larsen, P.G. (eds.) Industrial-Strength Formal Methods, 1st International Symposium of Formal Methods Europe. LNCS, vol. 670, pp. 294\u2013313, Odense, Denmark. Springer, New York (1993)"},{"issue":"9","key":"9258_CR25","doi-asserted-by":"crossref","first-page":"1005","DOI":"10.1109\/32.58787","volume":"16","author":"DM Goldshlag","year":"1990","unstructured":"Goldshlag, D.M.: Mechanically verifying concurrent programs with the Boyer\u2013Moore prover. IEEE Trans. Softw. Eng. 16(9), 1005\u20131023 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9258_CR26","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1109\/FMCAD.2006.6","volume-title":"Proceedings on the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD-2006)","author":"MJC Gordon","year":"2006","unstructured":"Gordon, M.J.C., Hunt, W.A., Jr., Kaufmann, M., Reynolds, J.: An integration of HOL and ACL2. In: Gupta, A., Manolios, P. (eds.) Proceedings on the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD-2006), pp. 153\u2013160. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"9258_CR27","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proceedings of the 9th International Conference on Computer-Aided Verification (CAV 1997)","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Proceedings of the 9th International Conference on Computer-Aided Verification (CAV 1997), LNCS, vol. 1254, pp. 72\u201383. Springer, New York (1997)"},{"issue":"3","key":"9258_CR28","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF00121125","volume":"2","author":"A Gupta","year":"1992","unstructured":"Gupta, A.: Formal hardware verification methods: a survey. Form. Method Syst. Des. 2(3), 151\u2013238 (1992)","journal-title":"Form. Method Syst. Des."},{"key":"9258_CR29","series-title":"LNCS","first-page":"662","volume-title":"Proceedings of the 3rd Intermational Symposium of Formal Methods Europe (FME 1996)","author":"K Havelund","year":"1996","unstructured":"Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M., Woodcock, J. (eds.) Proceedings of the 3rd Intermational Symposium of Formal Methods Europe (FME 1996), LNCS, vol. 1051, pp. 662\u2013681. Springer, New York (1996)"},{"key":"9258_CR30","first-page":"58","volume-title":"Proceedings of the 29th ACM-SIGPLAN Conference on Principles of Programming Languages (POPL 2002)","author":"TA Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM-SIGPLAN Conference on Principles of Programming Languages (POPL 2002), pp. 58\u201370. ACM Press, New York (2002)"},{"key":"9258_CR31","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/3-540-45442-X_8","volume-title":"Proceedings of Mathematics of Program Construction","author":"W Hesselink","year":"2002","unstructured":"Hesselink, W.: Eternity variables to simulate specification. In: Proceedings of Mathematics of Program Construction. LNCS, vol. 2386, pp. 117\u2013130, Dagstuhl, Germany. Springer, New York (2002)"},{"key":"9258_CR32","unstructured":"Hooman, J.: Compositional verification of timed components using PVS. In: Biel, B., Gruhn, V. (eds.) Software Engineering 2006, Fachtagung des GI-Fachbereichs Softwaretechnik. LNI, vol. 79, pp. 143\u2013154 (2006)"},{"key":"9258_CR33","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BFb0055139","volume-title":"Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 1998)","author":"PB Jackson","year":"1998","unstructured":"Jackson, P.B.: Verifying a garbage collector algorithm. In: Grundy, J., Newer, M. (eds.) Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 1998). LNCS, vol. 1479, pp.225\u2013244. Springer, New York (1998)"},{"issue":"2\u20133","key":"9258_CR34","first-page":"129","volume":"12","author":"B Jonsson","year":"1999","unstructured":"Jonsson, B., Pnueli, A., Rump, C.: Proving refinement using transduction. Distrib. Comput. 12(2\u20133), 129\u2013149 (1999)","journal-title":"Distrib. Comput."},{"key":"9258_CR35","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 home page. See URL http:\/\/www.cs.utexas.edu\/users\/moore\/acl2 (1997)"},{"key":"9258_CR36","unstructured":"Kaufmann, M., Moore, J.S.: A precise description of the ACL2 logic. See URL http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/km97.ps.gz (1997)"},{"key":"9258_CR37","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic, Boston (2000)"},{"key":"9258_CR38","first-page":"141","volume-title":"Proceedings of 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002)","author":"M Kaufmann","year":"2002","unstructured":"Kaufmann, M., Sumners, R.: Efficient rewriting of data structures in ACL2. In: Borrione, D., Kaufmann, M., Moore, J.S. (eds.) Proceedings of 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002), pp. 141\u2013150. Grenoble, France (2002)"},{"issue":"2","key":"9258_CR39","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C Kern","year":"1999","unstructured":"Kern, C., Greenstreet, M.: Formal verification in hardware design: a survey. ACM Transact. Des. Automat. Electron. Syst. 4(2), 123\u2013193 (1999)","journal-title":"ACM Transact. Des. Automat. Electron. Syst."},{"issue":"4","key":"9258_CR40","first-page":"97","volume":"8","author":"M Kyas","year":"2006","unstructured":"Kyas, M., Hooman, J.: A semantics of communicating reactive objects with timing. Softw. Tools Technol. Transf. (STTT) 8(4), 97\u2013112 (2006)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"9258_CR41","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-540-27813-9_11","volume-title":"Proceedings of the 16th International Conference on Computer-Aided Verification (CAV 2004)","author":"SK Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) Proceedings of the 16th International Conference on Computer-Aided Verification (CAV 2004). LNCS, vol. 3117, pp. 135\u2013147. Springer, New York (2004)"},{"key":"9258_CR42","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Proceedings of the 15th International Conference on Computer-Aided Verification","author":"SK Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Proceedings of the 15th International Conference on Computer-Aided Verification. LNCS, vol. 2275, pp. 141\u2013153. Springer, New York (2003)"},{"issue":"8","key":"9258_CR43","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"key":"9258_CR44","first-page":"657","volume":"83","author":"L Lamport","year":"1983","unstructured":"Lamport, L.: What good is temporal logic? Inf. Process. 83, 657\u2013688 (1983)","journal-title":"Inf. Process."},{"issue":"3","key":"9258_CR45","first-page":"827","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. (ACM TOPLAS) 16(3), 827\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (ACM TOPLAS)"},{"key":"9258_CR46","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1145\/1133373.1133382","volume-title":"Proceedings of the 10th ACM SIGOPS European Workshop","author":"L Lamport","year":"2002","unstructured":"Lamport, L., Matthews, J., Tuttle, M., Yu, Y.: Specifying and verifying systems with TLA+. In: Jul, E. (ed.) Proceedings of the 10th ACM SIGOPS European Workshop, pp. 45\u201348. Copenhagen, Denmark (2002)"},{"key":"9258_CR47","volume-title":"Distributed Algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Mateo (1996)"},{"key":"9258_CR48","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"9258_CR49","unstructured":"Manolios, P.: Mechanical verification of reactive systems. PhD thesis, Department of Computer Sciences, The University of Texas at Austin (2001)"},{"key":"9258_CR50","series-title":"LNCS","first-page":"218","volume-title":"Proceedings of the 12th Working Conference on Correct Hardware Design and Verification Methods","author":"P Manolios","year":"2003","unstructured":"Manolios, P.: A compositional theory of refinement for branching time. In: Geist, D. (ed.) Proceedings of the 12th Working Conference on Correct Hardware Design and Verification Methods. LNCS, vol. 2860, pp. 304\u2013218. Springer, New York (2003)"},{"key":"9258_CR51","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-540-45085-6_19","volume-title":"Proceedings of the 19th International Conference on Automated Deduction (CADE 2003)","author":"P Manolios","year":"2003","unstructured":"Manolios, P., Vroon, D.: Algorithms for ordinal arithmetic. In: Baader, F. (ed.) Proceedings of the 19th International Conference on Automated Deduction (CADE 2003). LNAI, vol. 2741, pp. 243\u2013257, Miami, FL. Springer, New York (2003)"},{"key":"9258_CR52","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-48683-6_32","volume-title":"Proceedings of the 11th International Conference on Computer-Aided Verification (CAV 1999)","author":"P Manolios","year":"1999","unstructured":"Manolios, P., Namjoshi, K., Sumners, R.: Linking model-checking and theorem-proving with well-founded bisimulations. In: Halbwacha, N., Peled, D. (eds.) Proceedings of the 11th International Conference on Computer-Aided Verification (CAV 1999). LNCS, vol. 1633, pp. 369\u2013379. Springer, New York (1999)"},{"key":"9258_CR53","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer, Norwell (1993)"},{"key":"9258_CR54","volume-title":"Communication and Concurrency","author":"R Milner","year":"1990","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1990)"},{"issue":"2","key":"9258_CR55","first-page":"273","volume":"3","author":"J Misra","year":"1995","unstructured":"Misra, J.: A logic of concurrent programing: progress. J. Comput. Softw. Engin. 3(2), 273\u2013300 (1995)","journal-title":"J. Comput. Softw. Engin."},{"issue":"2","key":"9258_CR56","first-page":"239","volume":"3","author":"J Misra","year":"1995","unstructured":"Misra, J.: A logic of concurrent programing: safety. J. Comput. Softw. Engin. 3(2), 239\u2013372 (1995)","journal-title":"J. Comput. Softw. Engin."},{"key":"9258_CR57","volume-title":"Monographs in Computer Science","author":"J Misra","year":"2001","unstructured":"Misra, J.: A discipline of multiprogramming: programming theory for distributed applications. In: Monographs in Computer Science. Springer, New York (2001)"},{"key":"9258_CR58","first-page":"227","volume-title":"Models, Algebras, and Logic of Engineering Software","author":"JS Moore","year":"2003","unstructured":"Moore, J.S.: Proving theorems about Java and the JVM with ACL2. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logic of Engineering Software, pp. 227\u2013290. IOS Press, Amsterdam (2003)"},{"issue":"3","key":"9258_CR59","first-page":"1","volume":"24","author":"JS Moore","year":"2002","unstructured":"Moore, J.S., Porter, G.: The apprentice challenge. ACM Transac. Program. Lang. Syst. (ACM TOPLAS) 24(3), 1\u201324 (2002)","journal-title":"ACM Transac. Program. Lang. Syst. (ACM TOPLAS)"},{"key":"9258_CR60","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"Proceedings of the 17th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1997)","author":"K Namjoshi","year":"1997","unstructured":"Namjoshi, K.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) Proceedings of the 17th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1997). LNCS, vol. 1346, pp. 284\u2013296. Springer, New York (1997)"},{"key":"9258_CR61","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"Proceedings of the 12th International Conference on Computer-Aided Verification (CAV 2000)","author":"KS Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) Proceedings of the 12th International Conference on Computer-Aided Verification (CAV 2000). LNCS, vol. 1855, pp. 435\u2013449. Springer, New York (2000)"},{"key":"9258_CR62","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Proceedings of the 5th GI-Conference on Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science. LNCS, vol. 104, pp. 167\u2013183. Springer, New York (1981)"},{"issue":"1","key":"9258_CR63","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/343369.343370","volume":"1","author":"L Paulson","year":"2000","unstructured":"Paulson, L.: Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log. 1(1), 3\u201332 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"9258_CR64","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2001)","author":"A Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) Proceedings of the 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2001). LNCS, vol. 2031, pp. 82\u201397. Springer, New York (2001)"},{"issue":"2","key":"9258_CR65","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1109\/MDT.2007.38","volume":"24","author":"S Ray","year":"2007","unstructured":"Ray, S., Sumners, R.: Combining theorem proving with model checking through predicate abstraction. IEEE Des. Test Comput. 24(2), 132\u2013139 (2007)","journal-title":"IEEE Des. Test Comput."},{"key":"9258_CR66","unstructured":"Ray, S., Sumners, R.: A theorem proving approach for verification of reactive concurrent programs. In: Burckhardt, S., Chaudhury, S., Farzan, A., Gopalakrishnen, G., Seigel, S. (eds.) 4th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC2 2011) (2011)"},{"key":"9258_CR67","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF01211305","volume":"6","author":"D Russinoff","year":"1994","unstructured":"Russinoff, D.: A mechanically verified incremental garbage collector. Form. Asp. Comput. 6, 359\u2013390 (1994)","journal-title":"Form. Asp. Comput."},{"key":"9258_CR68","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-63166-6_36","volume-title":"Proceedings of the 9th International Conference on Computer-Aided Verification (CAV 1997)","author":"J Sawada","year":"1997","unstructured":"Sawada, J., Hunt, W.A., Jr.: Trace table based approach for pipelined microprocessor verification. In: Grumberg, O. (ed.) Proceedings of the 9th International Conference on Computer-Aided Verification (CAV 1997). LNCS, vol. 1254, pp. 364\u2013375. Springer, New York (1997)"},{"key":"9258_CR69","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-55092-5_12","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"N Shankar","year":"1992","unstructured":"Shankar, N.: Mechanical verification of a generalized protocol for byzantine fault tolerant clock synchronization. In: Vytopil, J. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 571, pp. 217\u2013236. Springer, New York (1992)"},{"key":"9258_CR70","unstructured":"Sumners, R.: An incremental stuttering refinement proof of a concurrent program in ACL2. In: Kaufmann, M., Moore, J.S. (eds.) 2nd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2000). Austin, TX (2000)"},{"key":"9258_CR71","unstructured":"Sumners, R.: Fair environment assumptions in ACL2. In: Hunt, W.A., Jr., Kaufmann, M., Moore, J.S. (eds.) 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003). Boulder, CO (2003)"},{"key":"9258_CR72","unstructured":"Sumners, R., Ray, S.: Reducing invariant proofs to finite search via rewriting. In: Kaufmann, M., Moore, J.S. (eds.) 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004). Austin, TX (2004)"},{"key":"9258_CR73","unstructured":"Sumners, R., Ray, S.: Proving invariants via rewriting and abstraction. Technical report TR-05-35, Department of Computer Sciences, University of Texas at Austin (2005)"},{"issue":"2","key":"9258_CR74","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., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. J. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng. J."},{"key":"9258_CR75","series-title":"LNCS","first-page":"178","volume-title":"Proceedings of the 11th European Symposium on Programming (ESOP 2002)","author":"K Wansbrough","year":"2002","unstructured":"Wansbrough, K., Norrish, M., Sewell, P., Serjantov, A.: Timing UDP: mechanized semantics of sockets, threads and failures. In: Le M\u00e9tayer, D. (ed.) Proceedings of the 11th European Symposium on Programming (ESOP 2002). LNCS, vol. 2305, pp. 178\u2013294. Springer, New York (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9258-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9258-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9258-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,27]],"date-time":"2022-01-27T21:09:52Z","timestamp":1643317792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9258-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,30]]},"references-count":75,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["9258"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9258-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,30]]}}}