Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 29 novembre 2017 (10h--11h), Amphi 4 de l'EPITA. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2017-11-29 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 29 novembre 2017 : * 10h--11h: Industrial Formal Verification – Cadence’s JasperGold Formal Verification Platform -- Barbara Jobstmann, Cadence Design Systems Formal verification (aka Symbolic Model Checking) is becoming a mainstream technology in system on a chip (SoC)/intellectual property design and verification methodologies. In the past, the usage of formal verification was limited to a small range of applications; it was mainly used to verify complex protocols or intrinsic logic functionality by formal verification experts. In recent years, we saw a rapid adoption of formal verification technology and many new application areas, such as checking of configuration and status register accesses, SoC connectivity verification, low power design verification, security applications, and many more. In this talk, we give an overview of the JasperGold Formal Verification Platform. The platform provides a wide range of formal apps, which ease adoption of formal verification by offering property generation and other targeted capabilities for specific design and verification tasks. In addition, JasperGold offers a unique interactive debug environment (called Visualize) that allows the user to easily analyze the verification results. We present JasperGold from a user’s point of view, showcase selected apps, and discuss features that were essential for their wide adoption. -- Barbara Jobstmann is a field application engineer for Cadence Design Systems and a lecturer at the École Polytechnique Fédérale de Lausanne (EPFL). She joined Cadence in 2014 through the acquisition of Jasper Design Automation, where she worked since 2012 as an application engineer. In the past, she was also a CNRS researcher (chargé de recherche) in Verimag, an academic research laboratory belonging to the CNRS and the Communauté Université Grenoble Alpes in France. Her research focused on constructing correct and reliable computer systems using formal verification and synthesis techniques. She received a Ph.D. degree in Computer Science from the University of Technology in Graz, Austria in 2007. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre