ITF Belgium > Program > Speakers  > Bart Jacobs
Share
linkedin twitter facebook email

 

Bart Jacobs    
   

 

Save

Save

Bio

BART JACOBS, IMEC / KU LEUVEN
PROFESSOR DISTRINET RESEARCH GROUP

Bart Jacobs is a Professor at the imec-DistriNet research group of the Department of Computer Science of KU Leuven - University of Leuven since 2010. His research interests center around improving the ability of software development teams to cost-effectively deliver software with a high assurance of security and correctness, by developing techniques for effective formal verification of program modules. He explores and validates new formal verification approaches by means of the VeriFast program verification tool which he has been developing since 2008.

 

Back to session

Presentation abstract

THE ART OF WRITING SECURE SOFTWARE: HIGH-ASSURANCE VERIFICATION

I will present the technology we are developing to help software development teams deliver software with high assurance of security and correctness. We implemented the technology in a tool called VeriFast. This tool takes the source code for a C or Java program module, annotated with specifications and proof hints, as input, and, in a matter of seconds, reports either "0 errors found", or shows, in a debugger-like GUI, a symbolic execution trace leading to a verification failure. If the tool reports "0 errors found", the program module is guaranteed to satisfy its specification in all possible executions. I will demonstrate the tool by using it to verify the correct patching of a well-known program module that contains a highly publicized programming error that had a severe impact on the internet ecosystem.

 

 

Back to program

Back to speakers

 

Copyright imec 2017