Software security: experiments on the .NET common language run-time and the shared source common language infrastructure. - Frank Piessens; Bart Jacobs 002; Wouter Joosen (IEE Proc. Softw., 2003)

A Generic Architecture for Web Applications to Support Threat Analysis of Infrastructural Components. - Lieven Desmet; Bart Jacobs 002; Frank Piessens; Wouter Joosen (Communications and Multimedia Security, 2004)

Threat Modelling for Web Services Based Web Applications. - Lieven Desmet; Bart Jacobs 002; Frank Piessens; Wouter Joosen (Communications and Multimedia Security, 2004)

Support for Metadata-driven Selection of Run-time Services in .NET is Promising but Immature. - Frank Piessens; Bart Jacobs 002; Eddy Truyen; Wouter Joosen (J. Object Technol., 2004)

Boogie: A Modular Reusable Verifier for Object-Oriented Programs. - Michael Barnett 001; Bor-Yuh Evan Chang; Robert DeLine; Bart Jacobs 002; K. Rustan M. Leino (FMCO, 2005)

Safe Concurrency for Aggregate Objects with Invariants. - Bart Jacobs 002; Frank Piessens; K. Rustan M. Leino; Wolfram Schulte (SEFM, 2005)

The Spec# Programming System: Challenges and Directions. - Michael Barnett 001; Robert DeLine; Manuel Fähndrich; Bart Jacobs 002; K. Rustan M. Leino; Wolfram Schulte; Herman Venter (VSTTE, 2005)

A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. - Bart Jacobs 002; Jan Smans; Frank Piessens; Wolfram Schulte (ICFEM, 2006)

VC generation for functional behavior and non-interference of iterators. - Bart Jacobs 002; Frank Piessens; Wolfram Schulte (SAVCBS@FSE, 2006)

A Simple Sequential Reasoning Approach for Sound Modular Verification of Mainstream Multithreaded Programs. - Bart Jacobs 002; Jan Smans; Frank Piessens; Wolfram Schulte (TV@FLoC, 2006)

Static Verification of Code Access Security Policy Compliance of .NET Applications. - Jan Smans; Bart Jacobs 002; Frank Piessens (J. Object Technol., 2006)

Sound reasoning about unchecked exceptions. - Bart Jacobs 002; Peter Müller 001; Frank Piessens (SEFM, 2007)

Inspector Methods for State Abstraction. - Bart Jacobs 002; Frank Piessens (J. Object Technol., 2007)

An Automatic Verifier for Java-Like Programs Based on Dynamic Frames. - Jan Smans; Bart Jacobs 002; Frank Piessens; Wolfram Schulte (FASE, 2008)

VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language. - Jan Smans; Bart Jacobs 002; Frank Piessens (FMOODS, 2008)

A programming model for concurrent object-oriented programs. - Bart Jacobs 002; Frank Piessens; Jan Smans; K. Rustan M. Leino; Wolfram Schulte (ACM Trans. Program. Lang. Syst., 2008)

Security Monitor Inlining for Multithreaded Java. - Mads Dam; Bart Jacobs 002; Andreas Lundblad; Frank Piessens (ECOOP, 2009)

Failboxes: Provably Safe Exception Handling. - Bart Jacobs 002; Frank Piessens (ECOOP, 2009)

Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. - Jan Smans; Bart Jacobs 002; Frank Piessens (ECOOP, 2009)

Instruction-level countermeasures against stack-based buffer overflow attacks. - Francesco Gadaleta; Yves Younan; Bart Jacobs 002; Wouter Joosen; Erik De Neve; Nils Beosier (VDTS@EuroSys, 2009)

A Machine Checked Soundness Proof for an Intermediate Verification Language. - Frédéric Vogels; Bart Jacobs 002; Frank Piessens (SOFSEM, 2009)

A Quick Tour of the VeriFast Program Verifier. - Bart Jacobs 002; Jan Smans; Frank Piessens (APLAS, 2010)

Heap-Dependent Expressions in Separation Logic. - Jan Smans; Bart Jacobs 002; Frank Piessens (FMOODS/FORTE, 2010)

A machine-checked soundness proof for an efficient verification condition generator. - Frédéric Vogels; Bart Jacobs 002; Frank Piessens (SAC, 2010)

Automatic verification of Java programs with dynamic frames. - Jan Smans; Bart Jacobs 002; Frank Piessens; Wolfram Schulte (Formal Aspects Comput., 2010)

Provably correct inline monitoring for multithreaded Java-like programs. - Mads Dam; Bart Jacobs 002; Andreas Lundblad; Frank Piessens (J. Comput. Secur., 2010)

Verification of Unloadable Modules. - Bart Jacobs 002; Jan Smans; Frank Piessens (FM, 2011)

The 1st Verified Software Competition: Experience Report. - Vladimir Klebanov; Peter Müller 001; Natarajan Shankar; Gary T. Leavens; Valentin Wüstholz; Eyad Alkassar; Rob Arthan; Derek Bronish; Rod Chapman; Ernie Cohen; Mark A. Hillebrand; Bart Jacobs 002; et al. (FM, 2011)

Annotation Inference for Separation Logic Based Verifiers. - Frédéric Vogels; Bart Jacobs 002; Frank Piessens; Jan Smans (FMOODS/FORTE, 2011)

VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. - Bart Jacobs 002; Jan Smans; Pieter Philippaerts; Frédéric Vogels; Willem Penninckx; Frank Piessens (NASA Formal Methods, 2011)

Expressive modular fine-grained concurrency specification. - Bart Jacobs 002; Frank Piessens (POPL, 2011)

The Belgian Electronic Identity Card: a Verification Case Study. - Pieter Philippaerts; Frédéric Vogels; Jan Smans; Bart Jacobs 002; Frank Piessens (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Special Section on Formal Techniques for Java-like Programs. - Frank Piessens; Bart Jacobs 002; Gary T. Leavens (J. Object Technol., 2011)

Secure Compilation to Modern Processors. - Pieter Agten; Raoul Strackx; Bart Jacobs 002; Frank Piessens (CSF, 2012)

Subobject-Oriented Programming. - Marko van Dooren; Dave Clarke 001; Bart Jacobs 002 (FMCO, 2012)

Sound Formal Verification of Linux's USB BP Keyboard Driver. - Willem Penninckx; Jan Tobias Mühlberg; Jan Smans; Bart Jacobs 002; Frank Piessens (NASA Formal Methods, 2012)

Implicit dynamic frames. - Jan Smans; Bart Jacobs 002; Frank Piessens (ACM Trans. Program. Lang. Syst., 2012)

Sound Symbolic Linking in the Presence of Preprocessing. - Gijs Vanspauwen; Bart Jacobs 002 (SEFM, 2013)

VeriFast for Java: A Tutorial. - Jan Smans; Bart Jacobs 002; Frank Piessens (Aliasing in Object-Oriented Programming, 2013)

ICE: a passive, high-speed, state-continuity scheme. - Raoul Strackx; Bart Jacobs 002; Frank Piessens (ACSAC, 2014)

Modular type checking of anchored exception declarations. - Marko van Dooren; Bart Jacobs 002; Wouter Joosen (Sci. Comput. Program., 2014)

Software verification with VeriFast: Industrial case studies. - Pieter Philippaerts; Jan Tobias Mühlberg; Willem Penninckx; Jan Smans; Bart Jacobs 002; Frank Piessens (Sci. Comput. Program., 2014)

Provably live exception handling. - Bart Jacobs 002 (FTfJP@ECOOP, 2015)

Modular Termination Verification. - Bart Jacobs 002; Dragan Bosnacki; Ruurd Kuiper 001 (ECOOP, 2015)

Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. - Willem Penninckx; Bart Jacobs 002; Frank Piessens (ESOP, 2015)

Towards Modular Verification of Threaded Concurrent Executable Code Generated from DSL Models. - Dragan Bosnacki; Mark van den Brand; Joost Gabriels; Bart Jacobs 002; Ruurd Kuiper 001; Sybren Roede; Anton Wijs; Dan Zhang 002 (FACS, 2015)

First Steps Towards Cumulative Inductive Types in CIC. - Amin Timany; Bart Jacobs 002 (ICTAC, 2015)

Sound Modular Verification of C Code Executing in an Unverified Context. - Pieter Agten; Bart Jacobs 002; Frank Piessens (POPL, 2015)

Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications. - Gijs Vanspauwen; Bart Jacobs 002 (SEFM, 2015)

Featherweight VeriFast. - Frédéric Vogels; Bart Jacobs 002; Frank Piessens (Log. Methods Comput. Sci., 2015)

Security monitor inlining and certification for multithreaded Java. - Mads Dam; Bart Jacobs 002; Andreas Lundblad; Frank Piessens (Math. Struct. Comput. Sci., 2015)

Solving the VerifyThis 2012 challenges with VeriFast. - Bart Jacobs 002; Jan Smans; Frank Piessens (Int. J. Softw. Tools Technol. Transf., 2015)

Secure Compilation to Protected Module Architectures. - Marco Patrignani; Pieter Agten; Raoul Strackx; Bart Jacobs 002; Dave Clarke 001; Frank Piessens (ACM Trans. Program. Lang. Syst., 2015)

Partial Solutions to VerifyThis 2016 Challenges 2 and 3 with VeriFast. - Bart Jacobs 002 (FTfJP@ECOOP, 2016)

One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast. - Mahmoud Mohsen; Bart Jacobs 002 (FMICS-AVoCS, 2016)

Modular Verification of Termination and Execution Time Bounds Using Separation Logic. - Jafar Hamin; Bart Jacobs 002 (IRI, 2016)

Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations. - Dan Zhang 002; Dragan Bosnacki; Mark van den Brand; Cornelis Huizing; Bart Jacobs 002; Ruurd Kuiper 001; Anton Wijs (MODELSWARD (Revised Selected Papers), 2016)

Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code. - Dan Zhang 002; Dragan Bosnacki; Mark van den Brand; Cornelis Huizing; Ruurd Kuiper 001; Bart Jacobs 002; Anton Wijs (MODELSWARD, 2016)

Dependency Safety for Java: Implementing Failboxes. - Dragan Bosnacki; Mark van den Brand; Philippe Denissen; Cornelis Huizing; Bart Jacobs 002; Ruurd Kuiper 001; Anton Wijs; Maciej Wilkowski; Dan Zhang 002 (PPPJ, 2016)

Category Theory in Coq 8.5. - Amin Timany; Bart Jacobs 002 (FSCD, 2016)

Deadlock-Free Monitors. - Jafar Hamin; Bart Jacobs 002 (ESOP, 2018)

Modular Termination Verification of Single-Threaded and Multithreaded Programs. - Bart Jacobs 002; Dragan Bosnacki; Ruurd Kuiper 001 (ACM Trans. Program. Lang. Syst., 2018)

Transferring Obligations Through Synchronizations. - Jafar Hamin; Bart Jacobs 002 (ECOOP, 2019)

Specifying I/O using abstract nested hoare triples in separation logic. - Willem Penninckx; Amin Timany; Bart Jacobs 002 (FTfJP@ECOOP, 2019)

Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming. - Tuur Benoit; Bart Jacobs 002 (IFM, 2019)

Abstract I/O Specification. - Willem Penninckx; Amin Timany; Bart Jacobs 002 (CoRR, 2019)

Dependency safety for Java - Implementing and testing failboxes. - Dan Zhang 002; Dragan Bosnacki; Mark van den Brand; Cornelis Huizing; Bart Jacobs 002; Ruurd Kuiper 001; Anton Wijs (Sci. Comput. Program., 2019)

SμV - The Security MicroVisor: A Formally-Verified Software-Based Security Architecture for the Internet of Things. - Mahmoud Ammar; Bruno Crispo; Bart Jacobs 002; Danny Hughes 001; Wilfried Daniels (IEEE Trans. Dependable Secur. Comput., 2019)

A separation logic to verify termination of busy-waiting for abrupt program exit. - Tobias Reinhard; Amin Timany; Bart Jacobs 002 (FTfJP@ECOOP, 2020)

Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs. - Bart Jacobs 002 (ISoLA (1), 2020)

A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report. - Tobias Reinhard; Amin Timany; Bart Jacobs 002 (CoRR, 2020)

Ghost Signals: Verifying Termination of Busy-Waiting. - Tobias Reinhard; Bart Jacobs 002 (CoRR, 2020)

The future is ours: prophecy variables in separation logic. - Ralf Jung 002; Rodolphe Lepigre; Gaurav Parthasarathy; Marianna Rapoport; Amin Timany; Derek Dreyer; Bart Jacobs 002 (Proc. ACM Program. Lang., 2020)

Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting. - Tobias Reinhard; Bart Jacobs 002 (CAV (2), 2021)

Certifying C program correctness with respect to CompCert with VeriFast. - Stefan Wils; Bart Jacobs 002 (CoRR, 2021)

Modular Formal Verification of Rust Programs with Unsafe Blocks. - Nima Rahimi Foroushaani; Bart Jacobs 002 (CoRR, 2022)

Verification of C++ Programs with VeriFast. - Niels Mommen; Bart Jacobs 002 (CoRR, 2022)

Modular termination verification with a higher-order concurrent separation logic (Intermediate report). - Justus Fasse; Bart Jacobs 002 (CoRR, 2022)

Verifying C++ Dynamic Binding. - Niels Mommen; Bart Jacobs 002 (FTfJP@ECOOP, 2023)

Completeness Thresholds for Memory Safety of Array Traversing Programs. - Tobias Reinhard; Justus Fasse; Bart Jacobs 002 (SOAP@PLDI, 2023)

Certifying C program correctness with respect to CH2O with VeriFast. - Stefan Wils; Bart Jacobs 002 (CoRR, 2023)

Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract). - Tobias Reinhard; Justus Fasse; Bart Jacobs 002 (CoRR, 2023)

Expressive modular verification of termination for busy-waiting programs. - Justus Fasse; Bart Jacobs 002 (CoRR, 2023)

An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (X)C20 memory consistency model. - Bart Jacobs 002; Justus Fasse (CoRR, 2025)

VeriFast's separation logic: a higher-order(ish) logic without laters for modular verification of fine-grained concurrent programs. - Bart Jacobs 002 (CoRR, 2025)