{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T17:40:20Z","timestamp":1707068420240},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,6,1]],"date-time":"2006-06-01T00:00:00Z","timestamp":1149120000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2006,6]]},"DOI":"10.1007\/s00236-006-0016-x","type":"journal-article","created":{"date-parts":[[2006,6,2]],"date-time":"2006-06-02T15:38:11Z","timestamp":1149262691000},"page":"45-71","source":"Crossref","is-referenced-by-count":0,"title":["Compositional Analysis of C\/C++ Programs with VeriSoft"],"prefix":"10.1007","volume":"43","author":[{"given":"Juergen","family":"Dingel","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,3]]},"reference":[{"issue":"3","key":"16_CR1","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi M., Lamport L. (1995). Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3):507\u2013534","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR2","volume-title":"Foundations of Multithreaded, Parallel, and Distributed Programming","author":"G.R. Andrews","year":"2000","unstructured":"Andrews G.R. (2000) Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley, Reading"},{"issue":"1","key":"16_CR3","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1023\/A:1008744030390","volume":"15","author":"S. Bensalem","year":"1999","unstructured":"Bensalem S., Lakhnech Y. (1999). Automatic generation of invariants. Formal Methods Syst. Des., 15(1):75\u201392","journal-title":"Formal Methods Syst. Des.,"},{"issue":"2","key":"16_CR4","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1006\/inco.1996.0056","volume":"127","author":"S.D. Brookes","year":"1996","unstructured":"Brookes S.D. (1996). Full abstraction for a shared-variable parallel language. Information and Computation, 127(2):145\u2013163","journal-title":"Information and Computation,"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., P\u0103s\u0103reanu, C., Robby, Laubach, S., Zheng, H.: Bandera : Extracting finite-state models from Java source code. In: 22nd International Conference on Software Engineering (ICSE \u201900) (2000)","DOI":"10.1145\/337180.337234"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Colby, C., Godefroid, P., Jagadeesan, L.J.: Automatically closing open reactive programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201998), Montreal, Canada (1998)","DOI":"10.1145\/277650.277754"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201903), pp. 331\u2013346, Warsaw, Poland (2003)","DOI":"10.1007\/3-540-36577-X_24"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Collette, P., Jones, C.B.: Enhancing the tractability of rely\/guarantee specifications in the development of interfering operations. In: Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 277\u2013307. MIT Press, Cambridge (2000)","DOI":"10.7551\/mitpress\/5641.003.0016"},{"key":"16_CR9","unstructured":"du Bousquet, L., Ouabdesselam, F., Parissis, I., Richier, J.-L., Zuanon, N. (2000) Specification-based testing of synchronous software. In: International Workshop on Formal Methods for Industrial Critical Systems, Berlin, Germany (2000)"},{"key":"16_CR10","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s001650200032","volume":"14","author":"J. Dingel","year":"2002","unstructured":"Dingel J. (2002) A refinement calculus for shared-variable parallel and distributed programming. Formal Asp. Comput. 14:123\u2013197","journal-title":"Formal Asp. Comput."},{"key":"16_CR11","unstructured":"Dingel, J.: Automatic transition trace analysis of parallel programs using VeriSoft. Technical Report 2003-467, Queen\u2019s University, School of Computing, Kingston, Ontario, June 2003. Available at www.cs.queensu.ca\/TechReports."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Dingel, J.: Computer-assisted assume\/guarantee reasoning with VeriSoft. In: 25th International Conference on Software Engineering (ICSE \u201903), pp. 138\u2013148, Portland, Oregon (2003)","DOI":"10.1109\/ICSE.2003.1201195"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Ernst, M.D., Czeisler, A., Griswold, W.G., Notkin,D.: Quickly etecting relevant program invariants. In 22nd International Conference on Software Engineering (ICSE \u201900), pp. 449\u2013458, Limerick, Ireland (2000)","DOI":"10.1145\/337180.337240"},{"key":"16_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems \u2013 An Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid P. (1996). Partial-Order Methods for the Verification of Concurrent Systems \u2013 An Approach to the State-Explosion Problem. Springer, Berlin Heidelberg New York"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: 24th ACM Symposium on Principles of Programming Languages, pp. 174\u2013186, Paris (1997)","DOI":"10.1145\/263699.263717"},{"key":"16_CR16","unstructured":"Godefroid, P.: Software model checking in practice: an industrial case study. In: International Conference on Software Engineering (ICSE \u201902), Orlando (2002)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. In 6th International Symposium on the Foundations of Software Engineering (FSE-6), Orlando, Florida (1998)","DOI":"10.1145\/288195.288218"},{"key":"16_CR18","unstructured":"Jeffords, R., Heitmeyer, C.: An algorithm for strengthening state invariants generated from requirements specifications. In: 5th International Symposium on Requirements Engineering (RE \u201901), Toronto, Canada (2001)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Jeffords, R., Heitmeyer, C.: A strategy for efficiently verifying requirements specifications using composition and invariants. In: European Software Engineering Conference\/ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE 2003), Helsinki, Finland (2003)","DOI":"10.21236\/ADA464275"},{"issue":"4","key":"16_CR20","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones C.B. (1983). Tentative steps towards a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4):576\u2013619","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Jagadeesan, L.J., Porter, A., Ramming, J.C., Votta, L.: Specification-based testing of reactive software: Tools and experiments. In: 19th International Conference on Software Engineering (ICSE \u201997): (1997)","DOI":"10.1145\/253228.253435"},{"issue":"4","key":"16_CR22","first-page":"221","volume":"29","author":"D. Jackson","year":"1996","unstructured":"Jackson D., Wing J. (1996). Lightweight formal methods. IEEE Comput. 29(4):221\u201322","journal-title":"IEEE Comput."},{"key":"16_CR23","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. (1995). Temporal Verification of Reactive Systems: Safety. Springer, Berlin Heidelberg New York"},{"key":"16_CR24","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S.S. Owicki","year":"1976","unstructured":"Owicki S.S., Gries D. (1976). An axiomatic proof technique for parallel programs. Acta Inform 6:319\u2013340","journal-title":"Acta Inform"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of software: A comparative case study. In: Theoretical and Practical Aspects of SPIN Model Checking. Springer, Berlin Heidelberg New York LNCS 1680 (1999)","DOI":"10.1007\/3-540-48234-2_14"},{"key":"16_CR26","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"Peterson G.L. (1981). Myths about the mutual exclusion problem. Inform Process Lett 12:115\u2013116","journal-title":"Inform Process Lett"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems, NATO ASI F13, pp. 123\u2013144. Springer, Berlin Heidelberg New York (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Raymond, P., Weber, D., Nicollin, X., Halbwachs, N.: Automatic testing of reactive systems. In: 19th IEEE Real-Time Systems Symposium (RTSS \u201998) (1998)","DOI":"10.1109\/REAL.1998.739746"},{"key":"16_CR29","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1016\/0304-3975(88)90033-3","volume":"89","author":"C. Stirling","year":"1988","unstructured":"Stirling C. (1988). A generalization of Owicki-Gries\u2019 Hoare logic for a concurrent while language. Theoret. Comput. Sci. 89:347\u2013359","journal-title":"Theoret. Comput. Sci."},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"St\u00f8len, K.: A method for the development of totally correct shared-state parallel programs. In: 2nd International Conference on Concurrency Theory (CONCUR \u201991), pp. 510\u2013525 LNCS 789 (1991)","DOI":"10.1007\/3-540-54430-5_110"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"St\u00f8len, K.: Assumption\/commitment rules for dataflow networks - with an emphasis on completeness. In: 6th European Symposium on Programming (ESOP \u201996), pp. 356\u2013372 LNCS 1058 (1996)","DOI":"10.1007\/3-540-61055-3_48"},{"issue":"2","key":"16_CR32","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. (2003). Model checking programs. Automated Softw. Eng. J. 10(2):203\u2013232","journal-title":"Automated Softw. Eng. J."},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Zulkernine, M., Seviora, R.: Assume-guarantee supervisor for concurrent systems. In: International Parallel and Distributed Processing Symposium (IPDPS \u201901), pp. 1552\u20131560. IEEE Computer Science Press (2001)","DOI":"10.1109\/IPDPS.2001.925140"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0016-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-006-0016-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0016-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T17:10:31Z","timestamp":1707066631000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-006-0016-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,6]]}},"alternative-id":["16"],"URL":"https:\/\/doi.org\/10.1007\/s00236-006-0016-x","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,6]]}}}