@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} }