IMDEA initiative

Home > Research > Publications

IMDEA Software Institute's Publications



Articles in Refereed Journals

  1. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Local Reasoning for Global Invariants, Part I: Region Logic. Journal of the ACM, To Appear, 2013.
  2. Anindya Banerjee, David A. Naumann. Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. Journal of the ACM, To Appear, 2013.
  3. Manuel Carro, Ángel Herranz, Julio Mariño. A Model-Driven Approach to Teaching Concurrency. ACM Transactions on Computer Education, Vol. 13, Num. 1, 2013.
  4. Kyriakos Kritikos, Barbara Pernici, Pierluigi Plebani, Cinzia Cappiello, Marco Comuzzi, Salima Benbernou, Ivona Brandic, Attila Kertesz, Michael Parkin, Manuel Carro. A Survey on Service Quality Description. ACM Computing Surveys, To Appear, 2013.
  5. Dragan Ivanovic, Manuel Carro, Manuel V. Hermenegildo. A Sharing-Based Approach to Supporting Adaptation in Service Compositions. Computing, To Appear, Springer Wien, November 2012. 10.1007/s00607-012-0230-z.
  6. Juan Caballero, Dawn Song. Automatic Protocol Reverse-Engineering: Message Format Extraction and Field Semantics Inference. Computer Networks, To Appear, September 2012.
  7. Marina Zapater, César Sánchez, José L. Ayala, José M. Moya, José L. Risco-Martín. Ubiquitous Green Computing Techniques for High Demand Applications in Smart Environments. Sensors, Vol. 12, Num. 8, pages 10659--10677, August 2012.
  8. Juan Caballero. Understanding the Role of Malware in Cybercrime. ERCIM News, Vol. 2012, Num. 90, pages 15--16, July 2012.
  9. M. V. Hermenegildo, F. Bueno, M. Carro, P. López, E. Mera, J.F. Morales, G. Puebla. An Overview of Ciao and its Design Philosophy. Theory and Practice of Logic Programming, Vol. 12, Num. 1--2, pages 219--252, Cambridge University Press, January 2012. http://arxiv.org/abs/1102.5497.
  10. Murdoch J. Gabbay, Aleksandar Nanevski. Denotation of syntax and metaprogramming in contextual modal type theory (CMTT). Journal of Applied Logic (JAL), To Appear, 2012.
  11. Gilles Barthe, Jorge Cuéllar, Javier Lopez, Alexander Pretschner. Preface. Journal of Computer Security, Vol. 20, Num. 4, pages 307--308, 2012.
  12. Gilles Barthe, David Pichardie, Tamara Rezk. A Certified Lightweight Non-interference Java Bytecode Verifier. Mathematical Structures in Computer Science, To Appear, Cambridge University Press, 2012.
  13. Maria-Cristina Marinescu, César Sánchez. Fusing Statecharts and Java. ACM Transactions on Embedded Computing Systems, To Appear, 2012.
  14. Mark Marron, César Sánchez, Zhendong Su, Manuel Fähndrich. Abstracting Runtime Heaps for Program Understanding. IEEE Transactions on Software Engineering, Vol. 99, IEEE Computer Society, 2012.
  15. J. F. Morales, R. Haemmerlé, M. Carro, M. V. Hermenegildo. Lightweight compilation of (C)LP to JavaScript. Theory and Practice of Logic Programming, 28th Int'l. Conference on Logic Programming (ICLP'12) Special Issue, Vol. 12, Num. 4-5, pages 755--773, Cambridge U. Press, 2012.
  16. E. Albert, P. Arenas, G. Puebla, M. Hermenegildo. Certificate Size Reduction in Abstraction-Carrying Code. Theory and Practice of Logic Programming, Vol. 12, Num. 3, pages 283--318, 2012.
  17. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. Theories, Solvers and Static Analysis by Abstract Interpretation. Journal of the ACM, To Appear, ACM, 2012.
  18. Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir E. Dullerud. Verification of Bounded Discrete Horizon Hybrid Automata. IEEE Transactions on Automatic Control, Vol. 57, Num. 6, pages 1445--1455, 2012.
  19. Pierre Ganty, Rupak Majumdar. Algorithmic Verification of Asynchronous Programs. ACM Transactions on Programming Languages and Systems, To Appear, 2012.
  20. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Bounded Underapproximations. Formal Methods in System Design, Vol. 40, Num. 2, pages 206--231, 2012.
  21. Isabella Mastroeni, Anindya Banerjee. Modelling Declassification Policies using Abstract Domain Completeness. Mathematical Structures in Computer Science, Vol. 21, Num. 6, pages 1253--1299, December 2011.
  22. Gilles Barthe, Pedro D'Argenio, Tamara Rezk. Secure Information Flow by Self-Composition. Mathematical Structures in Computer Science, Vol. 21, Num. 6, pages 1207--1252, Cambridge University Press, October 2011.
  23. Gilles Barthe, César Kunz. An Abstract Model of Certificate Translation. ACM Trans. Program. Lang. Syst., Vol. 33, Num. 4, pages 1--13, ACM, July 2011.
  24. P. Chico de Guzmán, A. Casas, M. Carro, M. Hermenegildo. Parallel Backtracking with Answer Memoing for Independent And-Parallelism. Theory and Practice of Logic Programming, 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue, Vol. 11, Num. 4--5, pages 555--574, Cambridge U. Press, July 2011.
  25. G. Puebla, E. Albert, M. Hermenegildo. Efficient Local Unfolding with Ancestor Stacks. Theory and Practice of Logic Programming, Vol. 11, Num. 1, pages 1--32, Cambridge U. Press, January 2011.
  26. Julien Bertrane, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, X. Rival. Static Analysis by Abstract Interpretation of Embedded Critical Software. Software Engineering Notes, Vol. 36, Num. 1, pages 1--8, ACM, January 2011.
  27. Boris Köpf, David Basin. Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks. Journal of Computer Security, Vol. 1, pages 1--31, 2011.
  28. Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir E. Dullerud. Specifications for decidable hybrid games. Theoretical Computer Science, Vol. 412, Num. 48, pages 6770--6785, 2011.
  29. Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger. Parikh's Theorem: A simple and direct automaton construction. Information Processing Letters, Vol. 111, pages 614--619, 2011.
  30. Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld. Security of Multithreaded Programs by Compilation. ACM Trans. Inf. Syst. Secur., Vol. 13, Num. 3, 2010.
  31. A. Stivala, P. J. Stuckey, M. García de la Banda, M. Hermenegildo, A. Wirth. Lock-free Parallel Dynamic Programming. Journal of Parallel and Distributed Computing, Vol. 70, pages 839--848, Elsevier, 2010.
  32. P. López-García, F. Bueno, M. Hermenegildo. Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Information. New Generation Computing, Vol. 28, Num. 2, pages 117--206, Ohmsha, Ltd. and Springer, 2010.
  33. M. Egea, V. Rusu. Formal Executable Semantics for Conformance in the MDE Framework. Innovations in Systems and Software Engineering, Vol. 6, pages 73--81, Springer London, 2010.
  34. Pierre Ganty, Nicolas Maquet, Jean-Francois Raskin. Fixed Point Guided Abstraction Refinement for Alternating Automata. Theor. Comput. Sci., Vol. 411, Num. 38-39, pages 3444--3459, 2010.
  35. D. Cabeza, M. Hermenegildo. Non-Strict Independence-Based Program Parallelization Using Sharing and Freeness Information. Theoretical Computer Science, Vol. 46, Num. 410, pages 4704--4723, Elsevier Science, October 2009.
  36. Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk. Certificate Translation for Optimizing Compilers. ACM Trans. Program. Lang. Syst., Vol. 31, Num. 5, ACM, July 2009.
  37. Elvira Albert, John P. Gallagher, Miguel Gómez-Zamalloa, Germán Puebla. Type-based homeomorphic embedding for online termination. Inf. Process. Lett., Vol. 109, Num. 15, pages 879--886, Elsevier, July 2009.
  38. Toufik Taibi, Ángel Herranz, Juan José Moreno-Navarro. Stepwise Refinement Validation of Design Patterns Formalized in TLA+ Using the TLC Model Checker. Journal of Object Technology (JOT, (available online)), Vol. 8, Num. 2, pages 137--161, March 2009.
  39. Julio Mariño, Juan José Moreno-Navarro, Susana Muñoz Hernández. Implementing Constructive Intensional Negation. New Generation Computing, Vol. 27, Num. 1, pages 25--56, January 2009.
  40. D. Basin, M. Clavel, J. Doser, M. Egea. Automated Analysis of Security-Design Models. Information & Software Technology, Vol. 51, Num. 5, pages 815--831, 2009.
  41. E. Albert, G. Puebla, M. Hermenegildo. Abstraction-Carrying Code: A Model for Mobile Code Safety. New Generation Computing, Vol. 26, Num. 2, pages 171--204, March 2008.
  42. Julio Mariño, Ángel Herranz, Juan José Moreno-Navarro. Demandedness Analysis with Partial Predicates. Theory and Practice of Logic Programming, Vol. 7, Num. 1-2, pages 153--182, January 2007.
  43. M. Clavel, J. Meseguer, M. Palomino. Reflection in Membership Equational Logic, Many-Sorted Equational Logic, Horn Logic with Equality, and Rewriting Logic. Theoretical Computer Science, Vol. 373, Num. 1-2, pages 70--91, 2007.


Articles in Refereed Conferences

  1. Z. Drey, J. F. Morales, M. V. Hermenegildo, M. Carro. Reversible Language Extensions and their Application in Debugging. Practical Aspects of Declarative Languages (PADL'13), LNCS, Vol. 7752, Springer, January 2013.
  2. P. Chico de Guzmán, and M. Carro, M. Hermenegildo. Supporting Pruning in Tabled LP. Practical Aspects of Declarative Languages (PADL'13), LNCS, Springer Verlag, January 2013.
  3. Ruy Ley-Wild, Aleksandar Nanevski. Subjective Auxiliary State for Coarse-Grained Concurrency. Principles of Programming Languages (POPL), 2013. To appear.
  4. Mark Batty, Mike Dodds, Alexey Gotsman. Library abstraction for C/C++ concurrency. Proceedings of the 40th ACM Symposium on Principles of Programming Languages (POPL'13), Rome, Italy, ACM Press, 2013. To appear.
  5. Gilles Barthe, Juan Manuel Crespo, César Kunz. Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. Logical Foundations of Computer Science, International Symposium, LFCS 2013, Lecture Notes in Computer Science, Vol. 7734, pages 29--43, Springer, 2013.
  6. Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron. From Relational Verification to SIMD Loop Synthesis. ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '13, pages 123--134, ACM, 2013.
  7. Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan. Hybrid Automata based CEGAR for Rectangular Hybrid Automata. VMCAI, 2013. To appear.
  8. Dragan Ivanovic, Manuel Carro, Manuel Hermenegildo. A Constraint-Based Approach to Quality Assurance in Service Choreographies. 10th International Conference on Service Oriented Computing, ICSOC'12, LNCS, Num. 7637, Springer Verlag, November 2012.
  9. Chris Grier, Lucas Ballard, Juan Caballero, Neha Chachra, Christian J. Dietrich, Kirill Levchenko, Panayiotis Mavrommatis, Damon McCoy, Antonio Nappa, Andreas Pitsillidis, Niels Provos, M. Zubair Rafique, Moheeb Abu Rajab, Christian Rossow, Kurt Thomas, Vern Paxson, Stefan Savage, Geoffrey M. Voelker. Manufacturing Compromise: The Emergence of Exploit-as-a-Service. Proceedings of the 19th ACM Conference on Computer and Communication Security, October 2012.
  10. George Bariannys, Manuel Carro, Dimitris Plexousakis. Deriving Specifications for Composite Web Services. IEEE Signature Conference on Computers, Software, and Applications, IEEE Computer Society, IEEE, July 2012.
  11. J. F. Morales, M. V. Hermenegildo, R. Haemmerlé. Modular Extensions for Modular (Logic) Languages. Proceeding of the 21th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'11), LNCS, Vol. 7225, pages 139--154, Springer, July 2012.
  12. Juan Caballero, Gustavo Grieco, Mark Marron, Antonio Nappa. Early Detection of Dangling Pointers in Use-After-Free and Double-Free Vulnerabilities. Proceedings of the 2012 International Symposium on Software Testing and Analysis, July 2012.
  13. P. Chico de Guzmán, M. Carro, M. Hermenegildo, P. Stuckey. A General Implementation Framework for Tabled CLP. FLOPS'12, LNCS, Num. 7294, pages 104--119, Springer Verlag, May 2012.
  14. P. Chico de Guzmán, A. Casas, M. Carro, M. Hermenegildo. A Segment-Swapping Approach for Executing Trapped Computations. PADL'12, LNCS, Vol. 7149, pages 138--152, Springer Verlag, January 2012.
  15. Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang. Show no weakness: sequentially consistent specifications of TSO libraries. Proceedings of the International Symposium on Distributed Computing (DISC'12), Salvador, Bahia, Brazil, LNCS, Vol. 7611, pages 31--45, Springer, 2012.
  16. Alexey Gotsman, Hongseok Yang. Linearizability with ownership transfer. Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), Newcastle upon Tyne, UK, LNCS, Vol. 7454, pages 256--271, Springer, 2012.
  17. Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang. Concurrent library correctness on the TSO memory model. Proceedings of the 21st European Symposium on Programming (ESOP'12), Tallinn, Estonia, LNCS, Vol. 7211, pages 87--107, Springer, 2012.
  18. Stan Rosenberg, Anindya Banerjee, David A. Naumann. Decision Procedures for Region Logic. VMCAI, pages 379--395, 2012.
  19. Alexander Malkis, Anindya Banerjee. Verification of software barriers. PPOPP, pages 313--314, 2012.
  20. Mark Marron, Ondrej Lhoták, Anindya Banerjee. Programming Paradigm Driven Heap Analysis. CC, pages 41--60, 2012.
  21. José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin. Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. ACM Conference on Computer and Communications Security, pages 488--500, 2012.
  22. Gilles Barthe, David Pointcheval, Santiago Zanella Béguelin. Verified Security of Redundancy-Free Encryption from Rabin and RSA. ACM Conference on Computer and Communications Security, pages 724--735, 2012.
  23. Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. Certified Programs and Proofs - Second International Conference, CPP 2012, Lecture Notes in Computer Science, Vol. 7679, pages 7--8, Springer, 2012.
  24. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna. Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. 25th IEEE Computer Security Foundations Symposium, CSF 2012, pages 186--197, IEEE, 2012.
  25. Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin. Verified Security of Merkle-Damgrd. 25th IEEE Computer Security Foundations Symposium, CSF 2012, pages 354--368, IEEE, 2012.
  26. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin. Computer-Aided Cryptographic Proofs. Interactive Theorem Proving - Third International Conference, ITP 2012, Lecture Notes in Computer Science, Vol. 7406, pages 11--27, Springer, 2012.
  27. Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas. Secure Multi-Execution through Static Program Transformation. Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Lecture Notes in Computer Science, Vol. 7273, pages 186--202, Springer, 2012.
  28. Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. Mathematics of Program Construction - 11th International Conference, MPC 2012, Lecture Notes in Computer Science, Vol. 7342, pages 1--6, Springer, 2012.
  29. Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin. Computer-Aided Cryptographic Proofs. Static Analysis - 19th International Symposium, SAS 2012, Lecture Notes in Computer Science, Vol. 7460, pages 1--2, Springer, 2012.
  30. Gilles Barthe, Delphine Demange, David Pichardie. A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. 21st European Symposium on Programming, ESOP 2012, Lecture Notes in Computer Science, Vol. 7211, pages 47--66, Springer, 2012.
  31. Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pages 97--110, ACM, 2012.
  32. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin. Verified Indifferentiable Hashing into Elliptic Curves. 1st Conference on Principles of Security and Trust, POST 2012, Lecture Notes in Computer Science, Vol. 7215, Springer, 2012.
  33. Boris Köpf, Laurent Mauborgne, Martín Ochoa. Automatic Quantification of Cache Side-Channels. 24th International Conference on Computer Aided Verification (CAV '12), Lecture Notes in Computer Science, Vol. 7358, pages 564--580, Springer-Verlag, 2012.
  34. Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin. Probabilistic Relational Reasoning for Differential Privacy. Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12), pages 97--109, ACM, 2012.
  35. Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, Bor-Yuh Evan Chang. Invariant Generation for Parametrized Systems Using Self-reflection. Proc. of the 19th International Symposium on Static Analysis (SAS'12), LNCS, Vol. 7460, pages 146--163, Springer, 2012.
  36. César Sánchez, Julián Samborski-Forlese. Efficient Regular Linear Temporal Logic Using Dualization and Stratification. Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME'12), pages 13--20, IEEE Computer Society, 2012.
  37. César Sánchez, Julián Samborski-Forlese. How to Translate Efficiently Extensions of Temporal Logics into Alternating Automata. Proceedings of The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC'12), LNCS, Vol. 7521, pages 30--45, Springer, 2012.
  38. Mai Ajspur, John P. Gallagher. Towards Abstract Interpretation of Epistemic Logic. 8th Scandinavian Logic Symposium, 20-21 August 2012, Roskilde University, Denmark, Roskilde University, 2012. Extended Abstract.
  39. Boris Köpf, Laurent Mauborgne, Matín Ochoa. Automatic Quantification of Cache Side-Channels. 24th International Conference on Computer Aided Verification (CAV 2012), Lecture Notes in Computer Science, Vol. 7358, pages 564--580, Springer-Verlag, 2012.
  40. Pavithra Prabhakar. Foundations for Approximation Based Analysis of Stability Properties of Hybrid Systems. 50th Annual Allerton Conference on Communication, Control and Computing, 2012.
  41. Pavithra Prabhakar, Mahesh Viswanathan. Conformance Testing of Boolean Programs with Multiple Faults. Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings, Lecture Notes in Computer Science, Vol. 7273, pages 101--117, Springer, 2012.
  42. Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan. Pre-orders for reasoning about stability. Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC'12, Beijing, China, April 17-19, 2012, pages 197--206, ACM, 2012.
  43. Javier Esparza, Pierre Ganty, Rupak Majumdar. A Perfect Model for Bounded Verification. LICS '12: Proc. 27th Annual ACM/IEEE Symp. on Logic in Computer Science, 2012.
  44. Ruy Ley-Wild, Umut A. Acar, Guy Blelloch. Non-Monotonic Self-Adjusting Computation. European Symposium on Programming, ESOP 2012, Lecture Notes in Computer Science, Vol. 7211, pages 476--496, Springer, 2012.
  45. D. Ivanović, M. Carro, M. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. Service-Oriented Computing -- ICSOC 2011, LNCS, Num. 7084, pages 62--76, Springer Verlag, December 2011. Best paper award.
  46. Juan Manuel Crespo, César Kunz. A Machine-Checked Framework for Relational Separation Logic. Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, LNCS, Vol. 7041, pages 122--137, Springer, November 2011.
  47. Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin. Verifiable Security of Boneh-Franklin Identity-Based Encryption. 5th International Conference on Provable Security -- ProvSec 2011, Lecture Notes in Computer Science, Vol. 6980, pages 68--83, Springer, October 2011.
  48. Barthe, Gilles, Grégoire, Benjamin, Heraud, Sylvain, Zanella Béguelin, Santiago. Computer-Aided Security Proofs for the Working Cryptographer. Advances in Cryptology -- CRYPTO 2011, Lecture Notes in Computer Science, Vol. 6841, pages 71--90, Springer, August 2011.
  49. Juan Caballero, Chris Grier, Christian Kreibich, Vern Paxson. Measuring Pay-per-Install: The Commoditization of Malware Distribution. Proceedings of the 20th USENIX Security Symposium, August 2011.
  50. R. Haemmerlé, P. López, M. Hermenegildo. CLP Projection for Constraint Handling Rules. Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 137--148, ACM Press, July 2011.
  51. D. Ivanović, M. Carro, M. Hermenegildo. Automated Attribute Inference in Complex Service Workflows Based on Sharing Analysis. Proceedings of the 8th IEEE Conference on Services Computing SCC 2011, pages 120--127, IEEE Press, July 2011.
  52. Gilles Barthe, Juan Manuel Crespo, César Kunz. Relational Verification Using Product Programs. FM 2011: 17th International Symposium on Formal Methods, LNCS, Vol. 6664, pages 200--214, Springer, June 2011.
  53. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna. Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. FM 2011: 17th International Symposium on Formal Methods, LNCS, Vol. 6664, pages 231--245, Springer, June 2011.
  54. David A. Basin, Manuel Clavel, Marina Egea. A decade of model-driven security. SACMAT 2011, 16th ACM Symposium on Access Control Models and Technologies, pages 1--10, ACM, June 2011.
  55. Delbianco, Germán Andrés, Jaskelioff, Mauro, Pardo, Alberto. Applicative Shortcut Fusion. 12th International Symposium on Trends in Functional Programming, TFP'11, May 2011.
  56. Noah M. Johnson, Juan Caballero, Kevin Chen, Stephen McCamant, Pongsin Poosankam, Daniel Reynaud, Dawn Song. Differential Slicing: Identifying Causal Execution Differences for Security Applications. Proceedings of the IEEE Symposium on Security and Privacy, May 2011.
  57. Barthe, Gilles, Grégoire, Benjamin, Lakhnech, Yassine, Zanella Béguelin, Santiago. Beyond Provable Security Verifiable IND-CCA Security of OAEP. Topics in Cryptology --- CT-RSA 2011, Lecture Notes in Computer Science, Vol. 6558, pages 180--196, Springer, February 2011.
  58. E. Mera, T. Trigo, P. López-García, M. Hermenegildo. Profiling for Run-Time Checking of Computational Properties and Performance Debugging. Practical Aspects of Declarative Languages (PADL'11), LNCS, Vol. 6539, pages 38--53, Springer-Verlag, January 2011.
  59. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. How to make ad hoc proof automation less ad hoc. International Conference on Functional Programming (ICFP), pages 163--175, 2011.
  60. Aleksandar Nanevski, Anindya Banerjee, Deepak Garg. Verification of Information Flow and Access Control Policies with Dependent Types. IEEE Symposium on Security and Privacy (S&P), pages 165--179, 2011.
  61. Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski. Partiality, State and Dependent Types. Typed Lambda Calculi and Applications (TLCA), pages 198--212, 2011.
  62. Alexey Gotsman, Hongseok Yang. Modular verification of preemptive OS kernels. Proceedings of the 16th ACM International Conference on Functional Programming (ICFP'11), Tokyo, Japan, pages 404--417, ACM Press, 2011.
  63. Alexey Gotsman, Hongseok Yang. Liveness-Preserving Atomicity Abstraction. Proceedings of the 38th International Colloquium on Automata, Languages and Programming, (ICALP'11), Zurich, Switzerland, LNCS, Vol. 6756, pages 453--465, Springer, 2011.
  64. Alexey Gotsman, Josh Berdine, Byron Cook. Precision and the conjunction rule in concurrent separation logic. Proceedings of the 27th Conference on the Mathematical Foundations of Programming Semantics (MFPS'11), Pittsburgh, PA, USA, Elsevier, 2011.
  65. Aleksandar Nanevski, Anindya Banerjee, Deepak Garg. Verification of Information Flow and Access Control Policies with Dependent Types. IEEE Symposium on Security and Privacy, pages 165--179, 2011.
  66. Gilles Barthe, Exequiel Rivas. Static Enforcement of Information Flow Policies for a Concurrent Object-Oriented Language. Sixth Trusted Global Computing Conference 2011 (TGC'11), LNCS, Springer, 2011.
  67. Gilles Barthe, Boris Köpf. Information-theoretic Bounds for Differentially Private Mechanisms. Proc. 24rd IEEE Computer Security Foundations Symposium (CSF '11), pages 191--204, IEEE, 2011.
  68. Michael Backes, Matthias Berg, Boris Köpf. Non-Uniform Distributions in Quantitative Information-Flow. Proc. 6th ACM Conference on Information, Computer and Communications Security (ASIACCS '11), pages 367--375, ACM, 2011.
  69. Alejandro Sánchez, César Sánchez. A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes. Proc. of the 3rd NASA Formal Methods Symposium (NFM'11), LNCS, Vol. 6447, pages 343--358, Springer, 2011.
  70. M. Carro, Dimka Karastoyanova, Grace A. Lewis, Anna Liu. Third International Workshop on Principles of Engineering Service-Oriented Systems (PESOS 2011). ICSE, pages 1218--1219, 2011.
  71. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. The Reduced Product of Abstract Domains and the Combination of Decision Procedures. 14th International Conference on Fondations of Software Science and Computation Structures (FoSSaCS 2011), Lecture Notes in Computer Science, Vol. 6604, pages 456--472, Springer-Verlag, 2011.
  72. Alexander Malkis, Laurent Mauborgne. On the Strength of Owicki-Gries for Resources. 9th Asian Symposium on Programming Languages and Systems (APLAS 2011), Lecture Notes in Computer Science, Vol. 7078, pages 172--187, Springer, 2011.
  73. Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival. Proving the Absence of Runtime Errors with the Static Analyzer Astrée. Society of Automotive Engineering World Congress (SAE 2011), 2011.
  74. David A. Basin, Manuel Clavel, Marina Egea, Miguel Angel García de Dios, Carolina Dania, Gonzalo Ortiz, Javier Valdazo. Model-Driven Development of Security-Aware GUIs for Data-Centric Applications. Foundations of Security Analysis and Design VI (FOSAD 2010), LNCS, Vol. 6858, pages 101--124, Springer, 2011.
  75. Pavithra Prabhakar, Mahesh Viswanathan. A dynamic algorithm for approximate flow computations. Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pages 133--142, ACM, 2011.
  76. Mohamed Faouzi Atig, Pierre Ganty. Approximating Petri Net Reachability Along Context-free Traces. FSTTCS '11: Proc. 31st Int. Conf. on Fondation of Software Technology and Theoretical Computer Science, Leibniz International Proceedings in Informatics (LIPIcs), Vol. 13, Leibniz-Zentrum fuer Informatik, 2011.
  77. Laura Bozzelli, Pierre Ganty. Complexity Analysis of the Backward Coverability Algorithm for VASS. RP '11: Proc. 5th Workshop on Reachability Problems, LNCS, Vol. 6945, Springer, 2011.
  78. Javier Esparza, Pierre Ganty. Complexity of Pattern-based Verification for Multithreaded Programs. POPL '11: Proc. 38th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pages 499--510, ACM Press, 2011.
  79. T. Trigo, P. López-García, S. Muñoz-Hernandez. Towards Fuzzy Granularity Control in Parallel/Distributed Computing. International Conference on Fuzzy Computation (ICFC 2010), pages 43--55, SciTePress, October 2010.
  80. P. López-García, L. Darmawan, F. Bueno. A Framework for Verification and Debugging of Resource Usage Properties. Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 7, pages 104--113, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2010.
  81. Julien Bertrane, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, X. Rival. Static Analysis and Verification of Aerospace Software by Abstract Interpretation. AIAA InfotechAerospace 2010, pages 1--38, American Institue of Aeronautics and Astronautics, April 2010. AIAA-2010-3385.
  82. Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine. Structuring the verification of heap-manipulating programs. Principles of Programming Languages (POPL), pages 261--274, 2010.
  83. Alexander Malkis, Andreas Podelski, Andrey Rybalchenko. Thread-Modular Counterexample-Guided Abstraction Refinement. Static Analysis - 17th International Symposium, SAS 2010, Lecture Notes in Computer Science, Vol. 6337, pages 356--372, Springer, 2010.
  84. Moritz Y. Becker, Alexander Malkis, Laurent Bussard. A Practical Generic Privacy Language. Information Systems Security - 6th International Conference, ICISS 2010, Lecture Notes in Computer Science, Vol. 6503, pages 125--139, Springer, 2010.
  85. David A. Naumann, Anindya Banerjee. Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. ESOP, pages 2--22, 2010.
  86. Stan Rosenberg, Anindya Banerjee, David A. Naumann. Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. VSTTE, pages 183--198, 2010.
  87. Gilles Barthe, Pablo Buiras, César Kunz. A Functional Framework for Result Checking. Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Lecture Notes in Computer Science, Vol. 6009, pages 72--86, Springer, 2010.
  88. Gilles Barthe, César Kunz. Perspectives in Certificate Translation. Trustworthly Global Computing - 5th International Symposium, TGC 2010, Lecture Notes in Computer Science, Vol. 6084, pages 23--34, Springer, 2010.
  89. Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech. Computational Indistinguishability Logic. Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, pages 375--386, ACM, 2010.
  90. Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi. Robustness Guarantees for Anonymity. Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pages 91--106, IEEE Computer Society, 2010.
  91. Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte. On the Equality of Probabilistic Terms. Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Lecture Notes in Computer Science, Vol. 6355, Springer, 2010.
  92. Barthe, Gilles, Hedin, Daniel, Zanella Béguelin, Santiago, Gregoire, Benjamin, Heraud, Sylvain. A Machine-Checked Formalization of Sigma-Protocols. 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pages 246--260, IEEE Computer Society, 2010.
  93. Barthe, Gilles, Grégoire, Benjamin, Zanella Béguelin, Santiago. Programming Language Techniques for Cryptographic Proofs. 1st International Conference on Interactive Theorem Proving, ITP 2010, Lecture Notes in Computer Science, Vol. 6172, pages 115--130, Springer, 2010.
  94. César Kunz. Certificate Translation for the Verification of Concurrent Programs. Trustworthly Global Computing - 5th International Symposium, TGC 2010, Lecture Notes in Computer Science, Vol. 6084, pages 237--252, Springer, 2010.
  95. L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo. Program Parallelization using Synchronized Pipelining. Proceedings of the 19th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'09), LNCS, Num. 6037, pages 173--187, Springer, 2010.
  96. Boris Köpf, Geoffrey Smith. Vulnerability Bounds and Leakage Resilience of Blinded Cryptography under Timing Attacks. Proc 23rd. IEEE Computer Security Foundations Symposium (CSF '10), pages 44--56, IEEE, 2010.
  97. Boris Köpf, Andrey Rybalchenko. Approximation and Randomization for Quantitative Information-Flow Analysis. Proc. 23rd IEEE Computer Security Foundations Symposium (CSF '10), pages 3--14, IEEE, 2010.
  98. Michael Backes, Goran Doychev, Markus Dürmuth, Boris Köpf. Speaker Recognition in Encrypted Voice Streams. Proc. 15th European Symposium on Research in Computer Security (ESORICS '10), LNCS 6345, pages 508--523, Springer, 2010.
  99. Martin Leucker, César Sánchez. Regular Linear-Time Temporal Logic. Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), pages 3--5, IEEE Computer Society, 2010.
  100. César Sánchez, Martin Leucker. Regular Linear Temporal Logic with Past. Proc. of the 11th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation, (VMCAI'10), LNCS, Vol. 5944, pages 295--311, Springer, 2010.
  101. Krishnendu Chatterjee, Luca de Alfaro, Vishwanath Raman, César Sánchez. Analyzing the Impact of Change in Multi-threaded Programs. Proc. of the 13th Int'l Conf. on Fundamental Approaches to Software Engineering (FASE'10), LNCS, Vol. 6013, pages 293--307, Springer, 2010.
  102. Alejandro Sánchez, César Sánchez. Decision Procedures for the Temporal Verification of Concurrent Lists. Proc. of the 12th Int'l Conf. on Formal Engineering Methods (ICFEM'10), LNCS, Vol. 6447, pages 74--89, Springer, 2010.
  103. Dragan Ivanović, Manuel Carro, Manuel Hermenegildo. Automatic Fragment Identification in Workflows Based on Sharing Analysis. Service-Oriented Computing -- ICSOC 2010, LNCS, Num. 6470, pages 350--364, Springer Verlag, 2010.
  104. D. Ivanović, M. Carro, M. Hermenegildo. Towards Data-Aware QoS-Driven Adaptation for Service Orchestrations. Proceedings of the 2010 IEEE International Conference on Web Services (ICWS 2010), Miami, FL, USA, 5-10 July 2010, pages 107--114, IEEE, 2010.
  105. Gourinath Banda, John P. Gallagher. Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation. Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 6355, pages 27--45, Springer, 2010.
  106. Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival. Astrée: Proving the Absence of Runtime Errors. Embedded Real Time Software and Systems - ERTSS 2010, pages 1--9, 2010.
  107. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. A Scalable Segmented Decision Tree Abstract Domain. Pnueli Festschrift, Lecture Notes in Computer Science, Vol. 6200, pages 72--95, Springer-Verlag, 2010.
  108. Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur. Shape Analysis with Reference Set Relations. VMCAI, 2010.
  109. M. A. García de Dios, C. Dania, M. Schläpfer, D. Basin, M. Clavel, M. Egea. SSG: a Model-Based Development Environment for Smart, Security-Aware GUIs. Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, ICSE 2010, Cape Town, South Africa, 1-8 May 2010, pages 311--312, ACM, 2010.
  110. D. Basin, M. Clavel, M. Egea, M. Schläpfer. Automatic Generation of Smart, Security-Aware GUI Models. Engineering Secure Software and Systems, 2nd International Symposium, ESSoS 2010, Pisa, Italy, February 3-4, 2010. Proceedings, Lecture Notes in Computer Science, Vol. 5965, pages 201--217, Springer, 2010.
  111. M. Egea, C. Dania, M. Clavel. MySQL4OCL: A Stored Procedure-Based MySQL Code Generator for OCL. Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010), Electronic Communications of the EASST, Vol. 36, 2010.
  112. Pierre Ganty, Benjamin Monmege, Rupak Majumdar. Bounded Underapproximations. CAV'10: Proc. 20th Int. Conf. on Computer Aided Verification, LNCS, Vol. 6174, pages 600--614, Springer, 2010.
  113. Umut A. Acar, Guy E. Blelloch, Ruy Ley-Wild, Kanat Tangwongsan, Duru Türkoglu. Traceable data types for self-adjusting computation. PLDI, pages 483--496, 2010.
  114. A. Herranz, J. Mariño, M. Carro, J.J. Moreno-Navarro. Modeling Concurrent Systems with Shared Resources. 14th International Workshop on Formal Methods for Industrial Critical Systems, Lecture Notes in Computer Science, Vol. 5825, pages 102--116, November 2009.
  115. G. Marpons, J. Mariño, M. Carro, A. Herranz, L.Å. Fredlund, J.J. Moreno-Navarro, A. Polo. A Coding Rule Conformance Checker Integrated into GCC. Spanish Conference on Programming and Computer Languages (PROLE'09), ENTCS, Vol. 258, pages 149--159, Elsevier, August 2009.
  116. E. Mera, P. López-García, M. Hermenegildo. Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework. 25th International Conference on Logic Programming (ICLP'09), LNCS, Num. 5649, pages 281--295, Springer-Verlag, July 2009.
  117. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. A Tabling Implementation Based on Variables with Multiple Bindings. International Conference on Logic Programming (ICLP 2009), LNCS, Num. 5649, pages 190--204, Springer-Verlag, July 2009.
  118. V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee. Merlin: specification inference for explicit information flow problems. PLDI, pages 75--86, June 2009.
  119. Mark Marron, Deepak Kapur, Manuel Hermenegildo. Identification of Logically Related Heap Regions. ISMM'09: Proceedings of the 8th international symposium on Memory management, ACM Press, June 2009.
  120. P. Chico de Guzmán, M. Carro, M. Hermenegildo. Towards a Complete Scheme for Tabled Execution Based on Program Transformation. 11th International Symposium on Practical Aspects of Declarative Languages (PADL'09), LNCS, Num. 5418, pages 224--238, Springer-Verlag, January 2009.
  121. Avraham Shinnar, Marco Pistoia, Anindya Banerjee. A language for information flow: dynamic tracking in multiple interdependent dimensions. PLAS, pages 125--131, 2009.
  122. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet. Implementing a Direct Method for Certificate Translation. Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Lecture Notes in Computer Science, Vol. 5885, pages 541--560, Springer, 2009.
  123. Barthe, G., Grégoire, B., Zanella Béguelin, S.. Formal Certification of Code-Based Cryptographic Proofs. 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pages 90--101, ACM, 2009.
  124. Zanella Béguelin, S., Grégoire, B., Barthe, G., Olmedo, F.. Formally Certifying the Security of Digital Signature Schemes. 30th IEEE Symposium on Security and Privacy, S&P 2009, pages 237--250, IEEE Computer Society, 2009.
  125. Gourinath Banda, John P. Gallagher. Constraint-Based Abstraction of a Model Checker for Infinite State Systems. Proceedings of the 23rd Workshop on (Constraint) Logic Programming, University of Potsdam (Publikationsserver der Universität Potsdam), 2009.
  126. Henning Christiansen, John P. Gallagher. Non-discriminating Arguments and Their Uses. Logic Programming, 25th International Conference, ICLP 2009, Pasadena, CA, USA, July 14-17, 2009. Proceedings, Lecture Notes in Computer Science, Vol. 5649, pages 55--69, Springer, 2009.
  127. M. Clavel, M. Egea, M. A. García de Dios. Checking Unsatisfiability for OCL Constraints. Proceedings of the Workshop "The Pragmatics of OCL and Other Textual Specification Languages" at MoDELS 2009, Electronic Communications of the EASST, Vol. 24, 2009.
  128. M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. L. Talcott. Unification and Narrowing in Maude 2.4. Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, Lecture Notes in Computer Science, Vol. 5595, pages 380--390, Springer, 2009.
  129. Vlad Rusu, Manuel Clavel. Vérification d'invariants pour des syst`emes spécifiés en logique de réécriture. Vingti`emes Journées Francophones des Langages Applicatifs (JFLA 2009), Studia Informatica Universalis, Vol. 7.2, pages 317--350, 2009.
  130. Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko. Verifying Liveness for Asynchronous Programs. POPL '09: Proc. 36th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pages 102--113, ACM Press, 2009.
  131. Pierre Ganty, Nicolas Maquet, Jean-Francois Raskin. Fixpoint Guided Abstraction Refinement for Alternating Automata. CIAA '09: Proc. 14th Int. Conf. on Implementation and Application of Automata, LNCS, Vol. 5642, Springer, 2009.
  132. Pierre Ganty, Rupak Majumdar. Analyzing Real-time Event-driven Programs. FORMATS '09: Proc. 7th Int. Conf. on Formal Modelling and Analysis of Timed Systems, LNCS, Vol. 5813, pages 164--178, Springer, 2009.
  133. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo. Negative Ternary Set-Sharing. International Conference on Logic Programming, ICLP, LNCS, Num. 5366, pages 301--316, Springer-Verlag, December 2008.
  134. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. A Sketch of a Complete Scheme for Tabled Execution Based on Program Transformation. Int'l. Conference on Logic Programming, LNCS, Vol. 5366, pages 795--800, Springer Verlag, December 2008. Short paper.
  135. A. Casas, M. Carro, M. Hermenegildo. A High-Level Implementation of Non-Deterministic, Unrestricted, Independent And-Parallelism. 24th International Conference on Logic Programming (ICLP'08), LNCS, Vol. 5366, pages 651--666, Springer-Verlag, December 2008.
  136. Mark Marron, Mario Méndez-Lojo, Manuel Hermenegildo and Darko Stefanovic, Deepak Kapur. Sharing Analysis of Arrays, Collections, and Recursive Structures. ACM WS on Program Analysis for Software Tools and Engineering (PASTE'08), ACM, November 2008.
  137. Iván Pérez, Ángel Herranz, Susana Muñoz, Juan José Moreno-Navarro. Modelling Mash-Up Resources. 13th Conference on Software Engineering and Databases, JISBD'08, pages 135--146, October 2008.
  138. Mark Marron, Darko Stefanovic, Deepak Kapur, Manuel Hermenegildo. Identification of Heap-Carried Data Dependence Via Explicit Store Heap Models. 21st Int'l. WS on Languages and Compilers for Parallel Computing (LCPC'08), LNCS, Springer-Verlag, August 2008.
  139. J. Morales, M. Carro, M. Hermenegildo. Comparing Tag Scheme Variations Using an Abstract Machine Generator. 10th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), pages 32--43, ACM Press, July 2008.
  140. E. Mera, P. López-García, M. Carro, M. Hermenegildo. Towards Execution Time Estimation in Abstract Machine-Based Languages. 10th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), pages 174--184, ACM Press, July 2008.
  141. Mark Marron, Manuel Hermenegildo, Darko Stefanovic, Deepak Kapur. Efficient Context-Sensitive Shape Analysis with Graph-Based Heap Models. International Conference on Compiler Construction (CC 2008), Lecture Notes in Computer Science, 15 pages, Springer, April 2008.
  142. M. Méndez-Lojo, M. Hermenegildo. Precise Set Sharing Analysis for Java-style Programs. 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'08), LNCS, Num. 4905, pages 172--187, Springer-Verlag, January 2008.
  143. P. Chico de Guzmán, M. Carro, M. Hermenegildo, Claudio Silva, Ricardo Rocha. An Improved Continuation Call-Based Implementation of Tabling. 10th International Symposium on Practical Aspects of Declarative Languages (PADL'08), LNCS, Vol. 4902, pages 198--213, Springer-Verlag, January 2008.
  144. G. Marpons, J. Mariño, M. Carro, A. Herranz, J.J. Moreno-Navarro, L.Å. Fredlund. Automatic Coding Rule Conformance Checking Using Logic Programming. 10th International Symposium on Practical Aspects of Declarative Languages (PADL'08), LNCS, Vol. 4902, pages 18--34, Springer Verlag, January 2008.
  145. A. Casas, M. Carro, M. Hermenegildo. Towards a High-Level Implementation of Execution Primitives for Non-restricted, Independent And-parallelism. 10th International Symposium on Practical Aspects of Declarative Languages (PADL'08), LNCS, Vol. 4902, pages 230--247, Springer-Verlag, January 2008.
  146. P. Pietrzak, J. Correas, G. Puebla, M. Hermenegildo. A Practical Type Analysis for Verification of Modular Prolog Programs. ACM SIGPLAN 2008 Workshop on Partial Evaluation and Program Manipulation (PEPM'08), pages 61--70, ACM Press, January 2008.
  147. Anindya Banerjee, Michael Barnett, David A. Naumann. Boogie Meets Regions: A Verification Experience Report. VSTTE, pages 177--191, 2008.
  148. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Expressive Declassification Policies and Modular Static Enforcement. IEEE Symposium on Security and Privacy, pages 339--353, 2008.
  149. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Regional Logic for Local Reasoning about Global Invariants. ECOOP, pages 387--411, 2008.
  150. Gilles Barthe, César Kunz, Jorge Luis Sacchini. Certified Reasoning in Memory Hierarchies. Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Lecture Notes in Computer Science, Vol. 5356, pages 75--90, Springer, 2008.
  151. Gilles Barthe, César Kunz. Certificate Translation in Abstract Interpretation. 17th European Symposium on Programming, ESOP 2008, Lecture Notes in Computer Science, Vol. 4960, pages 368--382, Springer, 2008.
  152. Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese. Preservation of Proof Obligations for Hybrid Verification Methods. Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, pages 127--136, IEEE Computer Society, 2008.
  153. Gilles Barthe, Salvador Cavadini, Tamara Rezk. Tractable Enforcement of Declassification Policies. Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, pages 83--97, IEEE Computer Society, 2008.
  154. Gilles Barthe, Benjamin Grégoire, Colin Riba. Type-Based Termination with Sized Products. Computer Science Logic, 22nd International Workshop, CSL 2008, Lecture Notes in Computer Science, Vol. 5213, pages 493--507, Springer, 2008.
  155. Gilles Barthe, Benjamin Grégoire, Mariela Pavlova. Preservation of Proof Obligations from Java to the Java Virtual Machine. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Lecture Notes in Computer Science, Vol. 5195, pages 83--99, Springer, 2008.
  156. Tom Schrijvers, Maurice Bruynooghe, John P. Gallagher. From Monomorphic to Polymorphic Well-Typings and Beyond. Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 5438, pages 152--167, Springer, 2008.
  157. Gourinath Banda, John P. Gallagher. Analysis of Linear Hybrid Systems in CLP. Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers, Lecture Notes in Computer Science, pages 55--70, Springer, 2008.
  158. John P. Gallagher, Mads Rosendahl. Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation. Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, Lecture Notes in Computer Science, Vol. 5330, pages 682--696, Springer, 2008.
  159. M. Clavel, V. Silva, C. Braga, M. Egea. Model-Driven Security in Practice: An Industrial Experience. Proceedings of Model Driven Architecture - Industrial Track ECMDA-FA '08, Lecture Notes in Computer Science, Vol. 5095, pages 327--338, Springer-Verlag, 2008.
  160. M. Clavel, M. Egea, M. A. García de Dios. Building an Efficient Component for OCL Evaluation. Proceedings of the 8th International Workshop on OCL Concepts and Tools (OCL 2008) at MoDELS 2008, Electronic Communications of the EASST, Vol. 15, 2008.
  161. P. Pietrzak, M. Hermenegildo. Automatic Binding-related Error Diagnosis in Logic Programs. International Conference on Logic Programming (ICLP'07), LNCS, Num. 4670, pages 333--347, Springer-Verlag, September 2007.
  162. M. Méndez-Lojo, J. Navas, M. Hermenegildo. A Flexible (C)LP-Based Approach to the Analysis of Object-Oriented Programs. 17th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2007), LNCS, Num. 4915, pages 154--168, Springer-Verlag, August 2007.
  163. A. Casas, M. Carro, M. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. 17th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'07), LNCS, Num. 4915, pages 138--153, Springer-Verlag, August 2007.
  164. J.F. Morales, M. Carro, M. Hermenegildo. Towards Description and Optimization of Abstract Machines in an Extension of Prolog. Logic-Based Program Synthesis and Transformation (LOPSTR'06), LNCS, Num. 4407, pages 77--93, July 2007.
  165. Mark Marron, Darko Stefanovic, Manuel Hermenegildo, Deepak Kapur. Heap Analysis in the Presence of Collection Libraries. ACM WS on Program Analysis for Software Tools and Engineering (PASTE'07), ACM, June 2007.
  166. E. Mera, P. López-García, G. Puebla, M. Carro, M. Hermenegildo. Combining Static Analysis and Profiling for Estimating Execution Times. Ninth International Symposium on Practical Aspects of Declarative Languages (PADL'07), LNCS, Num. 4354, pages 140--154, Springer-Verlag, January 2007.
  167. J. Navas, E. Mera, P. López-García, M. Hermenegildo. User-Definable Resource Bounds Analysis for Logic Programs. 23rd International Conference on Logic Programming (ICLP'07), Lecture Notes in Computer Science, Vol. 4670, Springer, 2007.
  168. D. Basin, M. Clavel, J. Doser, M. Egea. A Metamodel-Based Approach for Analyzing Security-Design Models. Proceedings of the Tenth International Conference on Model Driven Engineering Languages and Systems, MODELS '07, Lecture Notes in Computer Science, Vol. 4735, pages 420--435, Springer-Verlag, 2007.
  169. M. Clavel, F. Durán, J. Hendrix, S. Lucas, J. Meseguer, P. C. Ölveczky. The Maude Formal Tool Environment. Algebra and Coalgebra in Computer Science, 2nd International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, Lecture Notes in Computer Science, Vol. 4624, pages 173--178, Springer, 2007.


Books and Monographs

  1. J. Valdazo. Developing Secure Business Applications from Secure BPMN Models. Ms. Thesis, Universidad Complutense de Madrid, Spain, September 2012.
  2. Gustavo Grieco. Typegrapher: Inferring the Type Graph of a Binary Program. Ms. Thesis, Facultad de Ciencias Exactas, Ingenieria y Agrimensura, Universidad Nacional de Rosario, Rosario, Argentina, August 2012.
  3. Gilles Barthe, Benjamin Livshits, Riccardo Scandariato. Engineering Secure Software and Systems - 4th International Symposium, ESSoS 2012, Eindhoven, The Netherlands, February, 16-17, 2012. Proceedings. Lecture Notes in Computer Science, Vol. 7159, Springer, 2012.
  4. Gilles Barthe, Anupam Datta, Sandro Etalle. Formal Aspects of Security and Trust - 8th International Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected Papers. Lecture Notes in Computer Science, Vol. 7140, Springer, 2012.
  5. Gilles Barthe, Alberto Pardo, Gerardo Schneider. Software Engineering and Formal Methods - 9th International Conference, SEFM 2011. Lecture Notes in Computer Science, Vol. 7041, Springer, November 2011.
  6. John P. Gallagher, Michael Gelfond. Theory and Practice of Logic Programming. 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue. Vol. 11 (4--5), pages 429--839, Cambridge University Press, July 2011.
  7. John P. Gallagher, Michael Gelfond. Technical Communications of the 27th International Conference on Logic Programming (ICLP'11). Leibniz International Proceedings in Informatics (LIPIcs), Vol. 11, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2011.
  8. Gilles Barthe. Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011. Lecture Notes in Computer Science, Vol. 6602, Springer, March 2011.
  9. M. Carro, J.H. Reppy. ACM SIGPLAN Proceedings of the Workshop on Declarative Aspects of Multicore Programming. ACM, January 2011.
  10. Jorge Cuéllar, Javier Lopez, Gilles Barthe, Alexander Pretschner. Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers. Lecture Notes in Computer Science, Vol. 6710, Springer, 2011.
  11. M. Hermenegildo, T. Schaub. Theory and Practice of Logic Programming. 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue. Vol. 10 (4--6), pages 361--778, Cambridge University Press, July 2010.
  12. M. Hermenegildo, T. Schaub. Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10). Leibniz International Proceedings in Informatics (LIPIcs), Vol. 7, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2010.
  13. J.F. Morales. Advanced Compilation Techniques for Logic Programming. Ph.D. Thesis, Universidad Politécnica de Madrid (UPM), Facultad Informática UPM, 28660-Boadilla del Monte, Madrid-Spain, July 2010.
  14. G. Barthe, M. Hermenegildo. Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010. LNCS, Num. 5944, Springer, January 2010.
  15. M. Carro, R. Peña-Mar&\acute;i. Practical Aspects of Declarative Languages -- 12th. International Symposium, PADL 2010. LNCS, Num. 5937, Springer-Verlag, January 2010.
  16. Rafael Caballero, John P. Gallagher. Proceedings of the 19th Workshop on Logic-based methods in Programming Environments (WLPE 2009). CoRR, abs/1002.4535, 2010.
  17. John P. Gallagher, Janis Voigtländer. Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010, Madrid, Spain, January 18-19, 2010. ACM, 2010.
  18. Anindya Banerjee. FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs. ACM, 2009.
  19. Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary Leavens, Peter Müller, Tobias Wrigstad. Formal Techniques for Java-Like Programs. Lecture Notes in Computer Science, Vol. 5475, pages 70--76, Springer Berlin / Heidelberg, 2009.
  20. Alessandro Aldini, Gilles Barthe, Roberto Gorrieri. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. Lecture Notes in Computer Science, Vol. 5705, Springer, 2009.
  21. J. Garrigue, M. Hermenegildo. Functional and Logic Programming, 9th International Symposium, FLOPS'08. LNCS, Num. 4989, Springer, April 2008.
  22. M. Hermenegildo. ACM SIGPLAN-Intel Workshop on Declarative Aspects of Multicore Programming, DAMP'08, Informal Proceedings. January 2008.
  23. Gilles Barthe, Frank S. de Boer. Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings. Lecture Notes in Computer Science, Vol. 5051, Springer, 2008.
  24. Gilles Barthe, Cédric Fournet. Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers. Lecture Notes in Computer Science, Vol. 4912, Springer, 2008.
  25. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. L. Talcott. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. Lecture Notes in Computer Science, Vol. 4350, Springer, 2007.


Invited Papers and Tutorials

  1. D. Ivanović, M. Carro, M. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. 22nd Workshop on Logic-based Methods in Programming Environments, 1 pages, September 2012. (abstract of invited talk).
  2. John P. Gallagher. Program Analysis With Regular Tree Languages. Logic-Based Program Synthesis and Transformation - 21st International Symposium, LOPSTR 2011, Odense, Denmark, July 18-20, 2011. Revised Selected Papers, Lecture Notes in Computer Science, Vol. 7225, Springer, 2012. Extended Abstract.
  3. M. V. Hermenegildo, F. Bueno, M. Carro, P. López-García, R. Haemmerlé, E. Mera, J. F. Morales, G. Puebla. An Overview of the Ciao System. Proc. of RuleML-Europe 2011, LNCS, Num. 6826, pages 2--3, Springer-Verlag, July 2011. (abstract of invited talk).
  4. John P. Gallagher, Michael Gelfond. Introduction to the 27th International Conference on Logic Programming (ICLP'11) Special Issue. Vol. 11, Num. 4-5, pages 429--432, Cambridge University Press, July 2011.
  5. John P. Gallagher, Michael Gelfond. Introduction to Technical Communications of the 27th Int'l. Conference on Logic Programming (ICLP'11). Technical Communications of the 27th International Conference on Logic Programming (ICLP'11), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 11, pages 1--9, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2011.
  6. M. Hermenegildo, T. Schaub. Introduction to the 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue. Vol. 10, Num. 4--6, pages 361--364, Cambridge University Press, July 2010.
  7. M. Hermenegildo, T. Schaub. Introduction to Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10). Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 7, pages 8--11, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2010.
  8. Anindya Banerjee. Semantics and Enforcement of Expressive Information Flow Policies. Formal Aspects in Security and Trust, Lecture Notes in Computer Science, Vol. 5983, pages 1--3, Springer Berlin / Heidelberg, 2010.
  9. Barthe, Gilles, Grégoire, Benjamin, Heraud, Sylvain, Zanella Béguelin, Santiago. Formal Certification of ElGamal Encryption. A Gentle Introduction to CertiCrypt. 5th International workshop on Formal Aspects in Security and Trust, FAST 2008, Lecture Notes in Computer Science, Vol. 5491, pages 1--19, Springer, 2009.
  10. Gilles Barthe. Certificate Translation. Proceedings of the 5th International Verification Workshop, VERIFY'08 in connection with IJCAR 2008, CEUR Workshop Proceedings, Vol. 372, CEUR-WS.org, 2008.
  11. M. Hermenegildo, F. Bueno, A. Casas, J. Navas, E. Mera, M. Carro, P. López-García. Automatic Granularity-Aware Parallelization of Programs with Predicates, Functions, and Constraints. DAMP'07, ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, pages 1--1, ACM, January 2007. (abstract of invited talk).


Invited Talks

  1. John P. Gallagher. Program Analysis With Regular Tree Languages. July 2011. Invited talk at LOPSTR'2011, Odense, Denmark.


Articles in Books and Other Collections

  1. Anindya Banerjee, David A. Naumann. State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings. Aliasing in Object-Oriented Programming, Springer, 2013. To appear.
  2. Juan Caballero, Adam Barth, Dawn Song. Content-Sniffing XSS Attacks: XSS with non-HTML Content. The Death of the Internet, Wiley, July 2012.
  3. P. Lopez-Garcia, L. Darmawan, F. Bueno, M. Hermenegildo. Interval-Based Resource Usage Verification: Formalization and Prototype. Foundational and Practical Aspects of Resource Analysis. Second Iternational Workshop FOPARA 2011, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 7177, pages 54--71, Springer-Verlag, 2012.
  4. V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee. Merlin: specification inference for explicit information flow problems. Mining Software Specifications, pages 377--410, Chapman & Hall/CRC, May 2011.
  5. Manuel Carro, Manuel V. Hermenegildo. Logic Languages. Encyclopedia of Parallel Computing, pages 1057--1068, Springer, 2011.
  6. T. Trigo, P. López-García, S. Muñoz-Hernandez. A Fuzzy Approach to Resource Aware Automatic Parallelization. 2nd International Joint Conference on Computational Intelligence, Selected Papers, Studies in Computational Intelligence (SCI), 19 pages, Springer-Verlag, 2011. To Appear.
  7. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. Logical Abstract Domains and Interpretations. The Future of Software Engineering, pages 48--71, Springer-Verlag, 2011.
  8. Manuel Clavel, Narciso Martí-Oliet, Miguel Palomino. Parameterized Metareasoning in Membership Equational Logic. Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, LNCS, Vol. 7000, pages 277--298, Springer, 2011.
  9. M. V. Hermenegildo, F. Bueno, M. Carro, P. López, J.F. Morales, G. Puebla. An Overview of The Ciao Multiparadigm Language and Program Development Environment and its Design Philosophy. Festschrift for Ugo Montanari, LNCS, Num. 5065, pages 209--237, Springer-Verlag, June 2008.
  10. Gilles Barthe, César Kunz. An Introduction to Certificate Translation. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, Lecture Notes in Computer Science, Vol. 5705, pages 51--95, Springer, 2008.
  11. Gilles Barthe, Benjamin Grégoire, Colin Riba. A Tutorial on Type-Based Termination. Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Lecture Notes in Computer Science, Vol. 5520, pages 100--152, Springer, 2008.
  12. César Sánchez, Matteo Slanina, Henny B. Sipma, Zohar Manna. The Reaction Algebra: A Formal Language for Event Correlation. Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, LNCS, Vol. 4800, pages 586--609, Springer-Verlag, 2008.
  13. Ángel Herranz, Juan José Moreno-Navarro. Modeling and Reasoning about Design Patterns in SLAM-SL. Design Pattern Formalization Techniques, IGI Publishing, March 2007.


Publications in Refereed Workshops

  1. Z. Drey, J.F. Morales, M. V. Hermenegildo. Reversible Language Extensions and their Application in Debugging. 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS 2012), 15 pages, September 2012.
  2. E.J. Gallego Arias, R. Haemmerlé, M. V. Hermenegildo, J.F. Morales . The Ciao CLP(FD) Library: A Modular CLP Extension for Prolog. 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS 2012), 15 pages, September 2012.
  3. Dragan Ivanovic, Manuel Carro, Manuel Hermenegildo. Analyzing Service-Oriented Systems Using Their Data and Structure. European Software Services and Systems Research -- Results and Challenges (ICSE Workshop), July 2012.
  4. Dimka Karastoyanova, Zsolt Nemeth, Manuel Carro, Dragan Ivanovic, Cesare Pautasso, Claudia Di Napoli, and Maurizio Giordano. Research Challenges on Service Technology Foundations. European Software Services and Systems Research -- Results and Challenges (ICSE Workshop), July 2012.
  5. D, Ivanović, M. Carro, M. Hermenegildo. Exploring the Impact of Inaccuracy and Imprecision of QoS Assumptions on Proactive Constraint-Based QoS Prediction for Service Orchestrations. Proceedings of the 4th International Workshop on Principles of Engineering Service-Oriented Systems, PESOS 2012, pages 931--937, IEEE Press, June 2012.
  6. D. Ivanović, M. Carro, M. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. XII Jornadas sobre Programación y Lenguajes (PROLE), Universidad de Almería, 2012.
  7. J. F. Morales, R. Haemmerlé, M. Carro, M. V. Hermenegildo. Lightweight compilation of (C)LP to JavaScript. XII Jornadas sobre Programación y Lenguajes (PROLE), Universidad de Almería, 2012.
  8. P. Chico de Guzmán, M. Carro, M. Hermenegildo, P. Stuckey. A General Implementation Framework for Tabled CLP. XII Jornadas sobre Programaciń y Lenguajes (PROLE), Universidad de Almería, 2012.
  9. Carolina Dania. Modeling Social Networking Privacy. ESSoS-DS 2012. Doctoral Symposium, Workshop Proceedings, Vol. 834, pages 49--54, CEUR, 2012.
  10. Fangzhe Chang, Pavithra Prabhakar, Ramesh Viswanathan. Behavior Based Service Composition. Web Services and Formal Methods - 8th International Workshop, WS-FM 2011, Clermont-Ferrand, France, September 1-2, 2011, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 7176, pages 17--31, Springer, 2012.
  11. F. Bueno, M. García de la Banda, M. V. Hermenegildo, P. López-García, E. Mera, P. J. Stuckey. Towards Resource Usage Analysis of MiniZinc Models. MiniZinc Workshop (MZN'11), 15 pages, September 2011.
  12. P. Lopez-Garcia, L. Darmawan, F. Bueno, M. Hermenegildo. Interval-based Resource Usage Verification: Formalization and Prototype. 2nd International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'2011), May 2011.
  13. M. V. Hermenegildo, F. Bueno, M. Carro, P. López, E. Mera, J.F. Morales, G. Puebla. The Ciao Approach to the Dynamic vs. Static Language Dilemma. Proceedings for the International Workshop on Scripts to Programs, STOP'11, 4 pages, ACM, 2011.
  14. D. Ivanović, M. Carro, M. Hermenegildo. An Initial Proposal for Data-Aware Resource Analysis of Orchestrations with Applications to Predictive Monitoring. International Workshops, ICSOC/ServiceWave 2009, Revised Selected Papers, LNCS, Num. 6275, Springer, September 2010.
  15. Álvaro García, Pablo Nogueira, Emilio Jesús Gallego Arias. The Beta Cube (Extended Abstract). Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS'10), pages 3--7, July 9 2010.
  16. D. Ivanović, M. Carro, M. Hermenegildo. An Initial Proposal for Data-Aware Resource Analysis of Orchestrations with Applications to Proactive Monitoring. Pre-proceedings of the 2nd Workshop on Monitoring, Adaptation and Beyond (MONA+), November 2009.
  17. L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo. Program Parallelization using Synchronized Pipelining. Pre-proceedings of the 19th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'09), September 2009.
  18. D. Ivanović, J.F. Morales, M. Carro, M. Hermenegildo. Towards Structured State Threading in Prolog. CICLOPS 2009, 15 pages, July 2009.
  19. J. Navas, M. Méndez-Lojo, M. Hermenegildo. User-Definable Resource Usage Bounds Analysis for Java Bytecode. Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09), Electronic Notes in Theoretical Computer Science, Vol. 253, Num. 5, pages 6--86, Elsevier - North Holland, March 2009.
  20. P. Chico de Guzmán, M. Carro, M. Hermenegildo. A Program Transformation for Continuation Call-Based Tabled Execution. Colloquium on Implementation of Constraint and LOgic Programming Systems (ICLP associated workshop), 15 pages, University of Udine, December 2008.
  21. G. Marpons, J. Mariño, M. Carro, A. Herranz, L.Å. Fredlund, J.J. Moreno-Navarro, A. Polo. A Coding Rule Conformance Checker Integrated into GCC. VIII Jornadas sobre Programación y Lenguajes, PROLE 2008, pages 245--249, October 2008.
  22. Pablo Nogueira, Juan José Moreno-Navarro. Bialgebra Views: A Way for Polytypic Programming to Cohabit with Data Abstraction. Proceedings of the 2nd ACM SIGPLAN Workshop on Generic Programming (ICFP-WGP'08), pages 61--73, ACM Press, September 2008.
  23. M. Méndez-Lojo, O. Lhoták, M. Hermenegildo. Efficient Set Sharing using ZBDDs. 21st Int'l. WS on Languages and Compilers for Parallel Computing (LCPC'08), LNCS, Springer-Verlag, August 2008.
  24. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo. Two Efficient Representations for Set-Sharing Analysis in Logic Programs . 17th International Workshop on Functional and (Constraint) Logic Programming, WFLP'08, 15 pages, July 2008.
  25. J. Navas, M. Méndez-Lojo, M. Hermenegildo. Safe Upper-bounds Inference of Energy Consumption for Java Bytecode Applications. The Sixth NASA Langley Formal Methods Workshop (LFM 08), April 2008. Extended Abstract.
  26. Gilles Barthe, César Kunz. Certificate Translation for Specification-Preserving Advices. Proceedings of the 7th Workshop on Foundations of Aspect-Oriented Languages, FOAL 2008, pages 9--18, ACM, 2008.
  27. G. Marpons-Ucero, J. Mariño, A. Herranz, L.Å. Fredlund, M. Carro, J.J. Moreno-Navarro. Automatic Coding Rule Conformance Checking Using Logic Programs. 17th Workshop on Logic-based methods in Programming Environments, WLPE 2007, September 2007.
  28. P. Chico de Guzmán, M. Carro, M. Hermenegildo, Claudio Silva, Ricardo Rocha. Some Improvements over the Continuation Call Tabling Implementation Technique. Colloquium on Implementation of Constraint and LOgic Programming Systems (ICLP associated workshop), 15 pages, Universidade do Porto, September 2007.
  29. A. Casas, M. Carro, M. Hermenegildo. Towards High-Level Execution Primitives for And-Parallelism: Preliminary Results. Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS'07, ICLP associated workshop), 15 pages, U. of Evora, September 2007.
  30. J. Navas, M. Méndez-Lojo, M. Hermenegildo. An Efficient, Context and Path Sensitive Analysis Framework for Java Programs. 9th Workshop on Formal Techniques for Java-like Programs FTfJP 2007, 12 pages, July 2007.
  31. A. Casas, M. Carro, M. Hermenegildo. Towards A High-Level Implementation of Flexible Parallelism Primitives for Symbolic Languages. Parallel Symbolic Computation (PASCO'07), 2 pages, ACM Press, July 2007. Extended Abstract.
  32. M. Hermenegildo, The Ciao Development Team. An Overview of The Ciao Multiparadigm Language and Program Development Environment and its Design Philosophy. ECOOP Workshop on Multiparadigm Programming with Object-Oriented Languages MPOOL 2007, July 2007.
  33. M. Méndez-Lojo, J. Navas, M. Hermenegildo. An Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode. ETAPS Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2007), Electronic Notes in Theoretical Computer Science, Elsevier - North Holland, March 2007.


Technical Reports and Manuals

  1. Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin. Verified Security of Redundancy-Free Encryption from Rabin and RSA. Cryptology ePrint Archive, Report 2012/308, 2012. (available online).
  2. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin. Automated Analysis and Synthesis of Padding-Based Encryption Schemes. Cryptology ePrint Archive, Report 2012/695, 2012. (available online).
  3. José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin. Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. Cryptology ePrint Archive, Report 2012/258, 2012. (available online).
  4. M. Busch, M. A. García de Dios. ActionUWE: Transformation of UWE to ActionGUI Models. Ludwig-Maximilians-Universität München, 2012.
  5. F. Bueno, M. Carro, M. Hermenegildo, R. Haemmerlé, P. López-García, E. Mera, and J.F. Morales, G. Puebla-(Eds.). The Ciao System. Ref. Manual (V1.14). July 2011. Available at http://ciao-lang.org.
  6. M. Hermenegildo, J.F. Morales. The LPdoc Documentation Generator. Ref. Manual (V3.0). July 2011. Available at http://ciao-lang.org.
  7. P. López-García, L. Darmawan, F. Bueno, M. Hermenegildo. Towards Resource Usage Function Verification based on Input Data Size Intervals. Num. CLIP4/2011.0, Technical University of Madrid (UPM), April 2011. Available at http://cliplab.org/papers/resource-verif-11-tr.pdf.
  8. P. Chico de Guzmán, A. Casas, M. Carro, M. Hermenegildo. A Simulation Study on Parallel Backtracking with Solution Memoing for Independent And-Parallelism. Num. CLIP1/2011.0, 12 pages, Technical University of Madrid (UPM), January 2011.
  9. J.F. Morales, M. Hermenegildo, R. Haemmerlé. Towards Modular Extensions for a Modular Language. Num. CLIP2/2011.0, 15 pages, Technical University of Madrid (UPM), January 2011.
  10. Alexander Malkis. On the strength of Owicki-Gries for resources. 2011. Technical report, (available online).
  11. D. Ivanović, M. Carro, M. Hermenegildo. Automated Attribute Inference in Complex Service Workflows Based on Sharing Analysis. Num. CLIP5/2010.0, Technical University of Madrid (UPM), December 2010.
  12. Dragan Ivanović, Manuel Carro, Manuel Hermenegildo. Automatic Fragment Identification in Workflows Based on Sharing Analysis. Num. CLIP4/2010.0, 15 pages, Technical University of Madrid (UPM), June 2010. Submitted.
  13. E. Mera, T. Trigo, P. López-García, M. Hermenegildo. An Approach to Profiling for Run-Time Checking of Computational Properties and Performance Debugging. Num. CLIP3/2010.0, 29 pages, Technical University of Madrid (UPM), March 2010.
  14. M. V. Hermenegildo, F. Bueno, M. Carro, P. López, E. Mera, J.F. Morales, G. Puebla. An Overview of Ciao and its Design Philosophy. Num. CLIP2/2010.0, Technical University of Madrid (UPM), March 2010. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).
  15. D. Ivanović, M. Carro, M. Hermenegildo, P. López, E. Mera. Towards Data-Aware Cost-Driven Adaptation for Service Orchestrations. Num. CLIP5/2009.1, Technical University of Madrid (UPM), March 2010.
  16. P. López-García, L. Darmawan, F. Bueno, M. Hermenegildo. Towards a Framework for Resource Usage Verification and Debugging in the CiaoPP System. Num. CLIP1/2010.0, Technical University of Madrid (UPM), February 2010. Available at http://cliplab.org/papers/resource-verif-10-tr.pdf.
  17. Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger. Parikh's Theorem: A simple and direct construction. 2010.
  18. Pierre Ganty, Rupak Majumdar. Algorithmic Verification of Asynchronous Programs. 2010.
  19. D. Ivanović, M. Carro, M. Hermenegildo. Sharing-Based Independence-Driven Fragment Identification for Service Orchestrations. Num. CLIP7/2009.0, Technical University of Madrid (UPM), December 2009.
  20. D. Ivanović, M. Carro, M. Hermenegildo, P. López, E. Mera. Towards Data-Aware Cost-Driven Adaptation for Service Orchestrations. Num. CLIP5/2009.0, Technical University of Madrid (UPM), November 2009. Replaced by a later version.
  21. J.F. Morales, M. Carro, M. Hermenegildo. Description and Optimization of Abstract Machines in a Dialect of Prolog. Num. CLIP4/2009.0, Technical University of Madrid (UPM), October 2009.
  22. D. Ivanović, M. Carro, M. Hermenegildo. Towards Data-Aware Resource Analysis for Service Orchestrations. Num. CLIP3/2009.0, Technical University of Madrid (UPM), June 2009.
  23. E. Mera, P. López-García, M. Hermenegildo. Towards Integrating Run-Time Checking and Software Testing in a Verification Framework. Num. CLIP1/2009.0, 19 pages, Technical University of Madrid (UPM), March 2009.
  24. P. López-García, F. Bueno, M. Hermenegildo. Inferring Determinacy and Mutual Exclusion in Logic Programs Using Mode and Type Analysis. Num. CLIP2/2009.0, Technical University of Madrid (UPM), February 2009.
  25. F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. López-García, G. Puebla-(Eds.). The Ciao System. Ref. Manual (V1.13). 2009. Available at http://ciao-lang.org.
  26. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Bounded Underapproximations. 2009.
  27. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo. Efficient Representations for Set-Sharing Analysis. Num. CLIP9/2008.0, University of New Mexico and Technical University of Madrid, September 2008.
  28. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. Bridge Program Transformation for the CCall Tabling Scheme. Num. CLIP6/2008.0, Technical University of Madrid (UPM), September 2008.
  29. A. Casas, M. Carro, M. Hermenegildo. A High-Level Implementation of Non-Deterministic, Unrestricted, Independent And-Parallelism. Num. TR-CS-2008-10, University of New Mexico (UNM), September 2008.
  30. J. Navas, E. Mera, P. López-García, M. Hermenegildo. Inference of User-Definable Resource Bounds Usage for Logic Programs and its Applications. Num. CLIP5/2008.0, Technical University of Madrid (UPM), July 2008.
  31. M. Méndez-Lojo, O. Lhoták, M. Hermenegildo. Fast Set Sharing using ZBDDs. University of New Mexico, June 2008.
  32. M. Hermenegildo, E. Albert, P. Arenas, F. Bueno, M. Carro, A. Casas, P. Chico de Guzmán, J. Correas, S. Genaim, J. Lipton, Pedro López García, M. Méndez, E. Mera, J. Morales, J. Navas, R. Padilla, P. Pietrzak, G. Puebla, M. Zamalloa, D. Zanardini. Rigorous Methods for Mobile and Heterogeneous Software Systems -- Second Year Report. Num. CLIP3/2008.0, Technical University of Madrid (UPM), April 2008.
  33. J. Navas, M. Méndez-Lojo, M. Hermenegildo. Customizable Resource Usage Analysis for Java Bytecode. Num. UNM TR-CS-2008-02 - CLIP1/2008.0, University of New Mexico, January 2008.
  34. A. Casas, M. Carro, M. Hermenegildo. Automatic Unrestricted Independent And-Parallelism in Logic Programs. Num. CLIP11/2007.0, Technical University of Madrid (UPM), December 2007. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).
  35. M. Méndez-Lojo, M. Hermenegildo. Precise Set Sharing for Java-style Programs (and proofs). Num. CLIP2/2007.1, Technical University of Madrid (UPM), November 2007.
  36. A. Casas, M. Carro, M. Hermenegildo. Towards a High-Level Implementation of Execution Primitives for Non-restricted, Independent And-parallelism. Num. TR-CS-2007-16, University of New Mexico (UNM), October 2007.
  37. A. Casas, M. Carro, M. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. Num. TR-CS-2007-14, University of New Mexico (UNM), September 2007.
  38. E. Mera, P. López-García, M. Carro, M. Hermenegildo. Towards Execution Time Estimation in Abstract Machine-Based (Logic) Languages. Num. CLIP8/2007.0, Technical University of Madrid (UPM), August 2007.
  39. G. Marpons, J. Mariño, M. Carro, A. Herranz, J.J. Moreno-Navarro, L.Å. Fredlund. Automatic Coding Rule Conformance Checking Using Logic Programming. Num. CLIP6/2007.0, Technical University of Madrid (UPM), August 2007.
  40. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. An Improved Continuation Call-Based Implementation of Tabling. Num. CLIP9/2007.0, Technical University of Madrid (UPM), August 2007.
  41. A. Casas, M. Carro, M. V. Hermenegildo. Towards a High-Level Implementation of Execution Primitives for Non-Restricted, Independent And-Parallelism. Num. CLIP7/2007.0, Technical University of Madrid (UPM), August 2007.
  42. A. Casas, M. Carro, M. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. Num. CLIP5/2007.0, Technical University of Madrid (UPM), June 2007.
  43. M. Hermenegildo, E. Albert, P. Arenas, A. Beascoa, F. Bueno, D. Cabeza, M. Carro, J. Correas, A. García Pañoso, J. Lipton, Pedro López García, E. Mera, J. Morales, C. Ochoa, G. Puebla. Rigorous Methods for Mobile and Heterogeneous Software Systems -- First Year Report. Num. CLIP4/2007.0, Technical University of Madrid (UPM), March 2007.
  44. M. Méndez-Lojo, M. Hermenegildo. Precise Set Sharing and Nullity Analysis for Java-style Programs. Num. CLIP2/2007.0, Technical University of Madrid (UPM), February 2007.
  45. P. López-García, F. Bueno, M. Hermenegildo. Inferring Determinacy in Logic Programs Using Mode and Type Information. Num. CLIP3/2007.0, Technical University of Madrid (UPM), February 2007.