The Z3 SMT solver and functional programming

location_city Online schedule Mar 26th 05:00 - 05:45 PM IST place Zoom people 41 Interested

Satisfiability modulo theories (SMT) solvers are extremely powerful tools that are indispensable in a number of applications of functional programming from mathematical analysis and optimization to computer security to program verification. SMT solvers allow you to determine if certain logical and mathematical formulas are satisfiable or (just as importantly) unsatisfiable in the context of theories like real arithmetic or set theory, and can provide definitive answers to commonly encountered programming problems involving logic, arithmetic, equations, and constraints.

Z3 is one of the most popular SMT solvers available today with APIs available for many different programming languages. Although Z3 is most commonly used from Python, functional languages like F# provide powerful metaprogramming facilities that make it very easy to translate F# code and expressions to Z3 expressions without the need for custom types or operators.

This presentation describes how the Z3 solver can be used from F# via quotations to quickly and easily solve common programming problems from Boolean formula satisfiability to arithmetic expression equality to linear programming to verifying fragments of source code.

 
 

Outline/Structure of the Demonstration

  • Background on SAT/SMT solvers (2.5min)
  • Background on first-order logic and theories (2.5min)
  • Background on F# quotations (5min)
  • Translating F# quotations to Z3 logical expressions(5min)
  • Propositional and first-order logic formula satisfiability(5min)
  • Solving logical puzzles(5min)
  • Solving integer and real arithmetic constraints(5min)
  • Integer linear programming(5min)
  • Solving abstract algebra problems: set theory, group theory...(5min)
  • Simple program verification using weakest precondition calculus (5min)

Learning Outcome

Participants will learn about the different kinds of logical and mathematical problems that can be solved quickly and easily using SMT solvers, using concise idiomatic functional language code. 

Target Audience

Functional programmers interested in incorporating an SMT solver into their projects for solving problems involving logic, games, verification, planning or scheduling.

Prerequisites for Attendees

Knowledge of a ML-family language will be helpful but not necessary. Only basic math and logic concepts are used and will all be explained.

Video


schedule Submitted 9 months ago

  • Bryan Hunter
    keyboard_arrow_down

    Bryan Hunter - Distributed Elixir (lessons from HCA Healthcare’s project Waterpark)

    Bryan Hunter
    Bryan Hunter
    Enterprise Fellow
    HCA Healthcare
    schedule 5 months ago
    Sold Out!
    45 Mins
    Keynote
    Intermediate

    At HCA Healthcare, we built Waterpark– a continuously available, geographically distributed, high velocity Enterprise Integration Platform. We built it from scratch in Elixir. Elixir and the ErlangVM are very powerful tools. Need to model millions of things? No problem. Need processes to self-heal when things break? No problem. Need to model millions of things that self heal on computers scattered across a continent? Hmmm… for that you’ve got some work to do, but in Elixir that work is very doable and fun. In this nuts-and-bolts session, we will discuss the distributed computing bits that are in-the-box with Elixir and what is missing. We will cover the missing bits that we built and “why”. Topics include: hashing functions, distributed process registries, the mailroom pattern, server topology, leader election, consensus, actor replication and recovery, and hot code loading. 

  • 20 Mins
    Talk
    Beginner

    Some people even say names don't matter. While it is widely held that good naming is one of the most important aspects of programming, is there such a thing as an objectively good name?

    As part of a discussion of the philosophy of programming, we'll look at what are the real aims of naming things well, and what considerations we should have in mind when discussing them. We'll have a look at alternatives and what they bring that names do not.

  • Dave Yarwood
    keyboard_arrow_down

    Dave Yarwood - Clojure through the lens of music

    Dave Yarwood
    Dave Yarwood
    Senior Software Engineer
    Kevel
    schedule 4 months ago
    Sold Out!
    45 Mins
    Talk
    Intermediate

    You may be familiar with what map, filter, and reduce do. But have you ever heard how these functions sound?

    The Alda language is centered around the idea that music can be represented as data. alda-clj is a Clojure library that maps Clojure data structures to the music theory concepts in the Alda language, including notes and chords. The library serves as an interface that takes Clojure code as input and produces music as output.

    In addition to the basic functions that you will find in the standard libraries of most functional programming languages, Clojure's standard library offers a wealth of interesting and useful functions that facilitate working with immutable data. In this talk, we will explore the Clojure standard library by applying interesting functions like cycle, mapcat, partition and reductions to transform data that represents music. Using the alda-clj library, we will not only see the result of each function call, we will also hear the results and observe how they can help us understand how each function works.

  • Daniel Steinberg
    keyboard_arrow_down

    Daniel Steinberg - Stumbling over State

    Daniel Steinberg
    Daniel Steinberg
    Author
    dimsumthinking.com
    schedule 4 months ago
    Sold Out!
    45 Mins
    Tutorial
    Beginner

    We each follow similar paths into the forest of functional programming. Some languages are better suited than others but we all hit a wall on our way to mastering monads. In this talk, I'll use examples from the Swift programming language to trace our understanding from types  that feel like containers such as Array and Optional to types that definitely don’t such as Reader and State Monads. We’ll learn to perform many magic tricks along the way.

  • Tony Morris
    keyboard_arrow_down

    Tony Morris - Type-hole development

    Tony Morris
    Tony Morris
    Software Engineer
    Simple Machines
    schedule 5 months ago
    Sold Out!
    45 Mins
    Tutorial
    Intermediate

    In this presentation, we will see coding problems, similar to those which can be found at https://github.com/system-f/fp-course/ using the Haskell programming language.

    Solving problems such as these can be daunting for many reasons and especially for beginners. A common stumbling block to these types of problems is coming up against unfamiliar problem-solving methods. For example, everyone knows how to add up the numbers in a list with a for-loop. This is a well-understood method of solving this particular coding problem.

    And then you hear the functional programmers, "just use the types" and "well you just do the only obvious thing to solve it." While true, this is not particularly helpful to someone who is not already fluent with this approach to problem-solving.

    You may have heard of using type-holes to solve coding problems. We'll be using type-holes, and a few other techniques, with the Haskell programming language to live-solve coding problems. We will solve both trivial and not-so-trivial problems while "thinking out aloud." Feel free to follow along! You'll just need Glasgow Haskell Compiler (GHC) and a text editor installed.

  • Aaron Hsu
    keyboard_arrow_down

    Aaron Hsu - DSLs, Architecture, and Structural Design in APL, 3 ways.

    Aaron Hsu
    Aaron Hsu
    Computer Researcher
    Dyalog Ltd.
    schedule 9 months ago
    Sold Out!
    45 Mins
    Talk
    Intermediate

    Beginning functional and APL programmers often express confusion about how to structure large software projects or larger pieces of code. Both APL and FP have a tendency to highlight their low-level features and de-emphasize system architecture patterns. This can leave programmers with a strong sense of how to write a set of small functions, but with less confidence or skill in designing, recognizing, and implementing more cohesive implicit system architectures that hold these lower level functions together. System architectures serve as a method for constraining the overall design of a system to give direction and focus to lower level implementation requirements. Especially in APL, where system architecture is often best implemented implicitly, it behooves the programmer to understand the ramifications of architecture and to implement them in their own systems. This talk unpacks a number of these "architecture level" questions within the framework of the APL programming language by exploring the same topic through 3 different architectural approaches, each of which has a very distinct flavor, presentation, and impact on the resulting source code. Particular attention is paid to the question of domain-specific languages, their design, and how they can interact with APL as tools for architectural exploration and guidance in APL source trees. 

  • Rodrigo Girão Serrão
    keyboard_arrow_down

    Rodrigo Girão Serrão - Why APL is a language worth knowing

    Rodrigo Girão Serrão
    Rodrigo Girão Serrão
    Consultant
    Dyalog Ltd.
    schedule 5 months ago
    Sold Out!
    45 Mins
    Talk
    Beginner

    “A language that doesn't affect the way you think about programming, is not worth knowing.” ― Alan Perlis, in “Epigrams in Programming”

    Following Alan Perlis's words, this talk will show why APL is a language worth knowing. In other words, I will devote the talk to showcasing characteristics of APL that are likely to, on the one hand, influence the way you use other programming languages, and, on the other hand, understand concepts of computer science.

    By listening to this talk, I hope to convince you that learning a language that is radically different from all the other languages you know isn't harmful. Learning a language that is radically different from all other languages you know won't scatter your knowledge or spread your brain too thin. In fact, learning a language that is radically different from all other languages you know will cement your programming  knowledge, helping you build bridges between topics you didn't even know were connected.

    To drive my point home, we take a closer look at two characteristics of APL: the fact that Boolean values are represented by the integers 0 and 1, and the fact that APL is an array-oriented language. In studying these two things, we draw connections to the traditional if statement and to list comprehensions, deepening our understanding of those.

  • Dhananjay Nene
    keyboard_arrow_down

    Dhananjay Nene - Snippets from an algorithmic trading system in Kotlin

    45 Mins
    Talk
    Intermediate

    This talk will introduce the audience to algorithmic trading, the design of an algorithmic trading system, and various snippets written in Kotlin that fulfil specific tasks that collectively contribute towards a full trading system. The rough sketch will be as follows

  • Shakthi Kannan
    keyboard_arrow_down

    Shakthi Kannan - Fast and Curious: Benchmarking (Multicore) OCaml

    Shakthi Kannan
    Shakthi Kannan
    Senior Software Engineer
    Tarides
    schedule 9 months ago
    Sold Out!
    20 Mins
    Experience Report
    Beginner

    An oft overlooked aspect of programming language development process is benchmarking. While popular CI/CD tools such as Azure pipelines, Gitlab CI, Circle CI, Drone.io and Github Actions are regularly used for continuous testing and deployment, there is a dearth of such tools for continuous benchmarking. This is because benchmarking well is challenging due to the care needed to choose appropriate benchmarks, the complexity of modern OSes and hardware that makes it hard to obtain reproducible results, and a powerful dashboard needed to surface resultant metrics in a useful manner that can be explored interactively by the developer.

    For benchmarking the compiler of the OCaml [1] programming language, we have developed Sandmark [2]. Sandmark is a (a) suite of well chosen benchmarks aimed at exercising different performance axes including CPU, memory and IO (b) a tool to run the benchmarks, building the compiler and its dependencies under varying configuration settings and (c) a dashboard [3] to interactively explore the results of the benchmark runs. Sandmark was originally developed for supporting the Multicore OCaml [4] project, which aims to add native support for concurrency and parallelism to OCaml, and has undergone significant improvements since the initial release [5]. 

    We have learnt several useful lessons in building a continuous benchmarking infrastructure that we would like to share in this talk, which may benefit developers who work on projects where performance is critical. In this talk, I will describe the Sandmark tool, illustrate the quirks of modern OSes and hardware and how we overcame them, highlighting useful takeaways for setting up continuous benchmarking for your own projects.

    References:

    [1] OCaml: https://ocaml.org/
    [2] Sandmark: https://github.com/ocaml-bench/sandmark
    [3] sandmark-nightly: https://github.com/ocaml-bench/sandmark-nightly
    [4] Multicore OCaml: https://github.com/ocaml-multicore/ocaml-multicore/
    [5] Tom Kelly. Benchmarking the OCaml compiler: our experience, OCaml Workshop 2019, https://icfp19.sigplan.org/details/ocaml-2019-papers/3/Benchmarking-the-OCaml-compiler-our-experience

  • Sudha Parimala
    keyboard_arrow_down

    Sudha Parimala - OCaml Platform in 2022

    Sudha Parimala
    Sudha Parimala
    Software Engineer
    Tarides
    schedule 9 months ago
    Sold Out!
    45 Mins
    Demonstration
    Beginner

    OCaml - a functional programming language from the ML family, recently celebrated its 25th year. For a language to be around for that long is an achievement in itself. Furthermore, people are actively working on adding exciting features to the language and its ecosystem.

    Thanks to efforts from various developers and maintainers, the OCaml developer platform has come a long way and continues to evolve at a rapid phase. My talk will cover all the existing tooling that makes a OCaml developer's life easy.

    The talk will demonstrate end-to-end state-of-the-art developer tooling, right from installing a OCaml compiler, using VSCode and vscode-ocaml-platform which provides IDE like features, to publishing a library and its documentation.

  • Aaron Hsu
    keyboard_arrow_down

    Aaron Hsu - Learning APL through Combinatoric Idioms

    Aaron Hsu
    Aaron Hsu
    Computer Researcher
    Dyalog Ltd.
    schedule 9 months ago
    Sold Out!
    90 Mins
    Tutorial
    Beginner

    After learning the basics of APL, the question is often, "What do I do next?" The intermediate process of learning how to write good APL can feel especially challenging to those who are not used to operating in a dataflow, array-oriented style. One valuable resource is the large number of APL Idioms available for use. These are often referenced as a kind of "standard library" of APL functionality, especially for more experienced APL programmers. Studying the idioms is often a source of new insights for APL programmers, but for the uninitiated, it can be unclear what exactly you should learn when looking at an Idiom. Many users mistakenly see Idioms as just a short implementation of what would be a library call in another language, and thus equate Idioms and Libraries as serving the same purpose. In this talk, we will discuss and explore three combinatorial idioms in detail, not only explaining how they work, the thought process behind them, and the lessons that you can learn from them, but also the meta-level question of how to go about extracting these lessons for yourself when reading idioms on your own. 

  • Gopal S Akshintala
    keyboard_arrow_down

    Gopal S Akshintala - Fight Complexity with Functional Programming

    45 Mins
    Demonstration
    Intermediate

    A Metric-driven approach to reduce Cognitive Complexity in a code base, using Functional Programming, demoed **hands-on**, by solving a complex real-world ubiquitous design challenge - REST API Bulk Request Validation, with an extensible Framework that separates what-to-do (Validations) from how-to-do (Validation Orchestration). Let's do a case study of a successful implementation done by our team in the world's largest SaaS org, _Salesforce_, through our in-house baked FOSS library **Vader**.

help