| 2026 | CHI | Decidos: Accessible, Usable and Secure Voting in Low-stakes Elections Using Identity Wallets. | Floris Jansen, Hanna Schraffenberger, Bart Jacobs |
| 2025 | CALCO | Drawing and Recolouring. | Bart Jacobs, Mrk Szles |
| 2024 | FOSSACS | Drawing from an Urn is Isometric. | Bart Jacobs |
| 2023 | CHI | PostGuard: Towards Easy and Secure Email Communication. | Leon Botros, Merel Brandon, Bart Jacobs, Daniel Ostkamp, Hanna Kathrin Schraffenberger, Marloes Venema |
| 2023 | CSL | Counting and Matching. | Bart Jacobs, Dario Stein |
| 2023 | FTfJP | Verifying C++ Dynamic Binding. | Niels Mommen, Bart Jacobs |
| 2023 | PLDI | Completeness Thresholds for Memory Safety of Array Traversing Programs. | Tobias Reinhard, Justus Fasse, Bart Jacobs |
| 2023 | WoLLIC | A Principled Approach to Expectation Maximisation and Latent Dirichlet Allocation Using Jeffrey's Update Rule. | Bart Jacobs |
| 2022 | LICS | Partitions and Ewens Distributions in element-free Probability Theory. | Bart Jacobs |
| 2022 | NordiCHI | Design Principles for Actual Security. | Merel Brandon, Hanna Kathrin Schraffenberger, Wouter Sluis-Thiescheffer, Thea van der Geest, Daniel Ostkamp, Bart Jacobs |
| 2021 | CAV | Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting. | Tobias Reinhard, Bart Jacobs |
| 2021 | LICS | From Multisets over Distributions to Distributions over Multisets. | Bart Jacobs |
| 2020 | ECOOP | A separation logic to verify termination of busy-waiting for abrupt program exit. | Tobias Reinhard, Amin Timany, Bart Jacobs |
| 2020 | ISoLA | Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs. | Bart Jacobs |
| 2019 | ECOOP | Transferring Obligations Through Synchronizations. | Jafar Hamin, Bart Jacobs |
| 2019 | ECOOP | Specifying I/O using abstract nested hoare triples in separation logic. | Willem Penninckx, Amin Timany, Bart Jacobs |
| 2019 | FOSSACS | Causal Inference by String Diagram Surgery. | Bart Jacobs, Aleks Kissinger, Fabio Zanasi |
| 2019 | IFM | Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming. | Tuur Benoit, Bart Jacobs |
| 2018 | ESOP | Deadlock-Free Monitors. | Jafar Hamin, Bart Jacobs |
| 2017 | CALCO | The EfProb Library for Probabilistic Calculations. | Kenta Cho, Bart Jacobs |
| 2017 | MFCS | A Formal Semantics of Influence in Bayesian Reasoning. | Bart Jacobs, Fabio Zanasi |
| 2016 | ECOOP | Partial Solutions to VerifyThis 2016 Challenges 2 and 3 with VeriFast. | Bart Jacobs |
| 2016 | FMICS | One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast. | Mahmoud Mohsen, Bart Jacobs |
| 2016 | IRI | Modular Verification of Termination and Execution Time Bounds Using Separation Logic. | Jafar Hamin, Bart Jacobs |
| 2016 | LICS | Healthiness from Duality. | Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo, Bart Jacobs |
| 2016 | MODELSWARD | Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations. | Dan Zhang, Dragan Bosnacki, Mark van den Brand, Cornelis Huizing, Bart Jacobs, Ruurd Kuiper, Anton Wijs |
| 2016 | MODELSWARD | Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code. | Dan Zhang, Dragan Bosnacki, Mark van den Brand, Cornelis Huizing, Ruurd Kuiper, Bart Jacobs, Anton Wijs |
| 2015 | CALCO | A Recipe for State-and-Effect Triangles. | Bart Jacobs |
| 2015 | ECOOP | Provably live exception handling. | Bart Jacobs |
| 2015 | ECOOP | Modular Termination Verification. | Bart Jacobs, Dragan Bosnacki, Ruurd Kuiper |
| 2015 | ESOP | Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. | Willem Penninckx, Bart Jacobs, Frank Piessens |
| 2015 | FOSSACS | States of Convex Sets. | Bart Jacobs, Bas Westerbaan, Bram Westerbaan |
| 2015 | ICTAC | First Steps Towards Cumulative Inductive Types in CIC. | Amin Timany, Bart Jacobs |
| 2015 | POPL | Sound Modular Verification of C Code Executing in an Unverified Context. | Pieter Agten, Bart Jacobs, Frank Piessens |
| 2015 | SEFM | Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications. | Gijs Vanspauwen, Bart Jacobs |
| 2014 | ACSAC | ICE: a passive, high-speed, state-continuity scheme. | Raoul Strackx, Bart Jacobs, Frank Piessens |
| 2013 | CALCO | From Kleisli Categories to Commutative C *-Algebras: Probabilistic Gelfand Duality. | Robert Furber, Bart Jacobs |
| 2013 | LICS | Measurable Spaces and Their Effect Logic. | Bart Jacobs |
| 2013 | SEFM | Sound Symbolic Linking in the Presence of Preprocessing. | Gijs Vanspauwen, Bart Jacobs |
| 2012 | FOSSACS | Fibrational Induction Meets Effects. | Robert Atkey, Neil Ghani, Bart Jacobs, Patricia Johann |
| 2011 | CALCO | Bases as Coalgebras. | Bart Jacobs |
| 2011 | FM | Verification of Unloadable Modules. | Bart Jacobs, Jan Smans, Frank Piessens |
| 2011 | FM | The 1st Verified Software Competition: Experience Report. | Vladimir Klebanov, Peter Mller, Natarajan Shankar, Gary T. Leavens, Valentin Wstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Wei |
| 2011 | FORTE | Annotation Inference for Separation Logic Based Verifiers. | Frdric Vogels, Bart Jacobs, Frank Piessens, Jan Smans |
| 2011 | FOSSACS | Coalgebraic Walks, in Quantum and Turing Computation. | Bart Jacobs |
| 2011 | ITP | Logical Formalisation and Analysis of the Mifare Classic Card in PVS. | Bart Jacobs, Ronny Wichers Schreur |
| 2011 | POPL | Expressive modular fine-grained concurrency specification. | Bart Jacobs, Frank Piessens |
| 2010 | APLAS | A Quick Tour of the VeriFast Program Verifier. | Bart Jacobs, Jan Smans, Frank Piessens |
| 2010 | CARDIS | Developing Efficient Blinded Attribute Certificates on Smart Cards via Pairings. | Lejla Batina, Jaap-Henk Hoepman, Bart Jacobs, Wojciech Mostowski, Pim Vullers |
| 2010 | FORTE | Heap-Dependent Expressions in Separation Logic. | Jan Smans, Bart Jacobs, Frank Piessens |
| 2010 | SAC | A machine-checked soundness proof for an efficient verification condition generator. | Frdric Vogels, Bart Jacobs, Frank Piessens |
| 2009 | CALCO | Coalgebraic Components in a Many-Sorted Microcosm. | Ichiro Hasuo, Chris Heunen, Bart Jacobs, Ana Sokolova |
| 2009 | CALCO | Traces, Executions and Schedulers, Coalgebraically. | Bart Jacobs, Ana Sokolova |
| 2009 | ECOOP | Security Monitor Inlining for Multithreaded Java. | Mads Dam, Bart Jacobs, Andreas Lundblad, Frank Piessens |
| 2009 | ECOOP | Failboxes: Provably Safe Exception Handling. | Bart Jacobs, Frank Piessens |
| 2009 | ECOOP | Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. | Jan Smans, Bart Jacobs, Frank Piessens |
| 2009 | EuroSys | Instruction-level countermeasures against stack-based buffer overflow attacks. | Francesco Gadaleta, Yves Younan, Bart Jacobs, Wouter Joosen, Erik De Neve, Nils Beosier |
| 2009 | SOFSEM | A Machine Checked Soundness Proof for an Intermediate Verification Language. | Frdric Vogels, Bart Jacobs, Frank Piessens |
| 2009 | WISTP | Performance Issues of Selective Disclosure and Blinded Issuing Protocols on Java Card. | Hendrik Tews, Bart Jacobs |
| 2008 | ESORICS | Dismantling MIFARE Classic. | Flavio D. Garcia, Gerhard de Koning Gans, Ruben Muijrers, Peter van Rossum, Roel Verdult, Ronny Wichers Schreur, Bart Jacobs |
| 2008 | FASE | An Automatic Verifier for Java-Like Programs Based on Dynamic Frames. | Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte |
| 2008 | FOSSACS | The Microcosm Principle and Concurrency in Coalgebra. | Ichiro Hasuo, Bart Jacobs, Ana Sokolova |
| 2007 | ICALP | Categorical Views on Computations on Trees (Extended Abstract). | Ichiro Hasuo, Bart Jacobs, Tarmo Uustalu |
| 2007 | SEFM | Sound reasoning about unchecked exceptions. | Bart Jacobs, Peter Mller, Frank Piessens |
| 2006 | ICFEM | A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. | Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte |
| 2006 | IWSEC | Crossing Borders: Security and Privacy Issues of the European e-Passport. | Jaap-Henk Hoepman, Engelbert Hubbers, Bart Jacobs, Martijn Oostdijk, Ronny Wichers Schreur |
| 2006 | MPC | Freyd is Kleisli, for Arrows. | Bart Jacobs, Ichiro Hasuo |
| 2005 | CALCO | Context-Free Languages via Coalgebraic Trace Semantics. | Ichiro Hasuo, Bart Jacobs |
| 2005 | COMPSAC | RIES - Internet Voting in Action. | Engelbert Hubbers, Bart Jacobs, Wolter Pieters |
| 2005 | POPL | Statically checking confidentiality via dynamic labels. | Bart Jacobs, Wolter Pieters, Martijn Warnier |
| 2005 | SEFM | Safe Concurrency for Aggregate Objects with Invariants. | Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte |
| 2001 | ESOP | A Formalisation of Java's Exception Mechanism. | Bart Jacobs |
| 2001 | FASE | A Logic for the Java Modeling Language JML. | Bart Jacobs, Erik Poll |
| 2001 | TACAS | The LOOP Compiler for Java and JML. | Joachim van den Berg, Bart Jacobs |
| 2000 | CARDIS | Specification of the JavaCard API in JML. | Erik Poll, Joachim van den Berg, Bart Jacobs |
| 2000 | FASE | Java Program Verification via a Hoare Logic with Abrupt Termination. | Marieke Huisman, Bart Jacobs |
| 2000 | OOPSLA | JML (poster session): notations and tools supporting detailed design in Java. | Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs |
| 1998 | ESOP | Reasonong about Classess in Object-Oriented Languages: Logical Models and Tools. | Ulrich Hensel, Marieke Huisman, Bart Jacobs, Hendrik Tews |
| 1998 | OOPSLA | Reasoning about Java Classes (Preliminary Report). | Bart Jacobs, Joachim van den Berg, Marieke Huisman, Martijn van Berkum |
| 1996 | ECOOP | Inheritance and Cofree Constructions. | Bart Jacobs |
| 1994 | CSL | An Algebraic View of Structural Induction. | Claudio Hermida, Bart Jacobs |
| 1994 | LFCS | Coalgebras and Approximation. | Bart Jacobs |