Publications Marieke Huisman

Last updated: August 23, 2024

For publications since August 1, 2008, see also the official University of Twente publication server.
For publications before August 1, 2008, see also the printer server from the Everest team at INRIA Sophia Antipolis.

2024

L. Armborst, P. Bos, L.B. van den Haak, M. Huisman, R. Rubbens, Ö. Sakar, P. Tasche. The VerCors Verifier: A Progress Report. CAV (2) 2024: 3-18. [link, pdf]
S. Lathouwers and M. Huisman. Survey of annotation generators for deductive verifiers. J. Syst. Softw. 211: 111972 [link]
L.B. van den Haak, A. Wijs, M. Huisman, M. van den Brand. HaliVer: Deductive Verification and Scheduling Languages Join Forces. TACAS (3) 2024: 71-89 [link]
D. van Oorschot, M. Huisman, Ö. Sakar. First Steps towards Deductive Verification of LLVM IR. FASE 2024: 290-303 [link]
E. Wittingen, M. Huisman and Ö. Şakar. Deductive verification of SYCL in VerCors. In Software Engineering and Formal Methods (SEFM 2024), to appear.
P. Tasche, P. Herber and M. Huisman. Automated Invariant Generation for Efficient Deductive Reasoning about Embedded Systems. In Software Engineering and Formal Methods (SEFM 2024), to appear.
R. Rubbens, P. van den Bos and M. Huisman. VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory. In integrated Formal Methods (iFM 2024), to appear.
L.B. van den Haak, A. Wijs, M. Huisman and M. van den Brand. Verifying a Radio Telescope Pipeline using HaliVer: Solving Nonlinear and Quantifier Challenges. In 29th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2024), to appear.
P. Tasche, R. E. Monti, S.E. Drerup, P. Blohm, P. Herber and M. Huisman. Deductive Verification of Parameterized Embedded Systems modeled in SystemC. In VMCAI 2024, Springer. [link]
L. Armborst and M. Huisman. Using Horn solvers to generate memory access permissions for deductive verification – a preliminary report. In Horn Clauses for Verification and Synthesis (HCVS), 2024. [link]
S. Johanns and M. Huisman. Replication of a Deductive Synthesizer for Programs with Pointers. In Third Workshop on Reproducibility and Replication of Research Results (RRRR 2024) [link]
J.F. Groote, M. Huisman. Formal Methods for Industrial Critical Systems. Int. J. Softw. Tools Technol. Transf. 26(2): 127-129. [link]

2023

M. Huisman and A. Wijs. Concise Guide to Software Verification - From Model Checking to Annotation Checking, Texts in Computer Science, Springer. [link]
L. Armborst, S. Lathouwers and M. Huisman. Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation. In International Conference on Integrated Formal Methods, LNCS, Springer, pages 153-171. [link, pdf]
W. Ahrendt, G. Ernst, P. Herber, M. Huisman, R.E. Monti, M. Ulbrich and A. Weigl. The VerifyThis Collaborative Long-term Challenge Series. In TOOLympics 2023. To appear.
J. Starink, M. Huisman, A. Peter, A. Continella. Understanding and Measuring Inter-Process Code Injection in Windows Malware. In EAI SecureComm.
S. Bliudze, P. van den Bos, M. Huisman, R.B. Rubbens, L. Safina Verified JavaBIP: Deductive & Runtime Verification of JavaBIP Models. FASE 2023. [link]
M. Huisman. A reply: On the need for program contracts. Journal of cross-disciplinary research in computational law 1 (3), pages 19-20. [link]
M. Huisman, A. Ravara. Formal Techniques for Distributed Objects, Components, and Systems - 43rd IFIP WG 6.1 International Conference, FORTE 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings. Lecture Notes in Computer Science 13910, Springer. [link]
M. Huisman, C.S. Pasareanu, N. Zhan. Introduction to the Special Section on FM 2021. Formal Aspects Comput. 35(2): 6:1-6:2 [link]
M. Huisman, C.S. Pasareanu, N. Zhan. Preface for the formal methods in system design special issue on ‘Formal Methods 2021’. Formal Methods in System Design, 1-2. [link]

2022

M. Safari, M. Huisman. Formal verification of parallel prefix sum and stream compaction algorithms in CUDA. Theor. Comput. Sci. 912: 81-99. [link]
Ö. Sakar, M. Safari, M. Huisman, A. Wijs. Alpinist: An Annotation-Aware GPU Program Optimizer. TACAS (2) 2022: 332-352. [link]
P. van den Bos, M. Huisman. The Integration of Testing and Program Verification - A Position Paper. A Journey from Process Algebra via Timed Automata to Model Learning 2022: 524-538 [link]
M. Huisman, R.E. Monti. Teaching Design by Contract Using Snap! The Logic of Software. A Tasting Menu of Formal Methods 2022: 243-263 [link]
S. Lathouwers, M. Huisman: Formal Specifications Investigated: A Classification and Analysis of Annotations for Deductive Verifiers. FormaliSE@ICSE 2022: 69-79 [link]
W. Ahrendt, P. Herber, M. Huisman, M. Ulbrich SpecifyThis - Bridging Gaps Between Program Specification Paradigms. ISoLA (1) 2022: 3-6 [link]
M. Huisman, C. Seceleanu. Verification and Validation of Concurrent and Distributed Heterogeneous Systems (Track Summary). ISoLA (1) 2022: 417-421 [link]
R.E. Monti, R.B. Rubbens, M. Huisman. On Deductive Verification of an Industrial Concurrent Software Component with VerCors. ISoLA (1) 2022: 517-534 [link]
J.F. Groote, M. Huisman. Formal Methods for Industrial Critical Systems - 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, Proceedings. Lecture Notes in Computer Science 13487, Springer 2022, ISBN 978-3-031-15007-4 [link]

2021

R.B. Rubbens, S. Lathouwers, M. Huisman. Modular Transformation of Java Exceptions Modulo Errors. FMICS 2021: 67-84. [link]
D. Beyer, M. Huisman. TOOLympics I: Competition on software testing. Int. J. Softw. Tools Technol. Transf. 23(6): 829-832 [link]
D. Beyer, M. Huisman. TOOLympics II: competitions on formal methods. Int. J. Softw. Tools Technol. Transf. 23(6): 879-881 [link]
M. Huisman, C.S. Pasareanu, N. Zhan. Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. Lecture Notes in Computer Science 13047, Springer 2021, ISBN 978-3-030-90869-0 [link]
M. Safari, W. Oortwijn, M. Huisman. Automated Verification of the Parallel Bellman--Ford Algorithm. In SAS 2021: 346 - 358. [link]
S. Monteiro, E. Sokolovas, E. Wittingen, T. van Dijk, M. Huisman. IntelliJML: a JML plugin for IntelliJ IDEA. In FTfJP 2021. [link]
L. Armborst, M. Huisman. Permission-Based Verification of Red-Black Trees and Their Merging. FormaliSE@ICSE 2021: 111-123. [link]
M. Huisman, R.E. Monti. Teaching Design by Contract using Snap! In SEENG@ICSE 2021. [link]
S. Blom, S. Darabi, M. Huisman, M. Safari. Correct program parallelisations. STTT. [link]
C. Dross, C.A. Furia, M. Huisman, R. Monahan and P. Müller. VerifyThis 2019: a program verification competition. STTT. [link]
D. Beyer, M. Huisman, F. Kordon, B. Steffen. TOOLympics II: competitions on formal methods. STTT. [link]
D. Beyer, M. Huisman. TOOLympics I: Competition on software testing. STTT. [link]

2020

M. Safari, M. Huisman. A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms. In iFM 2020. [link]
N. van Huizen, M. Huisman, S. Lathouwers, A. Schaafstal, and M. Stoelinga. Alice and Eve: a celebration of women in computer science. In SEFI 2020. [pdf]
W. Oortwijn, D. Gurov and M. Huisman. An Abstraction Technique for Verifying Shared-Memory Concurrency. Applied Sciences 10, 11, 3928. [link]
L. van den Haak, A. Wijs, M. van den Brand and M. Huisman. Formal Methods for GPGPU Programming: Is the Demand Met? In iFM 2020. [link]
M. Safari, M. Huisman. Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms. In ICTAC 2020. [link]
H. Mulder, M. Huisman and S. Joosten. Improving Performance of the VerCors Program Verifier. In 20 Years of KeY. [link]
M. Huisman and R.E. Monti. On the Industrial Application of Critical Software Verification with VerCors. In Isola 2020. [link]
D. Beyer and M. Huisman. Selected and Extended Papers from TACAS 2018: Preface. Journal of automated reasoning, 64(7). [link]
M. Huisman, R.E. Monti, M. Ulbrich and A. Weigl. The VerifyThis Collaborative Long Term Challenge. In 20 Years of KeY. [link]
D. Beyer and M. Huisman. Tools for the construction and analysis of systems A special issue for TACAS 2018. STTT 22(6). [link]
M. Huisman and A. Wijs. Towards verified construction of correct and optimised GPU software. In FTfJP 2020. [link]
M. Huisman and C. Seceleanu. Verification and Validation of Concurrent and Distributed Systems (Track Summary). In Isola 2020. [link]
M. Safari, W. Oortwijn, S. Joosten and M. Huisman. Formal Verification of Parallel Prefix Sum. In NFM 2020. [link]
W. Oortwijn, M. Huisman, S. Joosten and J.C. van de Pol. Automated Verification of Parallel Nested DFS. In TACAS 2020, pages 247-265. [link]
W. Oortwijn, D. Gurov and M. Huisman. Practical Abstractions for Automated Verification of Shared-Memory Concurrency. In VMCAI 2020, pages 401-425. [link]
S. Lathouwers, M.H. Everts and M. Huisman. Verifying Sanitizer Correctness through Black-Box Learning: A Symbolic Finite Transducer Approach. In ICISSP 2020, pages 784-795. [link]
M. Huisman, D. Gurov and A. Malkis. Formal Methods: From Academia to Industrial Practice. A Travel Guide. CoRR abs/2002.07279, 2020. [link]

2019

W. Oortwijn and M. Huisman. Practical Abstractions for Automated Verification of Message Passing Concurrency. In IFM 2019, pages 399-417 (best paper award). [link]
W. Oortwijn and M. Huisman. Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System. In IFM 2019, pages 418-436. [link]
R. Hähnle and M. Huisman. Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. In Computing and Software Science 2019, pages 345-373. [link]
J.J. Honig, M.H. Everts and M. Huisman. Practical Mutation Testing for Smart Contracts. In DPM/CBT@ESORICS 2019, pages 289-303. [link]
E. Bartocci, D. Beyer, P.E. Black, G. Fedyukovich, H. Garavel, A. Hartmanns, M. Huisman, F. Kordon, J. Nagele, M. Sighireanu, B. Steffen, M. Suda, G. Sutcliffe, T. Weber and A. Yamada. TOOLympics 2019: An Overview of Competitions in Formal Methods. In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics (TACAS volume 3), LNCS 11429, Springer, pages 3-24. [link]
G. Ernst, M. Huisman, W. Mostowski, M. Ulbrich. VerifyThis - Verification Competition with a Human Factor. In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics (TACAS volume 3), LNCS 11429, Springer, pages 176-195. [link]
D. Beyer, M. Huisman, F. Kordon, B. Steffen (editors). Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. LNCS 11429, Springer. [link]
M. Huisman, R. Monahan, P. Müller, A. Paskevich and G. Ernst. VerifyThis2018: A Program Verification Competition. Research Report Université Paris-Saclay (hal-01981937). [link]

2018

M. Huisman, S. Joosten. Towards Reliable Concurrent Software. In Principled Software Development, pages 129-146, Springer. [link]
W. Ahrendt, M. Huisman, G. Reger, K.Y. Rozier. A Broader View on Verification: From Static to Runtime and Back (Track Summary). In ISoLA 2018, Volume 2, LNCS 11245, pages 3- 7, Springer. [link]
M. Felderer, D. Gurov, M. Huisman, B. Lisper, Rupert Schlick. Formal Methods in Industrial Practice - Bridging the Gap (Track Summary). In ISoLA 2018, Volume 4, LNCS 11247, pages 77-81, Springer. [link]
M. Huisman. On Models and Code - A Unified Approach to Support Large-Scale Deductive Program Verification. In ISoLA 2018, Volume 1, LNCS 11244, pages 111-118, Springer. [link]
M. Huisman, S. Blom, S. Darabi and M. Safari. Program Correctness by Transformation. In ISOLA 2018, Volume 1, LNCS 11244, pages 365-380, Springer. [link]
S. Joosten and M. Huisman. Static Code Verification Through Process Models. In ISoLA 2018, Volume 3, LNCS 11246, pages 343-354, Springer. [link]
M. Huisman and J. Rubin. Software quality tools and techniques presented in FASE'17. STTT 20(6), pages 611-613, Springer. [link]
J. Boerman, M. Huisman and S. Joosten. Reasoning about JML: Differences between KeY and OpenJML. In iFM 2018, LNCS 11023, pages 30-46, Springer 2018. [pdf]
P. de Carvalho Gomes, D. Gurov, M. Huisman and C. Artho. Specification and verification of synchronization with condition variables. Sci. Comput. Program. 163: 174-189 (2018). [link|pdf]
M. Huisman, A.L. Varbanescu, B. van Werkhoven and A.J. Wijs. An overview of GPU Computing Research in the Netherlands: Results from the NIRICT GPGPU Reconnaissance workshop. Whitepaper. [pdf]
S. Joosten, W. Oortwijn, M. Safari and M. Huisman. An Exercise in Verifying Sequential Programs with VerCors. In FTfJP 2018. [pdf]
D. Beyer and M. Huisman. Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I and II. Lecture Notes in Computer Science 10805 and 10806, Springer 2018.
M. Huisman. Software Reliability for Everyone. Inaugural lecture. [pdf]
A. Amighi, M. Huisman and S. Blom. Verification of Shared-Reading Synchronisers. In 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid) 2018.

2017

M. Huisman, R. Monahan, W. Mostowski, P. Müller and M. Ulbrich. VerifyThis 2017: A Program Verification Competition. Karlsruhe Reports in Informatics: 2017 - 10. ISSN: 2190-4782. [link]
R. Hähnle and M. Huisman. 24 Challenges in Deductive Software Verification. In Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE) 2017. EPiC Series in Computing, volume 51. [link]
M. Huisman, T. Noll and M. Tatsuta. Analysis and Verification of Pointer Programs (NII Shonan Meeting 2017-14). [pdf]
W. Oortwijn M. Huisman S. Blom, M. Zaharieva-Stojanovski and D. Gurov. An Abstraction Technique for Describing Concurrent Program Behaviour. In 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) 2017. [pdf]
M. Huisman. A verification technique for deterministic parallel programs. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP) 2017, paper 3. [link]
M. Huisman. Verification of Concurrent Software with VerCors. In Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT) 2017, page 2. [link]
S. Blom, S. Darabi, M. Huisman and W. Oortwijn. The VerCors Tool Set: Verification of Parallel and Concurrent Software. In integreated Formal Methods (iFM) 2017. LNCS 10510, pp. 102 - 110 [link]
S. Darabi, S. Blom and M. Huisman. A Verification Technique for Deterministic Parallel Programs. Nasa Formal Methods (NFM) 2017. LNCS 10227, Springer, pp. 247 - 264. An extended version is available as CTIT technical report; no. TR-CTIT-17-01.
M. Huisman and J. Rubin (editors). Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Lecture Notes in Computer Science 10202, Springer 2017.
T. M. Ngo and M. Huisman. Complexity and information flow analysis for multi-threaded programs. The European Physical Journal Special Topics, volume 226, issue 10, pp. 2375-2392. [link]

2016

M. Huisman, W. Ahrendt, D. Grahl, and M. Hentschel. Formal Specification with the Java Modeling Language. In Deductive Software Verification - The KeY Book. LNCS, Volume 10001, Springer, pages 193-241. [link]
D. Gurov, K. Havelund, M. Huisman, and R. Monahan. Static and Runtime Verification, Competitors or Friends? (Track Summary). In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. LNCS, volume 9952, pages 397-401, Springer. [link]
P. Gomes, D. Gurov and M. Huisman. Specification and Verification of Synchronization with Condition Variables. In FTSCS 2016.[.pdf]
M. Huisman, V. Klebanov, R. Monahan and M. Tautschnig. VerifyThis 2015. International Journal on Software Tools for Technology Transfer, 19(6), 763 - 771. [link]
M. Huisman, H. Bos, S. Brinkkemper, A. van Deursen, J.F. Groote, P. Lago, J.C. van de Pol and E. Visser. Software that meets its Intent. In Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. ISoLA 2016. LNCS, Volume 9953, Springer, pages 609-625 [.pdf]
M. Huisman, R. Monahan, P. Müller, E. Poll. VerifyThis 2016: A Program Verification Competition. Technical Report TR-CTIT-16-07, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625 [.pdf]
E. Ábrahám and M. Huisman (editors). Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. Lecture Notes in Computer Science 9681, Springer 2016, ISBN 978-3-319-33692-3. [link]
M. Huisman and J.C. van de Pol. Preface - Special issue on Automated Verification of Critical Systems (AVoCS'14). In Science of Computer Programming, [link].
L. Wevers, M. Huisman and M. van Keulen. Lazy Evaluation for Concurrent OLTP and Bulk Transactions. In Proceedings of the 18th International Database Engineering & Applications Symposium (IDEAS 2016). [.pdf]
W. Oortwijn, S. Blom, and M. Huisman. Future-based Static Analysis of Message Passing Programs. In Places 2016. [link]
A. Amighi, S. Blom, and M. Huisman. VerCors: a Layered Approach to Practical Verification of Concurrent Software. In PDP 2016. [.pdf]
A. Amighi, P. de Carvalho Gomes, D. Gurov and M. Huisman. Provably correct control flow graphs from Java bytecode programs with exceptions. STTT 18(6), pp. 653-684. [.pdf]

2015

L. Wevers, M. Hofstra, M. Tammens, M. Huisman and M. van Keulen. Analysis of the Blocking Behaviour of Schema Transformations in Relational Database Systems. In ABDIS 2015. [.pdf]
L. Wevers, M. Hofstra, M. Tammens, M. Huisman and M. van Keulen. A Benchmark for Online Non-Blocking Schema Transformations. In DATA 2015. [.pdf]
A. Amighi, S. Darabi, S. Blom, and M. Huisman. Specification and Verification of Atomic Operations in GPGPU Programs. In SEFM 2015. [.pdf]
S. Blom, M. Huisman, and M. Zaharieva-Stojanovski. History-based Verification of Functional Behaviour of Concurrent Programs. In SEFM 2015. [.pdf] An earlier version appeared as CTIT Technical Report Series; no. TR-CTIT-15-02.
M. Huisman and W. Mostowski. A Symbolic Approach to Permission Accounting for Concurrent Reasoning. In ISPDC 2015. [.pdf, online version ]
Jorne Kandziora, M. Huisman, Christoph Bockisch, and M. Zaharieva-Stojanovski. Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML. In FTfJP 2015. [.pdf]
S. Soleimanifard, D. Gurov and M. Huisman. Procedure-Modular Specification and Verification of Temporal Safety Properties. Software and Systems Modeling. [.pdf]
S. Blom, S. Darabi, and M. Huisman. Verification of Loop Parallelisations. In FASE 2015. [.pdf]
S. Blom, and M. Huisman. Witnessing the Elimination of Magic Wands. STTT. [.pdf]
A. Amighi, C. Haack, M. Huisman, and C. Hurlin. Permission-Based Separation Logic for Multithreaded Java Programs. LMCS, volume 11, issue 1, paper 2.
M. Huisman, V. Klebanov, R. Monahan. VerifyThis 2012 - A Program Verification Competition. STTT 17(6). [pdf]

2014

A. Amighi, S. Blom, and M. Huisman. Resource protection using atomics: patterns and verification. In APLAS 2014, LNCS, Springer.
M. Huisman, W. Ahrendt, D. Bruns, and M. Hentschel. Formal Specification with JML. Karlsruhe Reports in Informatics; 2014, 10. To appear as a chapter in the forthcoming book on the KeY system. [.pdf]
A. Amighi, S. Blom, S. Darabi, M. Huisman, W. Mostowski, and M. Zaharieva-Stojanovski. Verification of Concurrent Systems with VerCors. In 14th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software Models, LNCS 8483, pages 172-216, Springer, 2014. [.pdf]
M. Zaharieva-Stojanovski, M. Huisman, and S. Blom. Verifying Functional Behaviour of Concurrent Programs. In Formal Techniques for Java-like Programs 2014.
S. Blom, M. Huisman, and M. Mihelcic. Specification and Verification of GPGPU Programs. Science of Computer Programming. [link]
S. Blom, and M. Huisman. The VerCors Tool Set for Verification of Concurrent Programs. In Formal Methods 2014.
M. Zaharieva-Stojanovski, and M. Huisman. Verifying Class Invariants in Concurrent Programs. In FASE 2014, Springer. An earlier version appeared as CTIT Technical Report TR-CTIT-14-01.
T.M. Ngo, M. Stoelinga and M. Huisman. Effective Verification of Confidentiality for Multi-threaded Programs, Journal of Computer Security 22, pages 269 - 300.
M. Huisman. SCP special issue on Bytecode 2012 - Preface, Science of Computer Programming, volume 92, part A.
S. Blom, S. Darabi, and M. Huisman. Verifying Parallel Loops with Separation Logic. In Places 2014.
A. Amighi, S. Blom, M. Huisman, W. Mostowski, and M. Zaharieva-Stojanovski. Formal specifications for Java's synchronisation classes. In 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, pages 725-733, IEEE Computer Society. [.pdf]
T.M. Ngo, and M. Huisman. Quantitative Security Analysis for Programs with Low Input and Noisy Output. ESSOS 2014, pp. 77-94. Lecture Notes in Computer Science 8364. Springer Verlag.

2013

S. Blom, J.R. Kiniry and M. Huisman. How Do Developers Use APIs? A Case Study in Concurrency. In International Conference on Engineering of Complex Computer Systems. [.pdf]
A. Amighi, S. Blom, and M. Huisman. Resource protection using atomics: patterns and verifications. Technical Report TR-CTIT-13-10, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625. [.pdf]
A. Amighi, S. Blom, and M. Huisman. W. Mostowski, and M. Zaharieva-Stojanovski. Formal specifications for Java’s synchronisation classes. Technical Report TR-CTIT-13-18, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625. [.pdf]
S. Blom, and M. Huisman. Witnessing the Elimination of Magic Wands. Technical Report TR-CTIT-13-22, Centre for Telematics and Information Technology, University of Twente , Enschede . ISSN 1381-3625. [.pdf]
S. Blom, M. Huisman, and M. Mihelcic. Specification and verification of GPGPU programs. Technical Report TR-CTIT-13-21, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625. [.pdf]
L. Wevers, M. Huisman and A. de Keijzer. Parallel transaction processing in functional languages, towards practical functional databases. Technical Report TR-CTIT-13-06, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625. [.pdf]
D. Gurov and M. Huisman. Reducing Behavioural to Structural Properties of Programs with Procedures. Theoretical Computer Science, volume 480, pages 69 - 103. [.pdf]
T.M. Ngo, M. Stoelinga and M. Huisman. Confidentiality for Probabilistic Multi-threaded Programs and Its Verification. In International Symposium on Engineering Secure Software and Systems (ESSoS 2013). LNCS, Springer. [.pdf]
T.M. Ngo, and M. Huisman. Quantitative Security Analysis for Multi-threaded Programs. In Quantitative Aspects of Programming Languages and Systems (QAPL 2013). EPTCS, volume 117.
M. Huisman and M. Mihelcic. Specification and Verification of GPGPU programs using Permission-based Separation logic. In Bytecode 2013. Also appeared as Technical Report TR-CTIT-13-12, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625. [.pdf]

2012

A. Amighi, P. de Carvalho Gomes, D. Gurov and M. Huisman. Sound Control-Flow Graph Extraction for Java programs with Exceptions. In Software Engineering and Formal Methods (SEFM 2012). LNCS 7504, pages 33 - 47, Springer. [.pdf]
M. Zaharieva-Stojanovski, M. Huisman and S. Blom. A History of BlockingQueues. In proceedings of Formal Languages and Analysis of Contract-Oriented Software (Flacos 2012), EPTCS 94, pages 31 - 35, 2012. [.pdf]
M. Huisman, V. Klebanov, R. Monahan. On the Organisation of Program Verification Competitions. In proceedings of 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012). CEUR Workshop Proceedings series, volume 873. [.pdf]
T. Bormer, M. Brockschmidt, D. Distefano, G. Ernst, J.-C. Filliâtre, R. Grigore, M. Huisman V. Klebanov, C. Marché, R. Monahan, W. Mostowski, N. Polikarpova, C. Scheben, G. Schellhorn, B. Tofan, J. Tschannen, M. Ulbrich. The COST IC0701 Verification Competition 2011. In proceedings of 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOos 2011). LNCS 7421, pages 3-21, Springer. [.pdf]
M. Huisman and T.M. Ngo. Scheduler-specific Confidentiality for Multi-threaded Programs and Its logic-based Verification. In proceedings of Formal Verification of Object-Oriented Systems (FoVeOos 2011). LNCS 7421, pages 178 - 195, Springer. [.pdf]
A. Amighi, S. Blom, M. Huisman, M. Zaharieva-Stojanovski. The VerCors Project. Setting Up Basecamp. In proceedings of Programming Languages meets Program Verification (PLPV 2012). ACM Digital Library. [.pdf]

2011

A. Amighi, P. de Carvalho Gomes and M. Huisman. Provably Correct Control-Flow Graphs from Java programs with Exceptions. In pre-proceedings of Formal Verification of Object-Oriented Systems (FoVeOos 2011).
M. Huisman and T.M. Ngo. Scheduler-specific Confidentiality for Multi-threaded Programs and Its logic-based Verification. In pre-proceedings of Formal Verification of Object-Oriented Systems (FoVeOos 2011). Subsumed by the version in the final proceedings.
M. Huisman and T.M. Ngo. Scheduler-related Confidentiality for Multi-threaded Programs. Accepted for presentation at SecCo 2011. A longer version is available as Technical Report TR-CTIT-11-22, Centre for Telematics and Information Technology, University of Twente, Enschede. [.pdf]
S. Soleimanifard, D. Gurov and M. Huisman. ProMoVer: Modular Verification of Temporal Safety Properties. In Proceedings of Software Engineering and Formal Methods (SEFM 2011). LNCS 7041, pages 366-381, Springer. [.pdf]
H. Rebelo, R. Coelho, R. Lima, Gary T. Leavens, M. Huisman, A. Mota and F. Castor. On the Interplay of Exception Handling and Design by Contract: An Aspect-Oriented Recovery Approach. In Formal Techniques for Java-like Programs (FTfJP) 2011. ACM Digital Library. [.pdf]
M. Huisman and H.-C. Blondeel. Model-checking Secure Information Flow for Multi-Threaded Programs. In Proceedings of Theory of Security and Applications (Tosca) 2011. LNCS 6993, pages 148 - 165 , Springer. [.pdf]
C. Haack, M. Huisman, and C. Hurlin. Permission-Based Separation Logic for Multithreaded Java Programs. In Newsletter of the NVTI, issue 15, 2011. [.pdf]

2010

M. Huisman and D. Gurov. CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties. In Proceedings of Formal Verification of Object-Oriented Software (FoVeOOS) 2010. LNCS 6528, pages 107 - 121, Springer. [.pdf]
S. Soleimanifard, D. Gurov and M. Huisman. Procedure-Modular Verification of Control Flow Safety Properties. In Formal Techniques for Java-like Programs (FTfJP) 2010, ACM Digital Library. [.pdf]

2009

M. Huisman. On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker. In Formal Techniques for Java-like Programs (FTfJP) 2009. [.pdf].
J. Chrzaszcz, M. Huisman, A. Schubert. BML and related tools. In Software Technologies Concertation on Formal Methods for Components and Objects (FMCO 2008). LNCS 5751, pp. 278 - 297, Springer. [.pdf].
M. Huisman and A. Tamalet. A Formal Connection between Security Automata and JML Annotations. In Fundamental Approaches to Sofware Engineering (FASE) 2009. LNCS 5503, pp. 340-354, Springer. (PVS source files) [.pdf].
D. Gurov and M. Huisman. Reducing Behavioural to Structural Properties of Programs with Procedures. In Proceedings of: VMCAI'09 Lecture Notes in Computer Science, vol. 5403, pp. 136-150, 2009 (web-interface tool). Full version available as: Technical Report TRITA-CSC-TCS 2007:3, December 2007. [.pdf]

2008

J. Chrzaszcz, M. Huisman, A. Schubert, J. Kiniry, M. Pavlova and E. Poll. BML Reference Manual, 2008. In progress. Available online.
C. Haack, M. Huisman, and C. Hurlin. Reasoning about Java's Reentrant Locks In 6th Asian Symposium on Programming Languages and Systems (APLAS) December 2008. Lecture Notes in Computer Science, vol. 5356, pp. 171-187. [.pdf] (Long version, available as Technical report ICIS-R08014, Radboud University Nijmegen.)
M. Huisman, I. Aktug, and D. Gurov. Program models for compositional verification. In ICFEM 2008, 2008. Lecture Notes in Computer Science, vol. 5256, pp. 147-166, 2008. [bib|.pdf]
M. Huisman. Run-time verification can miss errors - Why finally clauses can be dangerous, 2008. Manuscript. [bib| .pdf]
D. Gurov, M. Huisman, and C. Sprenger. An algorithmic approach to compositional verification of sequential programs with procedures: An overview. In Foundations of Interface Technologies (FIT 2008), 2008. [bib| .pdf]
M. Huisman and G. Petri. BicolanoMT: a formalization of multi-threaded Java at bytecode level. In Bytecode 2008, Electronic Notes in Theoretical Computer Science, 2008. [bib| .pdf]
D. Gurov, M. Huisman, and C. Sprenger. Compositional verification of sequential programs with procedures. Information and Computation, 206:840-868, 2008. [bib| link]

2007

M. Huisman and C. Hurlin. Permission specifications for common multithreaded programming patterns. In Reflections on Type Theory, Lambda Calculus, and the Mind. Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday, 2007. [bib| .pdf]
D. Gurov and M. Huisman. Reducing behavioural to structural properties of programs with procedures. Technical Report TRITA-CSC-TCS 2007:3, KTH Royal Institute of Technology, Stockholm, 2007. [bib| .pdf| .pdf]
M. Huisman and C. Hurlin. The stability problem for verification of concurrent object-oriented programs. In Verification and Analysis of Multi-threaded Java-like Programs (VAMP), 2007. [bib| .pdf]
M. Huisman and G. Petri. The Java memory model: a formal explanation. In Verification and Analysis of Multi-threaded Java-like Programs (VAMP), 2007. [bib| .pdf]
M. Huisman and D. Gurov. Composing modal properties of programs with procedures. In Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2007), 2007. [bib| .pdf]
L. Burdy, M. Huisman, and M. Pavlova. Preliminary design of BML: A behavioral interface specification language for Java bytecode. In Fundamental Approaches to Software Engineering (FASE 2007), volume 4422 of Lecture Notes in Computer Science, pages 215-229. Springer-Verlag, 2007. [bib| .pdf]
G. Barthe, L. Burdy, J. Charles, B. Grégoire, M. Huisman, J.-L. Lanet, M. Pavlova, and A.Requet. JACK: a tool for validation of security and behaviour of Java applications. In FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects, LNCS 4709, pages 152-174. Springer-Verlag, 2007. [bib| .pdf]

2006

M. Huisman, P.Worah, and K.Sunesen. A temporal logic characterisation of observational determinism. In 19th IEEE Computer Security Foundations Workshop. IEEE Computer Society, July 2006. [bib| .pdf]
D. Gurov, M. Huisman, and C. Sprenger. Compositional verification of sequential programs with procedures. Technical report, INRIA, 2006. [bib]

2005

D. Gurov and M. Huisman. Interface abstraction for compositional verification. In B.Aichernig and B.Beckert, editors, Proceedings of SEFM'05, pages 414-423, Koblenz, Germany, September 2005. IEEE Computer Society. An earlier version appeared as INRIA Technical Report, nr. RR-5330. [bib| .ps.gz]
M. Huisman and K.Trentelman. Factorising temporal specifications. In M.Atkinson and F.Dehne, editors, Proceedings of CATS'05, volume 41 of Conferences in Research and Practice in Information Technology, pages 87-96, Newcastle, Australia, February 2005. ACSC. An earlier version appeared as INRIA Technical Report, nr. RR-5326. [bib| .ps.gz]
C. Breunesse, N. Cataño, M. Huisman, and B. Jacobs. Formal methods for smart cards: an experience report. Science of Computer Programming, 55(1-3):53-80, 2005. [bib| .pdf]

2004

M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet. Enforcing high-level security properties for applets. In P.Paradinas and J.-J. Quisquater, editors, Proceedings of CARDIS'04, Toulouse, France, August 2004. Kluwer Academic Publishers. [bib| .pdf]
M. Huisman, D. Gurov, C. Sprenger, and G.Chugunov. Checking absence of illicit applet interactions: a case study. In M.Wermelinger and T.Margaria-Steffen, editors, Proceedings of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages 84-98, Barcelona, Spain, March 2004. Springer-Verlag. [bib| .ps.gz]
C. Sprenger, D. Gurov, and M. Huisman. Compositional verification for secure loading of smart card applets. In C.Heitmeyer and J.-P. Talpin, editors, Memocode'04, pages 211-222. IEEE Computer Society, 2004. An earlier version appeared as INRIA Technical Report RR-4890. [bib| .ps.gz]
F.Bellegarde, J.Groslambert, M. Huisman, O.Kouchnarenko, and J.Julliand. Verification of liveness properties with JML. Technical Report RR-5331, INRIA, 2004. [bib| .ps.gz]
D. Gurov and M. Huisman. Abstraction over public interfaces. Technical Report RR-5330, INRIA, 2004. [bib| .ps.gz]

2003

N. Cataño and M. Huisman. Chase: A static checker for JML's assignable clause. In L.D. Zuck, P.C. Attie, A.Cortesi, and S.Mukhopadhyay, editors, VMCAI: Verification, Model Checking and Abstract Interpretation, volume 2575 of Lecture Notes in Computer Science, pages 26-40. Springer-Verlag, January 9-11 2003. [bib| .ps.gz]
C.Breunesse, N. Cataño, M. Huisman, and B. Jacobs. Formal Methods for Smart Cards: an experience report. Technical Report NIII-R0316, NIII, 2003. [bib| .html]
C. Sprenger, D. Gurov, and M. Huisman. Simulation logic, applets and compositional verification. Technical Report RR-4890, INRIA, 2003. [bib| .ps.gz]
M.Pavlova, G.Barthe, L.Burdy, M. Huisman, and J.-L. Lanet. Enforcing high-level security properties for applets. Technical Report RR-5061, INRIA, 2003. [bib| .html]
M. Huisman. Secure smartcards: a component-based view, 2003. A position paper for the Trusted Components Workshop. [bib| .ps.gz]

2002

N. Cataño and M. Huisman. Formal specification of Gemplus' electronic purse case study using ESC/Java. In L.-H. Eriksson and P.Lindsay, editors, FME 2002: Formal Methods: International Symposium of Formal Methods Europe, volume 2391 of Lecture Notes in Computer Science, pages 272-289, Copenhagen, Denmark, July 2002. Springer-Verlag. [bib| .ps.gz]
G. Barthe, D. Gurov, and M. Huisman. Compositional verification of secure applet interactions. In Fundamental Approaches to Software Engineering (FASE'02), volume 2306 of Lecture Notes in Computer Science, pages 15-32. Springer-Verlag, 2002. [bib| .ps.gz]
K.Trentelman and M. Huisman. Extending JML specifications with temporal logic. In H.Kirchner and C.Ringessein, editors, Proceedings of AMAST'02, volume 2422 of Lecture Notes in Computer Science, pages 334-348. Springer-Verlag, 2002. [bib| .ps.gz]
M. Huisman. Verification of Java's AbstractCollection class: a case study. In E.Boiten and B.Möller, editors, Mathematics of Program Construction (MPC'02), number 2386 in Lecture Notes in Computer Science, pages 175 - 194. Springer-Verlag, 2002. [bib| .ps.gz]

2001

G. Barthe, G. Dufay, M. Huisman, and S.Melo deSousa. Jakarta: a toolset to reason about the JavaCard platform. In I.Attali and T.Jensen, editors, Proceedings of e-SMART'01, volume 2140 of Lecture Notes in Computer Science, pages 2-18. Springer-Verlag, 2001. [bib| .ps.gz]
G. Barthe, D. Gurov, and M. Huisman. Compositional specification and verification of control flow based security properties of multi-application programs. In Workshop on Formal Techniques for Java Programs (FTfJP), 2001. [bib| .ps.gz]
M. Huisman, B. Jacobs, and J.van den Berg. A Case Study in Class Library Verification: Java's Vector Class. Software Tools for Technology Transfer, 3/3:332-352, 2001. [bib| link]
M. Huisman. Reasoning about Java Programs in Higher Order Logic with PVS and Isabelle. PhD thesis, University of Nijmegen, 2001. [bib| .ps.gz]

2000

M. Huisman and B. Jacobs. Inheritance in higher order logic: Modeling and reasoning. In J.Harrison and M.Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference (TPHOLs 2000), number 1869 in Lecture Notes in Computer Science, pages 301-319. Springer-Verlag, 2000. [bib| .ps.gz]
J.van den Berg, M. Huisman, B. Jacobs, and E.Poll. A type-theoretic memory model for verification of sequential Java programs. In D.Bert, C.Choppy, and P.D. Mosses, editors, Recent Trends in Algebraic Development Techniques, number 1827 in Lecture Notes in Computer Science, pages 1-21. Springer-Verlag, 2000. [bib| .ps.Z]
M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In T.Maibaum, editor, Fundamental Approaches to Software Engineering (FASE 2000), number 1783 in Lecture Notes in Computer Science, pages 284-303. Springer-Verlag, 2000. [bib| link]

1999

M. Huisman, B. Jacobs, and J.van den Berg. A case study in class library verification: Java's Vector class (abstract). In B. Jacobs, G.T. Leavens, P.Müller, and A.Poetzsch-Heffter, editors, Formal Techniques for Java Programs, number 251 - 5/1999 in Informatik Berichte FernUniversität Hagen, 1999. [bib| .ps.Z]

1998

B. Jacobs, J.van den Berg, M. Huisman, M.van Berkum, U.Hensel, and H.Tews. Reasoning about Java classes (preliminary report). In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'98), pages 329-340. ACM Press, 1998. [bib| .ps.Z]
W.O.D. Griffioen and M. Huisman. A comparison of PVS and Isabelle/HOL. In J.Grundy and M.Newey, editors, Theorem Proving in Higher Order Logics: 11th International Conference (TPHOLs '98), number 1479 in Lecture Notes in Computer Science, pages 123-142, 1998. [bib| .ps.gz]
U.Hensel, M. Huisman, B. Jacobs, and H.Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In C.Hankin, editor, Proceedings of European Symposium on Programming (ESOP '98), number 1381 in Lecture Notes in Computer Science, pages 105-121. Springer-Verlag, 1998. [bib| .ps.gz]

1997

M. Huisman. Binary addition in Lego. Technical Report CSI-9714, Computing Science Institute, University of Nijmegen, 1997. [bib| .ps.Z]
M. Huisman. The specification of an antenna system: a case study. Technical Report CSI-9716, Computing Science Institute, University of Nijmegen, 1997. [bib| .ps.Z]

1996

M. Huisman. The calculation of a polytypic parser, 1996. Master Thesis, Utrecht University. [bib| .ps.gz]

This file has been generated by bibtex2html 1.87.

on Tue, 02 Sep 2008 00:00:09 +0200