{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:48:57Z","timestamp":1771573737897,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T00:00:00Z","timestamp":1667260800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T00:00:00Z","timestamp":1667260800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s10009-022-00680-0","type":"journal-article","created":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T03:02:46Z","timestamp":1667271766000},"page":"977-997","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Automated formal analysis of temporal properties of Ladder programs"],"prefix":"10.1007","volume":"24","author":[{"given":"Cl\u00e1udio","family":"Belo Louren\u00e7o","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Denis","family":"Cousineau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Faissole","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Mentr\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroaki","family":"Inoue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,11,1]]},"reference":[{"key":"680_CR1","doi-asserted-by":"publisher","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Tim King, J. D., Reynolds, A., Cesare, T.: CVC4. In: CAV: computer aided verification. Lecture notes in computer science, vol. 6806, pp. 171\u2013177. Springer. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"680_CR2","unstructured":"Baudin, L.: Deductive verification with the help of abstract interpretation. Technical report, Univ Paris-Sud. https:\/\/hal.inria.fr\/hal-01634318 (2017)"},{"key":"680_CR3","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C specification language, version 1.16. https:\/\/frama-c.com\/html\/acsl.html (2020)"},{"key":"680_CR4","doi-asserted-by":"publisher","unstructured":"Becker, B., Belo Louren\u00e7o, C., March\u00e9, C.: Explaining counterexamples with giant-step assertion checking. In: F-IDE \u2013 6th workshop on formal integrated development environments. Electronic proceedings in theoretical computer science. https:\/\/hal.inria.fr\/hal-03217393, https:\/\/doi.org\/10.4204\/EPTCS.338.10 (2021)","DOI":"10.4204\/EPTCS.338.10"},{"key":"680_CR5","doi-asserted-by":"publisher","unstructured":"Belo\u00a0Louren\u00e7o, C., Cousineau, D., Faissole, F., March\u00e9, C., Mentr\u00e9, D., Inoue, H.: Automated verification of temporal properties of ladder programs. In: FMICS: formal methods for industrial critical systems. Lecture notes in computer science, vol. 12863, pp. 21\u201338. https:\/\/hal.inria.fr\/hal-03281580, https:\/\/doi.org\/10.1007\/978-3-030-85248-1_2 (2021)","DOI":"10.1007\/978-3-030-85248-1_2"},{"key":"680_CR6","doi-asserted-by":"crossref","unstructured":"Biallas, S., Kowalewski, S., Stattelmann, S., Schlich, B.: Efficient handling of states in abstract interpretation of industrial programmable logic controller code. In: 12th international workshop on discrete event systems, pp. 400\u2013405. IFAC (2014)","DOI":"10.3182\/20140514-3-FR-4046.00065"},{"key":"680_CR7","unstructured":"Bobot, F, Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie\u2013first international workshop on intermediate verification languages, pp. 53\u201364. http:\/\/hal.inria.fr\/hal-00790310 (2011)"},{"issue":"6","key":"680_CR8","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/s10009-014-0314-5","volume":"17","author":"F Bobot","year":"2015","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Let\u2019s verify this with Why3. Int. J. Softw. Tools Technol. Transf (STTT) 17(6), 709\u2013727 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0314-5","journal-title":"Int. J. Softw. Tools Technol. Transf (STTT)"},{"key":"680_CR9","doi-asserted-by":"publisher","unstructured":"Bolton, W.: Programmable Logic Controllers (6th edn). Newnes. (2015) https:\/\/doi.org\/10.1016\/C2014-0-03884-1","DOI":"10.1016\/C2014-0-03884-1"},{"key":"680_CR10","unstructured":"Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-Ergo 2.2. In: SMT\u2013international workshop on satisfiability modulo theories. (2018) https:\/\/hal.inria.fr\/hal-01960203"},{"key":"680_CR11","doi-asserted-by":"publisher","unstructured":"Cousineau, D., Mentr\u00e9, D., Inoue, H.: Automated deductive verification for ladder programming. In: F-IDE\u2013fifth workshop on formal integrated development environments. Electronic Proceedings in Theoretical Computer Science, vol. 310, pp. 7\u201312. (2019) https:\/\/doi.org\/10.4204\/EPTCS.310.2","DOI":"10.4204\/EPTCS.310.2"},{"key":"680_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.jlamp.2018.05.003","volume":"99","author":"S Dailler","year":"2018","unstructured":"Dailler, S., Hauzar, D., March\u00e9, C., Moy, Y.: Instrumenting a weakest precondition calculus for counterexample generation. J. Log. Algebr. Methods Programm. 99, 97\u2013113 (2018). https:\/\/doi.org\/10.1016\/j.jlamp.2018.05.003","journal-title":"J. Log. Algebr. Methods Programm."},{"key":"680_CR13","doi-asserted-by":"publisher","unstructured":"Darvas, D., Majzik, I., Blanco\u00a0Vi\u00f1uela, E.: Formal verification of safety PLC based control software. In: IFM\u2013Integrated formal methods. Lecture Notes in Computer Science, vol. 9681, pp. 508\u2013522. Springer. (2016) https:\/\/doi.org\/10.1007\/978-3-319-33693-0_32","DOI":"10.1007\/978-3-319-33693-0_32"},{"key":"680_CR14","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L, Bj\u00f8rner, N.: Z3, an efficient SMT solver. In: TACAS : Tools and algorithms for the construction and analysis of systems. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer. (2008) https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"680_CR15","unstructured":"De\u00a0Oliveira, S., Pr\u00e9vosto, V., Bardin, S.: Au temps en emporte le C. In: JFLA: Vingt-sixi\u00e8mes Journ\u00e9es Francophones des langages applicatifs. (2015) https:\/\/hal.inria.fr\/hal-01099128"},{"key":"680_CR16","doi-asserted-by":"publisher","unstructured":"Drath, R., Luder, A., Peschke, J., Hundt, L.: AutomationML\u2013the glue for seamless automation engineering. In: ETFA\u2013IEEE international conference on emerging technologies and factory automation, pp. 616\u2013623. (2008). https:\/\/doi.org\/10.1109\/ETFA.2008.4638461","DOI":"10.1109\/ETFA.2008.4638461"},{"key":"680_CR17","doi-asserted-by":"publisher","unstructured":"Fehnker, A., Huuck, R., Schlich, B., Tapp, M.: Automatic bug detection in microcontroller software by static program analysis. In: SOFSEM \u2013 theory and practice of computer science. Lecture Notes in Computer Science, vol. 5404, pp. 267\u2013278. Springer (2009) https:\/\/doi.org\/10.1007\/978-3-540-95891-8_26","DOI":"10.1007\/978-3-540-95891-8_26"},{"key":"680_CR18","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: CAV \u2013 19th international conference on computer aided verification. Lecture Notes in Computer Science, vol. 4590, pp. 173\u2013177. Springer. (2007) https:\/\/hal.inria.fr\/inria-00270820v1, https:\/\/doi.org\/10.1007\/978-3-540-73368-3_21","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"680_CR19","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2013where programs meet provers. In: ESOP\u201322nd European symposium on programming. Lecture Notes in Computer Science, vol. 7792, pp. 125\u2013128. Springer (2013) http:\/\/hal.inria.fr\/hal-00789533","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"680_CR20","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Abstraction and genericity in Why3. In: ISoLA \u2013 9th international symposium on leveraging applications of formal methods, verification and validation. Lecture Notes in Computer Science, vol. 12476, pp. 122\u2013142. Springer. See also (2020) http:\/\/why3.lri.fr\/isola-2020\/. https:\/\/hal.inria.fr\/hal-02696246","DOI":"10.1007\/978-3-030-61362-4_7"},{"key":"680_CR21","doi-asserted-by":"crossref","unstructured":"Jeannet, Bertrand, Min\u00e9, Antoine: Apron: A library of numerical abstract domains for static analysis. In CAV \u2013 Computer Aided Verification, pages 661\u2013667. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"680_CR22","doi-asserted-by":"publisher","unstructured":"Kosmatov, N., March\u00e9, C., Moy, Y., Signoles, J.: Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: ISoLA\u20137th international symposium on leveraging applications of formal methods, verification and validation. Lecture Notes in Computer Science, vol. 9952, pp. 461\u2013478. Springer (2016) https:\/\/hal.inria.fr\/hal-01344110, https:\/\/doi.org\/10.1007\/978-3-319-47166-2_32","DOI":"10.1007\/978-3-319-47166-2_32"},{"key":"680_CR23","doi-asserted-by":"crossref","unstructured":"John, W., McCormick, Peter, C.: Building High Integrity Applications with SPARK. Cambridge University Press, Chapin (2015)","DOI":"10.1017\/CBO9781139629294"},{"key":"680_CR24","unstructured":"Mitsubishi Electric Corporation. MELSEC iQ-F FX5 CPU module function block reference (for GX Works3). (2016) https:\/\/dl.mitsubishielectric.com\/dl\/fa\/document\/manual\/plcf\/jy997d62701\/jy997d62701j.pdf. Online, accessed 14 June 2022"},{"key":"680_CR25","unstructured":"Mitsubishi Electric Corporation. MELSEC iQ-R Safety Function Block Reference (for GX Works3). (2016) https:\/\/dl.mitsubishielectric.com\/dl\/fa\/document\/manual\/plc\/bcn-p5999-0815\/bcnp59990815c.pdf. Online, accessed 14 June 2022"},{"key":"680_CR26","unstructured":"Mitsubishi Electric Corporation. Mitsubishi l\u00a0\u2014\u00a0MELSEC iQ-R series basic course (for GX Works3). (2016) https:\/\/dl.mitsubishielectric.com\/dl\/fa\/document\/manual\/school_text\/sh081898eng\/sh081898enga.pdf. Online, accessed 30 Mar 2021"},{"key":"680_CR27","doi-asserted-by":"publisher","unstructured":"Nguyen, T., Aoki, T., Tomita, T., Endo, J.: Integrating static program analysis tools for verifying cautions of microcontroller. In: APSEC\u2013Asia-Pacific software engineering conference, pp. 86\u201393. (2019) https:\/\/doi.org\/10.1109\/APSEC48747.2019.00021","DOI":"10.1109\/APSEC48747.2019.00021"},{"key":"680_CR28","doi-asserted-by":"publisher","unstructured":"Ovatman, T., Aral, A., Polat, D., Unver, A.: An overview of model checking practices on verification of PLC software. Softw. Syst. Model. 15, 1\u201324 (2014). https:\/\/doi.org\/10.1007\/s10270-014-0448-7","DOI":"10.1007\/s10270-014-0448-7"},{"key":"680_CR29","doi-asserted-by":"publisher","unstructured":"Ramanathan, R.: The IEC 61131-3 programming languages features for industrial control systems. In: WAC: World automation congress, pp. 598\u2013603. (2014) https:\/\/doi.org\/10.1109\/WAC.2014.6936062","DOI":"10.1109\/WAC.2014.6936062"},{"key":"680_CR30","unstructured":"Roques, A.: PlantUML standard library. https:\/\/plantuml.com\/stdlib (2009). Online, accessed 24 Mar 2021"},{"key":"680_CR31","unstructured":"Stouls, N., Groslambert, J.: V\u00e8rification de propri\u00e8t\u00e8s LTL sur des programmes C par g\u00e8n\u00e8ration d\u2019annotations. Research report. (2011) https:\/\/hal.inria.fr\/inria-00568947"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00680-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00680-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00680-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,2]],"date-time":"2022-12-02T11:58:55Z","timestamp":1669982335000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00680-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,1]]},"references-count":31,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["680"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00680-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,1]]},"assertion":[{"value":"18 October 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 November 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}