Bart Jacobs - RankMe

94 papers A* 2A 9B 11C 3Misc 2Journal 40Unranked 25

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