SMT Solving, A Very Short Introduction

Philipp Rümmer

Associate Professor at the IT Department of Uppsala University, Sweden  

Abstract

Satisfiability Modulo Theories, or SMT, describes a class of constraint solvers that are developed primarily for the purpose of program verification. SMT solvers combine efficient solvers for Boolean constraints, known as SAT solvers, with procedures for a wide range of theories and data types, including different forms of arithmetic, uninterpreted symbols, arrays, algebraic data-types and co-data-types, and strings. SMT solvers are widely applied in different verification applications, for instance deductive verification systems, model checkers, bounded model checkers, and white-box fuzzers. The presentation will give a high-level introduction of the algorithms, architecture, and use of SMT solvers, and outline in particular the application of SMT for security analysis.

Biography

Philipp Rümmer is an Associate Professor at the IT Department of Uppsala University, Sweden. He received his PhD from Gothenburg University in 2008, and is generally interested in any kind of technology that is useful for program verification. Over the years, he has contributed to deductive verification methods (including the tools Key and Boogie), developed software model checkers (including Eldarica and JayHorn), worked on theorem provers and SMT solvers (leading to a zoo of solvers, among others inhabited by Princess, Norn, Sloth, Ostrich, Trau, UppSAT), and investigated the application of verification methods in domains like Embedded Systems and Security.

   برگزار کننده: دانشگاه خاتم                               زمان: سه‌شنبه ۴ آذرماه 1399                                          ساعت: ۱۵:۳۰

از کلیه دانشجویان و علاقه‌مندان گرامی دعوت می‌شود در زمان مقرر در این سخنرانی شرکت نمایند. (سخنرانی به زبان انگلیسی می‌باشد.)

لطفا جهت شرکت در سخنرانی (رایگان)، فرم ثبت‌نام (الزامی) را از طریق آدرس و یا QR Code درج شده در زیر تکمیل فرمایید.

سخنرانی به صورت آنلاین می‌باشد. پس از ثبت‌نام، اطلاعات و نحوه شرکت در رویداد از طریق ایمیل اطلاع‌رسانی می‌گردد.