Bart Jacobs
I am a professor at the Department of Computer Science of the Katholieke Universiteit Leuven, Belgium. I am a member of the Security: Programming Languages task force of the DistriNet research group.
Zou je graag doctoreren rond een van de onderwerpen hieronder? Interested in doing a PhD in one of the below topics? Let's talk!
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/or 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:
PhD students:
- Frédéric Vogels (co-supervisor)
- Willem Penninckx
Information for students of Capita Selecta Software Engineering
Selected publications:
- Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, and Frank Piessens. Sound Formal Verification of Linux's USB BP Keyboard Driver. NFM 2012. [PDF] [More info]
- Bart Jacobs, Jan Smans, and Frank Piessens. Verification of Unloadable Modules. FM 2011. [PDF] [Slides (PDF)] See also TR CW-604 and the Coq proof.
- Bart Jacobs and Frank Piessens. Expressive modular fine-grained concurrency specification. POPL 2011. [PDF] [Slides (PDF)] See also TR CW-590 and the Coq proof.
- Bart Jacobs and Frank Piessens. Failboxes: Provably safe exception handling. ECOOP 2009. [PDF] [Downloads]
- Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, and Wolfram Schulte. A programming model for concurrent object-oriented programs. ACM TOPLAS 31(1), Dec 2008. [PDF] [Downloads]
Key publications:
- Bart Jacobs, Jan Smans, Frank Piessens, A quick tour of the VeriFast program verifier, Programming Languages and Systems (APLAS 2010), pages 304-311, Shanghai, China, 28 November - 1 December 2010
- Frédéric Vogels, Bart Jacobs, Frank Piessens, A machine-checked soundness proof for an efficient verification condition generator, Symposium on Applied Computing 2010, volume 3, pages 2517-2522, Sierre, Switzerland, 22-26 March 2010
- 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
- Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, Wolfram Schulte, A programming model for concurrent object-oriented programs, ACM transactions on programming languages and systems, volume 31, issue 1, 48 p. pages, December 2008
- Bart Jacobs, Jan Smans, Frank Piessens, Verifying the Composite pattern using separation logic, Workshop on Specification and Verification of Component-Based Systems, Challenge Problem Track, Atlanta, GA, USA, 9-10 November 2008
