Invited talks

Don Sannella

Contemplate Ltd & the University of Edinburgh, UK

ThreadSafe: Static Analysis for Java Concurrency

ThreadSafe is a commercial static analysis tool that focuses on detection of Java concurrency defects. By restricting attention to concurrency bugs, ThreadSafe can find bugs that other static analysis tools, both commercial and freely available, miss or are not designed to look for. Its findings are generated from information produced by a class-by-class flow-sensitive, path-sensitive, context-sensitive points-to and lock analysis, with heuristics to tune the analysis to avoid false positives. It has been successfully applied to codebases of more than a million lines.

Colin O'Halloran

D-RisQ Software Systems & the University of Oxford, UK

Verifying Critical Cyber-Physical Systems After Deployment

Cyber-Physical Systems are increasingly novel hardware and software compositions creating smart, autonomously acting devices, enabling efficient end-to-end workflows and new forms of user-machine interaction. The heterogeneous, evolving and distributed nature of CPS means that there is little chance of performing a top down development or anticipating all critical requirements such devices will need to satisfy individually and collectively. This paper describes an approach to verifying system requirements, when they become known, by performing an automated refinement check of its composed components abstracted from the actual implementation.