Bart Jacobs

Publication Activity (10 Years)

Years Active: 2003-2023
Publications (10 Years): 33

Top Topics

Imperative Programs

Rewrite Systems

Formal Specification

Top Venues

Sci. Comput. Program.

Publications

Niels Mommen, Bart Jacobs
Verifying C++ Dynamic Binding. FTfJP@ECOOP (2023)
Stefan Wils, Bart Jacobs
Certifying C program correctness with respect to CH2O with VeriFast. CoRR (2023)
Tobias Reinhard, Justus Fasse, Bart Jacobs
Completeness Thresholds for Memory Safety of Array Traversing Programs. CoRR (2023)
Tobias Reinhard, Justus Fasse, Bart Jacobs
Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract). CoRR (2023)
Niels Mommen, Bart Jacobs
Verifying C++ dynamic binding. CoRR (2023)
Tobias Reinhard, Justus Fasse, Bart Jacobs
Completeness Thresholds for Memory Safety of Array Traversing Programs. SOAP@PLDI (2023)
Justus Fasse, Bart Jacobs
Expressive modular verification of termination for busy-waiting programs. CoRR (2023)
Justus Fasse, Bart Jacobs
Modular termination verification with a higher-order concurrent separation logic (Intermediate report). CoRR (2022)
Nima Rahimi Foroushaani, Bart Jacobs
Modular Formal Verification of Rust Programs with Unsafe Blocks. CoRR (2022)
Niels Mommen, Bart Jacobs
Verification of C++ Programs with VeriFast. CoRR (2022)
Stefan Wils, Bart Jacobs
Certifying C program correctness with respect to CompCert with VeriFast. CoRR (2021)
Tobias Reinhard, Bart Jacobs
Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting. CAV (2) (2021)
Bart Jacobs
Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs. ISoLA (1) (2020)
Tobias Reinhard, Amin Timany, Bart Jacobs
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report. CoRR (2020)
Tobias Reinhard, Amin Timany, Bart Jacobs
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit. CoRR (2020)
Tobias Reinhard, Bart Jacobs
Ghost Signals: Verifying Termination of Busy-Waiting. CoRR (2020)
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs
The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. 4 (POPL) (2020)
Tobias Reinhard, Amin Timany, Bart Jacobs
A separation logic to verify termination of busy-waiting for abrupt program exit. FTfJP@ECOOP (2020)
Tuur Benoit, Bart Jacobs
Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming. IFM (2019)
Mahmoud Ammar, Bruno Crispo, Bart Jacobs, Danny Hughes, Wilfried Daniels
SμV - The Security MicroVisor: A Formally-Verified Software-Based Security Architecture for the Internet of Things. IEEE Trans. Dependable Secur. Comput. 16 (5) (2019)
Dan Zhang, Dragan Bosnacki, Mark van den Brand, Cornelis Huizing, Bart Jacobs, Ruurd Kuiper, Anton Wijs
Dependency safety for Java - Implementing and testing failboxes. Sci. Comput. Program. 184 (2019)
Jafar Hamin, Bart Jacobs
Transferring Obligations Through Synchronizations. ECOOP (2019)
Willem Penninckx, Amin Timany, Bart Jacobs
Specifying I/O using abstract nested hoare triples in separation logic. FTfJP@ECOOP (2019)
Willem Penninckx, Amin Timany, Bart Jacobs
Abstract I/O Specification. CoRR (2019)
Bart Jacobs, Dragan Bosnacki, Ruurd Kuiper
Modular Termination Verification of Single-Threaded and Multithreaded Programs. ACM Trans. Program. Lang. Syst. 40 (3) (2018)
Jafar Hamin, Bart Jacobs
Deadlock-Free Monitors. ESOP (2018)
Amin Timany, Bart Jacobs
Category Theory in Coq 8.5. FSCD (2016)
Bart Jacobs
Partial Solutions to VerifyThis 2016 Challenges 2 and 3 with VeriFast. FTfJP@ECOOP (2016)
Dragan Bosnacki, Mark van den Brand, Philippe Denissen, Cornelis Huizing, Bart Jacobs, Ruurd Kuiper, Anton Wijs, Maciej Wilkowski, Dan Zhang
Dependency Safety for Java: Implementing Failboxes. PPPJ (2016)
Mahmoud Mohsen, Bart Jacobs
One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast. FMICS-AVoCS (2016)
Dan Zhang, Dragan Bosnacki, Mark van den Brand, Cornelis Huizing, Bart Jacobs, Ruurd Kuiper, Anton Wijs
Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations. MODELSWARD (Revised Selected Papers) (2016)
Jafar Hamin, Bart Jacobs
Modular Verification of Termination and Execution Time Bounds Using Separation Logic. IRI (2016)
Dan Zhang, Dragan Bosnacki, Mark van den Brand, Cornelis Huizing, Ruurd Kuiper, Bart Jacobs, Anton Wijs
Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code. MODELSWARD (2016)
Bart Jacobs, Jan Smans, Frank Piessens
Solving the VerifyThis 2012 challenges with VeriFast. Int. J. Softw. Tools Technol. Transf. 17 (6) (2015)
Pieter Agten, Bart Jacobs, Frank Piessens
Sound Modular Verification of C Code Executing in an Unverified Context. POPL (2015)
Mads Dam, Bart Jacobs, Andreas Lundblad, Frank Piessens
Security monitor inlining and certification for multithreaded Java. Math. Struct. Comput. Sci. 25 (3) (2015)
Gijs Vanspauwen, Bart Jacobs
Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications. SEFM (2015)
Bart Jacobs, Dragan Bosnacki, Ruurd Kuiper
Modular Termination Verification. ECOOP (2015)
Frédéric Vogels, Bart Jacobs, Frank Piessens
Featherweight VeriFast. Log. Methods Comput. Sci. 11 (3) (2015)
Dragan Bosnacki, Mark van den Brand, Joost Gabriels, Bart Jacobs, Ruurd Kuiper, Sybren Roede, Anton Wijs, Dan Zhang
Towards Modular Verification of Threaded Concurrent Executable Code Generated from DSL Models. FACS (2015)
Willem Penninckx, Bart Jacobs, Frank Piessens
Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. ESOP (2015)
Amin Timany, Bart Jacobs
First Steps Towards Cumulative Inductive Types in CIC. ICTAC (2015)
Bart Jacobs
Provably live exception handling. FTfJP@ECOOP (2015)
Amin Timany, Bart Jacobs
Category Theory in Coq 8.5. CoRR (2015)
Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, Frank Piessens
Secure Compilation to Protected Module Architectures. ACM Trans. Program. Lang. Syst. 37 (2) (2015)
Pieter Philippaerts, Jan Tobias Mühlberg, Willem Penninckx, Jan Smans, Bart Jacobs, Frank Piessens
Software verification with VeriFast: Industrial case studies. Sci. Comput. Program. 82 (2014)
Marko van Dooren, Bart Jacobs, Wouter Joosen
Modular type checking of anchored exception declarations. Sci. Comput. Program. 87 (2014)
Raoul Strackx, Bart Jacobs, Frank Piessens
ICE: a passive, high-speed, state-continuity scheme. ACSAC (2014)
Gijs Vanspauwen, Bart Jacobs
Sound Symbolic Linking in the Presence of Preprocessing. SEFM (2013)
Pieter Agten, Raoul Strackx, Bart Jacobs, Frank Piessens
Secure Compilation to Modern Processors. CSF (2012)
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 (2012)
Jan Smans, Bart Jacobs, Frank Piessens
Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34 (1) (2012)
Marko van Dooren, Dave Clarke, Bart Jacobs
Subobject-Oriented Programming. FMCO (2012)
Bart Jacobs, Frank Piessens
Expressive modular fine-grained concurrency specification. POPL (2011)
Bart Jacobs, Jan Smans, Frank Piessens
Verification of Unloadable Modules. FM (2011)
Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, Frank Piessens
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. NASA Formal Methods (2011)
Frédéric Vogels, Bart Jacobs, Frank Piessens, Jan Smans
Annotation Inference for Separation Logic Based Verifiers. FMOODS/FORTE (2011)
Pieter Philippaerts, Frédéric Vogels, Jan Smans, Bart Jacobs, Frank Piessens
The Belgian Electronic Identity Card: a Verification Case Study. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46 (2011)
Frank Piessens, Bart Jacobs, Gary T. Leavens
Special Section on Formal Techniques for Java-like Programs. J. Object Technol. 10 (2011)
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, 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ß
The 1st Verified Software Competition: Experience Report. FM (2011)
Bart Jacobs, Jan Smans, Frank Piessens
A Quick Tour of the VeriFast Program Verifier. APLAS (2010)
Jan Smans, Bart Jacobs, Frank Piessens
Heap-Dependent Expressions in Separation Logic. FMOODS/FORTE (2010)
Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte
Automatic verification of Java programs with dynamic frames. Formal Aspects Comput. 22 (3-4) (2010)
Frédéric Vogels, Bart Jacobs, Frank Piessens
A machine-checked soundness proof for an efficient verification condition generator. SAC (2010)
Mads Dam, Bart Jacobs, Andreas Lundblad, Frank Piessens
Provably correct inline monitoring for multithreaded Java-like programs. J. Comput. Secur. 18 (1) (2010)
Frédéric Vogels, Bart Jacobs, Frank Piessens
A Machine Checked Soundness Proof for an Intermediate Verification Language. SOFSEM (2009)
Mads Dam, Bart Jacobs, Andreas Lundblad, Frank Piessens
Security Monitor Inlining for Multithreaded Java. ECOOP (2009)
Jan Smans, Bart Jacobs, Frank Piessens
Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. ECOOP (2009)
Francesco Gadaleta, Yves Younan, Bart Jacobs, Wouter Joosen, Erik De Neve, Nils Beosier
Instruction-level countermeasures against stack-based buffer overflow attacks. VDTS@EuroSys (2009)
Bart Jacobs, Frank Piessens
Failboxes: Provably Safe Exception Handling. ECOOP (2009)
Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte
An Automatic Verifier for Java-Like Programs Based on Dynamic Frames. FASE (2008)
Jan Smans, Bart Jacobs, Frank Piessens
VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language. FMOODS (2008)
Bart Jacobs, Frank Piessens, Jan Smans, K. Rustan M. Leino, Wolfram Schulte
A programming model for concurrent object-oriented programs. ACM Trans. Program. Lang. Syst. 31 (1) (2008)
Bart Jacobs, Peter Müller, Frank Piessens
Sound reasoning about unchecked exceptions. SEFM (2007)
Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte
A Simple Sequential Reasoning Approach for Sound Modular Verification of Mainstream Multithreaded Programs. Electron. Notes Theor. Comput. Sci. 174 (9) (2007)
Bart Jacobs, Frank Piessens
Inspector Methods for State Abstraction. J. Object Technol. 6 (5) (2007)
Bart Jacobs, Frank Piessens, Wolfram Schulte
VC generation for functional behavior and non-interference of iterators. SAVCBS@FSE (2006)
Jan Smans, Bart Jacobs, Frank Piessens
Static Verification of Code Access Security Policy Compliance of .NET Applications. J. Object Technol. 5 (3) (2006)
Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte
A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. ICFEM (2006)
Bart Jacobs, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte
Safe Concurrency for Aggregate Objects with Invariants. SEFM (2005)
Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino
Boogie: A Modular Reusable Verifier for Object-Oriented Programs. FMCO (2005)
Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte, Herman Venter
The Spec# Programming System: Challenges and Directions. VSTTE (2005)
Frank Piessens, Bart Jacobs, Eddy Truyen, Wouter Joosen
Support for Metadata-driven Selection of Run-time Services in .NET is Promising but Immature. J. Object Technol. 3 (2) (2004)
Lieven Desmet, Bart Jacobs, Frank Piessens, Wouter Joosen
Threat Modelling for Web Services Based Web Applications. Communications and Multimedia Security (2004)
Lieven Desmet, Bart Jacobs, Frank Piessens, Wouter Joosen
A Generic Architecture for Web Applications to Support Threat Analysis of Infrastructural Components. Communications and Multimedia Security (2004)
Frank Piessens, Bart Jacobs, Wouter Joosen
Software security: experiments on the .NET common language run-time and the shared source common language infrastructure. IEE Proc. Softw. 150 (5) (2003)