Publications Marieke Huisman

last updated: July 20, 2014

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

2014

A. Amighi, S. Blom, and M. Huisman. Resource protection using atomics: patterns and verification. In APLAS 2014, LNCS, Springer. To appear.
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, to appear.
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]
S. Soleimanifard, D. Gurov and M. Huisman. Procedure-Modular Specification and Verification of Temporal Safety Properties. Software and Systems Modeling. [.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. To appear. [.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| http]

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. To appear. [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. To appear. [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| http]
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| http]

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