1

Rule-Guided Reinforcement Learning Policy Evaluation and Improvement
We consider the challenging problem of using domain knowledge to improve deep reinforcement learning policies. To this end, we propose …
Martin Tappler, Ignacio D. Lopez-Miguel, Sebastian Tschiatschek, Ezio Bartocci
DOI
Rule-Guided Reinforcement Learning Policy Evaluation and Improvement
Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study
The increased technological complexity and demand for software reliability require organizations to formally design and verify their …
Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, Christine Betz
DOI
Student Research Abstract: Enhancing Safety in Cyber-Physical Systems Through Runtime Enforcement
The verification and safety assurance of cyber-physical systems pose significant challenges, necessitating innovative solutions for …
Ignacio D. Lopez-Miguel
Student Research Abstract: Enhancing Safety in Cyber-Physical Systems Through Runtime Enforcement
Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code
Formal verification techniques are widely used in critical industries to minimize software flaws. However, despite the benefits and …
Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Enrique Blanco Viñuela, Matias Salinas, Christine Betz
DOI
Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code
Progression for Monitoring in Temporal ASP
In recent years, there has been growing interest in the application of temporal reasoning approaches and non-monotonic logics from …
Davide Soldà, Ignacio D. Lopez-Miguel, Ezio Bartocci, Thomas Eiter
DOI
Progression for Monitoring in Temporal ASP
From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif
PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in …
Zsófi Ádám, Ignacio D. Lopez-Miguel, Anastasia Mavridou, Thomas Pressburger, Marcin Bęś, Enrique Blanco Viñuela, Andreas Katis, Jean-Charles Tournier, Khanh V. Trinh, Borja Fernández Adiego
DOI
From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif
Verification of Neural Networks Meets PLC Code: An LHC Cooling Tower Control System at CERN
In the last few years, control engineers have started to use artificial neural networks (NNs) embedded in advanced feedback control …
Ignacio D. Lopez-Miguel
DOI
Verification of Neural Networks Meets PLC Code: An LHC Cooling Tower Control System at CERN
Stop at red? Engineering meets ethics
Over the past few years, artificial intelligence has fueled a revolution in several scientific fields. Intelligent agents can now give …
Ignacio D. Lopez-Miguel
DOI
Simplification of numeric variables for PLC model checking
Software model checking has recently started to be applied in the verification of programmable logic controller (PLC) programs. It …
Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Jean-Charles Tournier, Enrique Blanco Viñuela, Juan A. Rodriguez-Aguilar
DOI
Simplification of numeric variables for PLC model checking
Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program
An important aspect of many particle accelerators is the constant evolution and frequent configuration changes that are needed to …
Borja Fernández Adiego, Ignacio D. Lopez-Miguel, Jean-Charles Tournier, Enrique Blanco Viñuela, Tomasz Ladzinski, Frederic Havart
DOI
Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program