Français Anglais
Accueil Annuaire Plan du site
Accueil > News du laboratoire > Séminaire Digiteo, 31 Mars 2014, 14:30, Supélec, F.3.05
Séminaire Digiteo, 31 Mars 2014, 14:30, Supélec, F.3.05
Séminaire Digiteo, 31 Mars 2014, 14:30, Supélec, F.3.05 Séminaire Digiteo, 31 Mars 2014, 14:30, Supélec, F.3.05
31 mars 2014

Title: The Satisfiability Modulo Theories solver Z3
Speaker: Nikolaj Bjorner, Principal Researcher at Microsoft Research, Redmond,
The Satisfiability Modulo Theories (SMT) solver Z3 from Microsoft Research powers a generation of tools, including SAGE, P
Title: The Satisfiability Modulo Theories solver Z3 Speaker: Nikolaj Bjorner (http://research.microsoft.com/en-us/people/nbjorner/)   Abstract: Automated reasoning has become an integral part of software engineering tools in recent years thanks to high-performance theorem provers. The Satisfiability Modulo Theories (SMT) solver Z3 from Microsoft Research powers a generation of tools, including SAGE, Pex, Spec#, Dafny, VCC, Havoc, Boogie, Slam, Yogi, Spec Explorer, SecGuru, and Terminator. These tools reduce program analysis, verification and testing problems to logic queries that are solved using Z3. The talk takes these applications of Z3 as a starting point and examines applications SAGE, Dafny and SecGuru in some more depth. SAGE uses dynamic symbolic execution. It has been used to eradicate hundreds of security vulnerabilities in media readers that are otherwise well-known to be prone to security critical bugs. Dafny is a program verification environment and presents the current state-of-the-art in program verification methodologies and tools. SecGuru is a tool for automatically validating network connectivity restriction policies in large scale data-centers such as Windows Azure. We then describe some of the current trends in Z3: including solving recursive Horn clauses, solving real and floating point arithmetic.   
Bio: Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 is developed by Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger. Previously, he designed the DFSR, Distributed File System - Replication, shipped with Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his Master’s and Ph.D. degrees in computer science from Stanford University, and spent the first three years of university at DTU and DIKU.
News
George Manoussakis, lauréat 2018, prix de thèse (accessit) Charles Delorme
18 septembre 2018
George Manoussakis, est lauréat de prix de thèse (accessit) Ch. Delorme 2018. Il a soutenu sa thèse au LRI/Galac en Novembre 2017 sous la direction de J. Cohen et A. Deza. Depuis Septembre 2018 il est MdeC à l'Université de Versailles/Li-PaRAD.

TrackML dans Nature
21 janvier 2018
L'apprentissage automatique peut-il aider la physique des hautes énergies à découvrir et à caractériser de nouvelles particules ? TAO participe à l'organisation du challenge TrackML avec le CERN. La seconde phase de la compétition utilisera Codalab.

Un article de Isabelle Guyon sur la démocratisation de l'IA
19 mars 2018
Lien vers l'article paru dans le journal le monde :
http://www.lemonde.fr/acces-restreint/sciences/article/2018/04/08/a4544bd07cad09fe52980c0f82c08b34_5282548_1650684.html