Automated Reasoning and the Behavior of the Smalltalk VM

To 110 years of L. E. J. Brouwer's dissertation

Boris Shingarov

LabWare

shingarov@labware.com

The Problem

    ...
    mov eax, dword ptr [edi]
; an unfound bug sometimes corrupts
; the value of ecx to point to
; a random location above stack
; limit; reset to preserve sanity
    mov ecx, 0
    push eax
    ...

TAM

Approach I:
Infer the backend

VLS

Approach II:
Formal Proof

Demo

A taste of automatic proof:
Commutativity of ∧

Place Under the Sun

  • Keep Being Relevant
    • Competition

Dedication

Luitzen Egbertus Jan Brouwer
1881 – 1966

Thank you

See you in 2018!