Travelled to:1 × Austria
1 × Canada
1 × Czech Republic
1 × Estonia
1 × India
1 × Ireland
1 × Poland
1 × Portugal
1 × Spain
1 × Switzerland
1 × The Netherlands
1 × USA
2 × Germany
2 × Hungary
4 × Italy
4 × United Kingdom
Collaborated with:F.Piessens G.Vanspauwen ∅ M.Huisman J.Smans J.v.d.Berg I.Hasuo W.Schulte E.Poll T.F.Melham P.Müller D.Bošnački R.Kuiper W.Penninckx B.Westerbaan B.Westerbaan P.Agten F.Vogels A.Sokolova T.Uustalu K.R.M.Leino R.Atkey N.Ghani P.Johann M.Dam A.Lundblad U.Hensel H.Tews M.v.Berkum V.Klebanov N.Shankar G.T.Leavens V.Wüstholz E.Alkassar R.Arthan D.Bronish R.Chapman E.Cohen M.A.Hillebrand R.Monahan N.Polikarpova T.Ridge S.Tobies T.Tuerk M.Ulbrich B.Weiß
Talks about:java (7) verif (6) sound (5) logic (5) modular (4) program (3) concurr (3) verifi (3) except (3) frame (3)
Person: Bart Jacobs
DBLP: Jacobs:Bart
Contributed to:
2015
2015
2015
2015
201520132012
20112011
20102009
20082008
20072007200520012001
200120001998
19981996
1993Wrote 27 papers:
- ECOOP-2015-JacobsBK #composition #termination #verification
- Modular Termination Verification (BJ, DB, RK), pp. 664–688.
- ESOP-2015-Penninckx0P #behaviour #composition #source code #verification
- Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs (WP, BJ, FP), pp. 158–182.
- FoSSaCS-2015-JacobsWW #set
- States of Convex Sets (BJ, BW, BW), pp. 87–101.
- POPL-2015-Agten0P #c #composition #verification
- Sound Modular Verification of C Code Executing in an Unverified Context (PA, BJ, FP), pp. 581–594.
- SEFM-2015-Vanspauwen0 #encryption #implementation #library #protocol #specification #verification
- Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications (GV, BJ), pp. 53–68.
- SEFM-2013-VanspauwenJ #preprocessor
- Sound Symbolic Linking in the Presence of Preprocessing (GV, BJ), pp. 122–136.
- FoSSaCS-2012-AtkeyGJJ #induction
- Fibrational Induction Meets Effects (RA, NG, BJ, PJ), pp. 42–57.
- FM-2011-JacobsSP #verification
- Verification of Unloadable Modules (BJ, JS, FP), pp. 402–416.
- FM-2011-KlebanovMSLWAABCCHJLMPPRSTTUW #case study #contest #experience
- The 1st Verified Software Competition: Experience Report (VK, PM, NS, GTL, VW, EA, RA, DB, RC, EC, MAH, BJ, KRML, RM, FP, NP, TR, JS, ST, TT, MU, BW), pp. 154–168.
- POPL-2011-JacobsP #composition #concurrent #fine-grained #specification
- Expressive modular fine-grained concurrency specification (BJ, FP), pp. 271–282.
- SAC-2010-VogelsJP #generative #performance #proving #verification
- A machine-checked soundness proof for an efficient verification condition generator (FV, BJ, FP), pp. 2517–2522.
- ECOOP-2009-DamJLP #java #monitoring #parallel #security #thread
- Security Monitor Inlining for Multithreaded Java (MD, BJ, AL, FP), pp. 546–569.
- ECOOP-2009-JacobsP #exception #named
- Failboxes: Provably Safe Exception Handling (BJ, FP), pp. 470–494.
- ECOOP-2009-SmansJP #logic
- Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic (JS, BJ, FP), pp. 148–172.
- FASE-2008-SmansJPS #automation #java #source code #verification
- An Automatic Verifier for Java-Like Programs Based on Dynamic Frames (JS, BJ, FP, WS), pp. 261–275.
- FoSSaCS-2008-HasuoJS #algebra #concurrent
- The Microcosm Principle and Concurrency in Coalgebra (IH, BJ, AS), pp. 246–260.
- ICALP-2007-HasuoJU #category theory
- Categorical Views on Computations on Trees (IH, BJ, TU), pp. 619–630.
- SEFM-2007-JacobsMP #exception #reasoning
- Sound reasoning about unchecked exceptions (BJ, PM, FP), pp. 113–122.
- SEFM-2005-JacobsPLS #concurrent #invariant
- Safe Concurrency for Aggregate Objects with Invariants (BJ, FP, KRML, WS), pp. 137–147.
- ESOP-2001-Jacobs #exception #formal method #java
- A Formalisation of Java’s Exception Mechanism (BJ), pp. 284–301.
- FASE-2001-JacobsP #java #logic #ml #modelling
- A Logic for the Java Modeling Language JML (BJ, EP), pp. 284–299.
- TACAS-2001-BergJ #compilation #java #ml
- The LOOP Compiler for Java and JML (JvdB, BJ), pp. 299–312.
- FASE-2000-HuismanJ #hoare #java #logic #termination #verification
- Java Program Verification via a Hoare Logic with Abrupt Termination (MH, BJ), pp. 284–303.
- ESOP-1998-HenselHJT #logic #modelling #object-oriented #tool support
- Reasonong about Classess in Object-Oriented Languages: Logical Models and Tools (UH, MH, BJ, HT), pp. 105–121.
- OOPSLA-1998-JacobsBHB #java #reasoning
- Reasoning about Java Classes (BJ, JvdB, MH, MvB), pp. 329–340.
- ECOOP-1996-Jacobs #inheritance
- Inheritance and Cofree Constructions (BJ), pp. 210–231.
- TLCA-1993-JacobsM #dependent type #higher-order #logic #type system
- Translating Dependent Type Theory into Higher Order Logic (BJ, TFM), pp. 209–229.