8 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 +1
LLM agents increasingly perform irreversible real-world actions, including database updates, API calls, file operations, and autonomous use of tools. However, no existing system pr…
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…