{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T06:21:44Z","timestamp":1783146104803,"version":"3.54.6"},"reference-count":74,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100010418","name":"Institute of Information & Communications Technology Planning & Evaluation","doi-asserted-by":"publisher","award":["RS-2024-00439856"],"award-info":[{"award-number":["RS-2024-00439856"]}],"id":[{"id":"10.13039\/501100010418","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100014188","name":"Ministry of Science and ICT, South Korea","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100014188","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["RS-2021-NR060080"],"award-info":[{"award-number":["RS-2021-NR060080"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Logical and Algebraic Methods in Programming"],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1016\/j.jlamp.2026.101130","type":"journal-article","created":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T23:16:19Z","timestamp":1776726979000},"page":"101130","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Bounded model checking of multitask PLC ST programs with preemption using rewriting modulo SMT"],"prefix":"10.1016","volume":"150","author":[{"given":"Jaeseo","family":"Lee","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.jlamp.2026.101130_bib0001","series-title":"Programmable Controllers-Part 3: Programming Languages","year":"1993"},{"key":"10.1016\/j.jlamp.2026.101130_bib0002","series-title":"International Conference on Accelerator and Large Experimental Physics Control Systems","first-page":"911","article-title":"PLCverif: a tool to verify PLC programs based on model checking techniques","author":"Darvas","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101130_bib0003","series-title":"International Workshop on Discrete Event Systems","first-page":"182","article-title":"Efficient representation for formal verification of PLC programs","author":"Gourcuff","year":"2006"},{"key":"10.1016\/j.jlamp.2026.101130_bib0004","series-title":"Discrete Event Systems: Analysis and Control","first-page":"247","article-title":"Formal verification of the sequential part of PLC programs","author":"Lamp\u00e9ri\u00e8re-Couffin","year":"2000"},{"key":"10.1016\/j.jlamp.2026.101130_bib0005","series-title":"Integration of Software Specification Techniques for Applications in Engineering, Priority Program SoftSpez of the German Research Foundation (DFG)","first-page":"517","article-title":"Verification of PLC programs given as sequential function charts","author":"Bauer","year":"2004"},{"key":"10.1016\/j.jlamp.2026.101130_bib0006","series-title":"Proceedings of the Norsk Informatikkonferanse","article-title":"Automatic translation from FBD-PLC-programs to NuSMV for model checking safety-critical control systems","author":"Li","year":"2016"},{"key":"10.1016\/j.jlamp.2026.101130_bib0007","series-title":"Proceedings of the American Control Conference","first-page":"234","article-title":"Formal verification of PLC programs","volume":"1","author":"Rausch","year":"1998"},{"key":"10.1016\/j.jlamp.2026.101130_bib0008","series-title":"Proceedings of the 33rd ACM Symposium on Applied Computing","first-page":"1891","article-title":"Cycle-Bounded model checking of PLC software via dynamic large-block encoding","author":"Bohlender","year":"2018"},{"issue":"2","key":"10.1016\/j.jlamp.2026.101130_bib0009","doi-asserted-by":"crossref","first-page":"151","DOI":"10.3311\/PPee.9743","article-title":"PLC program translation for verification purposes","volume":"61","author":"Darvas","year":"2017","journal-title":"Period. Polytechn. Electr. Eng. Comput. Sci."},{"issue":"10","key":"10.1016\/j.jlamp.2026.101130_bib0010","doi-asserted-by":"crossref","first-page":"4796","DOI":"10.1109\/TSE.2023.3315292","article-title":"K-ST: a formal executable semantics of the structured text language for PLCs","volume":"49","author":"Wang","year":"2023","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.jlamp.2026.101130_bib0011","doi-asserted-by":"crossref","first-page":"14593","DOI":"10.1109\/ACCESS.2019.2894026","article-title":"KST: Executable formal semantics of IEC 61131-3 structured text for verification","volume":"7","author":"Huang","year":"2019","journal-title":"IEEE Access"},{"issue":"6","key":"10.1016\/j.jlamp.2026.101130_bib0012","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","article-title":"An overview of the K semantic framework","volume":"79","author":"Rosu","year":"2010","journal-title":"J. Log. Algebr. Program."},{"key":"10.1016\/j.jlamp.2026.101130_bib0013","series-title":"Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2022)","first-page":"56","article-title":"Bounded model checking of PLC ST programs using rewriting modulo SMT","author":"Lee","year":"2022"},{"key":"10.1016\/j.jlamp.2026.101130_bib0014","series-title":"Handbook of Model Checking","first-page":"173","article-title":"Partial-order reduction","author":"Peled","year":"2018"},{"key":"10.1016\/j.jlamp.2026.101130_bib0015","series-title":"Formal Methods","first-page":"425","article-title":"Formal semantics and analysis of multitask PLC ST programs with preemption","author":"Lee","year":"2025"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101130_bib0016","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101130_bib0017","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","article-title":"Rewriting modulo SMT and open system analysis","volume":"86","author":"Rocha","year":"2017","journal-title":"J. Log. Algebr. Method. Program."},{"key":"10.1016\/j.jlamp.2026.101130_bib0018","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/j.scico.2019.03.006","article-title":"Symbolic state space reduction with guarded terms for rewriting modulo SMT","volume":"178","author":"Bae","year":"2019","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jlamp.2026.101130_bib0019","article-title":"All About Maude \u2013 A High-Performance Logical Framework","author":"Clavel","year":"2007"},{"key":"10.1016\/j.jlamp.2026.101130_bib0020","series-title":"Technical Report","article-title":"Maude Manual (Version 3.5)","author":"Clavel","year":"2024"},{"key":"10.1016\/j.jlamp.2026.101130_bib0021","series-title":"International Conference on Computer Aided Verification","first-page":"737","article-title":"Yices 2.2","author":"Dutertre","year":"2014"},{"key":"10.1016\/j.jlamp.2026.101130_bib0022","series-title":"International Conference on Computer Aided Verification","first-page":"171","article-title":"CVC4","author":"Barrett","year":"2011"},{"key":"10.1016\/j.jlamp.2026.101130_bib0023","series-title":"International Workshop on Rewriting Logic and its Applications","first-page":"179","article-title":"A flexible framework for integrating maude and SMT solvers using Python","author":"Yu","year":"2024"},{"key":"10.1016\/j.jlamp.2026.101130_bib0024","series-title":"Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"533","article-title":"An executable formal semantics of C with applications","volume":"47","author":"Ellison","year":"2012"},{"key":"10.1016\/j.jlamp.2026.101130_bib0025","series-title":"Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"445","article-title":"K-Java: A complete semantics of Java","author":"Bogdanas","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101130_bib0026","series-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation","first-page":"346","article-title":"KJS: A complete formal semantics of JavaScript","author":"Park","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101130_bib0027","series-title":"Proceedings of the International Symposium on Formal Methods","first-page":"267","article-title":"Executing formal semantics with the K tool","author":"Lazar","year":"2012"},{"key":"10.1016\/j.jlamp.2026.101130_bib0028","series-title":"International Workshop on Rewriting Logic and its Applications","first-page":"104","article-title":"K-Maude: A rewriting based tool for semantics of programming languages","author":"\u015eerb\u0103nu\u0163\u0103","year":"2010"},{"key":"10.1016\/j.jlamp.2026.101130_bib0029","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2014.05.002","article-title":"K overview and simple case study","volume":"304","author":"Ro\u015fu","year":"2014","journal-title":"Electron. Note. Theor. Comput. Sci."},{"key":"10.1016\/j.jlamp.2026.101130_bib0030","series-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"10.1016\/j.jlamp.2026.101130_bib0031","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/j.scico.2014.02.006","article-title":"Model checking linear temporal logic of rewriting formulas under localized fairness","volume":"99","author":"Bae","year":"2015","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jlamp.2026.101130_bib0032","unstructured":"T. Chikamasa, NXTway-GS C API for a two wheeled self-balancing robot, 2013, (https:\/\/lejos-osek.sourceforge.net\/nxtway_gs.htm). Accessed: 2024-04-19."},{"key":"10.1016\/j.jlamp.2026.101130_bib0033","series-title":"IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence","first-page":"854","article-title":"Linear temporal logic and linear dynamic logic on finite traces","author":"De Giacomo","year":"2013"},{"key":"10.1016\/j.jlamp.2026.101130_bib0034","series-title":"Proceedings of the Joint Conference on Artificial Intelligence","first-page":"2591","article-title":"LTLf Synthesis as AND-OR graph search: knowledge compilation at work","author":"De Giacomo","year":"2022"},{"key":"10.1016\/j.jlamp.2026.101130_bib0035","doi-asserted-by":"crossref","DOI":"10.4204\/EPTCS.36.8","article-title":"Specification and verification of distributed embedded systems: a traffic intersection product family","volume":"36","author":"\u00d6lveczky","year":"2010","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"10.1016\/j.jlamp.2026.101130_bib0036","series-title":"Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering","first-page":"338","article-title":"Arcade.PLC: a verification platform for programmable logic controllers","author":"Biallas","year":"2012"},{"key":"10.1016\/j.jlamp.2026.101130_bib0037","series-title":"Formal Techniques for Distributed Objects, Components, and Systems","first-page":"284","article-title":"Formal verification of complex properties on PLC programs","author":"Darvas","year":"2014"},{"key":"10.1016\/j.jlamp.2026.101130_bib0038","series-title":"International Conference on Software Testing, Verification and Validation","first-page":"439","article-title":"Model checking PLC software written in function block diagram","author":"Pavlovic","year":"2010"},{"issue":"2","key":"10.1016\/j.jlamp.2026.101130_bib0039","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1016\/j.arcontrol.2012.09.015","article-title":"Transformation of function block diagrams to UPPAAL timed automata for the verification of safety applications","volume":"36","author":"Soliman","year":"2012","journal-title":"Annu. Rev. Control"},{"issue":"15","key":"10.1016\/j.jlamp.2026.101130_bib0040","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/S1474-6670(17)40537-4","article-title":"Validation of a SFC software specification by using hybrid automata","volume":"31","author":"Hassapis","year":"1998","journal-title":"IFAC Proceed. Vol."},{"issue":"4","key":"10.1016\/j.jlamp.2026.101130_bib0041","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S1474-6670(17)36116-5","article-title":"Modelling and verification of PLC-based systems programmed with ladder diagrams","volume":"37","author":"Lobov","year":"2004","journal-title":"IFAC Proceed. Vol."},{"key":"10.1016\/j.jlamp.2026.101130_bib0042","series-title":"International Conference on Systems, Man and Cybernetics","first-page":"2449","article-title":"Towards the automatic verification of PLC programs written in instruction list","volume":"4","author":"Canet","year":"2000"},{"key":"10.1016\/j.jlamp.2026.101130_bib0043","series-title":"Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference, COMPSAC 2009, Seattle, Washington, USA, July 20\u201324, 2009. Volume 1","first-page":"553","article-title":"Translation-Based model checking for PLC programs","author":"Zhou","year":"2009"},{"key":"10.1016\/j.jlamp.2026.101130_bib0044","series-title":"Proceedings of the Joint Meeting on Foundations of Software Engineering","first-page":"326","article-title":"Symbolic execution of programmable logic controller code","author":"Guo","year":"2017"},{"issue":"4","key":"10.1016\/j.jlamp.2026.101130_bib0045","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1109\/TASE.2010.2050199","article-title":"Verification of a timed multitask system with uppaal","volume":"7","author":"Mokadem","year":"2010","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"10.1016\/j.jlamp.2026.101130_bib0046","series-title":"Proceedings of 11th Euromicro Conference on Real-Time Systems","first-page":"106","article-title":"Timed automaton models for simple programmable logic controllers","author":"Mader","year":"1999"},{"key":"10.1016\/j.jlamp.2026.101130_bib0047","series-title":"Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 11\u201314 September 2006, Riverside, California, USA","first-page":"125","article-title":"UPPAAL 4.0","author":"Behrmann","year":"2006"},{"issue":"4","key":"10.1016\/j.jlamp.2026.101130_bib0048","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1049\/iet-sen:20070009","article-title":"Modelling and verification of program logic controllers using timed automata","volume":"1","author":"Wang","year":"2007","journal-title":"IET Softw."},{"issue":"9","key":"10.1016\/j.jlamp.2026.101130_bib0049","doi-asserted-by":"crossref","first-page":"929","DOI":"10.1016\/j.conengprac.2011.01.001","article-title":"Verification and validation of safety applications based on PLCopen safety function blocks","volume":"19","author":"Soliman","year":"2011","journal-title":"Control Eng. Pract."},{"key":"10.1016\/j.jlamp.2026.101130_bib0050","series-title":"Winter Simulation Conference","first-page":"222","article-title":"PLCStudio: Simulation based PLC code verification","author":"Park","year":"2008"},{"key":"10.1016\/j.jlamp.2026.101130_bib0051","series-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation","first-page":"336","article-title":"Defining the undefinedness of C","author":"Hathhorn","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101130_bib0052","series-title":"IEEE Computer Security Foundations Symposium (CSF)","first-page":"204","article-title":"KEVM: a complete formal semantics of the ethereum virtual machine","author":"Hildenbrandt","year":"2018"},{"key":"10.1016\/j.jlamp.2026.101130_bib0053","series-title":"IEEE Computer Security Foundations Symposium (CSF)","first-page":"382","article-title":"Resource-bounded intruders in denial of service attacks","author":"Aires Urquiza","year":"2019"},{"key":"10.1016\/j.jlamp.2026.101130_bib0054","series-title":"International Workshop on Rewriting Logic and its Applications","first-page":"212","article-title":"Automating safety proofs about cyber-physical systems using rewriting modulo SMT","volume":"13252","author":"Nigam","year":"2022"},{"key":"10.1016\/j.jlamp.2026.101130_bib0055","series-title":"International Conference on Computer Aided Verification","first-page":"491","article-title":"HybridSynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL","author":"Lee","year":"2021"},{"key":"10.1016\/j.jlamp.2026.101130_bib0056","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1007\/s10009-022-00665-z","article-title":"Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL","author":"Lee","year":"2022","journal-title":"Int. J. Softw. Tool. Technol. Trans."},{"key":"10.1016\/j.jlamp.2026.101130_bib0057","series-title":"Advances in Computing","first-page":"611","article-title":"Reliable control architecture with PLEXIL and ROS for autonomous wheeled robots","author":"Cadavid","year":"2017"},{"key":"10.1016\/j.jlamp.2026.101130_bib0058","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2023.103074","article-title":"Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using maude and SMT solving","volume":"233","author":"Arias","year":"2024","journal-title":"Sci. Comput. Program."},{"issue":"3\u20134","key":"10.1016\/j.jlamp.2026.101130_bib0059","doi-asserted-by":"crossref","first-page":"261","DOI":"10.3233\/FI-242195","article-title":"A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time petri nets","volume":"192","author":"Arias","year":"2024","journal-title":"Fundam. Inform."},{"key":"10.1016\/j.jlamp.2026.101130_bib0060","series-title":"International Workshop on Rewriting Logic and its Applications","first-page":"76","article-title":"Symbolic specification and verification of data-aware BPMN processes using rewriting modulo SMT","author":"Dur\u00e1n","year":"2018"},{"issue":"4","key":"10.1016\/j.jlamp.2026.101130_bib0061","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/j.entcs.2007.06.005","article-title":"Abstraction and completeness for real-time Maude","volume":"176","author":"\u00d6lveczky","year":"2007","journal-title":"Electron. Note. Theor. Comput. Sci."},{"key":"10.1016\/j.jlamp.2026.101130_bib0062","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","article-title":"Semantics and pragmatics of real-time Maude","volume":"20","author":"\u00d6lveczky","year":"2007","journal-title":"High.-Order Symbol. Comput."},{"key":"10.1016\/j.jlamp.2026.101130_bib0063","series-title":"Static Analysis","first-page":"328","article-title":"Formal analysis of networked PLC controllers interacting with physical environments","author":"Lee","year":"2025"},{"key":"10.1016\/j.jlamp.2026.101130_bib0064","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2025.103332","article-title":"SMT-based robust model checking for signal temporal logic","volume":"246","author":"Lee","year":"2025","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jlamp.2026.101130_bib0065","series-title":"CAV","first-page":"524","article-title":"STLmc: Robust STL model checking of hybrid systems using SMT","author":"Yu","year":"2022"},{"issue":"POPL","key":"10.1016\/j.jlamp.2026.101130_bib0066","doi-asserted-by":"crossref","first-page":"51:1","DOI":"10.1145\/3290364","article-title":"Bounded model checking of signal temporal logic properties using syntactic separation","volume":"3","author":"Bae","year":"2019","journal-title":"Proc. ACM Program. Lang."},{"key":"10.1016\/j.jlamp.2026.101130_bib0067","series-title":"ASE","first-page":"343","article-title":"Efficient SMT-based model checking for signal temporal logic","author":"Lee","year":"2021"},{"key":"10.1016\/j.jlamp.2026.101130_bib0068","series-title":"Proceedings of the 18th International Conference on Term Rewriting and Applications (RTA 2007)","first-page":"153","article-title":"Symbolic model checking of infinite-state systems using narrowing","author":"Escobar","year":"2007"},{"key":"10.1016\/j.jlamp.2026.101130_bib0069","series-title":"24th International Conference on Rewriting Techniques and Applications (RTA 2013)","first-page":"81","article-title":"Abstract logical model checking of infinite-state systems using narrowing","author":"Bae","year":"2013"},{"key":"10.1016\/j.jlamp.2026.101130_bib0070","series-title":"Joint International Conference on Rewriting and Typed Lambda Calculi (RTA-TLCA)","first-page":"61","article-title":"Predicate abstraction of rewrite theories","author":"Bae","year":"2014"},{"key":"10.1016\/j.jlamp.2026.101130_bib0071","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2024.103097","article-title":"Narrowing and heuristic search for symbolic reachability analysis of concurrent object-oriented systems","volume":"235","author":"Kang","year":"2024","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jlamp.2026.101130_bib0072","series-title":"International Workshop on Rewriting Logic and its Applications (WRLA)","first-page":"3","article-title":"Verifying invariants by deductive model checking","author":"Bae","year":"2024"},{"key":"10.1016\/j.jlamp.2026.101130_bib0073","article-title":"DM-check: verifying invariants of concurrent systems by deductive model checking","author":"Bae","year":"2025","journal-title":"J. Log. Algebr. Method. Program."},{"key":"10.1016\/j.jlamp.2026.101130_bib0074","series-title":"International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)","article-title":"A formal executable semantics of PROMELA","author":"Son","year":"2026"}],"container-title":["Journal of Logical and Algebraic Methods in Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000222?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000222?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T06:06:37Z","timestamp":1783145197000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220826000222"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":74,"alternative-id":["S2352220826000222"],"URL":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101130","relation":{},"ISSN":["2352-2208"],"issn-type":[{"value":"2352-2208","type":"print"}],"subject":[],"published":{"date-parts":[[2026,6]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Bounded model checking of multitask PLC ST programs with preemption using rewriting modulo SMT","name":"articletitle","label":"Article Title"},{"value":"Journal of Logical and Algebraic Methods in Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101130","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Elsevier Inc. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"101130"}}