I am an associate professor at the Department of Computer Science of KU Leuven - University of Leuven, Belgium. I am a member of the Security: Programming Languages task force of the iMinds-DistriNet research group. I obtained my PhD here in 2007 under the supervision of Prof. Frank Piessens.
My research efforts are mainly in trying to find practical approaches for software development teams to verify security properties and other important properties of programs.
Topics that I am interested in include:
- Program logics, separation logic
- Program verification tools
- Programming language features for security, correctness, and concurrency
- Static analysis, type systems
- Concurrent programming; Programming language semantics
- Theorem proving technology, proof assistants
- Execution environments and techniques for security & correctness
Some verification tool prototypes:
Former PhD students:
- Frédéric Vogels (co-supervisor) (defended, December 2012)
- Featherweight VeriFast
By Frédéric Vogels, Bart Jacobs, and Frank Piessens.
In LMCS 11(3), 2015.
[PDF] [Homepage] [Slides, handouts, Coq proof]
- Provably live exception handling
By Bart Jacobs.
At FTfJP 2015.
- Modular termination verification
By Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper.
At ECOOP 2015.
[PDF] [TR] [Slides]
- Sound, modular and compositional verification of the input/output behavior of programs
By Willem Penninckx, Bart Jacobs, and Frank Piessens.
At ESOP 2015.
- Sound symbolic linking in the presence of preprocessing
By Gijs Vanspauwen and Bart Jacobs.
At SEFM 2013.
- Sound formal verification of Linux's USB BP keyboard driver
By Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, and Frank Piessens.
At NFM 2012.
[PDF] [More info]
- Verification of unloadable modules
By Bart Jacobs, Jan Smans, and Frank Piessens.
At FM 2011.
[PDF] [Slides (PDF)] See also TR CW-604 and the Coq proof.
- Expressive modular fine-grained concurrency specification
By Bart Jacobs and Frank Piessens.
At POPL 2011.
[PDF] [Slides (PDF)] See also TR CW-590 and the Coq proof.
- Failboxes: Provably safe exception handling
By Bart Jacobs and Frank Piessens.
At ECOOP 2009.
- A programming model for concurrent object-oriented programs
By Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, and Wolfram Schulte.
In ACM TOPLAS 31(1), Dec 2008.
- Member, organizing committee, Belgian Informatics Olympiad, member of the International Olympiad in Informatics.
- The Essence of Coq as a Formal System - A short text that attempts to introduce Coq as a formal system to anyone with a programming background. Note: This is not a Coq tutorial: It does not introduce type inference, implicit arguments, notations, modules, proof scripts, tactics, automation, or the standard library. Please report any inaccuracies.
- Bart Jacobs, Dragan Bosnacki, Ruurd Kuiper, Modular termination verification, 29th European Conference on Object-Oriented Programming (ECOOP 2015), volume 37, pages 664-688, Prague, 5-10 July 2015
- Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, Frank Piessens, Sound formal verification of Linux's USB BP keyboard driver, NASA Formal Methods, volume 7226, pages 210-215, Norfolk, Virginia, USA, 3-5 April 2012
- Bart Jacobs, Jan Smans, Frank Piessens, Verification of unloadable modules, 17th International Symposium on Formal Methods (FM 2011), volume 6664, pages 402-416, Limerick, Ireland, 20-24 June 2011
- Bart Jacobs, Frank Piessens, Expressive modular fine-grained concurrency specification, Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2011), pages 271-282, Austin, TX, USA, 26-28 January 2011
- Bart Jacobs, Frank Piessens, Failboxes: Provably safe exception handling, ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genova, Italy, July 6-10, 2009, Proceedings, volume 5653, pages 470-494, Genova, 6-10 July 2009