Logic as a lingua franca

Certifying

Prover

…

add %eax,%ebx

movl 8(%ecx,%ebx,4)

...

Proof

Proof

Checker

SFpol

VC

Safety of dataflow optimizations

can be verified.

Previous slide

Next slide

Back to first slide

View graphic version