Bart Jacobs

Bart Jacobs

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:

PhD students:

Former PhD students:

  • Frédéric Vogels (co-supervisor) (defended, December 2012)

Selected publications:

  • 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.
    [PDF] [Slides]
  • 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.
    [PDF]
  • Sound symbolic linking in the presence of preprocessing
    By Gijs Vanspauwen and Bart Jacobs.
    At SEFM 2013.
    [PDF]
  • 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.
    [PDF] [Downloads]
  • 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.
    [PDF] [Downloads]

All publications (see also dblp gs rid lirias)

Other duties:

Miscellaneous:

  • 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.
 

Key publications:

  1. 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 download0 491446bibtex
  2. 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 download0 336725bibtex
  3. 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 download0 300985bibtex
  4. 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 download0 278074bibtex
  5. 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 download0 221909bibtex
[More...]
 

 

Contact info

  • Office: 05.50
  • Address:
    Dept. Computer Science
    Celestijnenlaan 200A
    B-3001 Heverlee
    BELGIUM
  • Tel: +3216372014
  • Fax: +3216327996
  • Email: Bart Jacobs