Bart Jacobs

Bart Jacobs

ORCID 0000-0002-3605-249X, ResearcherID B-1271-2014 

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 imec-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:

Postdocs:

Former PhD students:

Selected technical reports:

These report on work in progress; we believe they are technically sound but they may not be of publication-level finish in terms of positioning, presentation, and discussion of related work.

  • Abstract I/O Specification
    By Willem Penninckx, Amin Timany, and Bart Jacobs.
    Technical report, arXiv:1901.10541, January 2019.
    [PDF] [Coq development]
    An earlier version appeared as TR CW-714, Dept. Comp. Sci., KU Leuven, May 2018.

Selected publications:

  • Specifying I/O using Abstract Nested Hoare Triples in Separation Logic
    By Willem Penninckx, Amin Timany, and Bart Jacobs.
    At FTfJP 2019.
    [PDF]
  • Transferring Obligations through Synchronizations
    By Jafar Hamin and Bart Jacobs.
    At ECOOP 2019.
    [PDF] [Coq proof]
  • Modular Termination Verification of Single-Threaded and Multithreaded Programs
    By Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper.
    In ACM TOPLAS 40(3), July 2018.
    [PDF] [Coq proof]
  • Deadlock-free monitors
    By Jafar Hamin and Bart Jacobs.
    At ESOP 2018.
    [PDF] [TR]
  • 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, (ed. John Tang Boyland), European Conference on Object-Oriented Programming (ECOOP) , 29th European Conference on Object-Oriented Programming (ECOOP 2015) , volume 37, pages 664-688, Prague, July 5-10, 2015 download0 1582564bibtex   1582564lirias 1582564doi
  2. Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, Frank Piessens, Sound formal verification of Linux's USB BP keyboard driver, (eds. Alwyn Goodloe, Suzette Person), NASA Formal Methods , NASA Formal Methods , volume 7226, pages 210-215, Norfolk, Virginia, USA, April 3-5, 2012 download0 1581718bibtex   1581718lirias 1581718doi
  3. Bart Jacobs, Jan Smans, Frank Piessens, Verification of unloadable modules, (eds. Michael Butler, Wolfram Schulte), 17th International Symposium on Formal Methods (FM 2011) , 17th International Symposium on Formal Methods (FM 2011) , volume 6664, pages 402-416, Limerick, Ireland, June 20-24, 2011 download0 1581725bibtex   1581725lirias 1581725doi
  4. Bart Jacobs, Frank Piessens, Expressive modular fine-grained concurrency specification, (ed. Mooly Sagiv), Principles of Programming Languages (POPL 2011) , Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2011) , pages 271-282, Austin, TX, USA, January 26-28, 2011 download0 95777bibtex   95777lirias 95777doi
  5. Bart Jacobs, Frank Piessens, Failboxes: Provably safe exception handling, (ed. Sophia Drossopoulou), ECOOP , ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genova, Italy, July 6-10, 2009, Proceedings , volume 5653, pages 470-494, Genova, July 6-10, 2009 download0 95779bibtex   95779lirias 95779doi
[More...]
 

 

Contact info

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