parlarjb

Analyzing programs with Z3: https://www.youtube.com/watch?v=ruNFcH-KibY

Software Synthesis via sketching thesis http://people.csail.mit.edu/asolar/papers/thesis.pdf

ericpony.github.io/z3py-tutorial/guide-examples.htm
http://ericpony.github.io/z3py-tutorial/advanced-examples.htm
https://theory.stanford.edu/~nikolaj/programmingz3.html
A big tutorial: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.367.9961&rep=rep1&type=pdf

parlarjb

open util/ordering[Time]

sig Time {}
sig Key {
  pressed: set Time
}

abstract sig Event {
  pre, post: Time,
  key: Key

parlarjb

from z3 import *
import itertools

s = Solver()

names = ['Ali', 'Kelsey', 'Yuan', 'Chris', 'Narges', 'Weija', 'Jay', 'Linh', 'Joseph', 'Lucy']
nmap = {} # Maps string name to integer value
imap = {} # Reverse map, integer value to string name
for i, name in enumerate(names):
  nmap[name] = i

parlarjb

from z3 import *

s = Solver()

Name, name_consts = EnumSort("Name",
                    ["Riker", "Beverly", "Data", "Troi"])
riker, beverly, data, troi = name_consts

Planet, planet_consts = EnumSort("Planet",
                    ["Betazed", "Dytallix B", "Risa", "Tellar"])

parlarjb

from z3 import *

s = Solver()

Name, name_consts = EnumSort("Name",
                    ["Riker", "Beverly", "Data", "Troi"])
riker, beverly, data, troi = name_consts

Planet, planet_consts = EnumSort("Planet",
                    ["Betazed", "Dytallix B", "Risa", "Tellar"])

parlarjb

from z3 import *

s = Solver()

Name, name_consts = EnumSort("Name",
                    ["Riker", "Beverly", "Data", "Troi"])
riker, beverly, data, troi = name_consts

Planet, planet_consts = EnumSort("Planet",
                    ["Betazed", "Dytallix B", "Risa", "Tellar"])

parlarjb

Zoom Code Review

===============

Why Code Review?

The most effective way to get bugs out of code is code review. More than running the code, more than unit tests, having someone else review an author's code is the best technique known to eliminate bugs (Fagan 1975 and Cohen 2006).

parlarjb

sig Account {
  resources: set Resource,
  users: set User
}

sig User {
  canAccess: some Resource
}

sig Resource {

parlarjb

one sig Person {
}

sig Resource {
  , access: set Person
  , parent: lone Resource
}

fact "No cycles" {

parlarjb

one sig Person {
}

sig Resource {
  , access: set Person
  , parent: lone Resource
}

fact "No cycles" {