Lindsey Kuper lkuper

Making Progress Under Uncertainty in SMT Solving, Research, and Life

Abstract

SAT and Satisfiability Modulo Theories (SMT) solvers have many important applications in PL, including verification, testing, type checking and inference, and program analysis – but they are often a mysterious black box to their users, even when those users are PL researchers with lots of solver experience! This talk will be partly a tutorial introduction to the inner workings of SAT and SMT solvers, and partly an extended analogy to navigating life as a researcher: making decisions when you have only incomplete information to go on, learning from decisions that turned out to be bad, and determining when to give up and when to try again. I’ll also highlight a variety of papers in this year’s POPL program that make use of SAT and SMT solving, and discuss why I think it’s worthwhile to learn about solver internals.

Outline

Introduction
Self-intro

	!!Con 2024
	August 24-25, 2024

	Santa Cruz, California
	and online

	Two days of ten-minute talks about
	the joy, excitement, and surprise of computing

	Let’s make local and accountable tech! (Dawn Walker) • Reverse-engineering a 30-year old synthesizer to perfectly recreate video game music! (Peter Sobot) • Programming with only exceptions! (Nicole Tietz-Sokolskaya) • Mitos! Handweaving My Ancestral DNA!!! (Sally Kong) • Let’s run a tiny chess neural network by hand! (Amédée d’Aboville) • The Astrolabe! Using modern digital computing to recreate ancient analog computers (Jes Wolfe) • A brief history of keyboards! (Jesse Chen) • Recreating Sketchpad, the first GUI! (Adam Solove) • Images from a 1970s Typewriter!! (Phil Warren) • bang! bang! he murdered math! {the musical!} (Taylor Troesh) • Huggable Data! Making the Ephemeral Last Longer with Textile Dataviz! (Aldís Elfarsdóttir) • Keyboarding Ain’t Easy?? What Not To Do When Building a Keyboard!! (Liz Frost) • The Perfect Blend!! Reverse engineering a bluetooth

	module Main where

	import Data.IORef

	data Counter = Counter { x :: IORef Int }

	makeCounter :: Int -> IO Counter
	makeCounter i = do iref <- newIORef i
	return (Counter iref)

	$ git log -p --word-diff 2015-12-29-refactoring-as-a-way-to-understand-code.markdown \| cat
	commit 698f4140d1f141b339731f8fe8c984137f93880e
	Author: Lindsey Kuper <lindsey@composition.al>
	Date: Fri Jun 9 14:00:31 2017 -0700

	Tweak a bunch of tags, mostly!

	diff --git a/source/_posts/2015-12-29-refactoring-as-a-way-to-understand-code.markdown b/source/_posts/2015-12-29-refactoring-as-a-way-to-understand-code.markdown
	index 8cafa552c1..e3ccd2b267 100644
	--- a/source/_posts/2015-12-29-refactoring-as-a-way-to-understand-code.markdown

	t = 0.0, t/dt = 0.0, mod(t/dt, 10) = 0.0
	t = 0.0001, t/dt = 1.0, mod(t/dt, 10) = 1.0
	t = 0.0002, t/dt = 2.0, mod(t/dt, 10) = 2.0
	t = 0.0003, t/dt = 2.9999999999999996, mod(t/dt, 10) = 2.9999999999999996
	t = 0.0004, t/dt = 4.0, mod(t/dt, 10) = 4.0
	t = 0.0005, t/dt = 5.0, mod(t/dt, 10) = 5.0
	t = 0.0006, t/dt = 5.999999999999999, mod(t/dt, 10) = 5.999999999999999
	t = 0.0007, t/dt = 7.0, mod(t/dt, 10) = 7.0
	t = 0.0008, t/dt = 8.0, mod(t/dt, 10) = 8.0
	t = 0.0009, t/dt = 9.0, mod(t/dt, 10) = 9.0

	lvars
	LVar's
	LVars
	elseif
	EuroSys
	tuples
	Karpinski
	Blandy's
	multi
	Amr

	julia> foo = 3
	3

	julia> function test(a::Type{Val{foo}}) return foo end
	test (generic function with 2 methods)

	julia> test(Val{foo})
	3

	julia> foo = 4

	# Dependencies: `gem install ruby-gmail`

	require 'gmail'
	require 'csv'

	email_subject = "subject line"

	email_body = File.open("email.txt", "rb").read

	username = "username"

	#lang racket

	;; A solver for the following puzzle:
	;; Given 5 integers a, b, c, d, and e,
	;; find an expression that combines a, b, c, and d with arithmetic operations (+, -, *, and /) to get e.

	(require srfi/1)

	(define ops '(+ - * /))

	;; permutations: takes a list and returns a list of lists,
	;; where each is a permutation of the original.
	;; I got the idea for the algorithm from http://stackoverflow.com/a/23718676/415518.
	(define (permutations ls)
	(cond
	;; base cases: lists of length 0, 1, or 2
	[(null? ls) '(())]
	[(equal? (length ls) 1) `((,(first ls)))]
	[(equal? (length ls) 2)
	`((,(first ls) ,(second ls))