{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T20:32:47Z","timestamp":1676925167126},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,7]],"date-time":"2013-03-07T00:00:00Z","timestamp":1362614400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10270-013-0321-0","type":"journal-article","created":{"date-parts":[[2013,3,6]],"date-time":"2013-03-06T07:58:22Z","timestamp":1362556702000},"page":"83-100","source":"Crossref","is-referenced-by-count":4,"title":["Procedure-modular specification and verification of temporal safety properties"],"prefix":"10.1007","volume":"14","author":[{"given":"Siavash","family":"Soleimanifard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,3,7]]},"reference":[{"key":"321_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. In: Logic in Computer Science (LICS \u201907), pp. 151\u2013160. IEEE Computer Society, Washington, DC (2007)","DOI":"10.1109\/LICS.2007.19"},{"key":"321_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Chaudhuri, S.: Temporal reasoning for procedural programs. In: Verification, Model Checking, and Abstract Interpretation (VMCAI \u201910), vol. 5944 of LNCS, pp. 45\u201360. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-11319-2_7"},{"key":"321_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic for nested calls and returns. In: Tools and Algorithms for the Analysis and Construction of Software (TACAS \u201904), vol. 2998 of LNCS, pp. 467\u2013481. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"321_CR4","doi-asserted-by":"crossref","unstructured":"Amighi, A., de Carvalho Gomes, P., Gurov, D., Huisman, M.: Sound control-flow graph extraction for Java programs with exceptions. In: Software Engineering and Formal Methods (SEFM \u201912), vol. 7504 of LNCS, pp. 33\u201347 (2012)","DOI":"10.1007\/978-3-642-33826-7_3"},{"key":"321_CR5","doi-asserted-by":"crossref","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 545\u2013623. North Holland, Amsterdam (2000)","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"321_CR6","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: A semantics based verification tool for finite state systems. In: International Symposium on Protocol Specification, Testing and Verification, pp. 287\u2013302. North-Holland Publishing Co., Amsterdam (1990)"},{"key":"321_CR7","doi-asserted-by":"crossref","unstructured":"Dam, M.: CTL* and ECTL* as fragments of the modal $$\\mu $$ -calculus. In :Colloquium on Trees in Algebra and Programming, (CAAP \u201992), vol. 581 of LNCS, pp. 145\u2013164. Springer, Berlin (1992)","DOI":"10.1007\/3-540-55251-0_8"},{"key":"321_CR8","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Programming Language Design and Implementation (PLDI \u201902), pp. 57\u201368. ACM (2002)","DOI":"10.1145\/512537.512538"},{"key":"321_CR9","unstructured":"Doclet overview. http:\/\/java.sun.com\/j2se\/1.3\/docs\/tooldocs\/javadoc\/overview.html"},{"key":"321_CR10","unstructured":"Gawell, N.: Automatic verification of applet interaction properties. Master\u2019s thesis, KTH Royal Institute of Technology, Stockholm, Sweden. Ref.: TRITA-CSC-E 2009:128 (2009)"},{"key":"321_CR11","doi-asserted-by":"crossref","unstructured":"Goldman, M., Katz, S.: MAVEN: Modular aspect verification. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201907), vol. 4424 of LNCS, pp. 308\u2013322. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71209-1_24"},{"key":"321_CR12","doi-asserted-by":"crossref","unstructured":"Gurov, D., Huisman, M.: Reducing behavioural to structural properties of programs with procedures. In: Verification, Model Checking, and Abstract Interpretation (VMCAI \u201909), vol. 5403 of LNCS, pp. 136\u2013150. Springer, Berlin (2009)","DOI":"10.1007\/978-3-540-93900-9_14"},{"issue":"7","key":"321_CR13","doi-asserted-by":"crossref","first-page":"840","DOI":"10.1016\/j.ic.2008.03.003","volume":"206","author":"D Gurov","year":"2008","unstructured":"Gurov, D., Huisman, M., Sprenger, C.: Compositional verification of sequential programs with procedures. Inf. Comput. 206(7), 840\u2013868 (2008)","journal-title":"Inf. Comput."},{"key":"321_CR14","unstructured":"Hubbers, E., Poll, E.: Transactions and non-atomic API methods in Java Card: specification ambiguity and strange implementation behaviours. Technical Report NIII-R0438, Radboud University Nijmegen (2004)"},{"key":"321_CR15","doi-asserted-by":"crossref","unstructured":"Hubert, L., Barr\u00e9, N., Besson, F. Demange, D., Jensen, T., Monfort, V., Pichardie, D., Turpin, T.: Sawja: Static Analysis Workshop for Java. In: Formal Verification of Object-Oriented Software (FoVeOOS \u201910), vol. 6528 of LNCS. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-18070-5_7"},{"key":"321_CR16","doi-asserted-by":"crossref","unstructured":"Huisman, M., Aktug, I., Gurov, D.: Program models for compositional verification. In: International Conference on Formal Engineering Methods (ICFEM \u201908), vol. 5256 of LNCS, pp. 147\u2013166. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88194-0_11"},{"key":"321_CR17","doi-asserted-by":"crossref","unstructured":"Huisman, M., Gurov, D.: CVPP: A tool set for compositonal verification of control-flow safety properties. In: Formal Verification of Object-Oriented Software (FoVeOOS \u201910), vol. 6528 of LNCS, pp. 107\u2013121. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-18070-5_8"},{"key":"321_CR18","unstructured":"Kiefer, S., Schwoon, S., Suwimonteerabuth, D.: Moped - a model-checker for pushdown systems. http:\/\/www.informatik.uni-stuttgart.de\/fmi\/szs\/tools\/moped\/"},{"key":"321_CR19","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ -calculus. Theo Comput Sci 27, 333\u2013354 (1983)","journal-title":"Theo Comput Sci"},{"key":"321_CR20","doi-asserted-by":"crossref","unstructured":"Larsen, K.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, vol. 407 of LNCS, pp. 232\u2013246. Springer, Berlin (1989)","DOI":"10.1007\/3-540-52148-8_19"},{"key":"321_CR21","unstructured":"Leavens, G., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual, Feb. 2007. Department of Computer Science, Iowa State University. Available from http:\/\/www.jmlspecs.org"},{"key":"321_CR22","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P.: Modular Specification and Verification of Object-Oriented Programs, vol. 2262 of LNCS. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45651-1"},{"key":"321_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: IEEE Symposium on Foundations of Computer Science (FOCS \u201977), pp. 46\u201357. IEEE Computer Society, Washington, DC (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"321_CR24","unstructured":"Rot, J., de Boer, F., Bonsangue. M.: A pushdown system representation for unbounded object creation. In: Informal pre-proceedings of Formal Verification of Object-Oriented Software (FoVeOOS \u201910) (2010)"},{"key":"321_CR25","unstructured":"Sail-web application, 2012. https:\/\/code.google.com\/p\/sail-web\/"},{"key":"321_CR26","doi-asserted-by":"crossref","unstructured":"Schaefer, I., Gurov, D., Soleimanifard, S.: Compositional algorithmic verification of software product lines. In: Formal Methods for Components and Objects (FMCO \u201910), vol. 6957 of LNCS, pp. 184\u2013203. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-25271-6_10"},{"issue":"1","key":"321_CR27","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Infin Syst Security 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Infin Syst Security"},{"key":"321_CR28","unstructured":"Soleimanifard, S., Gurov, D., Huisman, M.: PROMOVER web interface. http:\/\/www.csc.kth.se\/~siavashs\/ProMoVer"},{"key":"321_CR29","doi-asserted-by":"crossref","unstructured":"Soleimanifard, S., Gurov, D., Huisman, M.: ProMoVer: Modular verification of temporal safety properties. In: Barthe, G., Pardo, A., Schneider, G. (eds.) Software Engineering and Formal Methods (SEFM \u201911), vol. 7041 of LNCS, pp. 366\u2013381. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24690-6_25"},{"key":"321_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3550-5","volume-title":"Modal and Temporal Logics of Processes","author":"C Stirling","year":"2001","unstructured":"Stirling, C.: Modal and Temporal Logics of Processes. Springer, Berlin (2001)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0321-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-013-0321-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0321-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,10]],"date-time":"2019-07-10T10:39:00Z","timestamp":1562755140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-013-0321-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,7]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["321"],"URL":"https:\/\/doi.org\/10.1007\/s10270-013-0321-0","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,7]]}}}