To: seminaire@pauillac.inria.fr From: Nelly.Maloisel@inria.fr Subject: SEM - INRIA : LogiCal - 02/03/2001 - Paris - FR Vous pouvez maintenant vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/subscribe.html S E M I N A I R E . ___ / _ _ / _ / / / \ / \ / / __| / |___ |_/ |_/ / |__ |_/ |_ ___ . / / ___ __ /_ _ / _/ /| /| _ __ __ _ _ / / / /_ / __| / / |/ | / \ /_ / / \ | / __| |___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/ I N R I A - Rocquencourt Salle de conference du Bat 11 Vendredi 2 mars, 10h30 ------------ Dilian Gurov ------------ SICS, Suede =============================== Verification of Erlang programs =============================== The Erlang programming language has been developed and widely used at Ericsson for programming telecommunication applications. This kind of software is often of a highly concurrent and dynamic nature, and it is for this reason particularly hard to debug and test. We explore the alternative of verifying Erlang programs, that is, of formally proving that they behave correctly. For most real-world programming languages this is not feasible due to their complex nature, but the core fragment of the Erlang language is economic and clean, allowing a compact and elegant formalization. Nevertheless, verification of Erlang programs has to deal with challenging issues like dynamic process creation and asynchronous message passing, requiring a rich verification framework and adequate support by a software tool. In the course of the ErlVer project, which runs in collaboration with Ericsson's Computer Science Lab and is partly funded by the Advanced Software Technology competence centre, ASTEC, we developed such a framework, designed and implemented the Erlang Verification Tool which is publicly available, and evaluated these on a number of case studies of various size and complexity. This talk presents an overview of the main theoretical and practical achievements of the ErlVer project. I will motivate and present a verification framework for parametric, compositional and inductive reasoning, consisting of a compositional small-step semantics for Erlang, a recursive property specification language, and a proof system, focusing on the methodological, language-independent aspects of our approach. Then I will describe the Erlang Verification Tool, its implementation, support for semi-automatic proof search, graphical user interface, and the main case studies it has been applied to so far. The talk concludes with a summary of our future ambitions in the project.