@STRING{ACM-FOOL = {ACM Workshop on Foundations of Object-Oriented Languages}}

@STRING{ACSC = {Asian Computing Science Conference}}

@STRING{APLSS = {Asian Programming Languages and Systems Symposium}}

@STRING{BYTECODE = {Bytecode Semantics, Verification, Analysis and Transformation}}

@STRING{CALP = {Colloquium on Automata, Languages and Programming}}

@STRING{CATS = {Computing, Australasian Theory Symposium}}

@STRING{COCV = {Compiler Optimization Meets Compiler Verification}}

@STRING{CRPIT = {Conference in Research and Practice in Information Technology}}

@STRING{CSFW = {Computer Security Foundations Workshop}}

@STRING{DCM = {Workshop on Developments in Computational Models}}

@STRING{EAAI = {Emerging Applications of Abstract Interpretation}}

@STRING{ECOOP = {European Conference on Object-Oriented Programming}}

@STRING{ENTCS = {Electronic Notes in Theoretical Computer Science}}

@STRING{ESHOL = {Empirically Successful Automated Reasoning in Higher-Order Logics}}

@STRING{ESOP = {European Symposium on Programming}}

@STRING{FAC = {Formal Aspects of Computing}}

@STRING{FMCO = {Formal Methods for Components and Objects}}

@STRING{FTFJP = {Workshop on Formal Techniques for Java Programs}}

@STRING{ICLP = {International Conference on Logic Programming}}

@STRING{ICSE = {International Conference on Software Engineering}}

@STRING{IJCAR = {International Joint Conference on Automated Reasoning}}

@STRING{ITS = {Issues in the Theory of Security}}

@STRING{ITS = {Workshop on the Issues in the Theory of Security}}

@STRING{JCS = {Journal of Computer Security}}

@STRING{LNAI = {Lecture Notes in Artificial Intelligence}}

@STRING{LNCS = {Lecture Notes in Computer Science}}

@STRING{LOPSTR = {Logic-based Program Synthesis and Transformation}}

@STRING{LPAR = {Logic for Programming Artificial Intelligence and Reasoning}}

@STRING{LPE = {Workshop on Logic Programming Environments}}

@STRING{OWASP = {Open Web Application Security Project}}

@STRING{PADL = {Symposium on Practical Aspects of Declarative Languages}}

@STRING{POPL = {Principles of Programming Languages}}

@STRING{PPDP = {Principle and Practice of Declarative Programming}}

@STRING{PPPJ = {Principles and Practices of Programming in Java}}

@STRING{PSI = {Andrei Ershov International Conference on Perspectives of System Informatics}}

@STRING{PUB-ACM = {Association of Computing Machinery Press}}

@STRING{PUB-AW = {Addison-Wesley Publishing Company}}

@STRING{PUB-COMPSCI = {IEEE Computer Society}}

@STRING{PUB-ESP = {Elsevier Science, Inc.}}

@STRING{PUB-IEEE = {IEEE Press}}

@STRING{PUB-SV = {Springer-Verlag}}

@STRING{SAC = {Symposium on Applied Computing}}

@STRING{SAS = {Static Analysis Symposium}}

@STRING{SECRET = {Workshop on Security and Rewriting Techniques}}

@STRING{SETDQ = {Software Engineering Techniques: Design for Quality}}

@STRING{SOS = {Workshop on Structured Operational Semantics}}

@STRING{SSP = {Symposium on Security and Privacy}}

@STRING{SV = {Springer-Verlag}}

@STRING{SVV = {Workshop on Software Verification and Validation}}

@STRING{TASE = {IEEE and IFIP Int.\ Symp.\ on Theoretical Aspects of Software Engineering}}

@STRING{TCS = {Theoretical Computer Science}}

@STRING{TGC = {Trustworthy Global Computing}}

@STRING{VSTTE = {Verified Software: Theories, Tools, Experiements}}

@STRING{WLPE = {Workshop on Logic-Based Methods in Programming Environments}}

@STRING{WRV = {Workshop on Runtime Verification}}

@INPROCEEDINGS{AlbertAGPZ07,
  author = {E. Albert and P. Arenas and S. Genaim and G. Puebla
                 and D. Zanardini},
  title = {Cost Analysis of Java Bytecode},
  booktitle = ESOP,
  year = {2007},
  editor = {Rocco De Nicola},
  series = LNCS,
  month = MAR,
  publisher = PUB-SV,
  note = {To appear},
  keywords = {mobius,wp2}
}

@INPROCEEDINGS{AlbertAP06,
  author = {E. Albert and P. Arenas and G. Puebla},
  title = {Incremental Certificates and Checkers for
                 Abstraction-Carrying Code},
  booktitle = ITS,
  year = {2006},
  month = MAR,
  npages = {16},
  keywords = {mobius}
}

@INPROCEEDINGS{AlbertAP06d,
  author = {E. Albert and P. Arenas and G. Puebla},
  title = {Some {I}ssues on {I}ncremental
                 {A}bstraction-{C}arrying {C}ode},
  booktitle = WLPE,
  year = {2006},
  month = AUG,
  npages = {15},
  keywords = {mobius}
}

@INPROCEEDINGS{AlbertAPH06,
  author = {E.~Albert and P. Arenas and G.~Puebla and M.
                 Hermenegildo},
  title = {Reduced Cerficates for Abstraction-Carrying Code},
  booktitle = ICLP,
  year = {2006},
  month = AUG,
  npages = {16},
  pages = {163--178},
  publisher = PUB-SV,
  series = LNCS,
  number = {4079},
  keywords = {mobius}
}

@INPROCEEDINGS{AlbertG-ZHP06,
  author = {E. Albert and M. G\'omez-Zamalloa and L. Hubert and G.
                 Puebla},
  title = {Towards {J}ava {B}ytecode {V}erification using {T}ools
                 for {L}ogic {P}rogramming},
  booktitle = SVV,
  year = {2006},
  month = AUG,
  npages = {15},
  keywords = {mobius}
}

@INPROCEEDINGS{AlbertPG05,
  author = {E.~Albert and G.~Puebla and J.~Gallagher},
  title = {{N}on-{L}eftmost {U}nfolding in {P}artial {E}valuation
                 of {L}ogic {P}rograms with {I}mpure {P}redicates},
  booktitle = LOPSTR,
  year = {2006},
  month = APR,
  publisher = PUB-SV,
  series = LNCS,
  number = {3901},
  npages = {16},
  keywords = {mobius}
}

@INPROCEEDINGS{AskarovHS06,
  author = {A. Askarov and D. Hedin and A. Sabelfeld},
  title = {Cryptographically-Masked Flows},
  booktitle = SAS,
  year = {2006},
  publisher = PUB-SV,
  series = LNCS,
  address = {Seoul, Korea},
  month = AUG,
  pdfurl = {http://www.cs.chalmers.se/~andrei/cryptoflows.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{AskarovS05,
  author = {A. Askarov and A. Sabelfeld},
  title = {Security-typed languages for implementation of
                 cryptographic protocols: {A} case study},
  booktitle = ESCORICS,
  year = {2005},
  publisher = PUB-SV,
  series = LNCS,
  address = {Milan, Italy},
  month = SEP,
  pdfurl = {http://www.cs.chalmers.se/~andrei/askarov-sabelfeld-esorics05.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{AskarovS07,
  author = {A. Askarov and A. Sabelfeld},
  title = {Gradual Release: Unifying Declassification, Encryption and Key Release Policies},
  booktitle = SSP,
  year = 2007,
  month = MAY,
  pdfurl = {http://www.cs.chalmers.se/~andrei/askarov-sabelfeld-sp07.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{AspinallBM,
  author = {D. Aspinall and L. Beringer and A. Momigliano},
  title = {Optimisation Validation},
  booktitle = COCV,
  year = {2006},
  series = ENTCS,
  publisher = PUB-ESP,
  pdfurl = {http://homepages.inf.ed.ac.uk/amomigl1/papers/OptVal.pdf},
  keywords = {mobius}
}

@MISC{Barthe05,
  author = {G. Barthe},
  title = {{MOBIUS} - Securing the Next Generation of Java-Based
                 Global Computers},
  year = {2005},
  month = SEP,
  pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/p28-29.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{BartheBCGHMPPSV06,
  author = {G.~Barthe and L.~Beringer and Pierre~Cr\'egut
                 and Benjamin~Gr\'egoire and Martin~Hofmann and
                 Peter~M{\"u}ller and Erik~Poll and Germ\'{a}n~Puebla
                 and I.~Stark and Eric~V\'etillard},
  title = {{MOBIUS}: Mobility, Ubiquity, Security. Objectives and progress report},
  booktitle = TGC,
  series = LNCS,
  publisher = {Springer-Verlag},
  year = {2006},
  keywords = {mobius, wp7},
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/tgc06.pdf}
}

@INPROCEEDINGS{BartheGKR06,
  author = {G. Barthe and Benjamin Gr\'{e}goire and Cesar Kunz
                 and Tamara Rezk},
  title = {Certificate Translation for Optimizing Compilers},
  booktitle = SAS,
  year = {2006},
  publisher = PUB-SV,
  series = LNCS,
  address = {Seoul, Korea},
  month = AUG,
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Cesar.Kunz/publications/certtrans-SAS06.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{BartheNR06,
  author = {G. Barthe and D. Naumann and T. Rezk},
  title = {Deriving an Information Flow Checker and Certifying
                 Compiler for {Java}},
  booktitle = SSP,
  pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/Barthe-Naumann-Rezk-SP06.pdf},
  year = {2006},
  publisher = PUB-IEEE,
  keywords = {mobius}
}

@INPROCEEDINGS{BarthePR07,
  title = {A Certified Lightweight Non-Interference Java Bytecode
                 Verifier},
  author = {G. Barthe and D. Pichardie and T. Rezk},
  booktitle = ESOP,
  publisher = {Springer},
  year = {2007},
  editor = {R. De Niccola},
  series = LNCS,
  keywords = {mobius},
  note = {To appear}
}

@INPROCEEDINGS{BeringerH06,
  author = {L. Beringer and Martin Hofmann},
  title = {A Bytecode Logic for {JML} and Types},
  booktitle = APLSS,
  pages = {389--405},
  year = {2006},
  series = LNCS # {~4279},
  publisher = SV,
  url = {http://www.tcs.informatik.uni-muenchen.de/~beringer/},
  doi = {10.1007/11924661_24},
  keywords = {mobius, wp3, wp2}
}

@INPROCEEDINGS{BessonDJ06,
  author = {F. Besson and G. Dufay and T. Jensen},
  title = {A Formal Model of Access Control for Mobile
                 Interactive Devices},
  booktitle = {ESORICS},
  year = {2006},
  address = {Hamburg},
  month = SEP,
  publisher = {Springer Verlag},
  note = {To appear},
  keywords = {mobius, wp1},
  abstract = {This paper presents an access control model for
                 programming applications in which the access control to
                 resources can employ user interaction to obtain the
                 necessary permissions. This model is inspired by and
                 improves on the Java MIDP security architecture used in
                 Java-enabled mobile telephones. We consider access
                 control permissions with multiplicities in order to
                 allow to use a permission a certain number of times. An
                 operational semantics of the model and a formal
                 definition of what it means for an application to
                 respect the security model is given. A static analysis
                 which enforces the security model is defined and proved
                 correct. A constraint solving algorithm implementing
                 the analysis is presented.}
}

@INPROCEEDINGS{BurdyHP07,
  author = {L. Burdy and M. Huisman and M. Pavlova},
  title = {Preliminary Design of {BML}: {A} Behavioral Interface
                 Specification Language for {Java} bytecode},
  booktitle = {Fundamental Approaches to Software Engineering (FASE
                 2007)},
  publisher = SV,
  series = LNCS,
  volume = {4422},
  pages = {215--229},
  year = {2007},
  pdf = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/bml.pdf},
  keywords = {mobius,wp3}
}

@INPROCEEDINGS{BurdyP06,
  author = {L. Burdy and M. Pavlova},
  title = {Java bytecode specification and verification},
  booktitle = SAC,
  pages = {1835--1839},
  publisher = PUB-ACM,
  ee = {http://doi.acm.org/10.1145/1141277.1141708},
  crossref = {DBLP:conf/sac/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  year = {2006},
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{CarbobeHY06,
  title = {A Calculus of Global Interaction based on Session
                 Types},
  author = {K. Honda and M. Carbone and N. Yoshida},
  booktitle = DCM,
  month = JUL,
  year = {2006},
  url = {http://www.dcm-workshop.org.uk/2006},
  keywords = {mobius}
}

@INPROCEEDINGS{ChalinKLP06,
  author = {P. Chalin and J. R. Kiniry and G.T.
                 L. and Erik Poll},
  title = {Beyond Assertions: Advanced Specification and
                 Verification with {JML} and {ESC}/Java2},
  booktitle = FMCO,
  year = {2006},
  editor = PUB-SV,
  series = LNCS,
  pdfurl = {http://www.cs.ru.nl/~erikpoll/publications/fmco.pdf},
  keywords = {mobius, wp6}
}

@INPROCEEDINGS{Charles06,
  author = {J. Charles},
  title = {Adding Native Specifications to {JML}},
  booktitle = FTFJP,
  year = {2006},
  keywords = {mobius, wp1}
}

@INPROCEEDINGS{CieleckiFJJCSK06,
  author = {M. Cielecki and J. Fulara and K. Jakubczyk and {\L}.
                 Jancewicz and J. Chrz{\k a}szcz and A. Schubert and
                 {\L}. Kami{\'n}ski},
  title = {Propagation of {JML} non-null annotations in {Java}
                 Programs},
  editors = {R.~Gitzel and M.~Aleksy and M.~Schader and
                 Ch.~Krintz},
  booktitle = PPPJ,
  year = {2006},
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{CorreasPHB06,
  author = {J.~Correas and G.~Puebla and M.~Hermenegildo and
                 F.~Bueno},
  title = {{E}xperiments in {C}ontext-{S}ensitive {A}nalysis of
                 {M}odular {P}rograms},
  booktitle = LOPSTR,
  year = {2006},
  month = APR,
  publisher = PUB-SV,
  series = LNCS,
  number = {3901},
  npages = {16},
  keywords = {mobius}
}

@UNPUBLISHED{CunninghamDDEM06,
  author = {D. Cunningham and S. Drossopoulou and S.
                 Eisenbach and W. Dietl and P. M{\"u}ller},
  title = {{CUJ}: {U}niverse {T}ypes for {R}ace {S}afety},
  note = {Preliminary version at
                 \url{http://slurp.doc.ic.ac.uk/pubs.html\#cuj06}},
  url = {http://slurp.doc.ic.ac.uk/pubs.html\#cuj06},
  keywords = {mobius, wp2},
  optkey = {},
  optmonth = {},
  optyear = {},
  optannote = {}
}

@UNPUBLISHED{CunninghamDDFM06,
  author = {D. Cunningham and W. Dietl and S.
                 Drossopoulou and A. Francalanza and P.
                 M{\"u}ller},
  title = {{UJ}: {T}ype {S}oundness for {U}niverse {T}ypes},
  note = {To appear at
                 \url{http://slurp.doc.ic.ac.uk/pubs.html\#uj06}},
  url = {http://slurp.doc.ic.ac.uk/pubs.html\#uj06},
  keywords = {mobius, wp2},
  optkey = {},
  optmonth = {},
  optyear = {},
  optannote = {}
}

@TECHREPORT{DarvasM07,
  author = {Darvas, \'A. and M{\"u}ller, P.},
  title = {Formal encoding of {JML} {L}evel 0 specifications in \sc{Jive}},
  institution = {ETH Zurich},
  year = {2007},
  note = {To appear in the Annual Report of the Chair of Software Engineering},
  keywords = {mobius,wp3}
}

@INPROCEEDINGS{Dezani-CiancagliniMYD06,
  author = {M. Dezani-Ciancaglini and D. Mostrous
                 and N. Yoshida and S. Drossopoulou},
  title = {Session Types for Object-Oriented Languages},
  booktitle = ESOP,
  year = {2006},
  keywords = {mobius}
}

@UNPUBLISHED{DietlDM06,
  author = {W. Dietl and S. Drossopoulou and P. M{\"u}ller},
  title = {{GUJ}: {G}eneric {U}niverse {T}ypes},
  note = {Preliminary version available from
                 \url{http://www.sct.ethz.ch/publications/index.html}},
  url = {http://www.sct.ethz.ch/publications/index.html},
  keywords = {mobius, wp2},
  annote = {use DietlDM07 instead!}
}

@TECHREPORT{DietlDM06a,
  author = {W. Dietl and S. Drossopoulou and P. M{\"u}ller},
  title = {Formalization of {G}eneric {U}niverse {T}ypes},
  institution = {ETH Zurich},
  year = {2006},
  number = {532},
  keywords = {mobius, wp2}
}

@INPROCEEDINGS{DietlDM07,
  author = {W. Dietl and S. Drossopoulou and P. M{\"u}ller},
  title = {{G}eneric {U}niverse {T}ypes},
  booktitle = ECOOP,
  year = 2007,
  editor = {E. Ernst},
  series = LNCS,
  publisher = SV,
  note = {To appear},
  keywords = {mobius, wp2}
}

@INPROCEEDINGS{DietlDM07a,
  author = {W. Dietl and S. Drossopoulou and P. M{\"u}ller},
  title = {{G}eneric {U}niverse {T}ypes},
  booktitle = ACM-FOOL,
  month = {January},
  year = {2007},
  keywords = {mobius, wp2}
}

@INPROCEEDINGS{FradeSU07,
  author = {M.J. Frade and A. Saabas and T. Uustalu},
  title = {Foundational Certification of Data-Flow Analyses},
  booktitle = TASE,
  year = 2007,
  publisher = PUB-COMPSCI,
  note = {to appear},
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{GallagherPA05,
  author = {J.~Gallagher and G.~Puebla and E.~Albert},
  title = {Converting one Type-Based Abstract Domain to Another},
  booktitle = LOPSTR,
  year = {2006},
  month = APR,
  publisher = PUB-SV,
  series = LNCS,
  number = {3901},
  npages = {16},
  keywords = {mobius}
}

@INPROCEEDINGS{HaackPSS07,
  author = {C. Haack and E. Poll and J. Sch{\"{a}}fer and A.
                 Schubert},
  title = {Immutable Objects for a {J}ava-like Language},
  booktitle = ESOP,
  pages = {347--362},
  year = {2007},
  editor = {R. De Nicola},
  volume = {4421},
  series = {LNCS},
  publisher = PUB-SV,
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{HahnleG06,
  author = {R. H{\"{a}}hnle and T. Gedell},
  year = {2006},
  publisher = PUB-SV,
  series = LNCS,
  title = {Automating Verification of Loops by Parallelization},
  booktitle = LPAR,
  month = NOV,
  editor = {M. Hermann},
  keywords = {mobius}
}

@INPROCEEDINGS{HondaBY06,
  author = {K. Honda and M. Berger and N. Yoshida},
  title = {Descriptive and Relative Completeness of Logics for
                 Higher-Order Functions},
  booktitle = CALP,
  series = LNCS,
  publisher = PUB-SV,
  month = JUL,
  year = {2006},
  keywords = {mobius}
}

@INPROCEEDINGS{HuismanWS06,
  author = {M. Huisman and P. Worah and K. Sunesen},
  title = {A temporal logic characterisation of observational
                 determinism},
  booktitle = CSFW,
  year = {2006},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/personnel/Marieke.Huisman/obsequiv_char.pdf},
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{HuntS06,
  author = {S. Hunt and D. Sands},
  url = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/Hunt-Sands-POPL06.pdf},
  title = {On Flow-Sensitive Security Types},
  booktitle = POPL,
  address = {Charleston, South Carolina, USA},
  month = JAN,
  year = {2006},
  publisher = PUB-ACM,
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{KiniryCH05,
  author = {J.R. Kiniry and P. Chalin and C.
                 Hurlin},
  title = {Integrating Static Checking and Interactive
                 Verification: Supporting Multiple Theories and Provers
                 in Verification},
  booktitle = VSTTE,
  pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/KiniryChalinHurlin_VSTTE05.pdf},
  year = {2005},
  address = {Zurich, Switzerland},
  month = OCT,
  keywords = {mobius,wp3}
}

@ARTICLE{LaudUV05,
  author = {P. Laud and T. Uustalu and V. Vene},
  title = {Type Systems Equivalent to Data-Flow Analyses for
                 Imperative Languages},
  journal = TCS,
  year = {2006},
  volume = 364,
  number = 3,
  pages = {292--310},
  doi = {10.1016/j.tcs.2006.08.013},
  pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/laud-uustalu-vene-appsem05-tcs.pdf},
  keywords = {mobius}
}

@ARTICLE{LeavensLM07,
  author = {G. T. Leavens and K. R. M. Leino and P. M{\"u}ller},
  title = {Specification and verification challenges for
                 sequential object-oriented programs},
  journal = FAC,
  year = {2007},
  note = {Accepted for publication},
  keywords = {mobius, wp3}
}

@PROCEEDINGS{LeavensM07,
  author = {G. T. Leavens and P. M{\"u}ller},
  title = {Information Hiding and Visibility in Interface Specifications},
  year = {2007},
  booktitle = ICSE,
  note = {To appear},
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{LehnerM07,
  author = {H. Lehner and P. M{\"u}ller},
  title = {{F}ormal {T}ranslation of {B}ytecode into
                 {B}oogie{PL}},
  booktitle = BYTECODE,
  editor = {M. Huisman and F. Spoto},
  year = {2007},
  series = ENTCS,
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{LeinoM06,
  author = {K.R.M. Leino and P. M{\"u}ller},
  title = {A verification methodology for model fields},
  booktitle = ESOP,
  editor = {P. Sestoft},
  volume = {3924},
  pages = {115--130},
  year = {2006},
  series = LNCS,
  publisher = PUB-SV,
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{MantelR07,
  author = {H. Mantel and A. Reinhard},
  title = {Controlling the What and Where of Declassification in Language-Based Security},
  booktitle = ESOP,
  year = {2007},
  editor = {R. De Nicola},
  series = LNCS,
  volume = {4421},
  isbn = {978-3-540-71314-2},
  publisher = PUB-SV,
  keywords = {mobius,wp2},
  pages = {141--156}
}

@INPROCEEDINGS{MantelSK06,
  author = {H. Mantel and H. Sudbrock and T. Krau�r},
  title = {Combining Different Proof Techniques for Verifying
                 Information Flow Security},
  booktitle = LOPSTR,
  year = {2006},
  editor = {G. Puebla},
  volume = {Raporta di Ricerca CS-2006-5, Universit{\`a}
                 Ca'~Foscari Di Venezia},
  address = {Venice, Italy},
  month = JUL # { 12--14},
  keywords = {mobius},
  abstract = {When giving a program access to secret information,
                 one must ensure that the program does not leak the
                 secrets to untrusted sinks. For reducing the complexity
                 of such an information flow analysis, one can employ
                 compositional proof techniques. In this article, we
                 present a new approach to analyzing information flow
                 security in a compositional manner. Instead of
                 committing to a proof technique at the beginning of a
                 verification, this choice is made during verification
                 with the option of flexibly migrating to another proof
                 technique. Our approachalso increases the precision of
                 compositional reasoning in comparison to the
                 traditional approach. We illustrate the advantages in
                 two exemplary security analyses, on the semantic level
                 and on the syntactic level.}
}

@INPROCEEDINGS{MeraLPCH,
  author = {E. Mera and P. L\'{o}pez-Garc\'{\i}a and G. Puebla and
                 M. Carro and M. Hermenegildo},
  title = {{U}sing {C}ombined {S}tatic {A}nalysis and {P}rofiling
                 for {L}ogic {P}rogram {E}xecution {T}ime {E}stimation},
  booktitle = ICLP,
  npages = {2},
  year = {2006},
  month = AUG,
  publisher = PUB-SV,
  series = LNCS,
  number = {4079},
  keywords = {mobius}
}

@INPROCEEDINGS{MeraLPCH06,
  author = {E. Mera and P. L\'{o}pez-Garc\'{\i}a and G. Puebla and
                 M. Carro and M. Hermenegildo},
  title = {{T}owards {E}xecution {T}ime {E}stimation for {L}ogic
                 {P}rograms via {S}tatic {A}nalysis and {P}rofiling},
  booktitle = LPE,
  pages = {16},
  year = {2006},
  month = AUG,
  keywords = {mobius}
}

@INPROCEEDINGS{MeraLPCH07,
  author = {E. Mera and P. L\'{o}pez-Garc\'{\i}a and G. Puebla and
                 M. Carro and M. Hermenegildo},
  title = {{C}ombining {S}tatic {A}nalysis and {P}rofiling for
                 {E}stimating {E}xecution {T}imes},
  booktitle = PADL,
  npages = {15},
  year = {2007},
  month = JAN,
  publisher = PUB-SV,
  series = LNCS,
  paper_presentation_city = {Nice},
  paper_presentation_country = {France},
  note = {To appear},
  keywords = {mobius, wp2}
}

@INPROCEEDINGS{Miller06a,
  author = {D. Miller},
  title = {Representing and reasoning with operational
                 semantics},
  booktitle = IJCAR,
  month = AUG,
  year = {2006},
  pages = {4--20},
  editor = {U. Furbach and N. Shankar},
  series = LNAI,
  volume = {4130},
  keywords = {mobius},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcat06.pdf},
  dvi = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcat06.dvi}
}

@INPROCEEDINGS{Miller06b,
  author = {D. Miller},
  title = {Collection analysis for {Horn} clause programs},
  booktitle = PPDP,
  month = JUL,
  pages = {179--188},
  year = {2006},
  keywords = {mobius},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ppdp06.pdf},
  ps = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ppdp06.ps}
}

@UNPUBLISHED{MobiusDeliverable1.1,
  author = {Mobius Consortium},
  title = {Deliverable~1.1: Resource and Information Flow
                 Security Requirements},
  year = {2006},
  keywords = {mobius, wp1},
  note = {Available online from \url{http://mobius.inria.fr}}
}

@UNPUBLISHED{MobiusDeliverable1.2,
  author = {Mobius Consortium},
  title = {Deliverable~1.2: Framework-Specific and
                 Application-Specific Security Requirements},
  year = {2006},
  keywords = {mobius, wp1},
  note = {Available online from \url{http://mobius.inria.fr}}
}

@UNPUBLISHED{MobiusDeliverable2.1,
  author = {Mobius Consortium},
  title = {Deliverable~2.1: Intermediate Report on Type Systems},
  year = {2006},
  keywords = {mobius, wp2},
  note = {Available online from \url{http://mobius.inria.fr}}
}

@UNPUBLISHED{MobiusDeliverable3.1,
  author = {Mobius Consortium},
  title = {Deliverable~3.1: Bytecode Specification Language and
                 Program Logic},
  year = {2006},
  keywords = {mobius, wp3},
  note = {Available online from \url{http://mobius.inria.fr}}
}

@UNPUBLISHED{MobiusDeliverable3.3,
  author = {Mobius Consortium},
  title = {Deliverable~3.3: Thread-Modular Verification},
  year = {2007},
  keywords = {mobius, wp3},
  note = {Available online from \url{http://mobius.inria.fr}}
}

@UNPUBLISHED{MobiusDeliverable4.1,
  author = {Mobius Consortium},
  title = {Deliverable~4.1: Scenarios for Proof-Carrying Code},
  year = {2006},
  keywords = {mobius, wp3},
  note = {Available online from \url{http://mobius.inria.fr}}
}

@UNPUBLISHED{MobiusDeliverable6.1,
  author = {Mobius Consortium},
  title = {Deliverable~6.1: Dissemination and Training Plan},
  year = {2006},
  month = MAR,
  keywords = {mobius, wp6},
  note = {Available online from \url{http://mobius.inria.fr}}
}

@TECHREPORT{MuellerR07,
  author = {P. M\"uller and A. Rudich},
  title = {Formalization of Ownership Transfer in {U}niverse {T}ypes},
  institution = {ETH Zurich},
  year = {2007},
  number = {556},
  keywords = {mobius, wp2}
}

@ARTICLE{MyersSZ06,
  author = {A. C. Myers and A. Sabelfeld and S. Zdancewic},
  title = {Enforcing Robust Declassification and Qualified
                 Robustness},
  year = {2006},
  journal = JCS,
  month = MAY,
  pages = {157--196},
  volume = {14},
  number = {2},
  pdfurl = {http://www.cs.chalmers.se/~andrei/msz-jcs.pdf},
  keywords = {mobius}
}

@MISC{OWASP,
  author = {Open Web Application Security Project Consortium},
  title = {The Top Ten Most Critical Web Application Security
                 Vulnerabilities -- 2004 Update},
  year = {2004},
  note = {Available from \url{http://www.owasp.org}}
}

@INPROCEEDINGS{OchoaPH06,
  author = {C.~Ochoa and G.~Puebla and M.~Hermenegildo},
  title = {{R}emoving {S}uperfluous {V}ersions in {P}olyvariant
                 {S}pecialization of {P}rolog {P}rograms},
  booktitle = LOPSTR,
  year = {2006},
  month = APR,
  npages = {17},
  publisher = PUB-SV,
  series = LNCS,
  number = {3901},
  keywords = {mobius}
}

@INPROCEEDINGS{PietrzakCPH06,
  author = {P. Pietrzak and J. Correas and G. Puebla and M.
                 Hermenegildo},
  title = {Context-Sensitive Multivariant Assertion Checking in
                 Modular Programs},
  booktitle = LPAR,
  year = {2006},
  month = NOV,
  npages = {15},
  publisher = PUB-SV,
  series = LNCS,
  pdfurl = {http://clip.dia.fi.upm.es/papers/imod-ctchecks-lpar06.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{PueblaAAH06,
  author = {G.~Puebla and E.~Albert and P. Arenas and M.
                 Hermenegildo},
  title = {On Abstraction-Carrying Code and Certificate-Size
                 Reduction},
  booktitle = EAAI,
  year = {2006},
  month = MAR,
  npages = {15},
  keywords = {mobius}
}

@INPROCEEDINGS{PueblaAH06,
  author = {G. Puebla and E. Albert and M.~Hermenegildo},
  title = {Abstract Interpretation with Specialized Definitions},
  booktitle = SAS,
  year = {2006},
  month = AUG,
  publisher = PUB-SV,
  series = LNCS,
  number = {4134},
  pages = {107--126},
  address = {Seoul, Korea},
  pdfurl = {http://clip.dia.fi.upm.es/papers/ai-with-specs-sas06.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{PueblaO06,
  author = {G.~Puebla and C.~Ochoa},
  title = {Poly-Controlled Partial Evaluation},
  booktitle = PPDP,
  year = {2006},
  month = JUL,
  npages = {12},
  publisher = PUB-ACM,
  keywords = {mobius}
}

@INPROCEEDINGS{RahamanRS06,
  author = {M. A.~Rahaman and M.~Rits and A.~Schaad},
  title = {An Inline Approach for Secure {SOAP} Requests},
  booktitle = OWASP,
  year = {2006},
  month = {Mai},
  keywords = {mobius,wp1}
}

@INPROCEEDINGS{RussoHNS06,
  author = {A. Russo and J. Hughes and D. Naumann and A.
                 Sabelfeld},
  title = {Closing Internal Timing Channels by Transformation},
  booktitle = ACSC,
  year = {2007},
  publisher = PUB-SV,
  series = LNCS,
  pdfurl = {http://www.cs.chalmers.se/~andrei/asian06.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{RussoS06a,
  author = {A. Russo and A. Sabelfeld},
  title = {Securing interaction between threads and the
                 scheduler},
  booktitle = CSFW,
  pages = {177--189},
  year = {2006},
  pdfurl = {http://www.cs.chalmers.se/~andrei/russo-sabelfeld-csfw06.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{RussoS06b,
  author = {A. Russo and A. Sabelfeld},
  title = {Security for Multithreaded Programs under Cooperative
                 Scheduling},
  booktitle = PSI,
  year = {2006},
  volume = {4378},
  publisher = PUB-SV,
  series = LNCS,
  month = JUN,
  pdfurl = {http://www.cs.chalmers.se/~andrei/russo-sabelfeld-psi06.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{SaabasU06a,
  author = {A. Saabas and T. Uustalu},
  title = {Compositional Type Systems for Stack-Based Low-Level
                 Languages},
  editor = {B. Jay and J. Gudmundsson},
  booktitle = CATS,
  series = CRPIT,
  volume = {51},
  pages = {27--39},
  year = {2006},
  publisher = {Australian Computer Society},
  pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/saabas-uustalu-cats06.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{SaabasU06b,
  author = {A. Saabas and T. Uustalu},
  title = {A Compositional Natural Semantics and {H}oare Logic for
                 Low-Level Languages},
  editor = {P. D. Mosses and I. Ulidowski},
  booktitle = SOS,
  series = {Electron. Notes in Theor. Comput. Sci.},
  volume = {156(1)},
  pages = {151--168},
  year = {2006},
  publisher = PUB-ESP,
  pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/saabas-uustalu-sos05.pdf},
  keywords = {mobius}
}

@UNPUBLISHED{SaabasU06c,
  author = {A. Saabas and T. Uustalu},
  title = {Program and Proof Optimizations with Type Systems},
  note = {Submitted},
  year = {2006},
  keywords = {mobius, wp4}
}

@INPROCEEDINGS{SaabasU07,
  author = {A. Saabas and T. Uustalu},
  title = {Type Systems for Optimizing Stack-Based Code},
  booktitle = BYTECODE,
  year = {2007},
  keywords = {mobius, wp4},
  note = {To appear}
}

@ARTICLE{SaabasU07b,
  author = {A. Saabas and T. Uustalu},
  title = {A Compositional Natural Semantics and {H}oare Logic for
                 Low-Level Languages},
  journal = TCS,
  volume = 373,
  number = 3,
  pages = {273--302},
  year = 2007,
  doi = {10.1016/j.tcs.2006.12.020},
  keywords = {mobius}
}

@INPROCEEDINGS{SchubertC06,
  author = {A. Schubert and J. Chrz\k aszcz},
  title = {{ESC/Java2} as a Tool to Ensure Security in the Source
                 Code of {Java} Applications},
  booktitle = SETDQ,
  series = {IFIP},
  publisher = PUB-SV,
  year = {2006},
  address = {Warsaw},
  keywords = {mobius, wp3}
}

@INPROCEEDINGS{TiuNM05,
  author = {A. Tiu and G. Nadathur and D. Miller},
  title = {Mixing Finite Success and Finite Failure in an
                 Automated Prover},
  booktitle = ESHOL,
  pages = {79--98},
  year = {2005},
  month = DEC,
  pdfurl = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/eshol05.pdf},
  keywords = {mobius}
}

@MISC{Uustalu05,
  author = {T. Uustalu},
  howpublished = {Article in TUT newspaper, Mente \& Manu},
  year = {2005},
  month = NOV,
  pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/mente-manu.pdf},
  keywords = {mobius}
}

@INPROCEEDINGS{VasconcelosY06,
  title = {Language Primitives and Type Discipline for Structured
                 Communication-Based Programming Revisited},
  author = {V. Vasconcelos and N. Yoshida},
  booktitle = SECRET,
  month = JUL,
  year = {2006},
  url = {http://secret2006.loria.fr/},
  keywords = {mobius}
}

@INPROCEEDINGS{WangS03,
  author = {L. Wang and S. Stoller},
  title = {Run-Time Analysis for Atomicity},
  month = JUL,
  year = {2003},
  booktitle = WRV,
  series = ENTCS,
  publisher = PUB-ESP,
  volume = {89(2)},
  keywords = {mobius, wp3}
}

@BOOK{WarmerK99,
  author = {J. Warmer and A. Kleppe},
  title = {The Object Constraint Language: Precise Modeling with
                 {UML}},
  publisher = PUB-AW,
  year = {1999},
  review = {},
  keywords = {mobius, wp4}
}