Publications - Marieke Huisman in BibTeX Format
[Bibliography in Clear Text] huisman.bib@INPROCEEDINGS{HuismanAG08, author = {Marieke Huisman and Irem Aktug and Dilian Gurov}, title = {Program Models for Compositional Verification}, booktitle = {ICFEM 2008}, note = {To appear}, year = 2008, topic = {team} } @MISC{Huisman08, author = {Marieke Huisman}, title = {Run-time Verification can miss Errors - {W}hy Finally Clauses can be Dangerous}, note = {Manuscript}, year = 2008, topic = {team}, pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/finally.pdf} } @INPROCEEDINGS{HuismanH07b, author = {Marieke Huisman and Cl\'ement Hurlin}, title = {Permission Specifications for Common Multithreaded Programming Patterns}, booktitle = {Reflections on Type Theory, Lambda Calculus, and the Mind. Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday}, year = 2007, topics = {team}, pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/patterns.pdf} } @INPROCEEDINGS{GurovHS08, author = {D. Gurov and M. Huisman and C. Sprenger}, title = {An Algorithmic Approach to Compositional Verification of Sequential Programs with Procedures: An Overview}, booktitle = {Foundations of Interface Technologies (FIT 2008)}, year = 2008, editors = {K.G. Larsen and A. Wasowski and U. Nyman}, topics = {team}, pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fit.pdf} } @INPROCEEDINGS{HuismanP08, author = {Marieke Huisman and Gustavo Petri}, title = {{BicolanoMT}: a formalization of multi-threaded {Java} at bytecode level}, year = 2008, booktitle = {Bytecode 2008}, editors = {F. Logozzo and J. Vitek}, series = {Electronic Notes in Theoretical Computer Science}, topics = {team}, pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/bytecode.pdf} } @TECHREPORT{Gur-Hui-TR-07, author = {D. Gurov and M. Huisman}, institution = {KTH Royal Institute of Technology, Stockholm}, number = {TRITA-CSC-TCS 2007:3}, title = {Reducing Behavioural to Structural Properties of Programs with Procedures}, pdfurl = {http://www.csc.kth.se/~dilian/Papers/techrep-07-3.pdf}, year = 2007, topics = {team}, url = {http://www.nada.kth.se/~dilian/Papers/techrep-07-3.pdf} } @ARTICLE{GurovHS08b, author = {D. Gurov and M. Huisman and C. Sprenger}, title = {Compositional Verification of Sequential Programs with Procedures}, journal = {Information and Computation}, volume = 206, issue = 7, pages = {840--868}, year = {2008}, note = {team}, url = {http://dx.doi.org/10.1016/j.ic.2008.03.003} } @INPROCEEDINGS{HuismanH07, author = {Marieke Huisman and Cl\'ement Hurlin}, title = {The Stability Problem for Verification of Concurrent Object-Oriented Programs}, booktitle = {Verification and Analysis of Multi-threaded Java-like Programs (VAMP)}, year = 2007, note = {To appear}, topics = {team}, pdfurl = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/vamp07.pdf}, texurl = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/vamp07.tex} } @INPROCEEDINGS{HuismanP07, author = {Marieke Huisman and Gustavo Petri}, title = {The {Java} Memory Model: a Formal Explanation}, booktitle = {Verification and Analysis of Multi-threaded Java-like Programs (VAMP)}, year = 2007, note = {To appear}, topics = {team}, pdfurl = {http://www-sop.inria.fr/everest/personnel/Gustavo.Petri/publis/jmm-vamp07.pdf} } @INPROCEEDINGS{HuismanG07, author = {Marieke Huisman and Dilian Gurov}, title = {Composing Modal Properties of Programs with Procedures}, booktitle = {Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2007)}, year = 2007, topics = {team}, pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fesca.pdf} } @INPROCEEDINGS{BurdyHP07, author = {Lilian Burdy and Marieke Huisman and Mariela Pavlova}, title = {Preliminary Design of {BML}: A Behavioral Interface Specification Language for {Java} bytecode}, booktitle = {Fundamental Approaches to Software Engineering (FASE 2007)}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 4422, pages = {215-229}, year = 2007, pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/bml.pdf}, topics = {team} } @INPROCEEDINGS{BBCGHLPR07:FMCO, author = {G. Barthe and L. Burdy and J. Charles and B. Gr{\'e}goire and M. Huisman and J.-L. Lanet and M. Pavlova and A. Requet}, title = {{JACK}: a tool for validation of security and behaviour of {Java} applications}, booktitle = {FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, year = {2007}, note = {To appear}, pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fmco06.pdf}, topics = {team} } @INPROCEEDINGS{HWS06, author = {M. Huisman and P. Worah and K. Sunesen}, title = {A temporal logic characterisation of observational determinism}, crossref = {csfw06}, topics = {team}, pdfurl = {ftp://ftp-sop.inria.fr/everest/personnel/Marieke.Huisman/obsequiv_char.pdf} } @INPROCEEDINGS{GH05, author = {D. Gurov and M. Huisman}, title = {Interface Abstraction for Compositional Verification}, crossref = {sefm05}, pages = {414-423}, psurl = {http://www.nada.kth.se/~dilian/Papers/sefm05.ps.gz}, note = {An earlier version appeared as INRIA Technical Report, nr. RR-5330}, topics = {team} } @INPROCEEDINGS{BGH02, author = {G. Barthe and D. Gurov and M. Huisman}, title = {Compositional Verification of Secure Applet Interactions}, crossref = {fase02}, pages = {15-32}, psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/fase02.ps.gz}, topics = {team} } @INPROCEEDINGS{CH02, author = {N. Cata{\~n}o and M. Huisman}, title = {Formal specification of {Gemplus'} electronic purse case study using {ESC/Java}}, pages = {272-289}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/fme37.ps.gz}, crossref = {fme02}, topics = {team} } @INPROCEEDINGS{HT02, author = {K. Trentelman and M. Huisman}, title = {Extending {JML} Specifications with Temporal Logic}, crossref = {amast02}, pages = {334-348}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/amast02.ps.gz}, topics = {team} } @INPROCEEDINGS{Hui-cats05, author = {M. Huisman and K. Trentelman}, title = {Factorising temporal specifications}, crossref = {cats05}, pages = {87--96}, note = {An earlier version appeared as INRIA Technical Report, nr. RR-5326}, psurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/factorisation.ps.gz}, topics = {team} } @INPROCEEDINGS{memocode04, author = {C. Sprenger and D. Gurov and M. Huisman}, title = {Compositional Verification for Secure Loading of Smart Card Applets}, crossref = {memocode04proc}, pages = {211--222}, psurl = {http://www.nada.kth.se/~dilian/Papers/memocode04.ps.gz}, note = {An earlier version appeared as INRIA Technical Report RR-4890}, topics = {team} } @INPROCEEDINGS{CH03, author = {N. Cata{\~n}o and M. Huisman}, title = {Chase: A Static Checker for {JML}'s Assignable Clause}, pages = {26--40}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/vmcai.ps.gz}, crossref = {vmcai03}, topics = {team} } @INPROCEEDINGS{m+04:cardis, author = {M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet}, title = {Enforcing High-Level Security Properties For Applets}, crossref = {cardis04}, pages = {}, topics = {team}, pdfurl = {ftp://ftp-sop.inria.fr/everest/publis/P+04cardis.pdf} } @INPROCEEDINGS{HuismanGSC03, author = {M. Huisman and D. Gurov and C. Sprenger and G. Chugunov}, title = {Checking Absence of Illicit Applet Interactions: a Case Study}, pages = {84-98}, crossref = {fase04}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/casestudy.ps.gz}, topics = {team} } @INPROCEEDINGS{g+01:esmart, author = {G. Barthe and G. Dufay and M. Huisman and S. Melo de Sousa}, title = {{Jakarta: a toolset to reason about the JavaCard platform}}, crossref = {esmart01}, pages = {2--18}, psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/esmart01.ps.gz} } @INPROCEEDINGS{Huisman02, author = {M. Huisman}, title = {{Verification of Java's AbstractCollection class: a case study}}, booktitle = {Mathematics of Program Construction (MPC'02)}, number = 2386, series = {Lecture Notes in Computer Science}, pages = {175 - 194}, publisher = {Springer-Verlag}, year = 2002, editor = {E. Boiten and B. M{\"o}ller}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/collection.ps.gz} } @INPROCEEDINGS{BartheGH01, author = {G. Barthe and D. Gurov and M. Huisman}, title = {Compositional specification and verification of control flow based security properties of multi-application programs}, crossref = {ftfjp01}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/model_short.ps.gz} } @INPROCEEDINGS{HuismanJ00b, author = {M. Huisman and B. Jacobs}, title = {Inheritance in Higher Order Logic: Modeling and Reasoning}, pages = {301--319}, editor = {J. Harrison and M. Aagaard}, booktitle = {Theorem Proving in Higher Order Logics: 13th International Conference (TPHOLs 2000)}, series = {Lecture Notes in Computer Science}, number = 1869, year = 2000, publisher = {Springer-Verlag}, psurl = {ftp://ftp-sop.inria.fr/lemme/personnel/Marieke.Huisman/inheritance.ps.gz} } @INPROCEEDINGS{BergHJP00, author = {Berg, J. van den and M. Huisman and B. Jacobs and E. Poll}, title = {A Type-Theoretic Memory Model for Verification of Sequential {Java} Programs}, booktitle = {Recent Trends in Algebraic Development Techniques}, series = {Lecture Notes in Computer Science}, number = 1827, pages = {1-21}, editor = {D. Bert and C. Choppy and P.D. Mosses}, publisher = {Springer-Verlag}, year = 2000, psurl = {http://www.cs.kun.nl/~bart/PAPERS/WADT99.ps.Z} } @INPROCEEDINGS{HuismanJ00a, author = {M. Huisman and B. Jacobs}, title = {{Java} Program Verification via a {Hoare} Logic with Abrupt Termination}, booktitle = {Fundamental Approaches to Software Engineering (FASE 2000)}, publisher = {Springer-Verlag}, editor = {T. Maibaum}, pages = {284--303}, series = {Lecture Notes in Computer Science}, number = {1783}, year = 2000, psurl = {http://link.springer.de/link/service/series/0558/bibs/1783/17830284.htm} } @INPROCEEDINGS{HuismanJB99a, author = {M. Huisman and B. Jacobs and Berg, J. van den}, title = {A case study in class library verification: {Java}'s {Vector} class (abstract)}, booktitle = {Formal Techniques for Java Programs}, editor = {B. Jacobs and G.T. Leavens and P. M{\"u}ller and A. Poetzsch-Heffter}, series = {Informatik Berichte FernUniversit{\"a}t Hagen}, number = {251 - 5/1999}, year = 1999, psurl = {http://www.cs.kun.nl/~bart/PAPERS/Vector_kort.ps.Z} } @INPROCEEDINGS{JacobsBHBHT98, author = {B. Jacobs and Berg, J. van den and M. Huisman and M. van Berkum and U. Hensel and H. Tews}, title = {Reasoning about {Java} Classes (Preliminary Report)}, booktitle = {Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'98)}, publisher = {ACM Press}, pages = {329--340}, year = {1998}, psurl = {http://www.cs.kun.nl/~bart/PAPERS/OOPSLA98.ps.Z} } @INPROCEEDINGS{GriffioenH98, author = {W.O.D. Griffioen and M. Huisman}, title = {A Comparison of {PVS} and {Isabelle/HOL}}, booktitle = {Theorem Proving in Higher Order Logics: 11th International Conference (TPHOLs '98)}, year = 1998, series = {Lecture Notes in Computer Science}, number = 1479, pages = {123--142}, editor = {J. Grundy and M. Newey}, psurl = {ftp://ftp-sop.inria.fr/lemme/personnel/Marieke.Huisman/Tphols98.ps.gz} } @INPROCEEDINGS{HenselHJT98, title = { Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools}, author = {U. Hensel and M. Huisman and B. Jacobs and H. Tews}, booktitle = {Proceedings of European Symposium on Programming (ESOP '98)}, year = 1998, editor = {C. Hankin}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, number = 1381, pages = {105--121}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/etaps98.ps.gz} } @ARTICLE{final:Form.Met, author = {C. Breunesse and N. Cata{\~n}o and M. Huisman and B. Jacobs}, title = {Formal Methods for Smart Cards: an experience report}, journal = {Science of Computer Programming}, year = {2005}, volume = 55, number = {1-3}, pages = {53-80}, pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fm_smart.pdf}, topics = {team} } @ARTICLE{HuismanJB01, author = {M. Huisman and B. Jacobs and Berg, J. van den}, title = {{A Case Study in Class Library Verification: Java's Vector Class}}, journal = {Software Tools for Technology Transfer}, volume = {3/3}, pages = {332--352}, year = 2001, url = {http://link.springer.de/link/service/journals/10009/bibs/1003003/10030332.htm} } @PHDTHESIS{Huisman01, author = {M. Huisman}, title = {{Reasoning about Java Programs in Higher Order Logic with PVS and Isabelle}}, school = {University of Nijmegen}, year = {2001}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/thesis.ps.gz} } @MISC{Huisman96, author = {M. Huisman}, title = {The calculation of a polytypic parser}, note = {Master Thesis, Utrecht University}, year = 1996, psurl = {ftp://ftp-sop.inria.fr/lemme/personnel/Marieke.Huisman/scriptie.ps.gz} } @TECHREPORT{BreunesseCHJ03, author = {C. Breunesse and N. Cata{\~n}o and M. Huisman and B. Jacobs}, title = {{Formal Methods for Smart Cards: an experience report}}, number = {NIII-R0316}, institution = {NIII}, year = {2003}, url = {http://www.cs.kun.nl/research/reports/info/NIII-R0316.html}, topics = {team} } @TECHREPORT{SprengerGH03, author = {C. Sprenger and D. Gurov and M. Huisman}, title = {Simulation Logic, Applets and Compositional Verification}, number = {RR-4890}, institution = {INRIA}, year = {2003}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/techreport.ps.gz}, topics = {team} } @TECHREPORT{mariela+03, author = {M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet}, title = {Enforcing High-Level Security Properties For Applets}, number = {RR-5061}, institution = {INRIA}, year = {2003}, url = {http://www-sop.inria.fr/rapports/sophia/RR-5061.html}, topics = {team} } @TECHREPORT{BGHKJ-5331, author = {F. Bellegarde and J. Groslambert and M. Huisman and O. Kouchnarenko and J. Julliand}, title = {Verification of Liveness Properties with {JML}}, institution = {INRIA}, year = {2004}, number = {RR-5331}, topics = {team}, psurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/liveness.ps.gz} } @TECHREPORT{GH-5330, author = {D. Gurov and M. Huisman}, title = {Abstraction over Public Interfaces}, institution = {INRIA}, year = {2004}, number = {RR-5330}, topics = {team}, psurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/interfaces_techreport.ps.gz} } @TECHREPORT{Huisman97a, author = {M. Huisman}, year = 1997, title = {Binary addition in {L}ego}, institution = {Computing Science Institute, University of N{ij}\-megen}, number = {CSI-9714}, psurl = {http://www.cs.kun.nl/csi/reports/full/CSI-R9714.ps.Z} } @TECHREPORT{Huisman97b, author = {M. Huisman}, title = {The specification of an antenna system: a case study}, institution = {Computing Science Institute, University of N{ij}\-megen}, year = 1997, number = {CSI-9716}, psurl = {http://www.cs.kun.nl/csi/reports/full/CSI-R9716.ps.Z} } @MISC{Huisman03, author = {M. Huisman}, title = {Secure smartcards: a component-based view}, year = 2003, note = {A position paper for the Trusted Components Workshop}, psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/trusted_components.ps.gz} } @TECHREPORT{GurovHS06, author = {D. Gurov and M. Huisman and C. Sprenger}, title = {Compositional Verification of Sequential Programs with Procedures}, institution = {INRIA}, year = {2006}, topics = {team} } @PROCEEDINGS{sefm05, title = {Software Engineering and Formal Methods (SEFM'05)}, booktitle = {Proceedings of SEFM'05}, editor = {B. Aichernig and B. Beckert}, publisher = {IEEE Computer Society}, month = {September}, address = {Koblenz, Germany}, year = 2005 } @PROCEEDINGS{csfw06, title = {19th IEEE Computer Security Foundations Workshop}, booktitle = {19th IEEE Computer Security Foundations Workshop}, publisher = {IEEE Computer Society}, month = {July}, year = 2006 } @PROCEEDINGS{cats05, title = {Proceedings of CATS'05}, booktitle = {Proceedings of CATS'05}, year = 2005, editor = {M. Atkinson and F. Dehne}, volume = 41, series = {Conferences in Research and Practice in Information Technology}, address = {Newcastle, Australia}, month = {February}, publisher = {ACSC} } @PROCEEDINGS{cardis04, editor = {P. Paradinas and J.-J. Quisquater}, booktitle = {{Proceedings of CARDIS'04}}, title = {{Proceedings of CARDIS'04}}, publisher = {Kluwer Academic Publishers}, year = {2004}, address = {Toulouse, France}, month = {August} } @PROCEEDINGS{memocode04proc, booktitle = {Memocode'04}, title = {Memocode'04}, year = {2004}, publisher = {IEEE Computer Society}, editor = {C. Heitmeyer and J.-P. Talpin} } @PROCEEDINGS{fase04, year = {2004}, booktitle = {Proceedings of {FASE}'04}, title = {Proceedings of {FASE}'04}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, volume = {2984}, editor = {M. Wermelinger and T. Margaria-Steffen}, address = {Barcelona, Spain}, month = {March} } @PROCEEDINGS{vmcai03, booktitle = {VMCAI: Verification, Model Checking and Abstract Interpretation}, title = {VMCAI: Verification, Model Checking and Abstract Interpretation}, editor = {L. D. Zuck and P. C. Attie and A. Cortesi and S. Mukhopadhyay}, volume = {2575}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, month = {January 9-11}, year = {2003} } @PROCEEDINGS{fase02, booktitle = {Fundamental Approaches to Software Engineering (FASE'02)}, title = {Fundamental Approaches to Software Engineering (FASE'02)}, year = {2002}, series = {Lecture Notes in Computer Science}, volume = {2306}, publisher = {Springer-Verlag} } @PROCEEDINGS{fme02, booktitle = {FME 2002: Formal Methods: International Symposium of Formal Methods Europe}, title = {FME 2002: Formal Methods: International Symposium of Formal Methods Europe}, year = {2002}, editor = {L.-H. Eriksson and P. Lindsay}, volume = {2391}, series = {Lecture Notes in Computer Science}, address = {Copenhagen, Denmark}, month = {July}, publisher = {Springer-Verlag} } @PROCEEDINGS{amast02, booktitle = {Proceedings of AMAST'02}, title = {Proceedings of AMAST'02}, editor = {H. Kirchner and C. Ringessein}, series = {Lecture Notes in Computer Science}, year = {2002}, publisher = {Springer-Verlag}, volume = {2422} } @PROCEEDINGS{ftfjp01, title = {Workshop on Formal Techniques for Java Programs (FTfJP)}, booktitle = {Workshop on Formal Techniques for Java Programs (FTfJP)}, year = 2001, url = {http://www.informatik.fernuni-hagen.de/import/pi5/workshops/ecoop2001_papers.html} } @PROCEEDINGS{esmart01, year = {2001}, booktitle = {Proceedings of e-SMART'01}, title = {Proceedings of e-SMART'01}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2140}, editor = {I. Attali and T. Jensen} } |