IT (Articles in internationally reviewed academic journals)

Jacobs B., Smans J., Piessens F. (2015). Solving the VerifyThis 2012 challenges with VeriFast. International Journal on Software Tools for Technology Transfer, 17 (6), 659-676.

Dam M., Jacobs B., Lundblad A., Piessens F. (2015). Security monitor inlining and certification for multithreaded Java. Mathematical Structures in Computer Science, 25 (3), 528-565.

Patrignani M., Agten P., Strackx R., Jacobs B., Clarke D., Piessens F. (2015). Secure compilation to protected module architectures. ACM Transactions on Programming Languages and Systems, 37 (2), art.nr. 6, 6:1-6:50.

Vogels F., Jacobs B., Piessens F. (2015). Featherweight VeriFast. Logical Methods in Computer Science, 11 (3), art.nr. 19, 1-57.

Philippaerts P., Mühlberg J., Penninckx W., Smans J., Jacobs B., Piessens F. (2014). Software verification with VeriFast: Industrial case studies. Science of Computer Programming, 82 (1), art.nr. 6, 77-97.

van Dooren M., Jacobs B., Joosen W. (2014). Modular type checking of anchored exception declarations. Science of Computer Programming, 87, 44-61.

Smans J., Jacobs B., Piessens F. (2012). Implicit dynamic frames. ACM Transactions on Programming Languages and Systems, 34 (1), art.nr. 2.

Jacobs B., Piessens F. (2011). Expressive modular fine-grained concurrency specification. ACM SIGPLAN Notices, 46 (1), 271-282.

Dam M., Jacobs B., Lundblad A., Piessens F. (2010). Provably correct inline monitoring for multithreaded Java-like programs. Journal of Computer Security, 18 (1), 37-59.

Smans J., Jacobs B., Piessens F., Schulte W. (2010). Automatic verification of Java programs with dynamic frames. Formal Aspects of Computing, 22 (3-4), 423-457.

Jacobs B., Piessens F., Smans J., Leino K., Schulte W. (2008). A programming model for concurrent object-oriented programs. ACM transactions on programming languages and systems, 31 (1), art.nr. 1, 48 p..

Jacobs B., Piessens F. (2007). Inspector Methods for State Abstraction. Journal of Object Technology, 6 (5), 55-75.

Smans J., Jacobs B., Piessens F. (2006). Static Verification of Code Access Security Policy Compliance of .NET Applications. Journal of Object Technology, 5 (3), 35-58.

Barnett M., Chang B., DeLine R., Jacobs B., Leino K. (2006). Boogie: a modular reusable verifier for object-oriented programs. Lecture Notes in Computer Science, 4111, 364-387.

Piessens F., Jacobs B., Truyen E., Joosen W. (2004). Support for metadata-driven selection of run-time services in .NET is promising but immature. Journal of Object Technology, 3 (2), 27-35.

Piessens F., Jacobs B., Joosen W. (2003). Software security: experiments on the .NET common language run-time and the shared source common language infrastructure. IEE Proceedings - Software, 150 (05), 303-307.

IBe (Academic books, internationally recognised scientific publisher; as editor)

(2014). PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages Meets Program Verification. (Danielsson, N., Ed., Jacobs, B., Ed.). New York, NY, USA: ACM.

IHb (Article in academic book, internationally recognised scientific publisher)

Smans J., Jacobs B., Piessens F. (2013). VeriFast for Java: A tutorial. In: Clarke D., Wrigstad T., Noble J. (Eds.), bookseries: Lecture Notes in Computer Science, vol: 7850, Aliasing in Object-Oriented Programming, (pp. 407-442). Berlin: Springer-Verlag.

van Dooren M., Clarke D., Jacobs B. (2013). Subobject-oriented programming. In: Giachino E., Hähnle R., de Boer F., Bonsangue M. (Eds.), bookseries: Lecture Notes in Computer Science, vol: 7866, Formal Methods for Components and Objects, 11th International Symposium, FMCO 2012, Bertinoro, Italy, September 24-28, 2012, Revised Lectures, (pp. 38-82). Berlin Heidelberg: Springer.

Desmet L., Jacobs B., Piessens F., Joosen W. (2005). Threat modelling for web services based web applications. In: Chadwick D., Preneel B. (Eds.), Communications and Multimedia Security, (pp. 131-144).

Desmet L., Jacobs B., Piessens F., Joosen W. (2005). A generic architecture for web applications to support threat analysis of infrastructural components. In: Chadwick D., Preneel B. (Eds.), Communications and Multimedia Security, (pp. 125-130).

IC (Papers at international scientific conferences and symposia, published in full in proceedings)

Bosnacki D., van den Brand M., Gabriels J., Jacobs B., Kuiper R., Roede S., Wijs A., Zhang D. (2016). Towards modular verification of threaded concurrent executable code generated from DSL models. In Braga, C. (Ed.), Csaba Ölveczky, P. (Ed.), Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niterói, Brazil, October 14-16, 2015, Revised Selected Papers: Vol. 9539. Formal Aspects of Component Software. Niterói, Brazil, 14-16 October 2015 (pp. 141-160) Springer.

Jacobs B. (2016). Partial solutions to VerifyThis 2016 challenges 2 and 3 with VeriFast. In Klebanov, V. (Ed.), Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs. Workshop on Formal Techniques for Java-like Programs. Rome, Italy, 19 July 2016 (art.nr. 7) (pp. 7:1-7:6). New York, NY, USA: ACM.

Mohsen M., Jacobs B. (2016). One step towards automatic inference of formal specification using Automated VeriFast. In Beek, M. (Ed.), Gnesi, S. (Ed.), Knapp, A. (Ed.), Critical Systems: Formal Methods and Automated Verification. International Workshop on Formal Methods for Industrial Critical Systems, International Workshop on Automated Verification of Critical Systems. Pisa, Italy, Pisa, Italy, 26-28 September 201626-28 September 2016 (pp. 56-64). Gewerbestrasse 11, 6330 Cham, Switzerland: Springer International Publishing.

Timany A., Jacobs B. (2016). Category theory in Coq 8.5. Leibniz International Proceedings in Informatics: Vol. 52. Formal Structures for Computation and Deduction. Porto, Portugal, 22-26 June 2016 (pp. 30:1-30:18) Schloss Dagstuhl.

Vanspauwen G., Jacobs B. (2015). Verifying protocol implementations by augmenting existing cryptographic libraries with specifications. In Calinescu, R. (Ed.), Rumpe, B. (Ed.), Software Engineering and Formal Methods (13). Software Engineering and Formal Methods. York, UK, 7-11 September 2015 (pp. 53-68) Springer.

Penninckx W., Jacobs B., Piessens F. (2015). Sound, modular and compositional verification of the input/output behavior of programs. In Vitek, J. (Ed.), Programming Languages and Systems: Vol. 9032. European Symposium on Programming (ESOP 2015). London, UK, 14-16 April 2015 (pp. 158-182) Springer Berlin Heidelberg.

Agten P., Jacobs B., Piessens F. (2015). Sound modular verification of C code executing in an unverified context. Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015). POPL. Mumbai, India, 15-17 January 2015 (pp. 581-594) ACM.

Jacobs B. (2015). Provably live exception handling. In Monahan, R. (Ed.), Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015). Workshop on Formal Techniques for Java-like Programs. Prague, 7 July 2015 (art.nr. 7) (pp. 7:1-7:4). New York, NY, USA: ACM.

Jacobs B., Bosnacki D., Kuiper R. (2015). Modular termination verification. In Boyland, J. (Ed.), 29th European Conference on Object-Oriented Programming (ECOOP 2015): Vol. 37. European Conference on Object-Oriented Programming (ECOOP). Prague, 5-10 July 2015 (pp. 664-688). Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.

Timany A., Jacobs B. (2015). First Steps Towards Cumulative Inductive Types in CIC. In Leucker, M. (Ed.), Rueda, C. (Ed.), Valencia, F. (Ed.), Theoretical Aspects of Computing - ICTAC 2015: Vol. 9399. Theoretical Aspects of Computing - ICTAC 2015. Cali, Colombia, 29-31 October 2015 (pp. 608-617) Springer International Publishing.

Strackx R., Jacobs B., Piessens F. (2014). ICE: a passive, high-speed, state-continuity scheme. Proceedings of the 30th Annual Computer Security Applications Conference (ACSAC 2014). Annual Computer Security Applications Conference (ACSAC 2014). New Orleans, Louisiana, 8-12 December 2014 (pp. 106-115) ACM.

Vanspauwen G., Jacobs B. (2013). Sound symbolic linking in the presence of preprocessing. In Hierons, R. (Ed.), Merayo, M. (Ed.), Bravetti, M. (Ed.), Software Engineering and Formal Methods, 11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings. Software Engineering and Formal Methods. Madrid, Spain, 25-27 September 2013 (pp. 122-136) Springer Berlin Heidelberg.

Penninckx W., Mühlberg J., Smans J., Jacobs B., Piessens F. (2012). Sound formal verification of Linux's USB BP keyboard driver. In Goodloe, A. (Ed.), Person, S. (Ed.), NASA Formal Methods: Vol. 7226. NASA Formal Methods. Norfolk, Virginia, USA, 3-5 April 2012 (pp. 210-215) Springer.

Agten P., Strackx R., Jacobs B., Piessens F. (2012). Secure compilation to modern processors. In Kellenberger, P. (Ed.), 2012 IEEE 25th Computer Security Foundations Symposium (CSF 2012). Computer Security Foundations Symposium. Harvard University, Cambridge MA, USA, 25-27 June 2012 (pp. 171-185) IEEE.

Jacobs B., Smans J., Piessens F. (2011). Verification of unloadable modules. In Butler, M. (Ed.), Schulte, W. (Ed.), 17th International Symposium on Formal Methods (FM 2011): Vol. 6664. 17th International Symposium on Formal Methods (FM 2011). Limerick, Ireland, 20-24 June 2011 (pp. 402-416) Springer.

Jacobs B., Smans J., Philippaerts P., Vogels F., Penninckx W., Piessens F. (2011). VeriFast: A powerful, sound, predictable, fast verifier for C and Java. NASA Formal Methods: Vol. 6617. NASA Formal Methods (NFM 2011). Pasadena, USA, 18-20 April 2011 (pp. 41-55) Springer.

Philippaerts P., Vogels F., Smans J., Jacobs B., Piessens F. (2011). The Belgian electronic identity card: a verification case study. Proceedings of the International Workshop Automated Verification of Critical Systems (AVOCS'11). International Workshop Automated Verification of Critical Systems. Newcastle, 12-14 September 2011.

Klebanov V., Müller P., Natarajan S., Leavens G., Wüstholz V., Alkassar E., Arthan R., Bronish D., Chapman R., Cohen E., Hillebrand M., Jacobs B., Leino K., Monahan R., Piessens F., Polikarpova N., Ridge T., Smans J., Tobies S., Tuerk T., Ulbrich M., Weiss B. (2011). The 1st verified software competition: Experience report. In Butler, M. (Ed.), Schulte, W. (Ed.), 17th International Symposium on Formal Methods (FM 2011): Vol. 6664. 17th International Symposium on Formal Methods (FM 2011). Limerick, Ireland, 20-24 June 2011 (pp. 154-168) Springer.

Jacobs B., Piessens F. (2011). Expressive modular fine-grained concurrency specification. In Sagiv, M. (Ed.), Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2011). Principles of Programming Languages (POPL 2011). Austin, TX, USA, 26-28 January 2011 (pp. 271-282). New York, NY, USA: ACM.

Vogels F., Jacobs B., Piessens F., Smans J. (2011). Annotation inference for separation logic based verifiers. In Bruni, R. (Ed.), Dingel, J. (Ed.), Formal Techniques for Distributed Systems (FMOODS/FORTE 2011): Vol. 6722. FMOODS/FORTE 2011. Reykjavik, Iceland, 6-9 June 2011 (pp. 319-333) Springer.

Jacobs B., Smans J., Piessens F. (2010). VeriFast: Imperative Programs as Proofs. VSTTE workshop on Tools & Experiments. VSTTE workshop on Tools & Experiments. Edinburgh, Scotland, 19 August 2010.

Smans J., Jacobs B., Piessens F. (2010). Heap-dependent expressions in separation logic. In Zucca, E. (Ed.), Hatcliff, J. (Ed.), Formal Techniques for Distributed Systems: Vol. 6117. FMOODS/FORTE. Amsterdam, Netherlands, 7-9 June 2010 (pp. 170-185) Springer-Verlag.

Jacobs B., Smans J., Piessens F. (2010). A quick tour of the VeriFast program verifier. Programming Languages and Systems (APLAS 2010). Asian Symposium on Programming Languages and Systems. Shanghai, China, 28 November - 1 December 2010 (pp. 304-311) Springer-Verlag.

Vogels F., Jacobs B., Piessens F. (2010). A machine-checked soundness proof for an efficient verification condition generator. Symposium on Applied Computing 2010: Vol. 3. SAC. Sierre, Switzerland, 22-26 March 2010 (pp. 2517-2522) ACM.

Dam M., Jacobs B., Lundblad A., Piessens F. (2009). Security monitor inlining for multithreaded Java. In Drossopoulou, S. (Ed.), ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genova, Italy, July 6-10, 2009, Proceedings: Vol. 5653. ECOOP. Genova, 6-10 July 2009 (pp. 546-569). Berlin: Springer-Verlag.

Smans J., Jacobs B., Piessens F. (2009). Implicit dynamic frames: Combining dynamic frames and separation logic. In Drossopoulou, S. (Ed.), ECOOP 2009 - Object-oriented Programming, 23rd European Conference, Genova, Italy, July 6-10, 2009, Proceedings: Vol. 5653. European Conference on Object-oriented Programming (ECOOP). Genova, 6-10 July 2009 (pp. 148-172). Berlin: Springer-Verlag.

Jacobs B., Piessens F. (2009). Failboxes: Provably safe exception handling. In Drossopoulou, S. (Ed.), ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genova, Italy, July 6-10, 2009, Proceedings: Vol. 5653. ECOOP. Genova, 6-10 July 2009 (pp. 470-494). Berlin: Springer-Verlag.

Vogels F., Jacobs B., Piessens F. (2009). A machine checked soundness proof for an intermediate verification language. In Nielsen, M. (Ed.), Kucera, A. (Ed.), Milterson, P. (Ed.), Palamidessi, C. (Ed.), Tuma, P. (Ed.), Valencia, F. (Ed.), Lecture Notes in Computer Science: Vol. 5404. SOFSEM 2009. Špindlerův Mlýn, Czech Republic, 24-30 January 2009 (pp. 570-581) Springer.

Smans J., Jacobs B., Piessens F. (2008). VeriCool: An automatic verifier for a concurrent object-oriented language. Lecture Notes in Computer Science: Vol. 5051/2008. Formal Methods for Open Object-Based Distributed Systems. Oslo, Norway, 4-6 June, 2008 (pp. 220-239) Springer.

Smans J., Jacobs B., Piessens F. (2008). Implicit dynamic frames. In Huisman, M. (Ed.), Proceedings of the 10th ECOOP Workshop on Formal Techniques for Java-like Programs. Formal Techniques for Java-like Programs. Paphos, Cyphrus, 08 July 2008 (pp. 1-12).

Smans J., Jacobs B., Piessens F., Schulte W. (2008). An automatic verifier for Java-like programs based on dynamic frames. Lecture Notes in Computer Science: Vol. 4961. Fundamental Approaches to Software Engineering. Budapest, Hungary, March 29 - April 6 2008 (pp. 261-275) Springer.

Jacobs B., Müller P., Piessens F. (2007). Sound reasoning about unchecked exceptions. In Hinchey, M. (Ed.), Margaria, T. (Ed.), Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007). IEEE International Conference on Software Engineering and Formal Methods. London, UK, September 12-14, 2007 (pp. 113-122) IEEE Computer Society.

Jacobs B., Smans J., Piessens F., Schulte W. (2007). A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs. Electronic Notes in Theoretical Computer Science: Vol. 174 (9) (pp. 23-47).

Jacobs B., Piessens F. (2006). Verification of programs using inspector methods. In Zucca, E. (Ed.), Ancona, D. (Ed.), Proceedings of the Eighth Workshop on Formal Techniques for Java-like Programs. Eighth Workshop on Formal Techniques for Java-like Programs. Nantes, France, July 4, 2006 (pp. 1-22).

Jacobs B., Piessens F., Schulte W. (2006). VC generation for functional behavior and non-interference of iterators. In Aldrich, J. (Ed.), Proceedings of the 2006 conference on Specification and verification of component-based systems. Specificationand verification of component-based systems. Portland, Oregon, November 10-11, 2006 (pp. 67-70).

Jacobs B., Smans J., Piessens F., Schulte W. (2006). A statically verifiable programming model for concurrent object-oriented programs. In Liu, Z. (Ed.), He, J. (Ed.), Proceedings of the Eighth International Conference on Formal Engineering Methods (ICFEM2006). Eighth International Conference on Formal Engineering Methods. Macau, November 1-3, 2006 (pp. 420-439). Berlin / Heidelberg: Springer-Verlag.

Barnett M., DeLine R., Jacobs B., Fähndrich M., Leino K., Schulte W., Venter H. (2005). The Spec# programming system: challenges and directions. In Shankar, N. (Ed.), VSTTE Position Papers. Verified Software: Theories, Tools, Experiments. Zürich, Switzerland, October 10-13, 2005 (pp. 1-7).

Smans J., Jacobs B., Piessens F. (2005). Static verification of code access security policy compliance of .NET applications. In Skala, V. (Ed.), Nienaltowksi, P. (Ed.), Proceedings of the 3rd International Conference on .NET. .NET technologies 2005. Pilsen, Czech Republic, May 30 - June 1, 2005 (pp. 1-12).

Jacobs B., Leino K., Piessens F., Schulte W. (2005). Safe concurrency for aggregate objects with invariants. In Aichernig, B. (Ed.), Beckert, B. (Ed.), Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods. 3rd IEEE International Conference on Software Engineering and Formal Methods. Koblenz, Germany, September 7-9, 2005 (pp. 137-146). Los Alamitos, CA, USA: IEEE Computer Society.

Jacobs B., Meijer E., Piessens F., Schulte W. (2005). Iterators revisited: proof rules and implementation. In Logozzo, F. (Ed.), Proceedings of the 7th ECOOP Workshop on Formal Techniques for Java-like Programs. Formal Techniques for Java-like Programs. Glasgow, Scotland, July 26, 2005 (pp. 1-21).

Jacobs B., Leino K., Schulte W. (2004). Verification of multithreaded object-oriented programs with invariants. In Barnett, M. (Ed.), Edwards, S. (Ed.), Giannakopoulou, D. (Ed.), Leavens, G. (Ed.), Sharygina, N. (Ed.), SAVCBS 2004 specification and verification of component-based systems: workshop proceedings: Vol. 04-09. Third workshop on specification and verification of component-based systems. Newport Beach, CA, USA, October 31-November 1, 2004 (pp. 2-9).

IMa (Meeting abstracts, presented at international scientific conferences and symposia, published or not published in proceedings or journals)

Timany A., Jacobs B. (2016). The category-theoretic solution of recursive ultra-metric space equations. CoqPL. St. Petersburg, Florida, 23 January 2016.

Timany A., Jacobs B. (2016). Simple dependent polymorphic I/O effects. Hope. Nara, Japan, 18 September 2016.

Mohsen M., Jacobs B. (2016). Automated VeriFast: Supporting formal specification authoring through specification inference. Workshop on Tools for Automatic Program Analysis. Edinburgh, UK, 7 September 2016.

Timany A., Jacobs B. (2015). Category Theory in Coq 8.5. Coq Workshop.

Gadaleta F., Younan Y., Jacobs B., Joosen W., De Neve E., Beosier N. (2009). Instruction-level countermeasures against stack-based buffer overflow attacks. Eurosys. Nuremberg, 1-3 April 2009.

Jacobs B., Smans J., Piessens F. (2008). Verifying the Composite pattern using separation logic. Workshop on Specification and Verification of Component-Based Systems, Challenge Problem Track. Atlanta, GA, USA, 9-10 November 2008.

Schulte W., Jacobs B. (2006). Invited talk: A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs. First International Workshop on Thread Verification. Seattle, August 21-22, 2006.

Desmet L., Jacobs B., Piessens F., Schulte W., Smans J., Vanoverberghe D. (2006). Concern-specific annotation languages to support static detection of bugs in Java-like programs. International Symposium on Methods for Components and Objects. Amsterdam, November 7-10, 2006.

Jacobs B., Smans J., Piessens F., Schulte W. (2006). A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs. First International Workshop on Thread Verification. Seattle, August 21-22, 2006.

Jacobs B. (2005). Tutorial: The Spec# programming system: an overview. Formal Methods. Newcastle upon Tyne, United Kingdom, July 19, 2005.

Piessens F., Jacobs B., Joosen W. (2003). Teaching Software Security: Courseware and Projects on .NET and Rotor. Second Annual SSCLI Workshop. Redmond, Washington, USA, September 17-19, 2003.

Jacobs B., Piessens F., Truyen E., Joosen W. (2003). Selection of run-time services in .NET: there is room for improvement. ECOOP Workshop on .NET: The programmer's Perspective. Darmstadt, Germany, July 22, 2003.

Jacobs B., Piessens F., Bekaert P., Steegmans E. (2002). Whole-program specifications permit better abstraction and concurrent implementations. The 13th International Symposium on Software Reliability Engineering. Annapolis, Maryland, USA, November 12-15, 2002.

TH (Thesis)

Noorman J., Piessens, F. (sup.), Jacobs, B. (sup.) (2017). Sancus: A Low-Cost Security Architecture for Distributed IoT Applications on a Shared Infrastructure.

Agten P., Piessens, F. (sup.), Jacobs, B. (cosup.) (2015). Sound Modular Reasoning about Security Properties of Imperative Programs, 198 pp.

Vogels F., Piessens, F. (sup.), Jacobs, B. (sup.) (2012). Formalisation and Soundness of Static Verification Algorithms for Imperative Programs (Formalisatie en correctheid van statische verificatiealgoritmes voor imperatieve programma's), 482 pp.

Jacobs B., Piessens, F. (sup.), Steegmans, E. (cosup.) (2007). A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs (Een statisch verifieerbaar programmeermodel voor gelijktijdige objectgeoriënteerde programma's), 135 + vi pp.

IR (Internal report)

Vanspauwen G., Jacobs B. (2016). Verifying cryptographic protocols. Applying the symbolic model to cryptographic APIs for C. CW Reports, CW694, 66 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Hamin J., Jacobs B. (2016). Modular verification of termination and execution time bounds using separation logic. CW Reports, CW696, 8 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Timany A., Jacobs B. (2016). Category theory in Coq 8.5: Extended version. CW Reports, CW697, 26 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Jacobs B., Bosnacki D., Kuiper R. (2015). Modular termination verification: extended version. CW Reports, CW680, 32 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Timany A., Jacobs B. (2015). First steps towards cumulative inductive types in CIC: Extended version. CW Reports, CW684, 13 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Jacobs B. (2014). Verifying TSO programs. CW Reports, CW660, 18 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Agten P., Jacobs B., Piessens F. (2014). Sound modular verification of C code executing in an unverified context: extended version. CW Reports, CW676, 17 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Smans J., Vanoverberghe D., Devriese D., Jacobs B., Piessens F. (2014). Shared boxes: rely-guarantee reasoning in VeriFast. CW Reports, CW662, 19 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Penninckx W., Jacobs B., Piessens F. (2014). Modular, compositional and sound verification of the input/output behavior of programs. CW Reports, CW663, 15 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Strackx R., Jacobs B., Piessens F. (2014). ICE: A Passive, high-speed, state-continuity scheme (extended version). CW Reports, CW672, 17 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Timany A., Jacobs B. (2014). A local shape analysis based on separation logic: Detailed presentation and soundness proof. CW Reports, CW661, 35 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Fontaine A., Gadyatskaya O., Piessens F., Simplot-Ryl I., Mühlberg J., Massacci F., Phillipov A., Capelastegui P., Jacobs B., Philippaerts P. (2012). SecureChange public project deliverable D6.6: Development-time and on-device interplay, 97 pp.

Agten P., Strackx R., Jacobs B., Piessens F. (2012). Secure compilation to modern processors: extended version. CW Reports, CW619, 41 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Vogels F., Jacobs B., Piessens F. (2012). Featherweight VeriFast: Extended version. CW Reports, CW614, 78 pp. Leuven, Belgium: Department of Computer Science, KU Leuven.

Jacobs B., Smans J., Piessens F. (2011). Verification of unloadable C modules (Extended version). CW Reports, CW604, 22 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Smans J., Piessens F. (2010). Verification of imperative programs: The VeriFast approach. A draft course text. CW Reports, CW578, 34 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Piessens F. (2010). Expressive modular fine-grained concurrency specification (Extended version). CW Reports, CW590, 17 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Vogels F., Jacobs B., Piessens F. (2010). A machine-checked soundness proof for an efficient verification condition generator: technical report. CW Reports, CW568, 156 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Smans J., Piessens F. (2009). Verification of unloadable C modules - status report. CW Reports, CW567, 17 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Smans J., Piessens F. (2009). Verification of unloadable C modules - Soundness proof. CW Reports, CW570, 20 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Cuypers C., Jacobs B., Piessens F. (2009). Verification of data-race-freedom of a Java chat server with VeriFast. CW reports, CW550, 5 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Piessens F. (2009). Modular full functional specification and verification of lock-free data structures. CW Reports, CW551, 11 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Smans J., Jacobs B., Piessens F. (2009). Implicit dynamic frames: Combining dynamic frames and separation logic (soundness proof). CW Reports, CW542, 59 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Piessens F. (2009). Dynamic Owicki-Gries reasoning using ghost fields and fractional permissions. CW Reports, CW549, 2 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Piessens F. (2008). The VeriFast program verifier. CW Reports, CW520, 7 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Piessens F. (2008). Subsystems: provably safe exception handling (status report). CW Reports, CW516, 35 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Vogels F., Jacobs B., Piessens F. (2008). A machine checked soundness proof for an intermediate verification language: extended version. CW Reports, CW526, 52 pp. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Müller P., Piessens F. (2007). Sound reasoning about unchecked exceptions: soundness proof. CW Reports, CW494: Department of Computer Science, K.U.Leuven, Leuven, Belgium.

Jacobs B., Piessens F. (2007). Inspector methods for state abstraction: soundness proof. CW Reports, CW493: Department of Computer Science, K.U.Leuven, Leuven, Belgium.

Jacobs B., Piessens F., Schulte W. (2006). Safe Fine-Grained Locking for Aggregate Objects. CW Reports, CW444, 10 pp: K.U.Leuven, Department of Computer Science.

Jacobs B., Piessens F. (2005). Verifying programs using inspector methods for state abstraction. CW Reports, CW432, 21 pp: Department of Computer Science, K.U.Leuven, Leuven, Belgium.

Jacobs B., Leino K., Piessens F., Schulte W. (2005). Safe concurrency for aggregate objects with invariants: soundness proof, nr. MSR-TR-2005-85, 14 pp: Microsoft Research.

De Win B., Jacobs B., Joosen W., Neven G., Piessens F., Verhanneman T. (2005). Formal technologies for information and software security: An annotated bibliography. CW Reports, CW423. Leuven, Belgium: Department of Computer Science, K.U.Leuven.

Jacobs B., Piessens F. (2003). A $\pi$-Calculus Semantics of Java: The Full Definition. CW Reports, CW355, 25 pp: Department of Computer Science, K.U.Leuven, Leuven, Belgium.

DI (Misc.)

Vanspauwen G., Jacobs B. (2016). Verifying cryptographic protocols: a symbolic model for cryptographic APIs for C.

Piessens F., Jacobs B., Leavens G. (2011). Special section on Formal Techniques for Java-like Programs. Journal of Object Technology, 10.

This list is generated from Lirias and contains data from Lirias as it is entered and validated by the researcher.