12 papers
LAAF: A Layered Accountability Architecture Framework for LLM Applications
Prachi Chaturvedi, Shahnawaz Ahmad, Ehsan Nowroozi +5
Large Language Models (LLMs) operate in hospitals, courtrooms, banks, and public service desks, where fluent, confident outputs are treated as authoritative even when ungrounded or…
Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement
Pierre Dantas, Lucas Cordeiro, Ehsan Nowroozi +2
Large Language Model (LLM) agents take irreversible real-world actions, yet no system gives formally grounded, task-level safety guarantees for their plans. In a PRISMA 2020 system…
K-ESBMC: An Executable Formal Semantics of IEC 61131-3 Ladder Diagram for Validating Verifier Translations
Pierre Dantas, Lucas Cordeiro, Waldir Junior
Automated verifiers for IEC 61131-3 ladder diagrams enhance safety by translating diagrams into model-checker inputs. Still, their unverified front-end translations risk silently r…
ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs
Pierre Dantas, Lucas Cordeiro, Waldir Junior
OpenPLC, Arduino OPTA, CONTROLLINO, and Industrial Shields M-Duino bring IEC 61131-3 to low-cost microcontrollers used in real automation and industrial control system (ICS) securi…
Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis
Pierre Dantas, Lucas Cordeiro, Waldir Junior
A Ladder Logic Bomb (LLB) is malicious control logic in a Programmable Logic Controller (PLC) program that lies dormant until a trigger activates a payload to manipulate actuators,…
ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor
Pierre Dantas, Lucas Cordeiro, Waldir Junior
PLCverif is the most mature open-source platform for PLC formal verification, developed at CERN and in production use since 2019. Yet it has two fundamental limitations: no support…
ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
Pierre Dantas, Lucas Cordeiro, Waldir Junior
PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs: a textual encoding using <rung> elements, and a graphical encoding that represents rung logic as a…
Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang +2
Loop invariant synthesis remains a central and pivotal bottleneck in formal software verification. Recent LLM-based Neuro-Symbolic tools have achieved impressive solve rates. Howev…
ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking
Pierre Dantas, Lucas Cordeiro, Waldir Junior
PLCs execute safety-critical programs across industrial sectors. The dominant PLC notation, ladder diagram (LD) per IEC 61131-3, remains absent from formal verification: SMT-based…
ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
Pierre Dantas, Lucas Cordeiro, Waldir Junior
The Efficient SMT-Based Context-Bounded Model Checker (ESBMC) has grown from a research prototype for verifying embedded ANSI-C software into one of the most versatile and industri…
ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
Muhammad A. A. Pirzada, Weiqi Wang, Yiannis Charalambous +2
Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by…
UnitTenX: Generating Tests for Legacy Packages with AI Agents Powered by Formal Verification
Yiannis Charalambous, Claudionor N. Coelho, Luis Lamb +1
This paper introduces UnitTenX, a state-of-the-art open-source AI multi-agent system designed to generate unit tests for legacy code, enhancing test coverage and critical value tes…