Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Verification and Automatic Reasoning Group

The members of this group are interested in developing tools and methods for reasoning about complex systems. Example application areas include operating systems, biological systems, or distributed algorithms. Particular projects include the SLAyer shape analysis engine, the Terminator termination prover, and BioCheck modelling and analysis tool for gene regulatory networks.

Recent Papers

SLAyer: Memory Safety for Systems-Level Code
Josh Berdine,
Byron Cook,
Samin Ishtiaq
CAV'11 (Snowbird)

Making prophecies with decision predicates
Byron Cook,   
Eric Koskinen
POPL'11 (Austin)

Proving stabilization of biological systems
Byron Cook,
Jasmin Fisher,
Elzbieta Krepska,
Nir Piterman
VMCAI'11 (Austin)

 

Projects

BioCheck
SLAyer 
Terminator

 

Publications

Tools

Download SLAyer.zip