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