Automatically Deriving Symbolic Invariants for PLC Programs Written in IL - Forms/Format 2010 - page 245

11. S. K. Lahiri and S. Qadeer. Back to the future: revisiting precise program
verification using SMT solvers. In POPL , pages 171-182. ACM, 2008.
12. T. Mertke and G. Frey. Formal verification of PLC-programs generated from
signal interpreted petri nets. In 2001 IEEE International Conference on Sys-
tems, Man, and Cybernetics , volume 4, pages 2700-2705. IEEE Computer So-
ciety Press, 2001.
13. T. Mertke and T. Menzel. Methods and tools to the verification safety-related
control software. In SMC , pages 2455-2457, 2000.
14. G. Nelson. Verifying reachability invariants of linked structures. In POPL ,
pages 83-47. ACM, 1983.
15. O. Pavlovic, R. Pinger, and M. Kollmann. Automated formal verification of
PLC programms written in IL. In VERIFY , number 259 in Workshop Proce.,
pages 152-163. CEUR-WS.org, 2007.
16. PLCopen TC5. Safety Software Technical Specification, Version 1.0, Part 1:
Concepts and Function Blocks . PLCopen, Germany, 2006.
17. B. Schlich, J. Brauer, J. Wernerus, and S. Kowalewski. Direct model checking
of PLC programs in IL. In DCDS , 2009. To appear.
18. D. Soliman and G. Frey. Verification and validation of safety applications based
on PLCopen Safety Function Blocks using Timed Automata in UPPAAL. In
DCDS , 2009. To appear.
19. A. Sülflow and R. Drechsler. Verification of plc programs using formal proof
techniques. In FORMS/FORMAT , pages 43-50. L'Harmattan, 2008.