« BACK TO PROGRAM

Lessons from verifying legacy Java code for C++ specification & verification

David Cok

Legacy code is typically written with no regard for specification and verification. Consequently verification tools applied to legacy code must support most language features and be able to scale to the size and scope of industrial software. This talk will use case study examples from a verification project targeting industrial Java code to demonstrate both how verification of features in Java 8 was achieved and what challenges still remain for such projects. Then we will illustrate how the lessons learned from that project are informing the design of a specification language for C++.

Download this presentation

About David Cok

David Cok is a researcher in formal methods and deductive verification, with an emphasis on practical application to industrial software. He is currently working with the Frame-C team at CEA on specification for C++. He also consults on software verification for industrial software, contributes to the definition of the Java Modeling Language, and is the primary open source developer of the OpenJML tool for verifying Java software. Previously, Dr. Cok worked as manager, researcher and project leader at GrammaTech, proposing and executing US government-funded research projects in program analysis. Before joining GrammaTech, Dr. Cok was a Senior Research Associate and leader of research and product development groups at Eastman Kodak Company. He has taught Computer Science courses at Rochester Institute of Technology. He serves on multiple Industrial Advisory Boards for university departments and on boards for non-profit and educational institutions. He earned an A.M. and Ph.D. in Physics from Harvard University and graduated with honors from Calvin College with A.B. degrees in Physics and Mathematics.