T.M. Ngo,
and
M. Huisman.
Quantitative Security Analysis for Programs with Low Input and Noisy Output.
ESSOS
2014, pp. 7794. 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 TRCTIT1310, Centre for
Telematics and Information Technology, University of Twente,
Enschede. ISSN 13813625. [.pdf]

A. Amighi,
S. Blom, and
M. Huisman.
W.
Mostowski, and
M. ZaharievaStojanovski.
Formal specifications for Java’s synchronisation
classes. Technical Report TRCTIT1318, Centre for
Telematics and Information Technology, University of Twente,
Enschede. ISSN 13813625. [.pdf]

S. Blom, and
M. Huisman.
Witnessing the Elimination of Magic Wands. Technical Report
TRCTIT1322, Centre for Telematics and Information
Technology, University of Twente , Enschede . ISSN
13813625.
[.pdf]

S. Blom,
M. Huisman,
and
M. Mihelcic. Specification and verification of GPGPU
programs. Technical Report TRCTIT1321, Centre for
Telematics and Information Technology, University of Twente,
Enschede. ISSN 13813625. [.pdf]

L. Wevers,
M. Huisman and
A. de Keijzer. Parallel transaction processing in functional
languages, towards practical functional databases. Technical
Report TRCTIT1306, Centre for Telematics and Information
Technology, University of Twente, Enschede. ISSN
13813625. [.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.
ProcedureModular Specification and Verification of Temporal Safety
Properties.
Software and Systems Modeling. [.pdf]

T.M. Ngo,
M. Stoelinga
and
M. Huisman.
Confidentiality for Probabilistic Multithreaded 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 Multithreaded 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 Permissionbased Separation logic.
In Bytecode
2013. Also appeared as Technical Report TRCTIT1312, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 13813625.
[.pdf]

2012
A. Amighi,
P. de Carvalho Gomes,
D. Gurov and
M. Huisman.
Sound ControlFlow Graph Extraction for Java programs with Exceptions.
In Software Engineering
and Formal Methods (SEFM 2012). LNCS 7504, pages 33  47,
Springer. [.pdf]

M. ZaharievaStojanovski,
M. Huisman and
S. Blom. A
History of BlockingQueues. In proceedings of Formal Languages and
Analysis of ContractOriented 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 ObjectOriented Software
(FoVeOos 2011). LNCS 7421, pages 321, Springer. [.pdf]

M. Huisman and
T.M. Ngo.
Schedulerspecific Confidentiality for Multithreaded Programs and Its logicbased Verification.
In proceedings of Formal Verification of ObjectOriented Systems
(FoVeOos 2011). LNCS 7421, pages 178  195, Springer. [.pdf]

A. Amighi,
S. Blom,
M. Huisman,
M. ZaharievaStojanovski.
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 ControlFlow Graphs from Java programs with Exceptions.
In preproceedings of Formal Verification of ObjectOriented Systems (FoVeOos 2011).

M. Huisman and
T.M. Ngo.
Schedulerspecific Confidentiality for Multithreaded Programs and Its logicbased Verification.
In preproceedings of Formal Verification of ObjectOriented Systems
(FoVeOos 2011). Subsumed by the version in the final proceedings.

M. Huisman and
T.M. Ngo.
Schedulerrelated Confidentiality for
Multithreaded Programs.
Accepted for presentation at SecCo 2011.
A longer version is available as Technical Report TRCTIT1122, 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 366381, 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 AspectOriented Recovery Approach.
In Formal Techniques for Javalike Programs
(FTfJP) 2011. ACM Digital Library.
[.pdf]

M. Huisman and H.C. Blondeel. Modelchecking Secure Information Flow for MultiThreaded 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.
PermissionBased 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 ControlFlow Safety Properties.
In Proceedings of Formal Verification of ObjectOriented Software (FoVeOOS) 2010. LNCS 6528, pages 107  121, Springer. [.pdf]

S. Soleimanifard,
D. Gurov and
M. Huisman.
ProcedureModular Verification of Control Flow Safety Properties.
In Formal Techniques for Javalike Programs
(FTfJP) 2010, ACM Digital Library. [.pdf]

2009
M. Huisman.
On the Interplay between the Semantics of Java's Finally Clauses and the JML RunTime Checker.
In Formal Techniques for Javalike 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. 340354, 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. 136150, 2009 (webinterface tool).
Full version available as:
Technical Report TRITACSCTCS 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. 171187. [.pdf] (Long version, available as Technical report ICISR08014, 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. 147166, 2008.
[bib.pdf]

M. Huisman.
Runtime 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 multithreaded 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:840868, 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 TRITACSCTCS 2007:3, KTH Royal Institute of
Technology, Stockholm, 2007.
[bib
.pdf
.pdf]

M. Huisman and C. Hurlin.
The stability problem for verification of concurrent objectoriented
programs.
In Verification and Analysis of Multithreaded Javalike
Programs (VAMP), 2007.
[bib
.pdf]

M. Huisman and G. Petri.
The Java memory model: a formal explanation.
In Verification and Analysis of Multithreaded Javalike
Programs (VAMP), 2007.
[bib
.pdf]

M. Huisman and D. Gurov.
Composing modal properties of programs with procedures.
In Formal Foundations of Embedded Software and ComponentBased
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 215229.
SpringerVerlag, 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 152174.
SpringerVerlag, 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 414423, Koblenz, Germany, September 2005. IEEE Computer
Society.
An earlier version appeared as INRIA Technical Report, nr. RR5330.
[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 8796, Newcastle, Australia, February 2005. ACSC.
An earlier version appeared as INRIA Technical Report, nr. RR5326.
[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(13):5380, 2005.
[bib
.pdf]

2004
M. Pavlova,
G. Barthe,
L. Burdy,
M. Huisman, and
J.L. Lanet.
Enforcing highlevel 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.MargariaSteffen, editors, Proceedings
of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages
8498, Barcelona, Spain, March 2004. SpringerVerlag.
[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
211222. IEEE Computer Society, 2004.
An earlier version appeared as INRIA Technical Report RR4890.
[bib
.ps.gz]

F.Bellegarde, J.Groslambert, M. Huisman, O.Kouchnarenko, and J.Julliand.
Verification of liveness properties with JML.
Technical Report RR5331, INRIA, 2004.
[bib
.ps.gz]

D. Gurov and M. Huisman.
Abstraction over public interfaces.
Technical Report RR5330, 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 2640.
SpringerVerlag, January 911 2003.
[bib
.ps.gz]

C.Breunesse, N. Cataño, M. Huisman, and B. Jacobs.
Formal Methods for Smart Cards: an experience report.
Technical Report NIIIR0316, NIII, 2003.
[bib
.html]

C. Sprenger, D. Gurov, and M. Huisman.
Simulation logic, applets and compositional verification.
Technical Report RR4890, INRIA, 2003.
[bib
.ps.gz]

M.Pavlova, G.Barthe, L.Burdy, M. Huisman, and J.L. Lanet.
Enforcing highlevel security properties for applets.
Technical Report RR5061, INRIA, 2003.
[bib
.html]

M. Huisman.
Secure smartcards: a componentbased 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 272289, Copenhagen, Denmark,
July 2002. SpringerVerlag.
[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 1532.
SpringerVerlag, 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
334348. SpringerVerlag, 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. SpringerVerlag, 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 eSMART'01,
volume 2140 of Lecture Notes in Computer Science, pages 218.
SpringerVerlag, 2001.
[bib
.ps.gz]

G. Barthe,
D. Gurov, and
M. Huisman.
Compositional specification and verification of control flow based
security properties of multiapplication 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:332352, 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 301319. SpringerVerlag,
2000.
[bib
.ps.gz]

J.van den Berg, M. Huisman, B. Jacobs, and E.Poll.
A typetheoretic 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 121. SpringerVerlag, 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 284303. SpringerVerlag, 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.PoetzschHeffter,
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 ObjectOriented Programming, Systems, Languages and
Applications (OOPSLA'98), pages 329340. 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 123142, 1998.
[bib
.ps.gz]

U.Hensel, M. Huisman, B. Jacobs, and H.Tews.
Reasoning about classes in objectoriented 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 105121. SpringerVerlag, 1998.
[bib
.ps.gz]

1997
M. Huisman.
Binary addition in Lego.
Technical Report CSI9714, Computing Science Institute, University of
Nijmegen, 1997.
[bib
.ps.Z]

M. Huisman.
The specification of an antenna system: a case study.
Technical Report CSI9716, 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
