< retour aux séminaires

Prof. Jean-Luc LAMBERT, Valiosys SA, Caen, France

Theme: LPV: a new technique, based on linear programming, to formally prove or disprove safety properties on software and hardware systems
Date: 19 October 2000


Jean-Luc Lambert is the Chief Technologist Officer of the company Valiosys at Caen. He passed his PhD degree in computer science in 1987 at the university of Orsay . He was associate professor at the university of Paris-Nord at Villetaneuse and in 1991 he became Professor at the university of Caen. He founded Valiosys in september 1999. His main areas of interest are Petri net theory, algorithmics and linear programming


A lot of logical theories were used in order to prove that a software or a hardware system satisfies predefined safety properties. Strangely the linear programming theory was left beside and never considered as a theory to make formal proof. Even so it appears that linear programming, by the way of the duality theorem, is a logical theory with nice completeness properties. Moreover proving with linear programming uses well-known efficient polynomial time algorithms. In this talk we will show how the behavior of a software/hardware system can be modeled with linear programming and we will show that the duality theorem gives an inference engine that is both powerful and algorithmically efficient.