A Programmable Logic Controller Program analysis method comprising the following steps: - translating (TRANS 1) an original program (PROG) of the type of a Programmable Logic Controller Program, into a program model (PMOD) in a logical framework; - translating (TRANS2), based at least on said program model (PMOD), user specifications into a specification model (SMOD) in a logical framework; - determining, from at least said program model (PMOD) and predefined language formalization, a set of properties (Prop) on internal variables of said original program; - verifying, by an automated solver, satisfiability of said set of properties (Prop) coupled with interlocking properties (IntProp) obtained from the specification model (SMOD) and providing, if contraposition of a property (Prop) from said set of properties (Prop) is satisfiable, a set of counter-examples (PROOF NOK) representative of program model's inputs and internal memory values for which said property (Prop) contraposition is satisfiable, or providing, if said set of properties (Prop) is always satisfied, confirmation (PROOF OK) thereof; - translating counter-examples (PROOF NOK), into error initial configurations (IniConf) of said program model, said initial configurations (IniConf) comprising initial values of inputs and internal memory; - simulating the execution of the program model with error initial configurations (IniConf) of said program model, and recording error intermediary configurations (AST-IntConf) of said program model simulation, from the beginning of execution up to said property violation, said intermediary configurations comprising intermediary values of internal memory; - translating error initial configurations (IniConf) of said program model and error intermediary configurations (AST-IntConf) of said program model simulation, into error initial and intermediary configurations (Lad-IniConf, Lad-IntConf) of said original program (PROG); and displaying said program error initial and intermediary configurations (Lad-IniConf, Lad-IntConf). - translating (TRANS 1) an original program (PROG) of the type of a Programmable Logic Controller Program, into a program model (PMOD) in a logical framework; - translating (TRANS2), based at least on said program model (PMOD), user specifications into a specification model (SMOD) in a logical framework; - determining, from at least said program model (PMOD) and predefined language formalization, a set of properties (Prop) on internal variables of said original program; - verifying, by an automated solver, satisfiability of said set of properties (Prop) coupled with interlocking properties (IntProp) obtained from the specification model (SMOD) and providing, if contraposition of a property (Prop) from said set of properties (Prop) is satisfiable, a set of counter-examples (PROOF NOK) representative of program model's inputs and internal memory values for which said property (Prop) contraposition is satisfiable, or providing, if said set of properties (Prop) is always satisfied, confirmation (PROOF OK) thereof; - translating counter-examples (PROOF NOK), into error initial configurations (IniConf) of said program model, said initial configurations (IniConf) comprising initial values of inputs and internal memory; - simulating the execution of the program model with error initial configurations (IniConf) of said program model, and recording error intermediary configurations (AST-IntConf) of said program model simulation, from the beginning of execution up to said property violation, said intermediary configurations comprising intermediary values of internal memory; - translating error initial configurations (IniConf) of said program model and error intermediary configurations (AST-IntConf) of said program model simulation, into error initial and intermediary configurations (Lad-IniConf, Lad-IntConf) of said original program (PROG); and displaying said program error initial and intermediary configurations (Lad-IniConf, Lad-IntConf).