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

legionus

#!/bin/ash -efux

export DISPLAY=:0
export LIBDIR="$(getconf LIBDIR)"

# $ hsh --init
# $ hsh-install firefox xauth
# $ hsh-install fonts-ttf-google-droid-sans fonts-ttf-google-droid-sans-mono fonts-ttf-google-droid-serif
# $ grep -v '^#' /etc/hasher-priv/fstab 
# tmpfs /dev/shm tmpfs size=500m,nr_inodes=4096 0 0

phizev

#! /bin/sh -

ENABLED=$(cat /sys/module/zswap/parameters/enabled)
COMPRESSOR=$(cat /sys/module/zswap/parameters/compressor)
ZPOOL=$(cat /sys/module/zswap/parameters/zpool)
PAGE_SIZE=$(getconf PAGE_SIZE)
STORED_PAGES=$(cat /sys/kernel/debug/zswap/stored_pages)
POOL_TOTAL_SIZE=$(cat /sys/kernel/debug/zswap/pool_total_size)

POOL_SIZE=$(numfmt --to=iec-i $POOL_TOTAL_SIZE)

Eugnis

#include <pthread.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#ifdef _MSC_VER
#include <intrin.h> /* for rdtscp and clflush */
#pragma optimize("gt", on)
#else
#include <x86intrin.h> /* for rdtscp and clflush */

jirutka

The MIT License

Copyright 2018-2019 Jakub Jirutka <[email protected]>.

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

syagev

[2016/08/08 21:16:37.424364,  0] ../lib/util/become_daemon.c:124(daemon_ready)
  STATUS=daemon 'nmbd' finished starting up and ready to serve connections
[2016/08/08 21:16:52.442012,  0] ../source3/nmbd/nmbd_become_lmb.c:533(become_local_master_browser)
  become_local_master_browser: Error - cannot find server IP-172-31-41-197 in workgroup WORKGROUP on subnet 172.31.41.197
[2016/08/08 21:22:15.771932,  0] ../source3/nmbd/nmbd_become_lmb.c:533(become_local_master_browser)
  become_local_master_browser: Error - cannot find server IP-172-31-41-197 in workgroup WORKGROUP on subnet 172.31.41.197
[2016/08/08 21:27:19.081832,  0] ../source3/nmbd/nmbd_become_lmb.c:533(become_local_master_browser)
  become_local_master_browser: Error - cannot find server IP-172-31-41-197 in workgroup WORKGROUP on subnet 172.31.41.197
[2016/08/08 21:32:20.479712,  0] ../source3/nmbd/nmbd_become_lmb.c:533(become_local_master_browser)
  become_local_master_browser: Error - cannot find server IP-172-31-41-197 in workgroup WORKGROUP on sub

giovtorres

#!/bin/bash

## **Updates to this file are now at https://github.com/giovtorres/kvm-install-vm.**
## **This updated version has more options and less hardcoded variables.**

# Take one argument from the commandline: VM name
if ! [ $# -eq 1 ]; then
    echo "Usage: $0 <node-name>"
    exit 1
fi

dove-young

(defun set-outline-minor-mode-regexp ()
  ""
  (outline-minor-mode 1)
  (let ((regexp-list (append outline-minor-mode-list nil))
  (find-regexp
	 (lambda (lst)
	   ""
	   (let ((innerList (car lst)))
	     (if innerList
		 (if (string= (car innerList) major-mode)

kechol

// The main ray tracer.

#pragma warning (disable: 4786)

#include "RayTracer.h"
#include "scene/light.h"
#include "scene/material.h"
#include "scene/ray.h"

#include "parser/Tokenizer.h"