Start of topic | Skip to actions
Publications
Search for a bibliography entry:Results found:
366 entries found in Publications/publis.bib:
(details: wp1: 6; wp2: 99; wp3: 84; wp4: 93; wp5: 7; wp6: 10; others: 7)
(details: wp1: 6; wp2: 99; wp3: 84; wp4: 93; wp5: 7; wp6: 10; others: 7)
| [SummersDrossopoulou10] |
A. J. Summers and S. Drossopoulou.
Considerate reasoning and the composite design pattern.
In VMCAI 2010, 2010. [ bib ]
Keywords: mobius, wp3 |
| [MacKenzie09] |
Kenneth Mac Kenzie?.
Resource analysis for iterative Java programs via lattice-point
enumeration in polytopes.
Technical Report EDI-INF-RR-1341, School of Informatics, University
of Edinburgh, August 2009. [ bib ]
Keywords: mobius, wp2 |
| [MostowskiP09] |
Wojciech Mostowski and Erik Poll.
Midlet Navigation Graphs in JML.
Technical Report ICIS-R09004, Radboud University Nijmegen, August
2009.
Available at
https://pms.cs.ru.nl/iris-diglib/src/getContent.php?id=2009-Mostowski-MidletGraphs. [ bib ]
Keywords: mobius, wp5 |
| [HurlinBS09] |
C. Hurlin, F. Bobot, and A. J. Summers.
Size does matter: Two certified abstractions to disprove entailment
in intuitionistic and classical separation logic.
In International Workshop on Aliasing, Confinement and Ownership
in object-oriented programming. ACM Digital Library, July 2009. [ bib ]
Keywords: mobius,wp3 |
| [MeraLH09] |
E. Mera, P. López-García, and M. Hermenegildo.
Integrating software testing and run-time checking in an assertion
verification framework.
In International Conference on Logic Programming, Lecture Notes
in Computer Science. Springer-Verlag, July 2009. [ bib ]
Keywords: mobius, wp2 |
| [AlbertGG09] |
E. Albert, S. Genaim, and M. Gómez-Zamalloa.
Live heap space analysis for languages with garbage collection.
In ISMM'09: Proceedings of the 8th International Symposium on
Memory Management, New York, NY, USA, June 2009. ACM Press. [ bib | .pdf ]
Keywords: mobius,wp2 |
| [BartheGKR09] |
G. Barthe, B. Grégoire, C. Kunz, and T. Rezk.
Certificate translation for optimizing compilers.
ACM Transactions on Programming Languages and Systems,
31(5):18:1-18:45, June 2009. [ bib | http ]
Keywords: mobius, wp4 |
| [FularaJ09] |
J. Fulara and K. Jakubczyk.
Practically applicable formal methods.
In
http://www.mimuw.edu.pl/~fulara/CodeStatistics/loopconditions.pdf, June
2009. [ bib ]
Keywords: mobius, wp3 |
| [MarronKH09] |
M. Marron, D. Kapur, and M.Hermenegildo.
Identification of logically related heap regions.
In ISMM'09: Proceedings of the 8th International Symposium on
Memory Management, New York, NY, USA, June 2009. ACM Press. [ bib | .pdf ]
Keywords: mobius,wp2 |
| [SummersDrossopoulouMueller09] |
A. J. Summers, S. Drossopoulou, and P. Müller.
Universe-type-based verification techniques for mutable static fields
and methods.
Journal of Object Technology (JOT), 8(4), June 2009. [ bib ]
Keywords: mobius, wp3 |
| [Hurlin09] |
C. Hurlin.
Specifying and checking protocols of multithreaded classes.
In Symposium on Applied Computing, pages 587-592. ACM Press,
March 2009. [ bib ]
Keywords: mobius, wp3 |
| [NavasMH09] |
J. Navas, M. Méndez-Lojo, and M. Hermenegildo.
User-definable resource usage bounds analysis for Java bytecode.
In Proceedings of the Workshop on Bytecode Semantics,
Verification, Analysis and Transformation (BYTECODE'09), Electronic Notes in
Theoretical Computer Science. Elsevier - North Holland, March 2009. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [APLAS09] |
Programming Languages and Systems: Proceedings of the 7th Asian Symposium
APLAS 2009, Seoul, Korea 14-16 December 2009, Lecture Notes in Computer
Science. Springer-Verlag, 2009.
To appear. [ bib ] |
| [ARSPA-WITS09] |
Foundations and Applications of Security Analysis: Revised Selected Papers
from the Joint Workshop on Automated Reasoning for Security Protocol Analysis
and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March
28-29, 2009, number 5511 in Lecture Notes in Computer Science.
Springer-Verlag, 2009. [ bib ] |
| [AhrendtBH09] |
W. Ahrendt, R. Bubel, and R. Hähnle.
Integrated and tool-supported teaching of testing, debugging, and
verification.
In Second International Conference on Teaching Formal Methods,
Eindhoven, Netherlands. Springer-Verlag, 2009.
To appear. [ bib | .pdf ]
Keywords: mobius, wp6 |
| [AlbertAAGP09] |
E. Albert, D. Alonso, P. Arenas, S. Genaim, and G. Puebla.
Asymptotic resource usage bounds.
In Programming Languages and Systems: Proceedings of the 7th
Asian Symposium APLAS 2009 [APLAS09].
To appear. [ bib ]
Keywords: mobius,wp4 |
| [AlbertAGGPRRZ09] |
E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, G. Puebla,
D. Ramírez, G. Román, and D. Zanardini.
Termination and cost analysis with COSTA and its user interfaces.
In Spanish Conference on Programming and Computer Languages.
Electronic Notes in Theoretical Computer Science, 2009.
To appear. [ bib | .pdf ]
Keywords: mobius,wp2 |
| [AlbertAGHP09] |
E. Albert, P. Arenas, S. Genaim, I. Herraiz, and G. Puebla.
Comparing cost functions in resource analysis.
In FOPARA '09: Proceedings of the International Workshop on
Foundational and Practical Aspects of Resource Analysis, 2009. [ bib ]
Keywords: mobius,wp4 |
| [AlbertAGP09] |
E. Albert, P. Arenas, S. Genaim, and G. Puebla.
Closed-form upper-bounds in static cost analysis.
Journal of Automated Reasoning, 2009.
Submitted for publication. [ bib ]
Keywords: mobius, wp2 |
| [AlbertAGP09b] |
E. Albert, P. Arenas, S. Genaim, and G. Puebla.
Field-sensitive value analysis by field-insensitive analysis.
In 16th International Symposium on Formal Methods (FM2009),
number To appear in Lecture Notes in Computer Science, 2009. [ bib | .pdf ]
Keywords: mobius,wp5 |
| [AlbertAGPZ09] |
E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini.
Resource usage analysis and its application to resource
certification.
In Foundations of Security Analysis and Design. FOSAD 2008/2009
Tutorial Lectures, LNCS. Springer-Verlag, To appear. 2009. [ bib | .pdf ]
Keywords: mobius,wp2 |
| [AlbertAGPZ09b] |
E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini.
Cost analysis of object-oriented bytecode programs.
ACM Transactions on Programming Languages and Systems, 2009.
Submitted for publication. [ bib ]
Keywords: mobius, wp2 |
| [BartheRRS09] |
G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld.
Security of multithreaded programs by compilation.
ACM Transactions Information and Systems Security, 2009.
http://www.cse.chalmers.se/~russo/. [ bib ]
Keywords: mobius, wp2 |
| [BejleriY09] |
Andi Bejleri and Nobuko Yoshida.
Synchronous multiparty session types.
Electr. Notes Theor. Comput. Sci., 241:3-33, 2009. [ bib ]
Keywords: mobius, wp2 |
| [BubelHW09] |
Richard Bubel, Reiner Hähnle, and Benjamin Weiß.
Abstract interpretation of symbolic execution with explicit state
updates.
In Springer-Verlag, editor, Formal Methods for Components and
Objects, Lecture Notes in Computer Science, 2009.
Accepted to FMCO'08 post proceedings (to appear). [ bib | .pdf ]
Keywords: mobius, wp3 |
| [Campbell09] |
Brian Campbell.
Amortised memory analysis using the depth of data structures.
In ESOP 2009 [ESOP09], pages 190-204. [ bib | http ]
Keywords: mobius, wp2 |
| [ChrzaszczHS09] |
J. Chrz aszcz, M. Huisman, and A. Schubert.
BML and related tools.
In Formal Methods for Components and Objects, number 5751 in
Lecture Notes in Computer Science, pages 278-297. Springer-Verlag, 2009. [ bib | .pdf ]
Keywords: mobius, wp3, wp4 |
| [DezaniMYD08] |
Mariangiola Dezani-Ciancaglini, Sophia Drossopoulou, Dimitris Mostrous, and
Nobuko Yoshida.
Objects and session types.
Information and Computation, 207(5):595-641, 2009. [ bib ]
Keywords: mobius, wp4 |
| [DrossopoulouFrancalanzaMuellerSummers10] |
S. Drossopoulou, A. Francalanza, P. Müller, and A. J. Summers.
A unified framework for verification techniques for object
invariants.
ACM Transactions on Programming Languages and Systems, 2009.
accepted, to appear. [ bib ]
Keywords: mobius, wp3 |
| [ESOP09] |
Programming Languages and Systems: Proceedings of the 18th European
Symposium on Programming, ESOP 2009, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2009, York, UK,
March 22-29, 2009, number 5502 in Lecture Notes in Computer Science.
Springer-Verlag, 2009. [ bib ] |
| [FTP09] |
FTP 2009: Proceedings of the International Workshop on First-Order Theorem
Proving, Oslo, Norway, July 2009, number 386 in University of Oslo
Department of Informatics Research Report, 2009. [ bib ] |
| [FischerSU09] |
B. Fischer, A. Saabas, and T. Uustalu.
Program repair as sound optimization of broken programs.
In IEEE and IFIP Int. Symp. on Theoretical Aspects of Software
Engineering, pages 165-173. IEEE Press, 2009. [ bib ]
Keywords: mobius, wp3 |
| [FradeSU09] |
M. J. Frade, A. Saabas, and T. Uustalu.
Bidirectional data-flow analyses, type-systematically.
In ACM SIGPLAN Workshop on Partial Evaluation and
Semantics-based Program Manipulation, pages 141-149. ACM Press, 2009. [ bib ]
Keywords: mobius, wp3 |
| [GeorgievaM09] |
Lilia Georgieva and Patrick Maier.
Inductive reasoning for shape invariants.
In FTP 2009: Proceedings of the International Workshop on
First-Order Theorem Proving [FTP09], pages 75-89. [ bib ]
Keywords: mobius, wp2 |
| [GrigoreCFK09] |
R. Grigore, J. Charles, F. Fairmichael, and J.R. Kiniry.
Strongest Postcondition of Unstructured Programs.
In Workshop on Formal Techniques for Java Programs, 2009. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [GurovH09] |
D. Gurov and M. Huisman.
Reducing behavioural to structural properties of programs with
procedures.
In Verification, Model Checking and Abstract Interpretation,
volume 5403 of Lecture Notes in Computer Science, pages 136-150.
Springer-Verlag, 2009. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [HaackPoll2009] |
C. Haack and E. Poll.
Type-based object immutability with flexible initialization.
In European Conference on Object-Oriented Programming, volume
5653 of Lecture Notes in Computer Science, pages 520-545. Springer,
2009. [ bib ]
Keywords: mobius, wp3 |
| [HaackPoll2009a] |
C. Haack and E. Poll.
Type-based object immutability with flexible initialization (long
version).
Technical Report ICIS-R09001, Radboud University Nijmegen, 2009. [ bib ]
Keywords: mobius, wp3 |
| [HondaVY09] |
Kohei Honda, Vasco Thudichum Vasconcelos, and Nobuko Yoshida.
Type-directed compilation for multicore programming.
Electr. Notes Theor. Comput. Sci., 241:101-111, 2009. [ bib ]
Keywords: mobius, wp4 |
| [Huisman09] |
M. Huisman.
On the interplay between the semantics of java's finally clauses and
the jml run-time checker.
In A. Banerjee, editor, Workshop on Formal Techniques for Java
Programs. ACM, 2009. [ bib | .pdf ]
Keywords: mobius, WP3 |
| [HuismanT09] |
M. Huisman and A. Tamalet.
A formal connection between security automata and JML annotations.
In Fundamental Approaches to Software Engineering, volume 5503
of Lecture Notes in Computer Science, pages 340-354. Springer-Verlag,
2009. [ bib | .pdf ]
Keywords: mobius, WP3 |
| [Hurlin09b] |
C. Hurlin.
Automatic parallelization and optimization of programs by proof
rewriting.
In Static Analysis Symposium, volume 5673 of Lecture Notes
in Computer Science, pages 52-68. Springer-Verlag, 2009. [ bib ]
Keywords: mobius,wp3 |
| [HurlinPhd] |
C. Hurlin.
Specification and Verification of Multithreaded Object-Oriented
Programs with Separation Logic.
Ph D? thesis, Université Nice Sophia Antipolis, 2009. [ bib ]
Keywords: mobius,wp3 |
| [KaegiLM09] |
A. Kägi, H. Lehner, and P. Müller.
A formalization of JML in the Coq proof system.
Technical report, ETH Zurich, 2009.
Available as technical report from
http://www.pm.inf.ethz.ch/people/lehnerh/jmlcoq. [ bib ]
Keywords: mobius, wp4 |
| [KeighrenAS09] |
Gavin Keighren, David Aspinall, and Graham Steel.
Towards a type system for security APIs.
In Foundations and Applications of Security Analysis: Selected
Papers from ARSPA-WITS 2009 [ARSPA-WITS09], pages 173-192. [ bib ]
Keywords: mobius, wp2 |
| [KiniryF09] |
J.R. Kiniry and F. Fairmichael.
Ensuring consistency between designs, documentation, formal
speciÞcations, and implementations.
In International Symposium on Component Based Software
Engineering, 2009. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [LADC09] |
Dependable Computing: Proceedings of the Fourth Latin American Symposium
LADC 2009, Joao Pessoa, Paraíba, Brazil, September 1-4, 2009,
2009. [ bib ] |
| [LoidlMJB09] |
Hans-Wolfgang Loidl, Kenneth Mac Kenzie?, Steffen Jost, and Lennart Beringer.
A proof-carrying-code infrastructure for resources.
In Dependable Computing: Proceedings of the Fourth Latin
American Symposium LADC 2009 [LADC09]. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [LuxM09a] |
A. Lux and H. Mantel.
Who can declassify?
In P. Degano, J. Guttman, and F. Martinelli, editors, Workshop
on Formal Aspects in Security and Trust, volume 5491 of Lecture Notes
in Computer Science, pages 35-49. Springer-Verlag, 2009. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [LuxM2009b] |
A. Lux and H. Mantel.
Declassification with explicit reference points.
In M. Backes and P. Ning, editors, European Symposium On
Research In Computer Security, volume 5789 of Lecture Notes in Computer
Science, pages 69-85. Springer-Verlag, 2009. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [Maier09] |
Patrick Maier.
Deciding extensions of the theories of vectors and bags.
In Jones and Müller-Olm [VMCAI09], pages 245-259. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [MobiusDeliverable2.7] |
Consortium.
Deliverable 2.7: Report on advanced resource policies, 2009.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp2 |
| [MobiusDeliverable4.7] |
Consortium.
Deliverable 4.7: Report on on-device checking, 2009.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp4 |
| [MobiusDeliverable5.2] |
Consortium.
Deliverable 5.2: Evaluation of type based and logical verification
technology, 2009. [ bib ]
Keywords: mobius, wp5 |
| [MostrousY09] |
D. Mostrous and N. Yoshida.
Session-based communication optimisations for higher-order mobile
processes.
In Typed Lambda Calculi and Applications, volume 5608 of
Lecture Notes in Computer Science, pages 203-218. Springer-Verlag, 2009. [ bib ]
Keywords: mobius, wp4 |
| [MostrousYH09] |
D. Mostrous, N. Yoshida, and K. Honda.
Global principal typing in partially commutative asynchronous
sessions.
In G. Castagna, editor, European Symposium on Programming,
volume 5502 of Lecture Notes in Computer Science, pages 316-332.
Springer-Verlag, 2009. [ bib ]
Keywords: mobius, wp4 |
| [NakataU09] |
K. Nakata and T. Uustalu.
Trace-based coinductive semantics for While: Big-step and
small-step, relational and functional styles.
In T. Nipkow and C. Urban, editors, Theorem Proving in
Higher-Order Logics, volume 5674 of Lecture Notes in Computer Science,
pages 375-390. Springer-Verlag, 2009. [ bib ]
Keywords: mobius, wp4 |
| [NakataU09b] |
K. Nakata and T. Uustalu.
A Hoare logic for the coinductive trace-based big-step semantics of
While.
Manuscript, submitted, 2009. [ bib ]
Keywords: mobius, wp4 |
| [PuglieseTY09] |
Rosario Pugliese, Francesco Tiezzi, and Nobuko Yoshida.
A symbolic semantics for a calculus for service-oriented computing.
Electr. Notes Theor. Comput. Sci., 241:135-164, 2009. [ bib ]
Keywords: mobius, wp4 |
| [SaabasU09] |
A. Saabas and T. Uustalu.
Proof optimization for partial redundancy elimination.
Journal of Logic and Algebraic Programming, 78(7):620-643,
2009. [ bib ]
Keywords: mobius, wp3, wp4 |
| [SummersDM09] |
Alexander J. Summers, S. Drossopoulou, and P. Müller.
A universe-type-based verification technique for mutable static
fields and methods.
In Journal of Object Technology, 2009. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [SummersDM09b] |
Alexander J. Summers, S. Drossopoulou, and P. Müller.
The need for flexible object invariants.
In International Workshop on Aliasing, Confinement and Ownership
in object-oriented programming, 2009. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [SummersDrossopoulouMueller09a] |
A. J. Summers, S. Drossopoulou, and P. Müller.
The need for flexible object invariants.
In International Workshop on Aliasing, Confinement and Ownership
in object-oriented programming (IWACO), 2009. [ bib ]
Keywords: mobius, wp3 |
| [VMCAI09] |
Neil D. Jones and Markus Müller-Olm, editors.
Verification, Model Checking, and Abstract Interpretation, 10th
International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20,
2009, volume 5403 of Lecture Notes in Computer Science.
Springer-Verlag, 2009. [ bib ] |
| [YoshidaVPH08] |
N. Yoshida, V. Vasconcelos, H. Paulino, and K. Honda.
Session-based compilation framework for multicore programming.
In Formal Methods for Components and Objects, Lecture Notes in
Computer Science. Springer-Verlag, 2009. [ bib ]
Keywords: mobius, wp4 |
| [HaackHH08] |
C. Haack, M. Huisman, and C. Hurlin.
Reasoning about Java's reentrant locks.
In G. Ramalingam, editor, Asian Programming Languages and
Systems Symposium, volume 5356 of Lecture Notes in Computer Science,
pages 171-187. Springer-Verlag, December 2008. [ bib | .pdf ]
Keywords: mobius, WP3 |
| [AskarovHS08] |
A. Askarov, D. Hedin, and A. Sabelfeld.
Cryptographically-masked flows.
Theoretical Computer Science, 402:82-101, August 2008.
Special issue for TGC 2006. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [BubelHS08] |
R. Bubel, R. Hähnle, and P.H. Schmitt.
Specification predicates with explicit dependency information.
In Proceedings of the 5th International Verification Workshop,
volume 372, pages 28-43. CEUR Workshop Proceedings, August 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [AlbertAGP08c] |
E. Albert, P. Arenas, S. Genaim, and G. Puebla.
Dealing with numeric fields in termination analysis of java-like
languages.
In Marieke Huisman, editor, 10th Workshop on Formal Techniques
for Java-like Programs, July 2008. [ bib ]
Keywords: mobius, wp4 |
| [AlbertAGPRZ08] |
E. Albert, P. Arenas, S. Genaim, G. Puebla, D. Ramírez, and D. Zanardini.
The COSTA cost and termination analyzer for java bytecode and its
web interface (tool demo).
In Anna Philippou, editor, 22nd European Conference on
Object-Oriented Programming, July 2008. [ bib ]
Keywords: mobius, wp4 |
| [GenaimS08] |
S. Genaim and F. Spoto.
Constancy analysis.
In Marieke Huisman, editor, 10th Workshop on Formal Techniques
for Java-like Programs, July 2008. [ bib ]
Keywords: mobius, wp2 |
| [HaackH08b] |
C. Haack and C. Hurlin.
Separation logic contracts for a Java-like language with fork/join.
In J. Meseguer and G. Rosu, editors, Algebraic Methodology and
Software Technology, volume 5140 of Lecture Notes in Computer Science,
pages 199-215. Springer-Verlag, July 2008. [ bib ]
Keywords: mobius, WP3 |
| [MeraLCH08] |
E. Mera, P. López-García, M. Carro, and M. Hermenegildo.
Towards execution time estimation in abstract machine-based
languages.
In 10th Int'l. ACM SIGPLAN Symposium on Principles and Practice
of Declarative Programming (PPDP'08), pages 174-184. ACM Press, July 2008. [ bib ]
Keywords: mobius, wp2 |
| [BartheCR08] |
G. Barthe, S. Cavadini, and T. Rezk.
Tractable enforcement of declassification policies.
In IEEE Computer Security Foundations Symposium, June 2008. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [AlbertAGPZ08b] |
E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini.
Removing Useless Variables in Cost Analysis of Java
Bytecode.
In SAC - Software Verification Track (SV08), pages 368-375,
Fortaleza, Brasil, March 2008. ACM Press, New York. [ bib ]
Keywords: mobius, wp4 |
| [APLAS08] |
G. Ramalingam, editor.
Programming Languages and Systems, 6th Asian Symposium, APLAS
2008, Bangalore, India, December 9-11, 2008. Proceedings, volume 5356 of
Lecture Notes in Computer Science. Springer, 2008. [ bib ] |
| [AlbertACGPZ08] |
Elvira Albert, Puri Arenas, Michael Codish, Samir Genaim, Germán Puebla,
and Damiano Zanardini.
Termination analysis of Java bytecode.
In FMOODS 2008 [FMOODS08], pages 2-18. [ bib ]
Keywords: mobius, wp2 |
| [AlbertAGP08] |
E. Albert, P. Arenas, S. Genaim, and G. Puebla.
Automatic inference of upper bounds for recurrence relations in cost
analysis.
In Mar'a Alpuente and Germán Vidal, editors, Static
Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July
15-17, 2008, Proceedings, number 5079 in Lecture Notes in Computer Science,
pages 221-237. Springer-Verlag, 2008. [ bib ]
Keywords: mobius, wp2 |
| [AlbertAGPZ08] |
E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini.
COSTA: A cost and termination analyzer for Java bytecode.
In BYTECODE, ENTCS. Elsevier, 2008.
To appear. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [AspinallMS07] |
David Aspinall, Patrick Maier, and Ian Stark.
Monitoring external resources in Java MIDP.
Electronic Notes in Theoretical Computer Science,
197(1):17-30, 2008. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [AspinallMS08] |
David Aspinall, Patrick Maier, and Ian Stark.
Safety guarantees from explicit resource management.
In de Boer et al. [FMCO07], pages 52-71. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [AydemirCPPW08] |
Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack,
and Stephanie Weirich.
Engineering formal metatheory.
In Necula and Wadler [POPL08], pages 3-15. [ bib ]
Keywords: mobius, wp3 |
| [BartheK08] |
G. Barthe and C. Kunz.
Certificate translation in abstract interpretation.
In Drossopoulou [ESOP08], pages 368-382. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [BartheK08b] |
G. Barthe and C. Kunz.
Certificate translation for specification-preserving advices.
In Clifton [FOAL08], pages 9-18. [ bib | http ]
Keywords: mobius, wp4 |
| [BartheKPS08] |
G. Barthe, C. Kunz, D. Pichardie, and J. Samborski-Forlese.
Preservation of proof obligations for hybrid verification methods.
In Cerone and Gruner [DBLP:conf/sefm/2008], pages 127-136. [ bib ]
Keywords: mobius, wp4 |
| [BartheKS08] |
G. Barthe, C. Kunz, and J. L. Sacchini.
Certified reasoning in memory hierarchies.
In Ramalingam [APLAS08], pages 75-90. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [BergerHY08] |
M. Berger, K. Honda, and N. Yoshida.
Completeness and logical full abstraction in modal logics for typed
mobile processes.
In ICALP, Lecture Notes in Computer Science, pages 99-111.
Springer-Verlag, 2008. [ bib ]
Keywords: mobius, wp4 |
| [BeringerHP08] |
Lennart Beringer, Martin Hofmann, and Mariela Pavlova.
Certification using the mobius base logic.
In de Boer et al. [FMCO07], pages 25-51. [ bib ]
Keywords: mobius, wp2 |
| [Besson:ecoop08] |
Frédéric Besson, Thomas Jensen, and Tiphaine Turpin.
Computing stack maps with interfaces.
In Proc. of the 22nd European Conference on Object-Oriented
Programming (ECOOP'08), volume 5142 of Lecture Notes in Computer
Science, pages 642-666. Springer-Verlag, 2008. [ bib ]
Keywords: mobius, wp4 |
| [BettiniCDDDY08] |
L. Bettini, M. Coppo, L. D'Antoni, M. De Luca, M. Dezani-Ciancaglini, and
N. Yoshida.
Global Progress in Dynamically Interleaved Multiparty Sessions.
In CONCUR, volume 5201 of Lecture Notes in Computer
Science, pages 418-433. Springer-Verlag, 2008. [ bib ]
Keywords: mobius, wp4 |
| [CharlesK08] |
J. Kiniry J. Charles.
A lightweight theorem prover interface for eclipse.
In User Interfaces for Theorem Proving, 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [Cregut08] |
Pierre Crégut.
Extracting control from data: User interfaces of MIDP applications.
In TGC 2007 [TGC07], pages 41-56. [ bib ]
Keywords: mobius, wp5 |
| [CunninghamDDFMS08] |
D. Cunningham, W. Dietl, S. Drossopoulou, A. Francalanza, P. Müller, and
A. J. Summers.
Universe types for topology and encapsulation.
In de Boer et al. [FMCO07]. [ bib ]
Keywords: mobius, wp2 |
| [CzarnikS08] |
P. Czarnik and A. Schubert.
Extending operational semantics of the java bytecode.
In TGC 2007 [TGC07], pages 57-72. [ bib | http ]
Keywords: mobius, wp3 |
| [DBLP:conf/sefm/2008] |
Antonio Cerone and Stefan Gruner, editors.
Sixth IEEE International Conference on Software Engineering and
Formal Methods, SEFM 2008, Cape Town, South Africa, 10-14 November 2008.
IEEE Press, 2008. [ bib ] |
| [DarvasFR08] |
Á. Darvas, F. Mehta, and A. Rudich.
Efficient well-definedness checking.
In A. Armando, P. Baumgartner, and G. Dowek, editors,
International Joint Conference on Automated Reasoning, volume 5195 of
Lecture Notes in Computer Science, pages 100-115. Springer-Verlag, 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [DezaniCiancagliniDLY08] |
M. Dezani-Ciancaglini, U. de'Liguoro, and N. Yoshida.
On progress for structured communications.
In Trustworthy Global Computing, Lecture Notes in Computer
Science, pages 257-275. Springer-Verlag, 2008. [ bib ]
Keywords: mobius, wp4 |
| [DrossopoulouFMS08] |
S. Drossopoulou, A. Francalanza, Peter Müller, and A. J. Summers.
A unified framework for verification techniques for object
invariants.
In European Conference of Object Oriented Programming, 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [DrossopoulouFrancalanzaMuellerSummers08] |
S. Drossopoulou, A. Francalanza, P. Müller, and A. J. Summers.
A unified framework for verification techniques for object
invariants.
In J. Vitek, editor, European Conference on Object-Oriented
Programming (ECOOP), Lecture Notes in Computer Science. Springer-Verlag,
2008. [ bib ]
Keywords: mobius, wp3 |
| [ESOP08] |
S. Drossopoulou, editor.
Programming Languages and Systems: Proceedings of the 17th
European Symposium on Programming, ESOP 2008, Held as Part of the Joint
European Conferences on Theory and Practice of Software, ETAPS 2008,
Budapest, Hungary, March 29-April 6, 2008, volume 4960 of Lecture
Notes in Computer Science. Springer-Verlag, 2008. [ bib ] |
| [FMCO07] |
Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever,
editors.
Formal Methods for Components and Objects: Revised Lectures from
the 6th International Symposium FMCO 2007, Amsterdam, The Netherlands,
October 24-26, 2007, volume 5382 of Lecture Notes in Computer
Science. Springer-Verlag, 2008. [ bib ] |
| [FMOODS08] |
Formal Methods for Open Object-Based Distributed Systems: Proceedings of
the 10th IFIP WG 6.1 International Conference FMOODS 2008, number 5051 in
Lecture Notes in Computer Science. Springer-Verlag, 2008. [ bib ] |
| [FOAL08] |
Curtis Clifton, editor.
Proceedings of the 7th Workshop on Foundations of
Aspect-Oriented Languages, FOAL 2008, Brussels, Belgium, April 1, 2008. ACM,
2008. [ bib ] |
| [FularaJS08] |
J. Fulara, K. Jakubczyk, and A. Schubert.
Supplementing java bytecode with specifications.
In T. Hruska, L. Madeyski, and M. Ochodek, editors, Software
Engineering Techniques in Progress, pages 215-228. Oficyna Wydawnicza
Politechniki Wroclawskiej, 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [GregoireS08] |
B. Grégoire and J.L. Sacchini.
Combining a verification condition generator for a bytecode language
with static analyses.
In TGC 2007 [TGC07], pages 23-40. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [GurovHS08] |
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, 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [GurovHS08b] |
D. Gurov, M. Huisman, and C. Sprenger.
Compositional verification of sequential programs with procedures.
Information and Computation, 206:840-868, 2008.
team. [ bib | http ]
Keywords: mobius, wp3 |
| [HaackH08] |
C. Haack and C. Hurlin.
Separation logic contracts for a Java-like language with fork/join.
Technical Report 6430, INRIA, January 2008. [ bib ]
Keywords: mobius, WP3 |
| [HaackH08c] |
C. Haack and C. Hurlin.
Resource usage protocols for iterators.
In International Workshop on Aliasing, Confinement and Ownership
in object-oriented programming, 2008.
Revised version available
from http://www.cs.ru.nl/~chaack/papers/iterators.pdf. [ bib ]
Keywords: mobius, WP3 |
| [HaackHH08b] |
C. Haack, M. Huisman, and C. Hurlin.
Reasoning about Java's reentrant locks.
Technical Report ICIS-R08014, Radboud University Nijmegen, 2008. [ bib | http ]
Keywords: mobius, WP3 |
| [HaehnlePRW08] |
Reiner Hähnle, Jing Pan, Philipp Rümmer, and Dennis Walter.
Integration of a security type system into a program logic.
Theoretical Computer Science, 402(2-3):172-189, 2008. [ bib ]
Keywords: mobius, wp3 |
| [HofmannP08] |
Martin Hofmann and Mariela Pavlova.
Elimination of ghost variables in program logics.
In TGC 2007 [TGC07], pages 1-20. [ bib ]
Keywords: mobius, wp3 |
| [HondaYC08] |
Kohei Honda, Nobuko Yoshida, and Marco Carbone.
Multiparty asynchronous session types.
In Principles of Programming Languages, pages 273-284. ACM
Press, 2008. [ bib ]
Keywords: mobius, wp4 |
| [HuYH08] |
R. Hu, N. Yoshida, and K. Honda.
Session-based distributed programming in java.
In ECOOP, Lecture Notes in Computer Science, pages 516-541.
Springer-Verlag, 2008. [ bib ]
Keywords: mobius, wp4 |
| [HubertJP08] |
Laurent Hubert, Thomas Jensen, and David Pichardie.
Semantic foundations and inference of non-null annotations.
In FMOODS 2008 [FMOODS08], pages 132-149. [ bib ]
Keywords: mobius, wp2 |
| [HuismanAG08] |
M. Huisman, I. Aktug, and D. Gurov.
Program models for compositional verification.
In ICFEM 2008, volume 5256 of Lecture Notes in Computer
Science, pages 147-166. Springer-Verlag, 2008. [ bib | .pdf ]
Keywords: mobius, WP3 |
| [HuismanP08] |
M. Huisman and G. Petri.
Bicolano MT?: a formalization of multi-threaded Java at bytecode
level.
In BYTECODE, ENTCS. Elsevier, 2008. [ bib | .pdf ]
Keywords: mobius, WP3 |
| [Laud08] |
Peeter Laud.
On the computational soundness of cryptographically masked flows.
In POPL, pages 337-348. ACM Press, 2008. [ bib ]
Keywords: mobius, wp2 |
| [LuxM08] |
A. Lux and H. Mantel.
Who can declassify?
In Preproceedings of FAST, 2008. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [MarronHKS08] |
M. Marron, M. V. Hermenegildo, D. Kapur, and D. Stefanovic.
Efficient context-sensitive shape analysis with graph based heap
models.
In Laurie Hendren, editor, Compiler Construction, 17th
International Conference, CC 2008, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2008, Budapest,
Hungary, March 29 - April 6, 2008. Proceedings, volume 4959 of Lecture
Notes in Computer Science, pages 245-259. Springer-Verlag, 2008. [ bib ]
Keywords: mobius, wp2 |
| [Mendez-LojoH08] |
M. Méndez-Lojo and M. V. Hermenegildo.
Precise set sharing analysis for Java-style programs.
In Francesco Logozzo, Doron Peled, and Lenore D. Zuck, editors,
Verification, Model Checking, and Abstract Interpretation, 9th International
Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings,
volume 4905 of Lecture Notes in Computer Science, pages 172-187.
Springer-Verlag, 2008. [ bib ]
Keywords: mobius, wp2 |
| [MobiusDeliverable2.4] |
Consortium.
Deliverable 2.4: Report on type system prototypes, 2008.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp2 |
| [MobiusDeliverable2.5] |
Consortium.
Deliverable 2.5: Report on safe information release, 2008.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp2 |
| [MobiusDeliverable2.6] |
Consortium.
Deliverable 2.6: Preliminary report on advanced resource policies,
2008.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp2 |
| [MobiusDeliverable3.5] |
Consortium.
Deliverable 3.5: Preliminary report on program verification
environment and annotation generation, 2008.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp3 |
| [MobiusDeliverable4.5] |
Consortium.
Deliverable 4.5: Report on proof transformation for optimizing
compilers, 2008.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp4 |
| [MobiusDeliverable6.5] |
Consortium.
Deliverable 6.5: Demonstration report, 2008.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp6 |
| [MobiusDeliverable6.6] |
Consortium.
Deliverable 6.6: Dissemination and training activity report, year 3,
2008.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp6 |
| [NavasMLH08] |
J. Navas, M. Méndez-Lojo, and M. Hermenegildo.
Customizable resource usage analysis for Java bytecode.
Technical Report UNM TR-CS-2008-02 - CLIP1/2008.0, University of New
Mexico, Department of Computer Science, UNM, January 2008. [ bib ]
Keywords: mobius, wp2 |
| [POPL08] |
George C. Necula and Philip Wadler, editors.
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2008, San Francisco, California,
USA, January 7-12, 2008. ACM, 2008. [ bib ] |
| [PollRavelo08] |
E. Poll and J. N. Ravelo.
Generalised navigation graphs, their refinement, and their use for
midp applications, 2008.
Manuscript. 48 pages. [ bib ]
Keywords: mobius, wp4 |
| [RudichDM08] |
A. Rudich, Á. Darvas, and P. Müller.
Checking well-formedness of pure-method specifications.
In J. Cuellar and T. Maibaum, editors, Formal Methods, volume
5014 of Lecture Notes in Computer Science, pages 68-83.
Springer-Verlag, 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [RudichDM08a] |
A. Rudich, Á. Darvas, and P. Müller.
Checking well-formedness of pure-method specifications.
Technical Report 588, ETH Zurich, 2008. [ bib ]
Keywords: mobius, wp3 |
| [Russo08] |
A. Russo.
Language Support for Controlling Timing-Based Covert Channels.
Ph D? thesis, Chalmers University of Technology, 2008. [ bib | www ]
Keywords: mobius, wp2 |
| [Saabas08] |
A. Saabas.
Logics for Low-Level Code and Proof-Preserving Program
Optimizations.
Ph D? thesis, Tallinn University of Technology, 2008. [ bib | http ]
Keywords: mobius, wp3, wp4 |
| [SaabasU06c] |
A. Saabas and T. Uustalu.
Program and proof optimizations with type systems.
Journal of Logic and Algebraic Programming, 77(1-2):131-154,
2008. [ bib ]
Keywords: mobius, wp3, wp4 |
| [SaabasU08] |
A. Saabas and T. Uustalu.
Proof optimization for partial redundancy elimination.
In ACM SIGPLAN Workshop on Partial Evaluation and
Semantics-based Program Manipulation, pages 91-101. ACM Press, 2008. [ bib ]
Keywords: mobius, wp3, wp4 |
| [SchubertCBPW08] |
A. Schubert, J. Chrz aszcz, T. Batkiewicz, J. Paszek, and W. W as.
Technical aspects of class specification in the byte code of java
language.
In To be published in Bytecode'08 proceedings, Electronic Notes
in Theoretical Computer Science. Elsevier, 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [Sevcik08] |
Jaroslav Sevcík.
The Sun Hotspot JVM does not conform with the Java memory
model.
Technical Report EDI-INF-RR-1252, School of Informatics, University
of Edinburgh, 2008. [ bib ]
Keywords: mobius, wp3 |
| [SevcikA08] |
J. Sevcík and D. Aspinall.
On validity of program transformations in the Java memory model.
In European Conference on Object-Oriented Programming, pages
27-51, 2008. [ bib ]
Keywords: mobius, wp3 |
| [SevcikPhd] |
J. Sevcík.
Program Transformations in Weak Memory Models.
Ph D? thesis, University of Edinburgh, 2008. [ bib ]
Keywords: mobius, wp3 |
| [SummersDM08] |
Alexander J. Summers, S. Drossopoulou, and P. Müller.
A universe-type-based verification technique for mutable static
fields and methods (work in progress).
In Workshop on Formal Techniques for Java Programs, 2008. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [SummersDrossopoulouMueller08] |
A. J. Summers, S. Drossopoulou, and P. Müller.
A universe-type-based verification technique for mutable static
fields and methods.
In Formal Techniques for Java-like Programs, 2008. [ bib ]
Keywords: mobius, wp3 |
| [TGC07] |
Trustworthy Global Computing: Revised Selected Papers from the Third
Symposium TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, number
4912 in Lecture Notes in Computer Science. Springer-Verlag, 2008. [ bib ] |
| [Turpin08] |
Tiphaine Turpin.
Pruning program invariants.
Ph D? thesis, Univ. Rennes 1, 2008. [ bib ]
Keywords: mobius, wp4 |
| [YoshidaHB08] |
N. Yoshida, K. Honda, and M. Berger.
Logical reasoning for higher-order functions with local state.
Journal of Logical Methods in Computer Science, 4(4), 2008. [ bib ]
Keywords: mobius, wp4 |
| [AlbertAGPZ07b] |
E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini.
A generic framework for the cost analysis of Java bytecode.
In Spanish Conference on Programming and Computer Languages,
September 2007. [ bib ]
Keywords: mobius, wp2 |
| [BartheRRS07b] |
G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld.
Security of multithreaded programs by compilation.
In European Symposium On Research In Computer Security, Lecture
Notes in Computer Science. Springer-Verlag, September 2007. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [GrigoreM07] |
R. Grigore and M. Moskal.
Edit and verify.
In Workshop on First-Order Theorem Proving, September 2007. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [NavasMLH07] |
J. Navas, E. Mera, P. López-García, and M. Hermenegildo.
User-definable resource bounds analysis for logic programs.
In International Conference on Logic Programming, Lecture Notes
in Computer Science. Springer-Verlag, September 2007. [ bib ]
Keywords: mobius, wp2 |
| [AlbertGGP07] |
E. Albert, J. Gallagher, M. Gómez-Zamalloa, and G. Puebla.
Typed-based homeomorphic embedding for online termination.
In Logic-based Program Synthesis and Transformation, August
2007. [ bib ]
Keywords: mobius, wp4 |
| [MendezNH07] |
M. Méndez-Lojo, J. Navas, and M. Hermenegildo.
A flexible (c)lp-based approach to the analysis of object-oriented
programs.
In Logic-based Program Synthesis and Transformation, August
2007. [ bib ]
Keywords: mobius, wp4 |
| [NavasM-LH07] |
Jorge Navas, Mario Méndez-Lojo, and Manuel Hermenegildo.
A generic, context sensitive analysis framework for object oriented
programs.
In 9th Workshop on Formal Techniques for Java-like Programs
F Tf JP? 2007, Technical Report, Nanjing University, pages 109-120, July 2007. [ bib | http | .pdf ]
Keywords: mobius, wp4 |
| [AlbertACGPZ07] |
E. Albert, P. Arenas, M. Codish, S. Genaim, G. Puebla, and D. Zanardini.
Termination analysis of Java bytecode.
In Workshop on Termination, June 2007. [ bib ]
Keywords: mobius, wp2 |
| [AskarovS07a] |
A. Askarov and A. Sabelfeld.
Localized delimited release: Combining the what and where dimensions
of information release.
In ACM SIGPLAN Workshop on Programming Languages and Analysis
for Security, San Diego, California, June 2007. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [OchoaP07b] |
C. Ochoa and G. Puebla.
A study on the practicality of poly-controlled partial evaluation.
In Workshop on Functional and (Constraint) Logic Programming,
volume 177 of Electronic Notes in Theoretical Computer Science, pages
137-151. Elsevier, June 2007. [ bib ]
Keywords: mobius, wp4 |
| [AskarovS07] |
A. Askarov and A. Sabelfeld.
Gradual release: Unifying declassification, encryption and key
release policies.
In Symposium on Security and Privacy, May 2007. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [KrausserMS07] |
T. Kraußer, H. Mantel, and H. Sudbrock.
A probabilistic justification of the combining calculus under the
uniform scheduler assumption.
Technical Report 2007-09, RWTH Aachen, May 2007. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [AlbertAGPZ07c] |
E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini.
Experiments in cost analysis of Java bytecode.
In Bytecode Semantics, Verification, Analysis and
Transformation, Electronic Notes in Theoretical Computer Science. Elsevier,
March 2007. [ bib ]
Keywords: mobius, wp2 |
| [GomezAP07] |
M. Gómez-Zamalloa, E. Albert, and G. Puebla.
Improving the decompilation of Java bytecode to Prolog by partial
evaluation.
In Bytecode Semantics, Verification, Analysis and
Transformation, Electronic Notes in Theoretical Computer Science. Elsevier,
March 2007. [ bib ]
Keywords: mobius, wp4 |
| [MendezNV07] |
M. Méndez-Lojo, J. Navas, and M. Hermenegildo.
An efficient, parametric fixpoint algorithm for analysis of java
bytecode.
In Bytecode Semantics, Verification, Analysis and
Transformation, Electronic Notes in Theoretical Computer Science. Elsevier,
March 2007. [ bib ]
Keywords: mobius, wp4 |
| [AhernY07] |
A. Ahern and N. Yoshida.
Formalising Java RMI with explicit code mobility.
TCS, 389(3):341-410, 2007. [ bib ]
Keywords: mobius, wp4 |
| [AlbertAGPZ07] |
E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini.
Cost analysis of Java bytecode.
In ESOP 2007 [ESOP07], pages 157-172. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [AlbertGG07] |
E. Albert, S. Genaim, and M. Gómez-Zamalloa.
Heap space analysis of Java bytecode.
In ISMM '07: Proceedings of the 6th International Symposium on
Memory Management, pages 105-116, New York, NY, USA, 2007. ACM Press. [ bib ]
Keywords: mobius, wp2 |
| [AlbertGZHP07] |
E. Albert, M. G'omez-Zamalloa, L. Hubert, and G. Puebla.
Verification of Java bytecode using analysis and transformation of
logic programs.
In Ninth International Symposium on Practical Aspects of
Declarative Languages, number 4354 in Lecture Notes in Computer Science,
pages 124-139. Springer-Verlag, January 2007. [ bib ]
Keywords: mobius, wp4 |
| [AlbertPH07] |
E. Albert, G. Puebla, and M. Hermenegildo.
Abstraction-carrying code: A model for mobile code safety.
New Generation Computing, 2007. [ bib ]
Keywords: mobius, wp4 |
| [AspinallBM07] |
David Aspinall, Lennart Beringer, and Alberto Momigliano.
Optimisation validation.
Electronic Notes in Theoretical Computer Science,
176(3):37-59, 2007. [ bib | http | .pdf ]
Keywords: mobius, wp4 |
| [AspinallH07] |
David Aspinall and Piotr Hoffman.
Datatypes in memory.
In Algebra and Coalgebra in Computer Science: Proc.
CALCO 2007 [CALCO07], pages 111-125. [ bib | http | .pdf ]
Keywords: mobius, wp2 |
| [AspinallS07] |
D. Aspinall and J. Sevcík.
Formalising Java's data-race-free guarantee.
In TPHOLs 2007 [TPHOL07], pages 22-37. [ bib | .html ]
Keywords: mobius, wp3 |
| [AspinallS07b] |
D. Aspinall and J. Sevcík.
Java memory model examples: Good, bad and ugly.
In VAMP 2007 [VAMP07]. [ bib | .html ]
Keywords: mobius, wp3 |
| [BartheBCGHLPR07:FMCO] |
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 2006 [FMCO06], pages 152-174. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [BartheBCGHMPPSV06] |
Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire,
Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark,
and Eric Vétillard.
MOBIUS: Mobility, ubiquity, security - objectives and progress
report.
In TGC 2006 [TGC06]. [ bib | .pdf ]
Keywords: mobius, wp6 |
| [BarthePR07] |
G. Barthe, D. Pichardie, and T. Rezk.
A certified lightweight non-interference Java bytecode verifier.
In ESOP 2007 [ESOP07], pages 125-140. [ bib ]
Keywords: mobius |
| [BartheRRS07] |
G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld.
Security of multithreaded programs by compilation.
Technical report, Chalmers University of Technology, 2007.
http://www.cse.chalmers.se/~russo/tissecfull.pdf. [ bib ]
Keywords: mobius, wp2 |
| [BergerHY07] |
M. Berger, K. Honda, and N. Yoshida.
A logical analysis of aliasing for higher-order imperative functions.
J. Funct. Program., 17(4-5):473-546, 2007. [ bib ]
Keywords: mobius, wp4 |
| [BergerHY07-IL] |
M. Berger, K. Honda, and N. Yoshida.
Typed pi-calculus as an intermediate language for compilers, 2007.
In preparation. [ bib ]
Keywords: mobius, wp2 |
| [BergerY07] |
M. Berger and N. Yoshida.
Timed, distributed, probabilistic, typed processes.
In APLAS, Lecture Notes in Computer Science, pages 158-174.
Springer-Verlag, 2007. [ bib ]
Keywords: mobius, wp4 |
| [BeringerH07] |
L. Beringer and M. Hofmann.
Secure information flow and program logics.
In IEEE Computer Security Foundations Symposium, pages
233-248. IEEE Press, 2007. [ bib | http ]
Keywords: mobius, wp2, wp3 |
| [BessonJT07] |
Frédéric Besson, Thomas P. Jensen, and Tiphaine Turpin.
Small witnesses for abstract interpretation-based proofs.
In ESOP 2007 [ESOP07], pages 268-283. [ bib ]
Keywords: mobius, wp4 |
| [BugliesiG07] |
M. Bugliesi and M. Giunti.
Secure implementations of typed channel abstractions.
In Principles of Programming Languages, pages 251-262, 2007. [ bib ]
Keywords: mobius, wp2 |
| [BurdyHP07] |
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, volume 4422
of LNCS, pages 215-229. Springer-Verlag, 2007. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [CALCO07] |
Algebra and Coalgebra in Computer Science: Proceedings of the Second
International Conference CALCO 2007, Bergen, Norway, August 20-24, 2007,
number 4624 in Lecture Notes in Computer Science. Springer-Verlag, 2007. [ bib ] |
| [CameronCDNS07] |
D. Cameron, S. Drossopoulou, J. Noble, and M. Smith.
Multiple ownership.
In ACM Conference on Object-Oriented Programming Systems,
Languages, and Applications. ACM Press, 2007. [ bib ]
Keywords: mobius, wp2 |
| [CarboneHY07a] |
Marco Carbone, Kohei Honda, and Nobuko Yoshida.
Structured communication-centred programming for web services.
In European Symposium on Programming, volume 4421 of
Lecture Notes in Computer Science, pages 2-17. Springer-Verlag, 2007. [ bib ]
Keywords: mobius, wp4 |
| [CarboneHY07b] |
M. Carbone, K. Honda, and N. Yoshida.
A calculus of global interaction based on session types.
ENTCS, 171(3):127-151, 2007. [ bib ]
Keywords: mobius, wp4 |
| [Charles07] |
J. Charles.
Taking into account Java's security manager for static
verification.
Draft paper, 2007. [ bib ]
Keywords: mobius, wp4 |
| [CoppoDY07] |
Mario Coppo, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida.
Asynchronous session types and progress for object-oriented
languages.
In Marcello Bonsangue and Einar Broch Johnsen, editors,
International Conference on Formal Methods for Open Object-based Distributed
Systems, number 4468 in Lecture Notes in Computer Science, pages 1-31.
Springer-Verlag, 2007. [ bib ]
Keywords: mobius, wp4 |
| [DarvasM07] |
Á. Darvas and P. Müller.
Formal encoding of JML level 0 specifications in jive.
Technical report, ETH Zurich, 2007.
Annual Report of the Chair of Software Engineering. [ bib ]
Keywords: mobius, wp3 |
| [DezaniSGY07] |
Mariangiola Dezani-Ciancaglini, Sophia Drossopoulou, Elena Giachino, and Nobuko
Yoshida.
Bounded session types for object-oriented languages.
In FMCO 2006 [FMCO06], pages 207-245. [ bib ]
Keywords: mobius, wp4 |
| [DietlDM07] |
W. Dietl, S. Drossopoulou, and P. Müller.
Generic universe types.
In E. Ernst, editor, European Conference on Object-Oriented
Programming, Lecture Notes in Computer Science, pages 28 - 53.
Springer-Verlag, 2007. [ bib ]
Keywords: mobius, wp2 |
| [DietlDM07a] |
W. Dietl, S. Drossopoulou, and P. Müller.
Generic universe types.
In ACM Workshop on Foundations of Object-Oriented Languages,
January 2007. [ bib ]
Keywords: mobius, wp2 |
| [DietlM07] |
W. Dietl and P. Müller.
Runtime universe type inference.
In International Workshop on Aliasing, Confinement and Ownership
in object-oriented programming, 2007.
To appear. [ bib ]
Keywords: mobius, wp2 |
| [DrossopoulouFM07] |
S. Drossopoulou, A. Francalanza, and P. Müller.
A unified framework for verification techniques for object invariants
(full paper).
http://research.microsoft.com/~mueller/publications.html, 2007. [ bib ]
Keywords: mobius, wp2 |
| [DrossopoulouFM07Fool] |
S. Drossopoulou, A. Francalanza, and Peter Müller.
A unified framework for verification techniques for object
invariants.
In Foundations of Object Oriented Languages, 2007. [ bib ]
Keywords: mobius, wp3 |
| [ESOP07] |
Programming Languages and Systems: Proceedings of the 16th European
Symposium on Programming, ESOP 2007, Held as Part of the Joint European
Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal,
March 24-April 1, 2007, number 4421 in Lecture Notes in Computer Science.
Springer-Verlag, 2007. [ bib ] |
| [FMCO06] |
Formal Methods for Components and Objects: Revised Lectures from the 5th
International Symposium FMCO 2006, Amsterdam, The Netherlands,
November 7-10, 2006, number 4709 in Lecture Notes in Computer Science.
Springer-Verlag, 2007. [ bib ] |
| [FradeSU07] |
M. J. Frade, A. Saabas, and T. Uustalu.
Foundational certification of data-flow analyses.
In IEEE and IFIP Int. Symp. on Theoretical Aspects of Software
Engineering, pages 107-116. IEEE Press, 2007. [ bib ]
Keywords: mobius, wp3 |
| [HaackPSS07] |
C. Haack, E. Poll, J. Schäfer, and A. Schubert.
Immutable objects for a Java-like language.
In R. De Nicola, editor, ESOP'07, volume 4421 of Lecture
Notes in Computer Science, pages 347-362. Springer-Verlag, 2007. [ bib ]
Keywords: mobius, wp3 |
| [HaehnlePRW06] |
Reiner Hähnle, Jing Pan, Philipp Rümmer, and Dennis Walter.
Integration of a security type system into a program logic.
In TGC 2006 [TGC06], pages 166-131. [ bib ]
Keywords: mobius, wp3 |
| [HondaY07] |
K. Honda and N. Yoshida.
A uniform type structure for secure information flow.
ACM Transactions on Programming Languages and Systems,
29(6):101 pages, 2007. [ bib ]
Keywords: mobius, wp2 |
| [HondaYC06] |
Kohei Honda, Nobuko Yoshida, and Marco Carbone.
Web services, mobile processes and types.
The Bulletin of the European Association for Theoretical
Computer Science, February(91):165-185, 2007. [ bib ]
Keywords: mobius, wp4 |
| [HuismanG07] |
M. Huisman and D. Gurov.
Composing modal properties of programs with procedures.
In Formal Foundations of Embedded Software and Component-Based
Software Architectures, 2007. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [HuismanH07] |
M. Huisman and C. Hurlin.
The stability problem for verification of concurrent object-oriented
programs.
In VAMP 2007 [VAMP07]. [ bib | .pdf ]
Keywords: mobius, WP3 |
| [HuismanP07] |
M. Huisman and G. Petri.
The Java memory model: a formal explanation.
In VAMP 2007 [VAMP07]. [ bib | .pdf ]
Keywords: mobius, WP3 |
| [JacobsMP07] |
B. Jacobs, P. Müller, and F. Piessens.
Sound reasoning about unchecked exceptions.
In Software Engineering and Formal Methods. IEEE Press, 2007.
To appear. [ bib ]
Keywords: mobius, wp3 |
| [Janota07] |
M. Janota.
Assertion-based loop invariant generation.
In Workshop on Invariant Generation, 2007.
Workshop at CALCULEMUS 2007. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [JanotaGM07] |
M. Janota, R. Grigore, and M. Moskal.
Reachability analysis for annotated code.
In Specification and Verification of Component-Based Systems,
Dubrovnik, Croatia, 2007.
Workshop at ESEC/FSE 2007. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [JanotaK07] |
M. Janota and J. Kiniry.
Reasoning about feature models in higher-order logic.
In Proceedings of the 11th International Conference, SPL
[SPLC07]. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [Kiniry07] |
J. R. Kiniry.
Formally counting electronic votes (but still only trusting paper).
In IEEE International Conference on Engineering of Complex
Computer Systems, Auckland, New Zealand, 2007. [ bib ]
Keywords: mobius, wp3, wp5 |
| [KiniryCT07] |
J.R. Kiniry, D. Cochran, and P. Tierney.
A verification-centric realization of e-voting.
In International Workshop on Electronic Voting Technologies,
Boston, Massachusetts, 2007.
Workshop at USENIX/ACCURATE 2007. [ bib ]
Keywords: mobius, wp3, wp5 |
| [KiniryMCFCOH07] |
Joseph R. Kiniry, Alan E. Morkan, Dermot Cochran, Fintan Fairmichael, Patrice
Chalin, Martijn Oostdijk, and Engelbert Hubbers.
The KOA remote voting system: A summary of work to date.
In TGC 2006 [TGC06], pages 244-262. [ bib | .pdf ]
Keywords: mobius, ircset, wp3, wp5 |
| [LeavensLM07] |
G. T. Leavens, K. R. M. Leino, and P. Müller.
Specification and verification challenges for sequential
object-oriented programs.
Formal Aspects of Computing, 2007.
Accepted for publication. [ bib ]
Keywords: mobius, wp3 |
| [LeavensM07] |
G. T. Leavens and P. Müller.
Information hiding and visibility in interface specifications.
In International Conference on Software Engineering, pages
385-395. PUB-IEEE, 2007.
To appear. [ bib ]
Keywords: mobius, wp3 |
| [LehnerM07] |
H. Lehner and P. Müller.
Formal translation of bytecode into Boogie PL?.
In M. Huisman and F. Spoto, editors, Bytecode Semantics,
Verification, Analysis and Transformation, Electronic Notes in Theoretical
Computer Science, 2007. [ bib ]
Keywords: mobius, wp3 |
| [LiangM07] |
C. Liang and D. Miller.
Focusing and polarization in intuitionistic logic.
In Computer Science Logic, volume 4646 of Lecture Notes in
Computer Science, pages 451-465. Springer-Verlag, 2007. [ bib | <a href="./ http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/csl07liang.pdf">.pdf ]
Keywords: mobius, wp4 |
| [MantelK07] |
B. Köpf and H. Mantel.
Transformational typing and unification for automatically correcting
insecure programs.
International Journal of Information Security, 2007. [ bib ]
Keywords: mobius, wp2 |
| [MantelR07] |
H. Mantel and A. Reinhard.
Controlling the what and where of declassification in language-based
security.
In ESOP 2007 [ESOP07], pages 141-156. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [MantelSK07] |
H. Mantel, H. Sudbrock, and T. Kraußer.
Combining Different Proof Techniques for Verifying Information Flow
Security.
In G. Puebla, editor, Logic-based Program Synthesis and
Transformation, number 4407 in Lecture Notes in Computer Science.
Springer-Verlag, 2007. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [MeraLPCH07] |
E. Mera, P. López-García, G. Puebla, M. Carro, and M. Hermenegildo.
Combining static analysis and profiling for estimating execution
times.
In M. Hanus, editor, Symposium on Practical Aspects of
Declarative Languages, volume 4354 of Lecture Notes in Computer
Science, pages 140-154. Springer-Verlag, January 2007. [ bib ]
Keywords: mobius, wp2 |
| [MillerN07] |
D. Miller and V. Nigam.
Incorporating tables into proofs.
In J. Duparc and T. A. Henzinger, editors, Computer Science
Logic, volume 4646 of Lecture Notes in Computer Science, pages
466-480. Springer-Verlag, 2007. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [MobiusDeliverable2.3] |
Consortium.
Deliverable 2.3: Report on type systems, 2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp2 |
| [MobiusDeliverable3.2] |
Consortium.
Deliverable 3.2: Intermediate report on embedding type-based analyses
into program logics, 2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp3 |
| [MobiusDeliverable3.3] |
Consortium.
Deliverable 3.3: Thread-modular verification, 2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp3 |
| [MobiusDeliverable3.4] |
Consortium.
Deliverable 3.4: Report on logic for resources and information flow,
2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp3 |
| [MobiusDeliverable4.2] |
Consortium.
Deliverable 4.2: Certificates, 2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp4 |
| [MobiusDeliverable4.3] |
Consortium.
Deliverable 4.3: Intermediate report on proof-transforming compiler,
2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp4 |
| [MobiusDeliverable4.4] |
Consortium.
Deliverable 4.4: Report on certificate format and certificate
generation, 2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp4 |
| [MobiusDeliverable5.1] |
Consortium.
Deliverable 5.1: Selection of case studies, 2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp5 |
| [MobiusDeliverable6.4] |
Consortium.
Deliverable 6.4: Dissemination and training activity report, year 2,
2007.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp6 |
| [MostrousY07] |
Dimitris Mostrous and Nobuko Yoshida.
Two session typing systems for higher-order mobile processes.
In TLCA, number 4583 in Lecture Notes in Computer Science,
pages 321-335. Springer-Verlag, 2007. [ bib ]
Keywords: mobius, wp4 |
| [Mueller07] |
P. Müller.
Reasoning about object structures using ownership.
In Verified Software: Theories, Tools, Experiements, Lecture
Notes in Computer Science. Springer-Verlag, 2007. [ bib ]
Keywords: mobius, wp2 |
| [MuellerN07] |
P. Müller and M. Nordio.
Proof-transforming compilation of programs with abrupt termination.
In SAVCBS '07: Proceedings of the 2007 conference on
Specification and verification of component-based systems, pages 39-46, New
York, NY, USA, 2007. ACM. [ bib ]
Keywords: mobius, wp4 |
| [MuellerN07b] |
P. Müller and M. Nordio.
Proof-transforming compilation of programs with abrupt termination.
Technical Report 565, ETH Zurich, 2007. [ bib ]
Keywords: mobius, wp4 |
| [MuellerR07] |
P. Müller and A. Rudich.
Formalization of ownership transfer in universe types.
Technical Report 556, ETH Zurich, 2007. [ bib ]
Keywords: mobius, wp2 |
| [MuellerR07b] |
P. Müller and A. Rudich.
Ownership transfer in universe types.
In ACM Conference on Object-Oriented Programming Systems,
Languages, and Applications, 2007.
To appear. [ bib ]
Keywords: mobius, wp2 |
| [MuellerR07c] |
P. Müller and J. N. Ruskiewicz.
A modular verification methodology for C# delegates.
In U. Glässer and J.-R. Abrial, editors, Rigorous Methods
for Software Construction and Analysis, 2007.
To appear. [ bib ]
Keywords: mobius, wp3 |
| [OchoaP07a] |
C. Ochoa and G. Puebla.
Poly-controlled partial evaluation in practice.
In ACM SIGPLAN Workshop on Partial Evaluation and
Semantics-based Program Manipulation, pages 164-173. ACM Press, January
2007. [ bib ]
Keywords: mobius, wp4 |
| [PollS07] |
E. Poll and A. Schubert.
Verifying an implementation of SSH.
In Workshop on Issues in the Theory of Security, pages
164-177. IFIP WG1.7, 2007. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [RussoHNS06] |
A. Russo, J. Hughes, D. Naumann, and A. Sabelfeld.
Closing internal timing channels by transformation.
In Asian Computing Science Conference, Lecture Notes in
Computer Science. Springer-Verlag, 2007. [ bib | www ]
Keywords: mobius, wp2 |
| [RussoS07] |
A. Russo and A. Sabelfeld.
Securing interaction between threads and the scheduler in the
presence of synchronization.
Journal of Logic and Algebraic Programming, 2007.
Special Issue dedicated to the Nordic Workshop on Programming Theory. [ bib | www ]
Keywords: mobius, wp2 |
| [SPLC07] |
Software Product Lines, 2007. [ bib ] |
| [SaabasU07] |
A. Saabas and T. Uustalu.
Type systems for optimizing stack-based code.
In M. Huisman and F. Spoto, editors, Bytecode Semantics,
Verification, Analysis and Transformation, volume 190(1) of Electronic
Notes in Theoretical Computer Science, pages 103-119. Elsevier, 2007. [ bib ]
Keywords: mobius, wp4 |
| [SaabasU07b] |
A. Saabas and T. Uustalu.
A compositional natural semantics and Hoare logic for low-level
languages.
Theoretical Computer Science, 373(3):273-302, 2007. [ bib ]
Keywords: mobius |
| [SabelfeldS07] |
A. Sabelfeld and D. Sands.
Declassification: Dimensions and principles.
Journal of Computer Security, 2007. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [SannellaHAGSBLMMSDT07] |
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark,
Lennart Beringer, Hans-Wolfgang Loidl, Kenneth Mac Kenzie?, Alberto Momigliano,
and Olha Shkaravska.
Mobile resource guarantees.
In Trends in Functional Programming, volume 6, pages 211-226.
Intellect, 2007. [ bib | .pdf ]
Keywords: mobius, wp1 |
| [TGC06] |
Trustworthy Global Computing: Revised Selected Papers from the Second
Symposium TGC 2006, Lucca, Italy, November 7-9, 2006, number 4661 in
Lecture Notes in Computer Science. Springer-Verlag, 2007. [ bib ] |
| [TPHOL07] |
Theorem Proving in Higher Order Logics: Proceedings of the 20th
International Conference TPHOLs 2007, Kaiserslautern, Germany,
September 10-13, 2007, Lecture Notes in Computer Science 4732.
Springer-Verlag, 2007. [ bib ] |
| [VAMP07] |
VAMP 2007: Proceedings of the 1st International Workshop on Verification
and Analysis of Multi-Threaded Java-Like Programs, Lisbon, Portugal,
September 3, 2007, number ICIS-R07021 in Technical Report. Radboud
University Nijmegen, 2007. [ bib ]
Keywords: mobius, wp3 |
| [YoshidaHB07] |
N. Yoshida, K. Honda, and M. Berger.
Linearity and bisimulation.
Journal of Logic and Algebraic Programming, 72:207-238, 2007. [ bib ]
Keywords: mobius, wp2 |
| [YoshidaHB07a] |
N. Yoshida, K. Honda, and M. Berger.
Local state in Hoare logic for imperative higher-order functions.
In Foundations of Software Science and Computation Structures,
number 4423 in Lecture Notes in Computer Science, pages 361-377.
Springer-Verlag, 2007. [ bib ]
Keywords: mobius, wp4 |
| [YoshidaV07] |
Nobuko Yoshida and Vasco Thudichum Vasconcelos.
Language primitives and type discipline for structured
communication-based programming revisited: Two systems for higher-order
session communication.
Electronic Notes in Theoretical Computer Science,
171(4):73-93, 2007. [ bib ]
Keywords: mobius, wp4 |
| [AlbertAP06] |
E. Albert, P. Arenas, and G. Puebla.
An incremental approach to abstraction-carrying code.
In Logic for Programming Artificial Intelligence and Reasoning,
number 4246 in Lecture Notes in Computer Science, pages 392-406, November
2006. [ bib ]
Keywords: mobius, wp4 |
| [HahnleG06] |
R. Hähnle and T. Gedell.
Automating verification of loops by parallelization.
In M. Hermann, editor, Logic for Programming Artificial
Intelligence and Reasoning, Lecture Notes in Computer Science.
Springer-Verlag, November 2006. [ bib ]
Keywords: mobius, wp3 |
| [PietrzakCPH06] |
P. Pietrzak, J. Correas, G. Puebla, and M. Hermenegildo.
Context-sensitive multivariant assertion checking in modular
programs.
In Logic for Programming Artificial Intelligence and Reasoning,
Lecture Notes in Computer Science. Springer-Verlag, November 2006. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [AlbertAPH06b] |
E. Albert, P. Arenas, G. Puebla, and M. Hermenegildo.
Generation of reduced certificates in abstraction-carrying code.
In VI Jornadas Programación y Lenguajes (PROLE'06), October
2006. [ bib ]
Keywords: mobius, wp4 |
| [MaierAS06] |
P. Maier, D. Aspinall, and I. Stark.
Explicit accounting of resources using resource managers.
Technical Report EDI-INF-RR-0859, The University of Edinburgh,
October 2006. [ bib ]
Keywords: mobius, wp2 |
| [AlbertAP06d] |
E. Albert, P. Arenas, and G. Puebla.
Some issues on incremental abstraction-carrying code.
In Workshop on Logic-Based Methods in Programming Environments,
August 2006. [ bib ]
Keywords: mobius, wp4 |
| [AlbertAPH06] |
E. Albert, P. Arenas, G. Puebla, and M. Hermenegildo.
Reduced certificates for abstraction-carrying code.
In International Conference on Logic Programming, number 4079
in Lecture Notes in Computer Science, pages 163-178. Springer-Verlag, August
2006. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [AlbertGZHP06] |
E. Albert, M. Gómez-Zamalloa, L. Hubert, and G. Puebla.
Towards Java bytecode verification using tools for logic
programming.
In Workshop on Software Verification and Validation, August
2006. [ bib ]
Keywords: mobius, wp4 |
| [AskarovHS06] |
A. Askarov, D. Hedin, and A. Sabelfeld.
Cryptographically-masked flows.
In Static Analysis Symposium, number 4134 in Lecture Notes in
Computer Science, Seoul, Korea, August 2006. Springer-Verlag. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [MeraLPCH] |
E. Mera, P. López-García, G. Puebla, M. Carro, and M. Hermenegildo.
Using combined static analysis and profiling for logic program
execution time estimation.
In International Conference on Logic Programming, number 4079
in Lecture Notes in Computer Science. Springer-Verlag, August 2006. [ bib ]
Keywords: mobius, wp2 |
| [MeraLPCH06] |
E. Mera, P. López-García, G. Puebla, M. Carro, and M. Hermenegildo.
Towards execution time estimation for logic programs via static
analysis and profiling.
In Workshop on Logic Programming Environments, page 16, August
2006. [ bib ]
Keywords: mobius, wp2 |
| [Miller06a] |
D. Miller.
Representing and reasoning with operational semantics.
In U. Furbach and N. Shankar, editors, International Joint
Conference on Automated Reasoning, volume 4130 of Lecture Notes in
Artificial Intelligence, pages 4-20, August 2006. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [PueblaAH06] |
G. Puebla, E. Albert, and M. Hermenegildo.
Abstract interpretation with specialized definitions.
In Static Analysis Symposium, number 4134 in Lecture Notes in
Computer Science, pages 107-126, Seoul, Korea, August 2006. Springer-Verlag. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [CarbobeHY06] |
K. Honda, M. Carbone, and N. Yoshida.
A calculus of global interaction based on session types.
In Workshop on Developments in Computational Models, July 2006. [ bib | http ]
Keywords: mobius, wp4 |
| [HondaBY06] |
K. Honda, M. Berger, and N. Yoshida.
Descriptive and relative completeness of logics for higher-order
functions.
In International Colloquium on Automata, Languages and
Programming, Lecture Notes in Computer Science. Springer-Verlag, July 2006. [ bib ]
Keywords: mobius, wp4 |
| [KopfM06] |
B. Köpf and H. Mantel.
Eliminating Implicit Information Leaks by Transformational Typing
and Unification.
In T. Dimitrakos, F. M. elli, P. Y. A. Ryan, and S. Schneider,
editors, Workshop on Formal Aspects in Security and Trust, Lecture
Notes in Computer Science, pages 47-62, Newcastle, UK, July 2006.
Springer-Verlag. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [Miller06b] |
D. Miller.
Collection analysis for Horn clause programs.
In Principle and Practice of Declarative Programming, pages
179-188, July 2006. [ bib | .pdf ]
Keywords: mobius, wp4 |
| [PueblaO06] |
G. Puebla and C. Ochoa.
Poly-controlled partial evaluation.
In Principle and Practice of Declarative Programming. ACM
Press, July 2006. [ bib ]
Keywords: mobius, wp4 |
| [VasconcelosY06] |
V. Vasconcelos and N. Yoshida.
Language primitives and type discipline for structured
communication-based programming revisited.
In Workshop on Security and Rewriting Techniques, July 2006. [ bib | http ]
Keywords: mobius, wp4 |
| [RussoS06b] |
A. Russo and A. Sabelfeld.
Security for multithreaded programs under cooperative scheduling.
In Andrei Ershov International Conference on Perspectives of
System Informatics, volume 4378 of Lecture Notes in Computer Science.
Springer-Verlag, June 2006. [ bib | www ]
Keywords: mobius, wp2 |
| [MyersSZ06] |
A. C. Myers, A. Sabelfeld, and S. Zdancewic.
Enforcing robust declassification and qualified robustness.
Journal of Computer Security, 14(2):157-196, May 2006. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [RahamanRS06] |
M. A. Rahaman, M. Rits, and A. Schaad.
An inline approach for secure SOAP requests.
In Open Web Application Security Project, May 2006. [ bib ]
Keywords: mobius, wp1 |
| [Reinhard06] |
A. Reinhard.
Analyse nebenläufiger programme unter intransitiven
sicherheitspolitiken.
Master's thesis, RWTH Aachen, May 2006. [ bib ]
Keywords: mobius, wp2 |
| [AlbertPG05] |
E. Albert, G. Puebla, and J. Gallagher.
Non-leftmost unfolding in partial evaluation of logic programs with
impure predicates.
In Logic-based Program Synthesis and Transformation, number
3901 in Lecture Notes in Computer Science. Springer-Verlag, April 2006. [ bib ]
Keywords: mobius, wp4 |
| [CorreasPHB06] |
J. Correas, G. Puebla, M. Hermenegildo, and F. Bueno.
Experiments in context-sensitive analysis of modular programs.
In Logic-based Program Synthesis and Transformation, number
3901 in Lecture Notes in Computer Science. Springer-Verlag, April 2006. [ bib ]
Keywords: mobius, wp4 |
| [GallagherPA05] |
J. Gallagher, G. Puebla, and E. Albert.
Converting one type-based abstract domain to another.
In Logic-based Program Synthesis and Transformation, number
3901 in Lecture Notes in Computer Science. Springer-Verlag, April 2006. [ bib ]
Keywords: mobius, wp4 |
| [OchoaPH06] |
C. Ochoa, G. Puebla, and M. Hermenegildo.
Removing superfluous versions in polyvariant specialization of
Prolog programs.
In Logic-based Program Synthesis and Transformation, number
3901 in Lecture Notes in Computer Science. Springer-Verlag, April 2006. [ bib ]
Keywords: mobius, wp4 |
| [AlbertAP06c] |
E. Albert, P. Arenas, and G. Puebla.
Incremental certificates and checkers for abstraction-carrying code.
In Workshop on the Issues in the Theory of Security, March
2006. [ bib ]
Keywords: mobius, wp4 |
| [PueblaAAH06] |
G. Puebla, E. Albert, P. Arenas, and M. Hermenegildo.
On abstraction-carrying code and certificate-size reduction.
In Emerging Applications of Abstract Interpretation, March
2006. [ bib ]
Keywords: mobius, wp4 |
| [APLAS06] |
N. Kobayashi, editor.
Programming Languages and Systems: Proceedings of the 4th Asian
Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, volume 4279
of Lecture Notes in Computer Science. Springer-Verlag, 2006. [ bib ] |
| [BartheGKR06] |
G. Barthe, B. Grégoire, C. Kunz, and T. Rezk.
Certificate translation for optimizing compilers.
In K. Yi, editor, Static Analysis Symposium, number 4134 in
Lecture Notes in Computer Science, pages 301-317. Springer-Verlag, 2006. [ bib | http ]
Keywords: mobius, wp4 |
| [BartheNR06] |
G. Barthe, D. Naumann, and T. Rezk.
Deriving an information flow checker and certifying compiler for
Java.
In Symposium on Security and Privacy. IEEE Press, 2006. [ bib | .pdf ]
Keywords: mobius |
| [BeringerH06] |
L. Beringer and Martin Hofmann.
A bytecode logic for JML and types.
In Kobayashi [APLAS06], pages 389-405. [ bib | http ]
Keywords: mobius, wp3, wp2 |
| [BessonDJ06] |
Fréderic Besson, Guillaume Dufay, and Thomas Jensen.
A formal model of access control for mobile interactive devices.
In ESORICS 2006 [ESORICS06]. [ bib ]
Keywords: mobius, wp2 |
| [BurdyP06] |
L. Burdy and M. Pavlova.
Java bytecode specification and verification.
In Symposium on Applied Computing, pages 1835-1839. ACM Press,
2006. [ bib ]
Keywords: mobius, wp3 |
| [ChalinKLP06] |
P. Chalin, J. R. Kiniry, G. T. Leavens, and Erik Poll.
Beyond assertions: Advanced specification and verification with JML
and ESC/Java2.
In Springer-Verlag, editor, Formal Methods for Components and
Objects, volume 4111 of Lecture Notes in Computer Science, pages
342-363, 2006. [ bib | .pdf ]
Keywords: mobius, wp6 |
| [Charles06] |
J. Charles.
Adding native specifications to JML.
In Workshop on Formal Techniques for Java Programs, 2006. [ bib | .pdf ]
Keywords: mobius, wp1 |
| [CieleckiFJJCSK06] |
M. Cielecki, J. Fulara, K. Jakubczyk, . Jancewicz, J. Chrz aszcz,
A. Schubert, and . Kaminski.
Propagation of JML non-null annotations in Java programs.
In Principles and Practices of Programming in Java, 2006. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [Dezani-CiancagliniMYD0306] |
M. Dezani-Ciancaglini, D. Mostrous, N. Yoshida, and S. Drossopoulou.
Session types for object-oriented languages.
In European Conference on Object-Oriented Programming, Lecture
Notes in Computer Science. Springer-Verlag, 2006. [ bib ]
Keywords: mobius, wp4 |
| [DietlDM06a] |
W. Dietl, S. Drossopoulou, and P. Müller.
Formalization of generic universe types.
Technical Report 532, ETH Zurich, 2006. [ bib ]
Keywords: mobius, wp2 |
| [ESOP06] |
Programming Languages and Systems: Proceedings of the 15th European
Symposium on Programming, ESOP 2006, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria,
March 27-28, 2006, volume 3924 of Lecture Notes in Computer Science.
Springer-Verlag, 2006. [ bib ] |
| [ESORICS06] |
Computer Security - ESORICS 2006, Proceedings of the 11th European
Symposium on Research in Computer Security, Hamburg, Germany,
September 18-20, 2006, number 4189 in Lecture Notes in Computer Science.
Springer-Verlag, 2006. [ bib ] |
| [HaehnleG07] |
R. Hähnle and T. Gedell.
Verification by parallelization of parametric code.
In Algebraic and Proof-theoretic Aspects of Non-classical Logics
Essays in honour of Professor Daniele Mundici on occasion of his 60th
birthday, Lecture Notes in Computer Science. Springer-Verlag, 2006.
To appear. [ bib ]
Keywords: mobius, wp3 |
| [HofmannJ06] |
M. Hofmann and S. Jost.
Type-based amortised heap-space analysis.
In ESOP 2006 [ESOP06], pages 22-37. [ bib ]
Keywords: mobius, wp2 |
| [HuismanWS06] |
M. Huisman, P. Worah, and K. Sunesen.
A temporal logic characterisation of observational determinism.
In Computer Security Foundations Workshop, 2006. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [HuntS06] |
S. Hunt and D. Sands.
On flow-sensitive security types.
In Principles of Programming Languages, Charleston, South
Carolina, USA, January 2006. ACM Press. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [KiniryMD06] |
J. R. Kiniry, A. Morkan, and B. Denby.
Soundness and completeness warnings in ESC/Java2.
In Specification and Verification of Component-Based Systems,
2006. [ bib | .pdf ]
Keywords: mobius, ircset, wp3 |
| [LaudUV05] |
P. Laud, T. Uustalu, and V. Vene.
Type systems equivalent to data-flow analyses for imperative
languages.
Theoretical Computer Science, 364(3):292-310, 2006. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [LeinoM06] |
K. Rustan M. Leino and Peter Müller.
A verification methodology for model fields.
In ESOP 2006 [ESOP06], pages 115-130. [ bib ]
Keywords: mobius, wp3 |
| [MantelSK06] |
H. Mantel, H. Sudbrock, and T. Krauß er.
Combining different proof techniques for verifying information flow
security.
In G. Puebla, editor, Logic-based Program Synthesis and
Transformation, volume Raporta di Ricerca CS-2006-5, Università
Ca' Foscari Di Venezia, Venice, Italy, July 12-14 2006. [ bib | .pdf ]
Keywords: mobius, wp2 |
| [MobiusDeliverable1.1] |
Consortium.
Deliverable 1.1: Resource and information flow security requirements,
2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp1 |
| [MobiusDeliverable1.2] |
Consortium.
Deliverable 1.2: Framework-specific and application-specific security
requirements, 2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp1 |
| [MobiusDeliverable2.1] |
Consortium.
Deliverable 2.1: Intermediate report on type systems, 2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp2 |
| [MobiusDeliverable2.2] |
Consortium.
Deliverable 2.2: Intermediate report on implementation of type
systems, 2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp2 |
| [MobiusDeliverable3.1] |
Consortium.
Deliverable 3.1: Bytecode specification language and program logic,
2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp3 |
| [MobiusDeliverable4.1] |
Consortium.
Deliverable 4.1: Scenarios for proof-carrying code, 2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp4 |
| [MobiusDeliverable6.1] |
Consortium.
Deliverable 6.1: Dissemination and training plan, 2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp6 |
| [MobiusDeliverable6.2] |
Consortium.
Deliverable 6.2: Dissemination and training activity report, year 1,
2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp6 |
| [MobiusDeliverable6.3] |
Consortium.
Deliverable 6.3: Demonstration plan, 2006.
Available online from http://mobius.inria.fr. [ bib ]
Keywords: mobius, wp6 |
| [OsvigST06] |
D. A. Osvik, A. Shamir, and E. Tromer.
Cache attacks and countermeasures: the case of AES.
In RSA Conference, pages 1-20, 2006. [ bib ]
Keywords: mobius, wp2 |
| [RussoS06a] |
A. Russo and A. Sabelfeld.
Securing interaction between threads and the scheduler.
In Computer Security Foundations Workshop, pages 177-189,
2006. [ bib | www ]
Keywords: mobius, wp2 |
| [SaabasU06a] |
A. Saabas and T. Uustalu.
Compositional type systems for stack-based low-level languages.
In B. Jay and J. Gudmundsson, editors, Computing, Australasian
Theory Symposium, volume 51 of Conference in Research and Practice in
Information Technology, pages 27-39. Australian Computer Society, 2006. [ bib | http | .pdf ]
Keywords: mobius |
| [SaabasU06b] |
A. Saabas and T. Uustalu.
A compositional natural semantics and Hoare logic for low-level
languages.
In P. D. Mosses and I. Ulidowski, editors, Workshop on
Structured Operational Semantics, volume 156(1) of Electronic Notes in
Theoretical Computer Science, pages 151-168. Elsevier, 2006. [ bib | .pdf ]
Keywords: mobius |
| [SchubertC06] |
A. Schubert and J. Chrz aszcz.
ESC/Java2 as a tool to ensure security in the source code of Java
applications.
In Software Engineering Techniques: Design for Quality, IFIP,
Warsaw, 2006. Springer-Verlag. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [Yoshida06] |
Nobuko Yoshida.
Type-based security for mobile computing integrity, secrecy and
liveness.
ENTCS, 162:333-340, 2006. [ bib ]
Keywords: mobius, wp2 |
| [TiuNM05] |
A. Tiu, G. Nadathur, and D. Miller.
Mixing finite success and finite failure in an automated prover.
In Empirically Successful Automated Reasoning in Higher-Order
Logics, pages 79-98, December 2005. [ bib | .pdf ]
Keywords: mobius |
| [Uustalu05] |
T. Uustalu.
Article in TUT newspaper, Mente & Manu, November 2005. [ bib | .pdf ]
Keywords: mobius |
| [Barthe05] |
G. Barthe.
MOBIUS - Securing the next generation of Java-based global
computers.
ERCIM News, 63:28-29, October 2005. [ bib | .pdf ]
Keywords: mobius, wp6 |
| [KiniryCH05] |
J. R. Kiniry, P. Chalin, and C. Hurlin.
Integrating static checking and interactive verification: Supporting
multiple theories and provers in verification.
In Verified Software: Theories, Tools, Experiements, October
2005. [ bib | .pdf ]
Keywords: mobius, wp3 |
| [AskarovS05] |
A. Askarov and A. Sabelfeld.
Security-typed languages for implementation of cryptographic
protocols: A case study.
In European Symposium On Research In Computer Security, number
3679 in Lecture Notes in Computer Science. Springer-Verlag, September 2005. [ bib | .pdf ]
Keywords: mobius, wp1 |
| [HermenegildoALGP05] |
M. Hermenegildo, E. Albert, P. López-García, and G. Puebla.
Abstraction carrying code and resource-awareness.
In Principle and Practice of Declarative Programming. ACM
Press, July 2005. [ bib ]
Keywords: mobius, wp2 |
| [AhernY04] |
A. Ahern and N. Yoshida.
Formalising Java RMI with explicit code mobility.
In R. Johnson and R. P. Gabriel, editors, ACM Conference on
Object-Oriented Programming Systems, Languages, and Applications, pages
403-422. ACM Press, 2005.
A full version will appear in Theoretical Computer Science,
special issue of Global Computing. [ bib ]
Keywords: mobius, wp2 |
| [AlbertPH04a] |
E. Albert, G. Puebla, and M. V. Hermenegildo.
Abstraction-carrying code.
In F. and A. Voronkov, editors, Logic for Programming Artificial
Intelligence and Reasoning, number 3452 in Lecture Notes in Computer
Science, pages 380-397. Springer-Verlag, 2005. [ bib ]
Keywords: mobius, wp4 |
| [BegerHY05] |
M. Berger, K. Honda, and N. Yoshida.
A logical analysis of aliasing for higher-order imperative functions.
In International Conference on Functional Programming, 2005. [ bib ]
Keywords: mobius, wp2 |
| [DezaniYAD05] |
M. Dezani-Ciancaglini, N. Yoshida, A. Ahern, and S. Drossopoulou.
A distributed object oriented language with session types.
In Trustworthy Global Computing, volume 3705 of Lecture
Notes in Computer Science, pages 299-318, 2005. [ bib ]
Keywords: mobius, wp4 |
| [HondaYB05] |
K. Honda, N. Yoshida, and M. Berger.
An observationally complete program logic for imperative higher-order
functions.
In Logic in Computer Science, pages 270-279, 2005. [ bib ]
Keywords: mobius, wp4 |
| [HermenegildoALGP04] |
M. Hermenegildo, E. Albert, P. López-García, and G. Puebla.
Some techniques for automated, resource-aware distributed and mobile
computing in a multi-paradigm programming system.
In EURO-PAR, number 3149 in Lecture Notes in Computer Science,
pages 21-37. Springer-Verlag, August 2004. [ bib ]
Keywords: mobius, wp2 |
| [HondaYB04] |
K. Honda, N. Yoshida, and M. Berger.
Control in the pi-calculus.
In ACM SIGPLAN Continuation Workshop. ACM Press, 2004. [ bib ]
Keywords: mobius, wp2 |
| [CarboneHY] |
M. Carbone, K. Honda, and N. Yoshida.
A theoretical basis of communication-centered concurrent programming.
Web Services Choreography Working Group mailing list, to appear as a
WS-CDL working report. [ bib ]
Keywords: mobius, wp4 |
| [CunninghamDDFM06] |
D. Cunningham, W. Dietl, S. Drossopoulou, A. Francalanza, and P. Müller.
UJ: Type soundness for universe types.
To appear at http://slurp.doc.ic.ac.uk/pubs.html\#uj06. [ bib | http ]
Keywords: mobius, wp2 |
| [DietlDM06] |
W. Dietl, S. Drossopoulou, and P. Müller.
GUJ: Generic universe types.
Preliminary version available from
http://www.sct.ethz.ch/publications/index.html. [ bib | .html ]
Keywords: mobius, wp2 |
| [PollackS09] |
Randy Pollack and Masahiko Sato.
External and internal syntax of the lambda-calculus.
Journal of Symbolic Computation, to appear. [ bib ]
Keywords: mobius, wp3 |