{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:20:59Z","timestamp":1771485659738,"version":"3.50.1"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031384981","type":"print"},{"value":"9783031384998","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper introduces a uniform substitution calculus for <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf {d{}L}} {}_{\\text {CHP}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mrow>\n                      <mml:mi>d<\/mml:mi>\n                      <mml:mrow\/>\n                      <mml:mi>L<\/mml:mi>\n                    <\/mml:mrow>\n                    <mml:msub>\n                      <mml:mrow\/>\n                      <mml:mtext>CHP<\/mml:mtext>\n                    <\/mml:msub>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious prover kernels by using axioms instead of axiom schemata. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in side conditions. Even though communication and parallelism reasoning are notorious for necessitating subtle soundness-critical side conditions, uniform substitution when generalized to <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf {d{}L}} {}_{\\text {CHP}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mrow>\n                      <mml:mi>d<\/mml:mi>\n                      <mml:mrow\/>\n                      <mml:mi>L<\/mml:mi>\n                    <\/mml:mrow>\n                    <mml:msub>\n                      <mml:mrow\/>\n                      <mml:mtext>CHP<\/mml:mtext>\n                    <\/mml:msub>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> manages to limit and isolate their conceptual overhead. Since uniform substitution has proven to simplify the implementation of hybrid systems provers substantially, uniform substitution for <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf {d{}L}} {}_{\\text {CHP}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mrow>\n                      <mml:mi>d<\/mml:mi>\n                      <mml:mrow\/>\n                      <mml:mi>L<\/mml:mi>\n                    <\/mml:mrow>\n                    <mml:msub>\n                      <mml:mrow\/>\n                      <mml:mtext>CHP<\/mml:mtext>\n                    <\/mml:msub>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_6","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"96-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Uniform Substitution for\u00a0Dynamic Logic with\u00a0Communicating Hybrid Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9656-2830","authenticated-orcid":false,"given":"Marvin","family":"Brieger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3194-9759","authenticated-orcid":false,"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"KR Apt","year":"2010","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd edn. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-1-84882-745-5","edition":"3"},{"issue":"3","key":"6_CR2","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"KR Apt","year":"1980","unstructured":"Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 2(3), 359\u2013385 (1980). https:\/\/doi.org\/10.1145\/357103.357110","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-06251-8_4","volume-title":"Relational and Algebraic Methods in Computer Science","author":"A Armstrong","year":"2014","unstructured":"Armstrong, A., Gomes, V.B.F., Struth, G.: Algebras for program correctness in Isabelle\/HOL. In: H\u00f6fner, P., Jipsen, P., Kahl, W., M\u00fcller, M.E. (eds.) RAMICS 2014. LNCS, vol. 8428, pp. 49\u201364. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06251-8_4"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Armstrong, P.J., Lowe, G., Ouaknine, J., Roscoe, B.: Model checking timed CSP. In: Voronkov, A., Korovina, M.V. (eds.) HOWARD-60: A Festschrift on the Occasion of Howard Barringer\u2019s 60th Birthday, EPiC Series in Computing, vol. 42, pp. 13\u201333. EasyChair (2014). https:\/\/doi.org\/10.29007\/6fqk","DOI":"10.29007\/6fqk"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Brieger, M., Mitsch, S., Platzer, A.: Dynamic logic of communicating hybrid programs. CoRR abs\/2302.14546 (2023). https:\/\/doi.org\/10.48550\/arXiv.2302.14546","DOI":"10.48550\/arXiv.2302.14546"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Brieger, M., Mitsch, S., Platzer, A.: Uniform substitution for dynamic logic with communicating hybrid programs. CoRR abs\/2303.17333 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.17333","DOI":"10.48550\/arXiv.2303.17333"},{"key":"6_CR8","volume-title":"Introduction to Mathematical Logic","author":"A Church","year":"1956","unstructured":"Church, A.: Introduction to Mathematical Logic. Princeton University Press, Princeton (1956)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Cong, X., Yu, H., Xu, X.: Verification of hybrid chi model for cyber-physical systems using PHAVer. In: Barolli, L., You, I., Xhafa, F., Leu, F., Chen, H. (eds.) Proceedings of the 7th International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing (IMIS), pp. 122\u2013128. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/IMIS.2013.29","DOI":"10.1109\/IMIS.2013.29"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera\u00a0X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3\u2014a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-319-69483-2_7","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"DP Guelev","year":"2017","unstructured":"Guelev, D.P., Wang, S., Zhan, N.: Compositional Hoare-style reasoning about hybrid CSP in the duration calculus. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 110\u2013127. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_7"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09237-4","volume-title":"First-Order Dynamic Logic","year":"1979","unstructured":"Harel, D. (ed.): First-Order Dynamic Logic. LNCS, vol. 68. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09237-4"},{"issue":"8","key":"6_CR15","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978). https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"6_CR17","unstructured":"Jifeng, H.: From CSP to hybrid systems In: A Classical Mind: Essays in Honour of C. A. R. Hoare, pp. 171\u2013189. Prentice Hall International (1994)"},{"issue":"3","key":"6_CR18","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"6_CR19","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BF00289266","volume":"15","author":"G Levin","year":"1981","unstructured":"Levin, G., Gries, D.: A proof technique for communicating sequential processes. Acta Informatica 15(3), 281\u2013302 (1981). https:\/\/doi.org\/10.1007\/BF00289266","journal-title":"Acta Informatica"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17164-2_1","volume-title":"Programming Languages and Systems","author":"J Liu","year":"2010","unstructured":"Liu, J., et al.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1\u201315. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17164-2_1"},{"issue":"2","key":"6_CR21","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1142\/S0218194005002385","volume":"15","author":"KL Man","year":"2005","unstructured":"Man, K.L., Reniers, M.A., Cuijpers, P.J.L.: Case studies in the hybrid process algebra HyPA. Int. J. Softw. Eng. Knowl. Eng. 15(2), 299\u2013306 (2005). https:\/\/doi.org\/10.1142\/S0218194005002385","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"issue":"4","key":"6_CR22","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7(4), 417\u2013426 (1981). https:\/\/doi.org\/10.1109\/TSE.1981.230844","journal-title":"IEEE Trans. Softw. Eng."},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-64354-6_2","volume-title":"Deductive Software Verification: Future Perspectives","author":"S Mitsch","year":"2020","unstructured":"Mitsch, S., Platzer, A.: A retrospective on developing hybrid system provers in the KeYmaera family. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.) Deductive Software Verification: Future Perspectives. LNCS, vol. 12345, pp. 21\u201364. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_2"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-319-33693-0_28","volume-title":"Integrated Formal Methods","author":"A M\u00fcller","year":"2016","unstructured":"M\u00fcller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: A component-based approach to hybrid systems safety verification. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 441\u2013456. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_28"},{"key":"6_CR25","unstructured":"Nieto, L.P.: Verification of parallel programs with the Owicki-Gries and Rely-Guarantee methods in Isabelle\/HOL. Ph.D. thesis, Technical University Munich, Germany (2002). http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/prensa_nieto.html"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-49020-3_13","volume-title":"Fundamental Approaches to Software Engineering","author":"T Nipkow","year":"1999","unstructured":"Nipkow, T., Nieto, L.P.: Owicki\/Gries in Isabelle\/HOL. In: Finance, J.-P. (ed.) FASE 1999. LNCS, vol. 1577, pp. 188\u2013203. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-540-49020-3_13"},{"key":"6_CR27","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319\u2013340 (1976). https:\/\/doi.org\/10.1007\/BF00268134","journal-title":"Acta Informatica"},{"issue":"2","key":"6_CR28","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2), 143\u2013189 (2008). https:\/\/doi.org\/10.1007\/s10817-008-9103-8","journal-title":"J. Autom. Reas."},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Differential game logic. ACM Trans. Comput. Log. 17(1), 1:1\u20131:51 (2015). https:\/\/doi.org\/10.1145\/2817824","DOI":"10.1145\/2817824"},{"issue":"2","key":"6_CR30","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2017","unstructured":"Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas. 59(2), 219\u2013265 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9385-1","journal-title":"J. Autom. Reas."},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-319-94205-6_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2018","unstructured":"Platzer, A.: Uniform substitution for differential game logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 211\u2013227. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_15"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-030-29436-6_25","volume-title":"Automated Deduction \u2013 CADE 27","author":"A Platzer","year":"2019","unstructured":"Platzer, A.: Uniform substitution at one fell swoop. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 425\u2013441. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_25"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Platzer, A., Tan, Y.K.: Differential equation invariance axiomatization. J. ACM 67(1), 6:1\u20136:66 (2020). https:\/\/doi.org\/10.1145\/3380825","DOI":"10.1145\/3380825"},{"key":"6_CR34","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du I congr\u00e8s de Math\u00e9maticiens des Pays Slaves (1931)"},{"key":"6_CR35","unstructured":"de Roever, W.P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press (2001)"},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-031-08166-8_20","volume-title":"The Logic of Software. A Tasting Menu of Formal Methods","author":"G Schellhorn","year":"2022","unstructured":"Schellhorn, G., Bodenm\u00fcller, S., Bitterlich, M., Reif, W.: Software & system verification with KIV. In: Ahrendt, W., Beckert, B., Bubel, R., Johnsen, E.B. (eds.) The Logic of Software. A Tasting Menu of Formal Methods. LNCS, vol. 13360, pp. 408\u2013436. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-08166-8_20"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-031-27481-7_11","volume-title":"Formal Methods","author":"H Sheng","year":"2023","unstructured":"Sheng, H., Bentkamp, A., Zhan, B.: HHLPy: practical verification of hybrid systems using Hoare logic. In: Chechik, M., Katoen, J., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 160\u2013178. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_11"},{"issue":"3\u20134","key":"6_CR38","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/s00165-018-0453-7","volume":"30","author":"L Shi","year":"2018","unstructured":"Shi, L., Zhao, Y., Liu, Y., Sun, J., Dong, J.S., Qin, S.: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS. Formal Aspects Comput. 30(3\u20134), 351\u2013380 (2018). https:\/\/doi.org\/10.1007\/s00165-018-0453-7","journal-title":"Formal Aspects Comput."},{"key":"6_CR39","unstructured":"Smans, J., Vanoverberghe, D., Devriese, D., Jacobs, B., Piessens, F.: Shared boxes: rely-guarantee reasoning in VeriFast. Technical report, Katholieke Universiteit Leuven, Netherlands (2014). https:\/\/lirias.kuleuven.be\/handle\/123456789\/456819"},{"key":"6_CR40","doi-asserted-by":"publisher","unstructured":"Song, H., Compton, K.J., Rounds, W.C.: SPHIN: a model checker for reconfigurable hybrid systems based on SPIN. In: Lazic, R., Nagarajan, R. (eds.) Proceedings of the 5th International Workshop Automated Verification of Critical Systems (AVoCS). ENTCS, vol. 145, pp. 167\u2013183. Elsevier (2005). https:\/\/doi.org\/10.1016\/j.entcs.2005.10.011","DOI":"10.1016\/j.entcs.2005.10.011"},{"key":"6_CR41","doi-asserted-by":"publisher","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951). https:\/\/doi.org\/10.1525\/9780520348097","edition":"2"},{"key":"6_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-29952-0_13","volume-title":"Theory and Applications of Models of Computation","author":"S Wang","year":"2012","unstructured":"Wang, S., Zhan, N., Guelev, D.: An assume\/guarantee based compositional calculus for hybrid CSP. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) TAMC 2012. LNCS, vol. 7287, pp. 72\u201383. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29952-0_13"},{"key":"6_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25"},{"issue":"2","key":"6_CR44","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2), 149\u2013174 (1997). https:\/\/doi.org\/10.1007\/BF01211617","journal-title":"Formal Aspects Comput."},{"key":"6_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54108-7_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"L Zou","year":"2014","unstructured":"Zou, L., et al.: Verifying Chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262\u2013280. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_14"},{"key":"6_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/3-540-12896-4_384","volume-title":"Logics of Programs","author":"J Zwiers","year":"1984","unstructured":"Zwiers, J., de Bruin, A., de Roever, W.P.: A proof system for partial correctness of dynamic networks of processes. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 513\u2013527. Springer, Heidelberg (1984). https:\/\/doi.org\/10.1007\/3-540-12896-4_384"},{"key":"6_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/BFb0015776","volume-title":"Automata, Languages and Programming","author":"J Zwiers","year":"1985","unstructured":"Zwiers, J., de Roever, W.P., van Emde Boas, P.: Compositionality and concurrent networks: soundness and completeness of a proofsystem. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 509\u2013519. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/BFb0015776"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:04:22Z","timestamp":1693609462000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}