A Ladder program analysis method comprising the following steps: - translating (TRANS) an original program (PROG) of the type of a Ladder program, into a model in a logical framework; - determining, from at least said model 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 user specifications (IntProp) 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 model 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 said counter-examples (PROOF NOK), into error initial configurations (IniConf) of said model, said error initial configurations (IniConf) comprising initial values of inputs and internal memory; - simulating the execution of the model with the error initial configurations (IniConf) of said model, and recording error intermediary configurations (AST-IntConf) of said simulation of the execution of the model from the beginning of execution up to said contraposition of a property (Prop), said error intermediary configurations (AST-IntConf) comprising intermediary values of internal memory; - translating said error initial configurations (IniConf) of said model and said error intermediary configurations (AST-IntConf) of said simulation of the execution of the model into program 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) an original program (PROG) of the type of a Ladder program, into a model in a logical framework; - determining, from at least said model 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 user specifications (IntProp) 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 model 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 said counter-examples (PROOF NOK), into error initial configurations (IniConf) of said model, said error initial configurations (IniConf) comprising initial values of inputs and internal memory; - simulating the execution of the model with the error initial configurations (IniConf) of said model, and recording error intermediary configurations (AST-IntConf) of said simulation of the execution of the model from the beginning of execution up to said contraposition of a property (Prop), said error intermediary configurations (AST-IntConf) comprising intermediary values of internal memory; - translating said error initial configurations (IniConf) of said model and said error intermediary configurations (AST-IntConf) of said simulation of the execution of the model into program 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).