default search action
Bart Jacobs 0002
Person information
- affiliation: Katholieke Universiteit Leuven, Belgium
- not to be confused with: Bart Jacobs 0001
Other persons with the same name
- Bart Jacobs 0001
(aka: Bart P. F. Jacobs) — Radboud University Nijmegen, The Netherlands
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
- [c52]Niels Mommen
Verifying C++ Dynamic Binding. FTfJP@ECOOP 2023: 1-7 - [c51]Tobias Reinhard
Completeness Thresholds for Memory Safety of Array Traversing Programs. SOAP@PLDI 2023: 47-54 - [i14]Tobias Reinhard, Justus Fasse, Bart Jacobs:
Completeness Thresholds for Memory Safety of Array Traversing Programs. CoRR abs/2305.03606 (2023) - [i13]Niels Mommen, Bart Jacobs:
Verifying C++ dynamic binding. CoRR abs/2306.02073 (2023) - [i12]Stefan Wils, Bart Jacobs
Certifying C program correctness with respect to CH2O with VeriFast. CoRR abs/2308.15567 (2023) - [i11]Tobias Reinhard
Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract). CoRR abs/2309.09731 (2023) - [i10]Justus Fasse, Bart Jacobs:
Expressive modular verification of termination for busy-waiting programs. CoRR abs/2312.15379 (2023) - 2022
- [i9]Nima Rahimi Foroushaani, Bart Jacobs
Modular Formal Verification of Rust Programs with Unsafe Blocks. CoRR abs/2212.12976 (2022) - [i8]Niels Mommen
Verification of C++ Programs with VeriFast. CoRR abs/2212.13754 (2022) - [i7]Justus Fasse, Bart Jacobs:
Modular termination verification with a higher-order concurrent separation logic (Intermediate report). CoRR abs/2212.14126 (2022) - 2021
- [c50]Tobias Reinhard
Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting. CAV (2) 2021: 27-50 - [i6]Stefan Wils, Bart Jacobs:
Certifying C program correctness with respect to CompCert with VeriFast. CoRR abs/2110.11034 (2021) - 2020
- [j20]Ralf Jung
The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang. 4(POPL): 45:1-45:32 (2020) - [c49]Tobias Reinhard
A separation logic to verify termination of busy-waiting for abrupt program exit. FTfJP@ECOOP 2020: 26-32 - [c48]Bart Jacobs
Modular Verification of Liveness Properties of the I/O Behavior of Imperative Programs. ISoLA (1) 2020: 509-524 - [i5]Tobias Reinhard
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report. CoRR abs/2007.10215 (2020) - [i4]Tobias Reinhard
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit. CoRR abs/2010.07800 (2020) - [i3]Tobias Reinhard
Ghost Signals: Verifying Termination of Busy-Waiting. CoRR abs/2010.11762 (2020)
2010 – 2019
- 2019
- [j19]Dan Zhang, Dragan Bosnacki, Mark van den Brand
Dependency safety for Java - Implementing and testing failboxes. Sci. Comput. Program. 184 (2019) - [j18]Mahmoud Ammar
SμV - The Security MicroVisor: A Formally-Verified Software-Based Security Architecture for the Internet of Things. IEEE Trans. Dependable Secur. Comput. 16(5): 885-901 (2019) - [c47]Willem Penninckx, Amin Timany
Specifying I/O using abstract nested hoare triples in separation logic. FTfJP@ECOOP 2019: 5:1-5:7 - [c46]Jafar Hamin
Transferring Obligations Through Synchronizations. ECOOP 2019: 19:1-19:58 - [c45]Tuur Benoit, Bart Jacobs
Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming. IFM 2019: 46-64 - [i2]Willem Penninckx, Amin Timany
Abstract I/O Specification. CoRR abs/1901.10541 (2019) - 2018
- [j17]Bart Jacobs
Modular Termination Verification of Single-Threaded and Multithreaded Programs. ACM Trans. Program. Lang. Syst. 40(3): 12:1-12:59 (2018) - [c44]Jafar Hamin
Deadlock-Free Monitors. ESOP 2018: 415-441 - 2016
- [c43]Bart Jacobs:
Partial Solutions to VerifyThis 2016 Challenges 2 and 3 with VeriFast. FTfJP@ECOOP 2016: 7 - [c42]Mahmoud Mohsen, Bart Jacobs
One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast. FMICS-AVoCS 2016: 56-64 - [c41]Jafar Hamin, Bart Jacobs
Modular Verification of Termination and Execution Time Bounds Using Separation Logic. IRI 2016: 110-117 - [c40]Dan Zhang, Dragan Bosnacki, Mark van den Brand
Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations. MODELSWARD (Revised Selected Papers) 2016: 249-273 - [c39]Dan Zhang, Dragan Bosnacki, Mark van den Brand
Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code. MODELSWARD 2016: 578-588 - [c38]Dragan Bosnacki, Mark van den Brand
Dependency Safety for Java: Implementing Failboxes. PPPJ 2016: 15:1-15:6 - [c37]Amin Timany
Category Theory in Coq 8.5. FSCD 2016: 30:1-30:18 - 2015
- [j16]Frédéric Vogels, Bart Jacobs
Featherweight VeriFast. Log. Methods Comput. Sci. 11(3) (2015) - [j15]Mads Dam, Bart Jacobs
Security monitor inlining and certification for multithreaded Java. Math. Struct. Comput. Sci. 25(3): 528-565 (2015) - [j14]Bart Jacobs
Solving the VerifyThis 2012 challenges with VeriFast. Int. J. Softw. Tools Technol. Transf. 17(6): 659-676 (2015) - [j13]Marco Patrignani
Secure Compilation to Protected Module Architectures. ACM Trans. Program. Lang. Syst. 37(2): 6:1-6:50 (2015) - [c36]Bart Jacobs
Provably live exception handling. FTfJP@ECOOP 2015: 7:1-7:4 - [c35]Bart Jacobs
Modular Termination Verification. ECOOP 2015: 664-688 - [c34]Willem Penninckx, Bart Jacobs
Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. ESOP 2015: 158-182 - [c33]Dragan Bosnacki, Mark van den Brand
Towards Modular Verification of Threaded Concurrent Executable Code Generated from DSL Models. FACS 2015: 141-160 - [c32]Amin Timany
First Steps Towards Cumulative Inductive Types in CIC. ICTAC 2015: 608-617 - [c31]Pieter Agten, Bart Jacobs
Sound Modular Verification of C Code Executing in an Unverified Context. POPL 2015: 581-594 - [c30]Gijs Vanspauwen, Bart Jacobs
Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications. SEFM 2015: 53-68 - [i1]Amin Timany, Bart Jacobs:
Category Theory in Coq 8.5. CoRR abs/1505.06430 (2015) - 2014
- [j12]Pieter Philippaerts
Software verification with VeriFast: Industrial case studies. Sci. Comput. Program. 82: 77-97 (2014) - [j11]Marko van Dooren, Bart Jacobs
Modular type checking of anchored exception declarations. Sci. Comput. Program. 87: 44-61 (2014) - [c29]Raoul Strackx, Bart Jacobs
ICE: a passive, high-speed, state-continuity scheme. ACSAC 2014: 106-115 - [e1]Nils Anders Danielsson, Bart Jacobs:
Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, PLPV 2014, January 21, 2014, San Diego, California, USA, Co-located with POPL '14. ACM 2014, ISBN 978-1-4503-2567-7 [contents] - 2013
- [c28]Gijs Vanspauwen, Bart Jacobs
Sound Symbolic Linking in the Presence of Preprocessing. SEFM 2013: 122-136 - [p1]Jan Smans, Bart Jacobs
VeriFast for Java: A Tutorial. Aliasing in Object-Oriented Programming 2013: 407-442 - 2012
- [j10]Jan Smans, Bart Jacobs
Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1): 2:1-2:58 (2012) - [c27]Pieter Agten, Raoul Strackx, Bart Jacobs
Secure Compilation to Modern Processors. CSF 2012: 171-185 - [c26]Marko van Dooren, Dave Clarke, Bart Jacobs
Subobject-Oriented Programming. FMCO 2012: 38-82 - [c25]Willem Penninckx, Jan Tobias Mühlberg
Sound Formal Verification of Linux's USB BP Keyboard Driver. NASA Formal Methods 2012: 210-215 - 2011
- [j9]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) - [j8]Frank Piessens, Bart Jacobs
Special Section on Formal Techniques for Java-like Programs. J. Object Technol. 10 (2011) - [c24]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
The 1st Verified Software Competition: Experience Report. FM 2011: 154-168 - [c23]Bart Jacobs
Verification of Unloadable Modules. FM 2011: 402-416 - [c22]Frédéric Vogels, Bart Jacobs
Annotation Inference for Separation Logic Based Verifiers. FMOODS/FORTE 2011: 319-333 - [c21]Bart Jacobs
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. NASA Formal Methods 2011: 41-55 - [c20]Bart Jacobs
Expressive modular fine-grained concurrency specification. POPL 2011: 271-282 - 2010
- [j7]Jan Smans, Bart Jacobs
Automatic verification of Java programs with dynamic frames. Formal Aspects Comput. 22(3-4): 423-457 (2010) - [j6]Mads Dam, Bart Jacobs
Provably correct inline monitoring for multithreaded Java-like programs. J. Comput. Secur. 18(1): 37-59 (2010) - [c19]Bart Jacobs
A Quick Tour of the VeriFast Program Verifier. APLAS 2010: 304-311 - [c18]Jan Smans, Bart Jacobs
Heap-Dependent Expressions in Separation Logic. FMOODS/FORTE 2010: 170-185 - [c17]Frédéric Vogels, Bart Jacobs
A machine-checked soundness proof for an efficient verification condition generator. SAC 2010: 2517-2522
2000 – 2009
- 2009
- [c16]Jan Smans, Bart Jacobs
Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. ECOOP 2009: 148-172 - [c15]Bart Jacobs
Failboxes: Provably Safe Exception Handling. ECOOP 2009: 470-494 - [c14]Mads Dam, Bart Jacobs
Security Monitor Inlining for Multithreaded Java. ECOOP 2009: 546-569 - [c13]Francesco Gadaleta, Yves Younan, Bart Jacobs
Instruction-level countermeasures against stack-based buffer overflow attacks. VDTS@EuroSys 2009: 7-12 - [c12]Frédéric Vogels, Bart Jacobs
A Machine Checked Soundness Proof for an Intermediate Verification Language. SOFSEM 2009: 570-581 - 2008
- [j5]Bart Jacobs
A programming model for concurrent object-oriented programs. ACM Trans. Program. Lang. Syst. 31(1): 1:1-1:48 (2008) - [c11]Jan Smans, Bart Jacobs
An Automatic Verifier for Java-Like Programs Based on Dynamic Frames. FASE 2008: 261-275 - [c10]Jan Smans, Bart Jacobs
VeriCool: An Automatic Verifier for a Concurrent Object-Oriented Language. FMOODS 2008: 220-239 - 2007
- [j4]Bart Jacobs, Frank Piessens:
Inspector Methods for State Abstraction. J. Object Technol. 6(5): 55-75 (2007) - [c9]Bart Jacobs, Peter Müller, Frank Piessens:
Sound reasoning about unchecked exceptions. SEFM 2007: 113-122 - 2006
- [j3]Jan Smans, Bart Jacobs
Static Verification of Code Access Security Policy Compliance of .NET Applications. J. Object Technol. 5(3): 35-58 (2006) - [c8]Bart Jacobs
A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. ICFEM 2006: 420-439 - [c7]Bart Jacobs
VC generation for functional behavior and non-interference of iterators. SAVCBS@FSE 2006: 67-70 - [c6]Bart Jacobs
A Simple Sequential Reasoning Approach for Sound Modular Verification of Mainstream Multithreaded Programs. TV@FLoC 2006: 23-47 - 2005
- [c5]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: 364-387 - [c4]Bart Jacobs
Safe Concurrency for Aggregate Objects with Invariants. SEFM 2005: 137-147 - [c3]Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs
The Spec# Programming System: Challenges and Directions. VSTTE 2005: 144-152 - 2004
- [j2]Frank Piessens, Bart Jacobs
Support for Metadata-driven Selection of Run-time Services in .NET is Promising but Immature. J. Object Technol. 3(2): 27-35 (2004) - [c2]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: 125-130 - [c1]Lieven Desmet, Bart Jacobs, Frank Piessens, Wouter Joosen:
Threat Modelling for Web Services Based Web Applications. Communications and Multimedia Security 2004: 131-144 - 2003
- [j1]Frank Piessens, Bart Jacobs
Software security: experiments on the .NET common language run-time and the shared source common language infrastructure. IEE Proc. Softw. 150(5): 303-307 (2003)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-07-03 21:35 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: