For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Constantin Enea who has recently joined the Cosynus team. The seminar will be interactive: Constantin will present his work in order to hopefully start discussions with people working on related topics in the lab!

Abstract: I will talk about recent results concerning the problem of increasing the level of automation in formal verification of concurrent or distributed programs. These results span various approaches from testing, finite state model-checking, to SMT-based proofs. Also, they apply to various classes of programs from concurrent data types, to distributed databases, or applications thereof.