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
Prix de stage de recherche de l'École polytechnique
19 novembre 2019
Quentin Soubeyran a reçu le prix de stage de recherche de l'École polytechnique pour son travail au LRI dans l'équipe Systèmes Parallèles.

Prix FIEEC CARNOT de la recherche appliquée
18 octobre 2019
Claude Marché remporte le premier prix FIEEC CARNOT de la recherche appliquée pour sa collaboration avec la société AdaCore.

Ouvrage Informatique au lycée
24 septembre 2019
Parution d'un ouvrage pour la spécialité NSI en classe de première, co-écrit par quatre membres du LRI.