version française All team publications
Publications - Marieke Huisman
[BibTeX Format]

[HAG08] Marieke Huisman, Irem Aktug, and Dilian Gurov. Program models for compositional verification. In ICFEM 2008, 2008. To appear. [ bib ]
[Hui08] Marieke Huisman. Run-time verification can miss errors - Why finally clauses can be dangerous, 2008. Manuscript. [ bib | .pdf ]
[GHS08a] 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 ]
[HP08] Marieke Huisman and Gustavo Petri. BicolanoMT: a formalization of multi-threaded Java at bytecode level. In Bytecode 2008, Electronic Notes in Theoretical Computer Science, 2008. [ bib | .pdf ]
[GHS08b] D. Gurov, M. Huisman, and C. Sprenger. Compositional verification of sequential programs with procedures. Information and Computation, 206:840-868, 2008. team. [ bib | http ]
[HH07a] Marieke Huisman and Clément 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 ]
[GH07] 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 ]
[HH07b] Marieke Huisman and Clément 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 ]
[HP07] Marieke Huisman and Gustavo Petri. The Java memory model: a formal explanation. In Verification and Analysis of Multi-threaded Java-like Programs (VAMP), 2007. To appear. [ bib | .pdf ]
[HG07] Marieke Huisman and Dilian Gurov. Composing modal properties of programs with procedures. In Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2007), 2007. [ bib | .pdf ]
[BHP07] Lilian Burdy, Marieke Huisman, and Mariela 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 ]
[BBC+07] 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, Lecture Notes in Computer Science. Springer-Verlag, 2007. To appear. [ bib | .pdf ]
[HWS06] 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 ]
[GHS06] D. Gurov, M. Huisman, and C. Sprenger. Compositional verification of sequential programs with procedures. Technical report, INRIA, 2006. [ bib ]
[GH05] 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 ]
[HT05] 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 ]
[BCHJ05] 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 ]
[PBB+04] 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 ]
[HGSC04] 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 ]
[SGH04] 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 ]
[BGH+04] 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 ]
[GH04] D. Gurov and M. Huisman. Abstraction over public interfaces. Technical Report RR-5330, INRIA, 2004. [ bib | .ps.gz ]
[CH03] 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 ]
[BCHJ03] 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 ]
[SGH03] C. Sprenger, D. Gurov, and M. Huisman. Simulation logic, applets and compositional verification. Technical Report RR-4890, INRIA, 2003. [ bib | .ps.gz ]
[PBB+03] 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 ]
[Hui03] M. Huisman. Secure smartcards: a component-based view, 2003. A position paper for the Trusted Components Workshop. [ bib | .ps.gz ]
[CH02] 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 ]
[BGH02] 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 ]
[TH02] 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 ]
[Hui02] 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 ]
[BDHdS01] G. Barthe, G. Dufay, M. Huisman, and S. Melo de Sousa. 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 ]
[BGH01] 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 ]
[HJB01] 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 ]
[Hui01] M. Huisman. Reasoning about Java Programs in Higher Order Logic with PVS and Isabelle. PhD thesis, University of Nijmegen, 2001. [ bib | .ps.gz ]
[HJ00a] 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 ]
[BHJP00] 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 ]
[HJ00b] 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 ]
[HJB99] 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 ]
[JBH+98] 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 ]
[GH98] 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 ]
[HHJT98] 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 ]
[Hui97a] M. Huisman. Binary addition in Lego. Technical Report CSI-9714, Computing Science Institute, University of Nijmegen, 1997. [ bib | .ps.Z ]
[Hui97b] 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 ]
[Hui96] 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