Bibliography

Bibliography

The following publications are cited on one or more pages in this wiki:

Version: 8 Time: Fri Mar 28 14:31:57 2008 Author: dcochran (dcochran) IP: 193.1.132.32

Key	Author(s)	Title	In	Year
BBC+06	G. Barthe, L. Beringer, P. Cregut, B. Gregoire, M. Hofmann, P. Muller, E. Poll, G. Puebla, I. Stark and E. Vetillard	MOBIUS: Mobility, ubiquity, security - objectives and progress report	Trustworthy Global Computing, Lucca, Italy. Lecture Notes in Computer Science, Springer-Verlag	2006
BBC+07	G. Barthe, L. Burdy, J. Charles, B. Gregoire, M. Huisman, J.-L.Lanet, M. Pavlova and A. Requet	JACK: a tool for validation of security and behaviour of Java applications	Formal Methods for Components and Objects, Lecture Notes in Computer Science. Springer-Verlag	2007
BT07	C. Barrett and C. Tinelli	CVC3	Proceedings of the Nineteenth International Conference on Computer Aided Verification	2007
CJK07	P. Chalin, P. R. James, and G. Karabotsos	The architecture of JML4, a proposed integrated verification environment for JML	Technical report, Dependable Software Research Group, Concordia University. ENCS-CSE-TR 2007-006. [http://users.encs.concordia.ca/~chalin/papers/TR-2007-006-v1zr.pdf]	2007
Con04	The JSR 133 Consortium	The Java memory model causality test cases	[http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html]	2004
MOBIUS Consortium06a	MOBIUS Consortium	Deliverable 1.2: Framework-specific and application-specific security requirements	[http://mobius.inria.fr]	2006
MOBIUS Consortium06b	MOBIUS Consortium	Deliverable 3.1: Bytecode specification language and program logic	[http://mobius.inria.fr]	2006
MOBIUS Consortium07a	MOBIUS Consortium	Deliverable 4.2: Certificates	[http://mobius.inria.fr]	2007
MOBIUS Consortium07b	MOBIUS Consortium	Deliverable 4.3: Intermediate report on proof-transforming compiler	[http://mobius.inria.fr]	2007
Cre06	Pierre Cregut	Midlet navigation graphs	Unpublished draft	2006
dB08	L. de Moura and N. Bjørner	Z3: An efficient SMT solver	Proceedings of the Fourteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems	2008
FF00	C. Flanagan and S. N. Freund	Type-based race detection for Java	Programming Languages Design and Implementation, pages 219–232, New York, NY, USA, ACM Press	2000
FL00	C. Flanagan and K.R.M. Leino	Houdini, an annotation assistant for ESC/Java	Technical Report 2000-003, DEC-SRC	2000
Furnas86	G.W. Furnas	Generalized fisheye views	ACM SIGCHI Bulletin, 17(4):16–23	1986
GJSB05	J. Gosling, B. Joy, G. Steele, and G. Bracha	The Java Language Specification, Third Edition, chapter 17	Sun Microsystems [http://java.sun.com/docs/books/jls/]	2005
HM05	C. A. R. Hoare and J. Misra	Verified software: Theories, tools, experiments vision of a grand challenge project	A companion paper for VSTTE 2005, held in Zurich, Switzerland	2005
HO03	E. Hubbers and M. Oostdijk	Generating JML specifications from UML state diagrams	Forum on specification & Design Languages,pages 263–273. University of Frankfurt, Proceedings appeared as CD-Rom with ISSN 1636-9874	2003
HT08	M. Huisman and A. Tamalet	A formal connection between security automata and JML annotations	.	2008
Ini06	Unified Testing Initiative	Unified testing criteria for Java technology-based applications for mobile devices	Technical report, Sun Microsystems, Motorola, Nokia, Siemens, Sony Ericsson, Version 2.1	2006
Kin98	J. R. Kiniry	IDebug: An advanced debugging framework for Java	Technical Report CaltechCSTR:1998.cs-tr-98-16, California Institute of Technology	1998
Kin04	J. R. Kiniry	Formalizing the user’s context to support user interfaces for integrated mathematical environments	Electronic Notes in Theoretical Computer Science, 103	2004
KO03	J. R. Kiniry and S. Owre	Improving the PVS user interface	User Interfaces for Theorem Proving	September 2003
LPC+05	G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, and J. Kiniry	JML Reference Manual	In Progress. Department of Computer Science, Iowa State University. Available from [http://www.jmlspecs.org].	2005
ML06	M. Moskal and J. Lopuszanski	Fast quantifier reasoning with lazy proof explication.	[http://nemerle.org/malakith/smt/smt-tr-1.pdf]	2006
MR07a	P. Muller and A. Rudich	Formalization of ownership transfer in universe types	Technical Report 556, ETH Zurich	2007
MR07b	P. Muller and A. Rudich	Ownership transfer in universe types	ACM Conference on Object-Oriented Programming Systems, Languages, and Applications	2007
PBB+04	M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet	Enforcing high-level security properties for applets	P. Paradinas and J.-J. Quisquater, editors, CARDIS. Kluwer Academic Publishing	2004
Pic06	D. Pichardie	Bicolano – Byte Code Language in Coq	http://mobius.inria.fr/bicolano. Summary appears in [MOBIUS Consortium06b]	2006
SaB+08	A. Schubert, J. Chrzaszcz, T. Batkiewicz, J. Paszek, and W. Was	Technical aspects of class specification in the byte code of java language	To be published in Bytecode’08 proceedings, Electronic Notes in Theoretical Computer Science. Elsevier	2008
win08	.	The Wine user guide	Available via [http://www.winehq.org]	2008
WN95	K. Walden and J.M. Nerson	Seamless Object-Oriented Software Architecture - Analysis and Design of Reliable Systems	Prentice Hall	1995