Specification, Verification, and Synthesis Using Extended State Machines with Callbacks (2016)

2

Specification, Verification, and Synthesis Using Extended State Machines with Callbacks (2016) ☶ pdf slides c formalmethods hardware linux tuba.ece.ufl.edu
via nickpsecurity 5 months ago | cached | no comments

0

Aims to synthesize race-free, concurrent programs from models of concurrent components in a system. Aims to provably not add deadlocks if original model was deadlock-free. Case study is a USB driver for Linux.