{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T05:52:54Z","timestamp":1757310774913,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816872"},{"type":"electronic","value":"9783030816889"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>First-Order Linear Temporal Logic (FOLTL) is particularly convenient to specify distributed systems, in particular because of the unbounded aspect of their state space. We have recently exhibited novel decidable fragments of FOLTL which pave the way for tractable verification. However, these fragments are not expressive enough for realistic specifications. In this paper, we propose three transformations to translate a typical FOLTL specification into two of its decidable fragments. All three transformations are proved sound (the associated propositions are proved in Coq) and have a high degree of automation. To put these techniques into practice, we propose a specification language relying on FOLTL, as well as a prototype which performs the verification, relying on existing model checkers. This approach allows us to successfully verify safety and liveness properties for various specifications of distributed systems from the literature.\n<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_16","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"337-360","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Sound Verification Procedures for Temporal Properties of Infinite-State Systems"],"prefix":"10.1007","author":[{"given":"Quentin","family":"Peyras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Brunel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4136-783X","authenticated-orcid":false,"given":"David","family":"Chemouil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010). https:\/\/doi.org\/10.1017\/cbo9781139195881","DOI":"10.1017\/cbo9781139195881"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.: Parameterized verification with automatically computed inductive assertions? In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221\u2013234. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_19"},{"issue":"2","key":"16_CR3","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/68182.68193","volume":"17","author":"DL Black","year":"1989","unstructured":"Black, D.L., Rashid, R.F., Golub, D.B., Hill, C.R.: Translation lookaside buffer consistency: a software approach. ACM SIGARCH Comput. Archit. News 17(2), 113\u2013122 (1989). https:\/\/doi.org\/10.1145\/68182.68193","journal-title":"ACM SIGARCH Comput. Archit. News"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The electrum analyzer: model checking relational first-order temporal specifications. In: 33rd ACM\/IEEE International Conference on Automated Software Engineering (ASE 2018). Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ACM Press, Montpellier, France, September 2018. https:\/\/doi.org\/10.1145\/3238147.3240475","DOI":"10.1145\/3238147.3240475"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"issue":"5","key":"16_CR6","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"E Chang","year":"1979","unstructured":"Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281\u2013283 (1979). https:\/\/doi.org\/10.1145\/359104.359108","journal-title":"Commun. ACM"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Conchon, S., Declerck, D., Za\u00efdi, F.: Cubicle-$$\\cal{W}$$ : Parameterized model checking on weak memory. In: International Joint Conference on Automated Reasoning, pp. 152\u2013160. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_11","DOI":"10.1007\/978-3-319-94205-6_11"},{"issue":"7","key":"16_CR8","doi-asserted-by":"publisher","first-page":"1307","DOI":"10.1007\/s10817-020-09565-w","volume":"64","author":"S Conchon","year":"2020","unstructured":"Conchon, S., Declerck, D., Za\u00efdi, F.: Parameterized model checking on the TSO weak memory model. J. Autom. Reason. 64(7), 1307\u20131330 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09565-w","journal-title":"J. Autom. Reason."},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-31424-7_55","volume-title":"Computer Aided Verification","author":"S Conchon","year":"2012","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718\u2013724. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_55"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-19249-9_9","volume-title":"FM 2015: Formal Methods","author":"S Conchon","year":"2015","unstructured":"Conchon, S., Mebsout, A., Za\u00efdi, F.: Certificates for parameterized model checking. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 126\u2013142. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_9"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proving liveness of parameterized programs. In: 2016 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201312 (2016). https:\/\/doi.org\/10.1145\/2933575.2935310","DOI":"10.1145\/2933575.2935310"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., et al.: Ironfleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 1\u201317 (2015). https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"issue":"1\u20133","key":"16_CR13","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/s0168-0072(00)00018-x","volume":"106","author":"I Hodkinson","year":"2000","unstructured":"Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable fragments of first-order temporal logics. Ann. Pure Appl. Logic 106(1\u20133), 85\u2013134 (2000). https:\/\/doi.org\/10.1016\/s0168-0072(00)00018-x","journal-title":"Ann. Pure Appl. Logic"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45653-8_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"I Hodkinson","year":"2001","unstructured":"Hodkinson, I., Wolter, F., Zakharyaschev, M.: Monodic fragments of first-order temporal logics: 2000\u20132001 A.D. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 1\u201323. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45653-8_1"},{"issue":"1","key":"16_CR15","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1145\/3009837.3009893","volume":"52","author":"J Hoenicke","year":"2017","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. ACM SIGPLAN Not. 52(1), 473\u2013485 (2017). https:\/\/doi.org\/10.1145\/3009837.3009893","journal-title":"ACM SIGPLAN Not."},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-319-46520-3_14","volume-title":"Automated Technology for Verification and Analysis","author":"D Kuperberg","year":"2016","unstructured":"Kuperberg, D., Brunel, J., Chemouil, D.: On finite domains in first-order linear temporal logic. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 211\u2013226. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_14"},{"key":"16_CR17","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional (2002)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Padon, O.: Deductive Verification of Distributed Protocols in First-Order Logic. Ph.D. thesis, Ph.D. Dissertation. Tel Aviv University (2018)","DOI":"10.23919\/FMCAD.2018.8603010"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. In: Proceedings of the ACM Conference on Principles of Programming Languages (POPL) 2, 26 (2017). https:\/\/doi.org\/10.1145\/3158114","DOI":"10.1145\/3158114"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made epr: decidable reasoning about distributed protocols. Proc. ACM on Program. Lang. 1(OOPSLA), 108 (2017). https:\/\/doi.org\/10.1145\/3140568D","DOI":"10.1145\/3140568D"},{"issue":"6","key":"16_CR21","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1145\/2980983.2908118","volume":"51","author":"O Padon","year":"2016","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. ACM SIGPLAN Not. 51(6), 614\u2013630 (2016). https:\/\/doi.org\/10.1145\/2980983.2908118","journal-title":"ACM SIGPLAN Not."},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Peyras, Q., Bodeveix, J.P., Brunel, J., Chemouil, D.: Cervino prototype, Coq formalization and Benchmarks (CAV 2021 artifact) (Apr 2021). https:\/\/doi.org\/10.5281\/zenodo.4725675","DOI":"10.5281\/zenodo.4725675"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Peyras, Q., Brunel, J., Chemouil, D.: A bounded domain property for an expressive fragment of first-order linear temporal logic. In: Gamper, J., Pinchinat, S., Sciavicco, G. (eds.) 26th International Symposium on Temporal Representation and Reasoning, TIME 2019, October 16\u201319, 2019, M\u00e1laga, Spain. LIPIcs, vol. 147, pp. 15:1\u201315:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.TIME.2019.15","DOI":"10.4230\/LIPIcs.TIME.2019.15"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Peyras, Q., Brunel, J., Chemouil, D.: A decidable and expressive fragment of many-sorted first-order linear temporal logic. Information and Computation p. 104641 (2020). https:\/\/doi.org\/10.1016\/j.ic.2020.104641","DOI":"10.1016\/j.ic.2020.104641"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82\u201397. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_7"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Shapiro, M., Pregui\u00e7a, N., Baquero, C., Zawirski, M.: A comprehensive study of convergent and commutative replicated data types. Ph.D. thesis, Inria-Centre Paris-Rocquencourt; INRIA (2011)","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.: Verdi: a framework for implementing and formally verifying distributed systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 357\u2013368 (2015). https:\/\/doi.org\/10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81688-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:24:30Z","timestamp":1626452670000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"290","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":"63","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":"0","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":"22% - 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":"12","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)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}