(2013):
IEC 61131-3:2013, Programmable controllers - Part 3: Programming languages.
V. Balat (2006):
Ocsigen: Typing Web Interaction with Objective Caml.
In: ACM SIGPLAN workshop on ML,
Portland, United States,
doi:10.1145/1159876.1159889.
C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi\'c, T. King, A. Reynolds & C. Tinelli (2011):
CVC4.
In: Computer Aided Verification,
CAV'11.
Springer-Verlag,
doi:10.1007/3-540-45657-0_40.
F. Bobot, J-C. Filliâtre, C. Marché & A. Paskevich (2015):
Let's Verify This with Why3.
Software Tools for Technology Transfer (STTT) 17(6),
pp. 709–727,
doi:10.1007/s10009-014-0314-5.
E. W. Dijkstra (1997):
A Discipline of Programming.
Prentice Hall PTR,
Upper Saddle River, NJ, USA.
B. Fernández Adiego, D. Darvas, E. B. Viñuela, J. Tournier, S. Bliudze, J. O. Blech & V. M. González Suárez (2015):
Applying Model Checking to Industrial-Sized PLC Programs.
IEEE Transactions on Industrial Informatics 11(6),
pp. 1400–1410,
doi:10.1109/TII.2015.2489184.
G. Frey & L. Litz (2000):
Formal methods in PLC programming.
In: IEE International conference on systems, man and cybernetics 4,
pp. 2431–2436 vol.4,
doi:10.1109/ICSMC.2000.884356.
D. Hauzar, C. Marché & Y. Moy (2016):
Counterexamples from Proof Failures in SPARK.
In: Software Engineering and Formal Methods.
Springer,
doi:10.1007/978-3-662-49674-9_25.
S. Kottler, M. Khayamy, S. R. Hasan & O. Elkeelany (2017):
Formal verification of ladder logic programs using NuSMV.
In: SoutheastCon 2017,
pp. 1–5,
doi:10.1109/SECON.2017.7925390.
T. Ovatman, A. Aral, D. Polat & A. Osman Ünver (2014):
An overview of model checking practices on verification of PLC software.
Software and Systems Modeling,
pp. 1–24,
doi:10.1007/s10270-014-0448-7.
B. K. Rosen, M. N. Wegman & F. K. Zadeck (1988):
Global Value Numbers and Redundant Computations.
In: Symposium on Principles of Programming Languages,
POPL '88.
ACM,
pp. 12–27,
doi:10.1145/73560.73562.
J-M. Roussel & B. Denis (2002):
Safety properties verification of ladder diagram programs.
Journal Européen des Systèmes Automatisés (JESA) 36(7),
pp. pp. 905–917.
Z. Su (1997):
Automatic Analysis of Relay Ladder Logic Programs.
Technical Report UCB/CSD-97-969.
EECS Department, University of California, Berkeley.
eptcs@eptcs.org