default search action
Bart Jacobs 0002
- > Home > Persons > Bart Jacobs 0002
Publications
- 2023
- [c51]Tobias Reinhard, Justus Fasse, Bart Jacobs:
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) - [i11]Tobias Reinhard, Justus Fasse, Bart Jacobs:
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
- [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, Bart Jacobs:
Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting. CAV (2) 2021: 27-50 - 2020
- [j20]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): 45:1-45:32 (2020) - [c49]Tobias Reinhard, Amin Timany, Bart Jacobs:
A separation logic to verify termination of busy-waiting for abrupt program exit. FTfJP@ECOOP 2020: 26-32 - [i5]Tobias Reinhard, Amin Timany, Bart Jacobs:
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report. CoRR abs/2007.10215 (2020) - [i4]Tobias Reinhard, Amin Timany, Bart Jacobs:
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit. CoRR abs/2010.07800 (2020) - [i3]Tobias Reinhard, Bart Jacobs:
Ghost Signals: Verifying Termination of Busy-Waiting. CoRR abs/2010.11762 (2020) - 2019
- [j18]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): 885-901 (2019) - [c47]Willem Penninckx, Amin Timany, Bart Jacobs:
Specifying I/O using abstract nested hoare triples in separation logic. FTfJP@ECOOP 2019: 5:1-5:7 - [i2]Willem Penninckx, Amin Timany, Bart Jacobs:
Abstract I/O Specification. CoRR abs/1901.10541 (2019) - 2016
- [c37]Amin Timany, Bart Jacobs:
Category Theory in Coq 8.5. FSCD 2016: 30:1-30:18 - 2015
- [j16]Frédéric Vogels, Bart Jacobs, Frank Piessens:
Featherweight VeriFast. Log. Methods Comput. Sci. 11(3) (2015) - [j15]Mads Dam, Bart Jacobs, Andreas Lundblad, Frank Piessens:
Security monitor inlining and certification for multithreaded Java. Math. Struct. Comput. Sci. 25(3): 528-565 (2015) - [j14]Bart Jacobs, Jan Smans, Frank Piessens:
Solving the VerifyThis 2012 challenges with VeriFast. Int. J. Softw. Tools Technol. Transf. 17(6): 659-676 (2015) - [j13]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): 6:1-6:50 (2015) - [c34]Willem Penninckx, Bart Jacobs, Frank Piessens:
Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. ESOP 2015: 158-182 - [c32]Amin Timany, Bart Jacobs:
First Steps Towards Cumulative Inductive Types in CIC. ICTAC 2015: 608-617 - [c31]Pieter Agten, Bart Jacobs, Frank Piessens:
Sound Modular Verification of C Code Executing in an Unverified Context. POPL 2015: 581-594 - [i1]Amin Timany, Bart Jacobs:
Category Theory in Coq 8.5. CoRR abs/1505.06430 (2015) - 2014
- [j12]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: 77-97 (2014) - [j11]Marko van Dooren, Bart Jacobs, Wouter Joosen:
Modular type checking of anchored exception declarations. Sci. Comput. Program. 87: 44-61 (2014) - [c29]Raoul Strackx, Bart Jacobs, Frank Piessens:
ICE: a passive, high-speed, state-continuity scheme. ACSAC 2014: 106-115 - 2013
- [p1]Jan Smans, Bart Jacobs, Frank Piessens:
VeriFast for Java: A Tutorial. Aliasing in Object-Oriented Programming 2013: 407-442 - 2012
- [j10]Jan Smans, Bart Jacobs, Frank Piessens:
Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1): 2:1-2:58 (2012) - [c27]Pieter Agten, Raoul Strackx, Bart Jacobs, Frank Piessens:
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, Jan Smans, Bart Jacobs, Frank Piessens:
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, Gary T. Leavens:
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, 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: 154-168 - [c23]Bart Jacobs, Jan Smans, Frank Piessens:
Verification of Unloadable Modules. FM 2011: 402-416 - [c22]Frédéric Vogels, Bart Jacobs, Frank Piessens, Jan Smans:
Annotation Inference for Separation Logic Based Verifiers. FMOODS/FORTE 2011: 319-333 - [c21]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: 41-55 - [c20]Bart Jacobs, Frank Piessens:
Expressive modular fine-grained concurrency specification. POPL 2011: 271-282 - 2010
- [j7]Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte:
Automatic verification of Java programs with dynamic frames. Formal Aspects Comput. 22(3-4): 423-457 (2010) - [j6]Mads Dam, Bart Jacobs, Andreas Lundblad, Frank Piessens:
Provably correct inline monitoring for multithreaded Java-like programs. J. Comput. Secur. 18(1): 37-59 (2010) - [c19]Bart Jacobs, Jan Smans, Frank Piessens:
A Quick Tour of the VeriFast Program Verifier. APLAS 2010: 304-311 - [c18]Jan Smans, Bart Jacobs, Frank Piessens:
Heap-Dependent Expressions in Separation Logic. FMOODS/FORTE 2010: 170-185 - [c17]Frédéric Vogels, Bart Jacobs, Frank Piessens:
A machine-checked soundness proof for an efficient verification condition generator. SAC 2010: 2517-2522 - 2009
- [c16]Jan Smans, Bart Jacobs, Frank Piessens:
Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. ECOOP 2009: 148-172 - [c15]Bart Jacobs, Frank Piessens:
Failboxes: Provably Safe Exception Handling. ECOOP 2009: 470-494 - [c14]Mads Dam, Bart Jacobs, Andreas Lundblad, Frank Piessens:
Security Monitor Inlining for Multithreaded Java. ECOOP 2009: 546-569 - [c13]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: 7-12 - [c12]Frédéric Vogels, Bart Jacobs, Frank Piessens:
A Machine Checked Soundness Proof for an Intermediate Verification Language. SOFSEM 2009: 570-581 - 2008
- [j5]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): 1:1-1:48 (2008) - [c11]Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte:
An Automatic Verifier for Java-Like Programs Based on Dynamic Frames. FASE 2008: 261-275 - [c10]Jan Smans, Bart Jacobs, Frank Piessens:
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, Frank Piessens:
Static Verification of Code Access Security Policy Compliance of .NET Applications. J. Object Technol. 5(3): 35-58 (2006) - [c8]Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte:
A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. ICFEM 2006: 420-439 - [c7]Bart Jacobs, Frank Piessens, Wolfram Schulte:
VC generation for functional behavior and non-interference of iterators. SAVCBS@FSE 2006: 67-70 - [c6]Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte:
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, Frank Piessens, K. Rustan M. Leino, Wolfram Schulte:
Safe Concurrency for Aggregate Objects with Invariants. SEFM 2005: 137-147 - [c3]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: 144-152 - 2004
- [j2]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): 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, Wouter Joosen:
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)
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