{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T00:27:46Z","timestamp":1768264066788,"version":"3.49.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,3,10]],"date-time":"2012-03-10T00:00:00Z","timestamp":1331337600000},"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":[[2013,5]]},"DOI":"10.1007\/s10270-012-0230-7","type":"journal-article","created":{"date-parts":[[2012,3,9]],"date-time":"2012-03-09T01:47:50Z","timestamp":1331257670000},"page":"285-306","source":"Crossref","is-referenced-by-count":16,"title":["Relational interprocedural verification of concurrent programs"],"prefix":"10.1007","volume":"12","author":[{"given":"Bertrand","family":"Jeannet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,3,10]]},"reference":[{"key":"230_CR1","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Concurrency Theory, CONCUR\u201905. LNCS, vol. 3653 (2005)","DOI":"10.1007\/11539452_36"},{"issue":"8","key":"230_CR2","first-page":"377","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput 35(8), 377 (1986)","journal-title":"IEEE Trans. Comput"},{"issue":"1","key":"230_CR3","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D. Caucal","year":"1992","unstructured":"Caucal D.: On the regular structure of prefix rewriting. Theor. Comput. Sci 106(1), 61 (1992)","journal-title":"Theor. Comput. Sci"},{"key":"230_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Int. Symp. on Programming, Dunod, Paris (1976)","DOI":"10.1145\/390018.808314"},{"key":"230_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conf. on Formal Description of Programming Concepts (1977)","DOI":"10.1145\/390017.808314"},{"issue":"2\u20133","key":"230_CR6","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot P., Cousot R.: Abstract interpretation and application to logic programs. J. Logic Program 13(2\u20133), 103 (1992)","journal-title":"J. Logic Program"},{"key":"230_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Prog. Languages, POPL\u201978. ACM, New York (1978)","DOI":"10.1145\/512760.512770"},{"key":"230_CR8","doi-asserted-by":"crossref","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Foundations of Software Science and Computation Structure, FoSSaCS \u201999. LNCS, vol. 1578 (1999)","DOI":"10.1007\/3-540-49019-1_2"},{"key":"230_CR9","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: Principles of Prog. Languages, POPL\u201900. ACM, New York (2000)","DOI":"10.1145\/325694.325697"},{"key":"230_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Lifshin, M., Qadeer, S.: Types for atomicity: static checking and inference for java. ACM Trans. Program. Lang. Syst. 30(4) (2008)","DOI":"10.1145\/1377492.1377495"},{"issue":"1\u20133","key":"230_CR11","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/j.tcs.2004.12.006","volume":"338","author":"C. Flanagan","year":"2005","unstructured":"Flanagan C., Freund S.N., Qadeer S., Seshia S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci 338(1\u20133), 153\u2013183 (2005)","journal-title":"Theor. Comput. Sci"},{"key":"230_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: SPIN\u201903: Workshop on Model Checking Software. LNCS, vol. 2648 (2003)","DOI":"10.1007\/3-540-44829-2_14"},{"key":"230_CR13","doi-asserted-by":"crossref","unstructured":"Ghenassia, F. (ed.): Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems. Springer, Berlin (2005)","DOI":"10.1007\/b137175"},{"key":"230_CR14","unstructured":"Gopan, D., Reps, T.W.: Guided static analysis. In: Static Analysis Symposium, SAS\u201907. LNCS, vol. 4634 (Aug 2007)"},{"key":"230_CR15","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: SPIN\u201907: Model Checking Software. LNCS, vol. 4595 (2007)"},{"issue":"1","key":"230_CR16","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/s10703-006-0013-2","volume":"29","author":"N. Halbwachs","year":"2006","unstructured":"Halbwachs N., Merchat D., Gonnord L.: Some ways to reduce the space dimension in polyhedra computations. Formal Methods Syst. Des 29(1), 79\u201395 (2006)","journal-title":"Formal Methods Syst. Des"},{"key":"230_CR17","unstructured":"Jeannet, B.: The BDDAPRON logico-numerical abstract domains library. http:\/\/www.inrialpes.fr\/pop-art\/people\/bjeannet\/bjeannet-forge\/bddapron\/"},{"key":"230_CR18","unstructured":"Jeannet, B.: The ConcurInterproc interprocedural analyzer for concurrent programs. http:\/\/pop-art.inrialpes.fr\/interproc\/concurinterprocweb.cgi"},{"key":"230_CR19","unstructured":"Jeannet, B.: The Fixpoint equation solver http:\/\/www.inrialpes.fr\/pop-art\/people\/bjeannet\/bjeannet-forge\/fixpoint\/"},{"key":"230_CR20","doi-asserted-by":"crossref","unstructured":"Jeannet, B.: Relational interprocedural analysis of concurrent programs. Technical Report 6671, INRIA (Oct 2008)","DOI":"10.1109\/SEFM.2009.29"},{"key":"230_CR21","doi-asserted-by":"crossref","unstructured":"Jeannet, B.: Relational interprocedural verification of concurrent programs. In: Software Engineering and Formal Methods, SEFM\u201909. IEEE (Nov 2009)","DOI":"10.1109\/SEFM.2009.29"},{"key":"230_CR22","doi-asserted-by":"crossref","unstructured":"Jeannet, B.: Some experience on the software engineering of abstract interpretation tools. In: Int. Workshop on Tools for Automatic Program AnalysiS, TAPAS\u20192010. ENTCS, vol. 267, pp. 29\u201342. Elsevier, Amsterdam (2010)","DOI":"10.1016\/j.entcs.2010.09.016"},{"key":"230_CR23","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. In: Static Analysis Symposium, SAS\u201904. LNCS, vol. 3148 (2004)","DOI":"10.1007\/978-3-540-27864-1_19"},{"key":"230_CR24","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. ACM Trans. Program. Lang. Syst. (TOPLAS), 32(2), Article 5 (2010)","DOI":"10.1145\/1667048.1667050"},{"key":"230_CR25","unstructured":"Jeannet, B., Min\u00e9, A.: APRON: A library of numerical abstract domains for static analysis. In: Computer Aided Verification, CAV\u20192009. LNCS, vol. 5643, pp. 661\u2013667 (2009). http:\/\/apron.cri.ensmp.fr\/library\/"},{"key":"230_CR26","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Serwe, W.: Abstracting call stacks for interprocedural verification of imperative programs. In: Int. Conf. on Algebraic Methodology and Software Technology, AMAST\u201904. LNCS, vol. 3116 (2004)","DOI":"10.1007\/978-3-540-27815-3_22"},{"key":"230_CR27","doi-asserted-by":"crossref","unstructured":"Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Compiler Construction, CC\u201992. LNCS, vol. 641 (1992)","DOI":"10.1007\/3-540-55984-1_13"},{"key":"230_CR28","unstructured":"Lal, A., Touili, T., Kidd, N., Reps, T.W.: Interprocedural analysis of concurrent programs under a context bound. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908. LNCS (2008)"},{"key":"230_CR29","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symposium, SAS\u201900, pp. 280\u2013301 (2000)","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"230_CR30","doi-asserted-by":"crossref","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification is cartesian abstract interpretation. In: Int. Colloquium on Theoretical Aspects of Computing (ICTAC\u201906). LNCS, vol. 4281 (2006)","DOI":"10.1007\/11921240_13"},{"issue":"1","key":"230_CR31","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9 A.: The octagon abstract domain. Higher-Order Symb. Comput 19(1), 31\u2013100 (2006)","journal-title":"Higher-Order Symb. Comput"},{"key":"230_CR32","doi-asserted-by":"crossref","unstructured":"Patin, G., Sighireanu, M., Touili, T.: Spade: Verification of multithreaded dynamic and recursive programs. In: Computer Aided Verification, CAV\u201907. LNCS, vol. 4590 (2007)","DOI":"10.1007\/978-3-540-73368-3_28"},{"key":"230_CR33","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rajamani, S.K., Rehof, J.: Summarizing procedures in concurrent programs. In: Principles of Programming Languages, POPL\u201904. ACM, New York (2004)","DOI":"10.1145\/964001.964022"},{"issue":"2","key":"230_CR34","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst 22(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"230_CR35","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Principles of Prog. Languages, POPL\u201995. ACM, New York (1995)","DOI":"10.1145\/199448.199462"},{"issue":"1\u20132","key":"230_CR36","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T. Reps","year":"2005","unstructured":"Reps T., Schwoon S., Jha S., Melski D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program 58(1\u20132), 206\u2013263 (2005)","journal-title":"Sci. Comput. Program"},{"issue":"3","key":"230_CR37","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv M., Reps T., Wilhelm R.: Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Syst 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Prog. Lang. Syst"},{"key":"230_CR38","volume-title":"Program Flow Analysis: Theory and Applications, chap.~7","author":"M. Sharir","year":"1981","unstructured":"Sharir M., Pnueli A.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds) Program Flow Analysis: Theory and Applications, chap.~7, Prentice Hall, Upper Saddle River (1981)"},{"key":"230_CR39","unstructured":"Somenzi, F.: Cudd: Colorado University Decision Diagram Package. ftp:\/\/vlsi.colorado.edu\/pub"},{"key":"230_CR40","volume-title":"Synchronization Algorithms and Concurrent Programming","author":"G. Taubenfeld","year":"2006","unstructured":"Taubenfeld G.: Synchronization Algorithms and Concurrent Programming. Prentice Hall, Upper Saddle River (2006)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-012-0230-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-012-0230-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-012-0230-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,2]],"date-time":"2022-01-02T05:46:38Z","timestamp":1641102398000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-012-0230-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,10]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,5]]}},"alternative-id":["230"],"URL":"https:\/\/doi.org\/10.1007\/s10270-012-0230-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,10]]}}}