Iniciativa IMDEA

Inicio > Investigación > Publicaciones

Publicaciones del Instituto IMDEA Software



Artículos en Revistas

  1. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. Proving Expected Sensitivity of Probabilistic Programs. PACMPL (POPL), En Prensa, 2018.
  2. Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger. Monadic refinements for relational cost analysis. PACMPL (POPL), En Prensa, 2018.
  3. Pierre Ganty, Radu Iosif, Filip Konecný. Underapproximation of procedure summaries for integer programs. International Journal on Software Tools for Technology Transfer (STTT), Vol. 19, Núm. 5, páginas 565--584, Octubre 2017.
  4. Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub. A relational logic for higher-order programs. PACMPL (ICFP), Vol. 1, páginas 1--29, ACM, Agosto 2017.
  5. Alejandro Sánchez, César Sánchez. Parametrized Verification Diagrams: Temporal Verification of Symmetric Parametrized Concurrent Systems. Annals of Mathematics and Artificial Intelligence, Vol. 80, Núm. 3-4, páginas 249--282, Agosto 2017.
  6. Dario Catalano, Dario Fiore, Rosario Gennaro. A Certificateless Approach to Onion Routing. International Journal of Information Security, Vol. 16, Núm. 3, páginas 327--343, Springer, Junio 2017.
  7. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems. Formal Methods in System Design, Vol. 50, Núm. 2-3, páginas 140--167, Junio 2017.
  8. Javier Esparza, Pierre Ganty, Jér^ome Leroux, Rupak Majumdar. Verification of population protocols. Acta Informatica, Vol. 54, Núm. 2, páginas 191--215, Marzo 2017.
  9. Andrea Cerone, Alexey Gotsman. Analysing snapshot isolation. Journal of the ACM, En Prensa, ACM Press, 2017. To appear.
  10. Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky. Characterizing transactional memory consistency conditions using observational refinement. Journal of the ACM, En Prensa, ACM Press, 2017. To appear.
  11. Reza Shokri, George Theodorakopoulos, Carmela Troncoso. Privacy Games Along Location Traces: A Game-Theoretic Framework for Optimizing Location Privacy. ACM Trans. Priv. Secur., Vol. 19, Núm. 4, páginas 1--31, 2017.
  12. Apostolos Pyrgelis, Carmela Troncoso, Emiliano De Cristofaro. What Does The Crowd Say About You? Evaluating Aggregation-based Location Privacy. PoPETs, Vol. 2017, Núm. 4, 2017.
  13. Carmela Troncoso, George Danezis, Marios Isaakidis, Harry Halpin. Systematizing Decentralization and Privacy: Lessons from 15 years of research and deployments. PoPETs, Vol. 2017, Núm. 4, 2017.
  14. U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo. An Evolutionary Scheduling Approach for Trading-off Accuracy vs. Verifiable Energy in Multicore Processors. Logic Journal of the IGPL, En Prensa, Oxford Academic Press, 2017.
  15. N. Stulova, J. F. Morales, M. V. Hermenegildo. Some Trade-offs in Reducing the Overhead of Assertion Run-time Checks via Static Analysis. Science of Computer Programming, En Prensa, Elsevier North-Holland, 2017. (to appear).
  16. Fiore, Dario, Vasco, María Isabel González, Soriente, Claudio. Partitioned Group Password-Based Authenticated Key Exchange. The Computer Journal, Vol. , Núm. , páginas 1--11, 2017.
  17. Dario Catalano, Dario Fiore. Practical Homomorphic Message Authenticators for Arithmetic Circuits. Journal of Cryptology, En Prensa, Springer, 2017.
  18. Bishoksan Kafle, John P. Gallagher. Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. Computer Languages, Systems & Structures, Vol. 47, páginas 2--18, 2017.
  19. Bishoksan Kafle, John P. Gallagher. Constraint specialisation in Horn clause verification. Science of Computer Programming, Vol. 137, páginas 125--140, 2017.
  20. K. Eder, J.P. Gallagher, P. Lopez-Garcia, H. Muller, Z. Banković, K. Georgiou, R. Haemmerlé, M. V. Hermenegildo, B. Kafle, S. Kerrison, M. Kirkeby, M. Klemen, X. Li, U. Liqat, J. Morse, M. Rhiger, M. Rosendahl. ENTRA: Whole-Systems Energy Transparency. Microprocessors and Microsystems, Vol. 47, Part B, páginas 278--286, Elsevier, Noviembre 2016.
  21. I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo. Semantic Code Browsing. Theory and Practice of Logic Programming, 32nd Int'l. Conference on Logic Programming (ICLP'16) Special Issue, Vol. 16, Núm. 5-6, páginas 721--737, Cambridge U. Press, Octubre 2016.
  22. P. Lopez-Garcia, M. Klemen, U. Liqat, M. V. Hermenegildo. A General Framework for Static Profiling of Parametric Resource Usage. Theory and Practice of Logic Programming, 32nd Int'l. Conference on Logic Programming (ICLP'16) Special Issue, Vol. 16, Núm. 5-6, páginas 849--865, Cambridge U. Press, Octubre 2016.
  23. Manuel Carro, Andy King. Introduction to the 32nd International Conference on Logic Programming Special Issue. Theory and Practice of Logic Programming, Vol. 16, Núm. 5-6, páginas 509--514, Cambridge University Press, Septiembre 2016.
  24. Fredlund, Lars-Åke, Mariño, Julio, Alborodo, Raúl N.N., Herranz, Angel. A testing-based approach to ensure the safety of shared resource concurrent systems. Journal of Risk and Reliability, Proceedings of the Institution of Mechanical Engineers, Part O, Vol. 230, Núm. 5, páginas 457--472, Sage Publications, Julio 2016.
  25. Juan Caballero, Zhiqiang Lin. Type Inference on Executables. ACM Computing Surveys, Vol. 48, Núm. 4, páginas 1--35, ACM, Mayo 2016.
  26. Roberto Giacobazzi, Isabella Mastroeni. Making abstract models complete. Mathematical Structures in Computer Science, Vol. 26, Núm. 4, páginas 658--701, Cambridge University Press, Mayo 2016.
  27. Javier Esparza, Pierre Ganty, Rupak Majumdar. Parameterized Verification of Asynchronous Shared-Memory Systems. J. ACM, Vol. 63, Núm. 1, páginas 1--48, ACM, Marzo 2016.
  28. J. Hughes, C. Sparks, A. Stoughton, R. Parikh, A. Reuther, S. Jagannathan. Building Resource Adaptive Software Systems (BRASS): Objectives and System Evaluation. SIGSOFT Softw. Eng. Notes, Vol. 41, Núm. 1, páginas 1--2, ACM, Enero 2016.
  29. J.F. Morales, M. Carro, M. V. Hermenegildo. Description and Optimization of Abstract Machines in a Dialect of Prolog. Theory and Practice of Logic Programming, Vol. 16, páginas 1--58, Cambridge University Press, Enero 2016.
  30. Gilles Barthe, Juan Manuel Crespo, César Kunz. Product programs and relational program logics. J. Log. Algebr. Meth. Program., Vol. 85, Núm. 5, páginas 847--859, 2016.
  31. Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce. Programming language techniques for differential privacy. SIGLOG News, Vol. 3, Núm. 1, páginas 34--53, 2016.
  32. Axel Schulz, Loza Mencía, Eneldo, Benedikt Schmidt. A rapid-prototyping framework for extracting small-scale incident-related information in microblogs: Application of multi-label classification on tweets. Information Systems, Vol. 57, páginas 88--110, 2016.
  33. S. Oya, F. Pérez-González, C. Troncoso. Design of Pool Mixes Against Profiling Attacks in Real Conditions. IEEE/ACM Trans. Netw., Vol. 24, Núm. 6, páginas 3662--3675, 2016.
  34. Laura Bozzelli, César Sánchez. Foundations of Boolean Stream Runtime Verification. Theoretical Computer Science, Vol. 631, páginas 118--138, 2016.
  35. Bernd Finkbeiner, César Sánchez. Special issue on Rich Models, EU-COST Action IC0901 Rich-Model Toolkit. Acta Informatica, Vol. 53, Núm. 4, páginas 325--326, 2016.
  36. César Sánchez, Kristen Brent Venable, Esteban Zimányi. Special issue on temporal representation and reasoning (TIME'13). Acta Informatica, Vol. 53, Núm. 2, páginas 87--88, 2016.
  37. Zorana Banković, Umer Liqat, Pedro López-García. A General Methodology for Energy-efficient Scheduling in Multicore Environments based on Evolutionary Algorithms. Journal of Multiple-Valued Logic and Soft Computing, SOCO'15 Special Issue, En Prensa, Old City Publishing, 2016.
  38. Giovanni Bernardi, Matthew Hennessy. Using higher-order contracts to model session types. Logical Methods in Computer Science, Vol. 12, Núm. 2, 2016.
  39. Guillermo Vigueras, Juan M. Orduña. On the Use of GPU for Accelerating Communication-Aware Mapping Techniques. The Computer Journal, Vol. 59, Núm. 6, páginas 836--847, 2016.
  40. Kerstin Eder, John P. Gallagher, Pedro López-García, Henk L. Muller, Zorana Bankovic, Kyriakos Georgiou, Rémy Haemmerlé, Manuel V. Hermenegildo, Bishoksan Kafle, Steve Kerrison, Maja H. Kirkeby, Maximiliano Klemen, Xueliang Li, Umer Liqat, Jeremy Morse, Morten Rhiger, Mads Rosendahl. ENTRA: Whole-systems energy transparency. Microprocessors and Microsystems - Embedded Hardware Design, Vol. 47, páginas 278--286, 2016.
  41. Á. García-Pérez, P. Nogueira. No solvable lambda-value term left behind. Logical Methods in Computer Science, Vol. 12, Núm. 2, páginas 1--43, 2016.
  42. Julio Mariño, Raúl N.N. Alborodo, Ángel Herranz, Lars-Åke Fredlund. Synthesis of Verified Concurrent Java Components from Formal Models. International Journal on Software and Systems Modeling, En Prensa, Springer Berlin Heidelberg, 2016.
  43. Isabella Mastroeni, Roberto Giacobazzi. Weakening Additivity in Adjoining Closures. Order, Vol. 33, Núm. 3, páginas 503--516, 2016.
  44. Roberto Giacobazzi, Isabella Mastroeni, Mila Dalla Preda. Maximal incompleteness as obfuscation potency. Formal Aspects of Computing, En Prensa, 2016.
  45. Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Journal of Automated Reasoning, Vol. 56, Núm. 3, páginas 283--308, 2016.
  46. Bishoksan Kafle, John P. Gallagher. Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. Computer Languages, Systems & Structures, En Prensa, Pergamon, Noviembre 2015.
  47. N. Stulova, J. F. Morales, M. V. Hermenegildo. Practical Run-time Checking via Unobtrusive Property Caching. Theory and Practice of Logic Programming, 31st Int'l. Conference on Logic Programming (ICLP'15) Special Issue, Vol. 15, Núm. 04-05, páginas 726--741, Cambridge U. Press, Septiembre 2015. http://arxiv.org/abs/1507.05986.
  48. Goran Doychev, Boris Köpf, Laurent Mauborgne, Jan Reineke. CacheAudit: A Tool for the Static Analysis of Cache Side Channels. ACM Transactions on Information and System Security (TISSEC), Vol. 18, Núm. 1, páginas 1--32, ACM, Junio 2015.
  49. Vigueras, Guillermo, Orduña, Juan M.. On the Use of GPU for Accelerating Communication-Aware Mapping Techniques. The Computer Journal, En Prensa, Mayo 2015.
  50. Giovanni Bernardi, Matthew Hennessy. Mutually Testing Processes. Logical Methods in Computer Science, Vol. 11, Núm. 2, Abril 2015.
  51. Zorana Banković, Pedro Lopez-Garcia. Stochastic vs. Deterministic Evolutionary Algorithm-based Allocation and Scheduling for XMOS Chips. Neurocomputing, Vol. 150, páginas 82--89, Elsevier, Febrero 2015.
  52. Andreas Metzger, Philip Leitner, Dragan Ivanovic, Eric Schmieders, Roslin Franklin, Manuel Carro, Schahram Dustdar, Klaus Pohl. Comparing and Combining Predictive Business Process Monitoring Techniques. System, Man, and Cybernetics: Systems, IEEE Transactions on, Vol. 45, Núm. 2, páginas 276--290, Febrero 2015.
  53. Antonio Nappa, M. Zubair Rafique, Juan Caballero. The MALICIA Dataset: Identification and Analysis of Drive-by Download Operations. International Journal of Information Security, Vol. 14, Núm. 1, páginas 15--33, Springer Berlin Heidelberg, Febrero 2015.
  54. Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. Mtac: A Monad for Typed Tactic Programming in Coq. Journal of Functional Programming (JFP), Vol. 25, 2015.
  55. Antonio Carzaniga, Alessandra Gorla, Nicol`o, Mauro Pezz`e. Automatic Workarounds: Exploiting the Intrinsic Redundancy of Web Applications. ACM Transactions on Software Engineering and Methodologies, Vol. 24, Núm. 3, páginas 1--42, 2015.
  56. Andrea Cerone, Matthew Hennessy, Massimo Merro. Modelling MAC-Layer Communications in Wireless Systems. Logical Methods in Computer Science, Vol. 11, Núm. 1, 2015.
  57. Gilles Barthe. High-Assurance Cryptography: Cryptographic Software We can Trust. IEEE Security & Privacy, Vol. 13, Núm. 5, páginas 86--89, 2015.
  58. Gilles Barthe, Alberto Pardo, Gerardo Schneider. SEFM: Software Engineering and Formal Methods. Software and System Modeling, Vol. 14, Núm. 1, páginas 3--4, 2015.
  59. Backes, Michael, Köpf, Boris. Quantifying information flow in cryptographic systems. Mathematical Structures in Computer Science, Vol. 25, Núm. 2, páginas 457--479, 2 2015.
  60. Alejandro Sánchez, César Sánchez. Parametrized Invariance for Infinite State Processes. Acta Informatica, Vol. 52, Núm. 6, páginas 525--557, 2015.
  61. Dario Catalano, Dario Fiore, Rosario Gennaro, Konstantinos Vamvourellis. Algebraic (trapdoor) one-way functions: Constructions and applications. Theoretical Computer Science, Vol. 592, páginas 143--165, Springer, 2015.
  62. Guillermo Vigueras, Federico Sket, Cristóbal Samaniego, Ling Wu, Ludovic Noels, Denny Tjahjanto, Eva Casoni, Guillaume Houzeaux, Ahmed Makradi, Jon M. Molina-Aldareguia, Mariano Vázquez, Antoine Jérusalem. An XFEM/CZM implementation for massively parallel simulations of composites fracture. Composite Structures, Vol. 125, Núm. 0, páginas 542--557, 2015.
  63. Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan. Stability Preserving Simulations and Bisimulations for Hybrid Systems. IEEE Trans. Automat. Contr., Vol. 60, Núm. 12, páginas 3210--3225, 2015.
  64. Pavithra Prabhakar, Miriam Garcia Soto. AVERIST: An Algorithmic Verifier for Stability. Electr. Notes Theor. Comput. Sci., Vol. 317, páginas 133--139, 2015.
  65. Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan. Hybrid automata-based CEGAR for rectangular hybrid systems. Formal Methods in System Design, Vol. 46, Núm. 2, páginas 105--134, 2015.
  66. Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, Geir E. Dullerud. A decidable class of planar linear hybrid systems. Theoretical Computer Science, Vol. 574, páginas 1--17, 2015.
  67. Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray. Unveiling metamorphism by abstract interpretation of code properties. Theor. Comput. Sci., Vol. 577, páginas 74--97, 2015.
  68. Gilles Barthe, Delphine Demange, David Pichardie. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst., Vol. 36, Núm. 1, páginas 1--35, ACM, Marzo 2014.
  69. Álvaro García-Pérez, Pablo Nogueira. On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines. Science of Computer Programming, Vol. 95, páginas 176--199, Elsevier, 2014.
  70. Alexander Malkis, Anindya Banerjee. On Automation in the Verification of Software Barriers: Experience Report. J. Autom. Reasoning, Vol. 52, Núm. 3, páginas 275--329, 2014.
  71. Laura Bozzelli, César Sánchez. Visibly Rational Expressions. Acta Informatica, Vol. 51, Núm. 1, páginas 25--49, 2014.
  72. G.J. Duck, R. Haemmerlé, M. Sulzmann. On Termination, Confluence and Consistent CHR-based Type Inference. Theory and Practice of Logic Programming, 30th Int'l. Conference on Logic Programming (ICLP'14) Special Issue, Vol. 14, Núm. 4-5, páginas 619--632, Cambridge U. Press, 2014.
  73. A. Serrano, P. Lopez-Garcia, M. V. Hermenegildo. Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types. Theory and Practice of Logic Programming, 30th Int'l. Conference on Logic Programming (ICLP'14) Special Issue, Vol. 14, Núm. 4-5, páginas 739--754, Cambridge U. Press, 2014.
  74. Michel Abdalla, Dario Catalano, Dario Fiore. Verifiable Random Functions: Relations to Identity-Based Key-Encapsulation and New Constructions. Journal of Cryptology, Vol. 27, Núm. 3, páginas 544--593, Springer, 2014.
  75. Dupressoir, Francois, Gordon, Andrew D., Jürjens, Jan, Naumann, David A.. Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. Journal of Computer Security (JCS), Vol. 22, Núm. 5, páginas 823--866, IOS Press, 2014. Also appears as tech. rep. MSR-TR-2011-50.
  76. Vigueras, Guillermo, Roy, Ishani, Cookson, Andrew, Lee, Jack, Smith, Nicolas, Nordsletten, David. Toward GPGPU accelerated human electromechanical cardiac simulations. International Journal for Numerical Methods in Biomedical Engineering, Vol. 30, Núm. 1, páginas 117--134, 2014.
  77. Guillermo Vigueras, Juan M. Orduña, Miguel Lozano, Jose M. Cecilia, Jose M. Garcia. Accelerating collision detection for large-scale crowd simulation on multi-core and many-core architectures. International Journal of High Performance Computing and Applications, Vol. 28, Núm. 1, 2014.
  78. J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn. Pushdown flow analysis with abstract garbage collection. J. Funct. Program., Vol. 24, Núm. 2-3, páginas 218--283, 2014.
  79. John P. Gallagher, Bishoksan Kafle. Analysis and Transformation Tools for Constrained Horn Clause Verification. Theory and Practice of Logic Programming, Vol. 14, Núm. 4-5 (supplementary materials), páginas 90--101, Cambridge University Press, 2014.
  80. Juan Caballero, Simson Garfinkel. Fourteenth Annual DFRWS Conference. Digital Investigation, Vol. 11, Supplement 2, Núm. 0, páginas 1--2, 2014. The Proceedings of the 14th Annual Digital Forensics Research Conference.
  81. Ahmed Bouajjani, Michael Emmi. Bounded phase analysis of message-passing programs. STTT, Vol. 16, Núm. 2, páginas 127--146, 2014.
  82. David A. Basin, Manuel Clavel, Marina Egea, Miguel Ángel García de Dios, Carolina Dania. A Model-Driven Methodology for Developing Secure Data-Management Applications. IEEE Trans. Software Eng., Vol. 40, Núm. 4, páginas 324--337, 2014.
  83. Javier Esparza, Pierre Ganty, Tomás Poch. Pattern-based Verification for Multithreaded Programs. ACM Transactions on Programming Languages and Systems, Vol. 36, Núm. 3, páginas 1--29, 2014.
  84. Gilles Barthe, David Pichardie, Tamara Rezk. A Certified Lightweight Non-interference Java Bytecode Verifier. Mathematical Structures in Computer Science, Vol. 23, Núm. 5, páginas 1032--1081, Cambridge University Press, Octubre 2013.
  85. Alexey Gotsman, Hongseok Yang. Linearizability with ownership transfer. Logical Methods in Computer Science, Vol. 9, Núm. 3, Septiembre 2013.
  86. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. How to make ad hoc proof automation less ad hoc. Journal of Functional Programming (JFP), Vol. 23, Núm. 4, páginas 357--401, Julio 2013.
  87. Aleksandar Nanevski, Anindya Banerjee, Deepak Garg. Dependent Type Theory for Verification of Information Flow and Access Control. ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 35, Núm. 2(6), páginas 1--6, Julio 2013.
  88. Alexey Gotsman, Hongseok Yang. Modular verification of preemptive OS kernels. Journal of Functional Programming, Vol. 23, Núm. 4, páginas 452--514, Cambridge University Press, Julio 2013.
  89. D. Ivanovic, M. Carro, M. V. Hermenegildo. A Sharing-Based Approach to Supporting Adaptation in Service Compositions. Computing, Vol. 95, Núm. 6, páginas 453--492, Springer Wien, Junio 2013. 10.1007/s00607-012-0230-z.
  90. Vigueras, Guillermo, Orduña, Juan M., Lozano, Miguel, Jégou, Yvon. A Scalable Multiagent System Architecture for Interactive Applications. Sci. Comput. Program., Vol. 78, Núm. 6, páginas 715--724, Elsevier North-Holland, Inc., Junio 2013.
  91. Murdoch J. Gabbay, Aleksandar Nanevski. Denotation of syntax and metaprogramming in contextual modal type theory (CMTT). Journal of Applied Logic (JAPPL), Vol. 11, Núm. 1, páginas 1--29, Marzo 2013.
  92. Juan Caballero, Dawn Song. Automatic Protocol Reverse-Engineering: Message Format Extraction and Field Semantics. Computer Networks, Vol. 57, Núm. 2, páginas 451--474, Elsevier, Febrero 2013.
  93. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Local Reasoning for Global Invariants, Part I: Region Logic. Journal of the ACM, Vol. 60, Núm. 3, páginas 1--56, ACM, 2013.
  94. Anindya Banerjee, David A. Naumann. Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. Journal of the ACM, Vol. 60, Núm. 3, páginas 1--73, ACM, 2013.
  95. Aleksandar Nanevski, Anindya Banerjee, Deepak Garg. Dependent Type Theory for Verification of Information Flow and Access Control Policies. ACM Trans. Program. Lang. Syst., Vol. 35, Núm. 2, páginas 1--41, ACM, 2013.
  96. Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin. Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks. ACM Transactions on Programming Languages and Systems (TOPLAS), accepted for publication, En Prensa, ACM, 2013.
  97. Maria-Cristina Marinescu, César Sánchez. Fusing Statecharts and Java. ACM Transactions on Embedded Computing Systems, Vol. 12, páginas 1--21, 2013.
  98. Mark Marron, César Sánchez, Zhendong Su, Manuel Fähndrich. Abstracting Runtime Heaps for Program Understanding. IEEE Transactions on Software Engineering, Vol. 39, Núm. 6, páginas 774--786, IEEE Computer Society, 2013.
  99. M. Carro, Ángel Herranz, Julio Mariño. A Model-Driven Approach to Teaching Concurrency. ACM Transactions on Computer Education, Vol. 13, Núm. 1, 2013.
  100. Kyriakos Kritikos, Barbara Pernici, Pierluigi Plebani, Cinzia Cappiello, Marco Comuzzi, Salima Benbernou, Ivona Brandic, Attila Kertesz, Michael Parkin, M. Carro. A Survey on Service Quality Description. ACM Computing Surveys, Vol. 46, Núm. 1, 2013.
  101. Vigueras, Guillermo, Orduña, Juan M., Lozano, Miguel. A Read-Copy Update based parallel server for distributed crowd simulations. The Journal of Supercomputing, Vol. 64, Núm. 1, páginas 156--166, Springer US, 2013.
  102. C. Michler, A. N. Cookson, R. Chabiniok, E. Hyde, J. Lee, M. Sinclair, T. Sochi, A. Goyal, G. Vigueras, D. A. Nordsletten, N.P. Smith. A computationally efficient framework for the simulation of cardiac perfusion using a multi-compartment Darcy porous-media flow model. International Journal of Numerical Methods in Biomedical Engineering, Vol. 29, Núm. 2, 2013.
  103. Clay Shields, Juan Caballero. Thirteenth Annual DFRWS Conference. Digital Investigation, Vol. 10, Supplement, Núm. 0, páginas 1--2, 2013. The Proceedings of the 13th Annual Digital Forensics Research Conference.
  104. Ahmed Bouajjani, Michael Emmi. Analysis of Recursively Parallel Programs. ACM Trans. Program. Lang. Syst., Vol. 35, Núm. 3, páginas 1--49, 2013.
  105. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang. Secure distributed programming with value-dependent types. J. Funct. Program., Vol. 23, Núm. 4, páginas 402--451, 2013.
  106. 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, Núm. 8, páginas 10659--10677, Agosto 2012.
  107. Juan Caballero. Understanding the Role of Malware in Cybercrime. ERCIM News, Vol. 2012, Núm. 90, páginas 15--16, Julio 2012.
  108. 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, Núm. 1--2, páginas 219--252, Cambridge University Press, Enero 2012. http://arxiv.org/abs/1102.5497.
  109. Gilles Barthe, Jorge Cuéllar, Javier Lopez, Alexander Pretschner. Preface. Journal of Computer Security, Vol. 20, Núm. 4, páginas 307--308, 2012.
  110. Boris Köpf, Pasquale Malacaria, Catuscia Palamidessi. Quantitative Security Analysis (Dagstuhl Seminar 12481). Dagstuhl Reports, Vol. 2, Núm. 11, páginas 135--154, 2012.
  111. R. Haemmerlé. Diagrammatic confluence for Constraint Handling Rules. Theory and Practice of Logic Programming, 28th Int'l. Conference on Logic Programming (ICLP'12) Special Issue, Vol. 12, Núm. 4-5, páginas 737--754, Cambridge U. Press, 2012.
  112. 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, Núm. 4-5, páginas 755--773, Cambridge U. Press, 2012.
  113. E. Albert, P. Arenas, G. Puebla, M. Hermenegildo. Certificate Size Reduction in Abstraction-Carrying Code. Theory and Practice of Logic Programming, Vol. 12, Núm. 3, páginas 283--318, 2012.
  114. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. Theories, Solvers and Static Analysis by Abstract Interpretation. Journal of the ACM, En Prensa, ACM, 2012.
  115. Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir E. Dullerud. Verification of Bounded Discrete Horizon Hybrid Automata. IEEE Transactions on Automatic Control, Vol. 57, Núm. 6, páginas 1445--1455, 2012.
  116. Ganty, Pierre, Majumdar, Rupak. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., Vol. 34, Núm. 1, páginas 1--48, ACM, 2012.
  117. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Bounded Underapproximations. Formal Methods in System Design, Vol. 40, Núm. 2, páginas 206--231, 2012.
  118. Isabella Mastroeni, Anindya Banerjee. Modelling Declassification Policies using Abstract Domain Completeness. Mathematical Structures in Computer Science, Vol. 21, Núm. 6, páginas 1253--1299, Diciembre 2011.
  119. Gilles Barthe, Pedro D'Argenio, Tamara Rezk. Secure Information Flow by Self-Composition. Mathematical Structures in Computer Science, Vol. 21, Núm. 6, páginas 1207--1252, Cambridge University Press, Octubre 2011.
  120. Gilles Barthe, César Kunz. An Abstract Model of Certificate Translation. ACM Trans. Program. Lang. Syst., Vol. 33, Núm. 4, páginas 1--13, ACM, Julio 2011.
  121. P. Chico de Guzmán, A. Casas, M. Carro, M. V. 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, Núm. 4--5, páginas 555--574, Cambridge U. Press, Julio 2011.
  122. R. Haemmerlé. (Co)-Inductive Semantics for Constraint Handling Rules. Theory and Practice of Logic Programming, 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue, Vol. 11, Núm. 4--5, páginas 593--609, Cambridge U. Press, Julio 2011.
  123. R. Haemmerlé. Observational Equivalences for Linear Logic Concurrent Constraint Languages. Theory and Practice of Logic Programming, 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue, Vol. 11, Núm. 4--5, páginas 469--485, Cambridge U. Press, Julio 2011.
  124. G. Puebla, E. Albert, M. V. Hermenegildo. Efficient Local Unfolding with Ancestor Stacks. Theory and Practice of Logic Programming, Vol. 11, Núm. 1, páginas 1--32, Cambridge U. Press, Enero 2011.
  125. 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, Núm. 1, páginas 1--8, ACM, Enero 2011.
  126. Boris Köpf, David Basin. Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks. Journal of Computer Security, Vol. 1, páginas 1--31, 2011.
  127. Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir E. Dullerud. Specifications for decidable hybrid games. Theoretical Computer Science, Vol. 412, Núm. 48, páginas 6770--6785, 2011.
  128. Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger. Parikh's Theorem: A simple and direct automaton construction. Information Processing Letters, Vol. 111, páginas 614--619, 2011.
  129. Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld. Security of Multithreaded Programs by Compilation. ACM Trans. Inf. Syst. Secur., Vol. 13, Núm. 3, 2010.
  130. A. Stivala, P. J. Stuckey, M. García de la Banda, M. V. Hermenegildo, A. Wirth. Lock-free Parallel Dynamic Programming. Journal of Parallel and Distributed Computing, Vol. 70, Núm. 8, páginas 839--848, Elsevier, 2010.
  131. P. López-García, F. Bueno, M. V. Hermenegildo. Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Information. New Generation Computing, Vol. 28, Núm. 2, páginas 117--206, Ohmsha, Ltd. and Springer, 2010.
  132. M. Egea, V. Rusu. Formal Executable Semantics for Conformance in the MDE Framework. Innovations in Systems and Software Engineering, Vol. 6, páginas 73--81, Springer London, 2010.
  133. Pierre Ganty, Nicolas Maquet, Jean-Francois Raskin. Fixed Point Guided Abstraction Refinement for Alternating Automata. Theor. Comput. Sci., Vol. 411, Núm. 38-39, páginas 3444--3459, 2010.
  134. D. Cabeza, M. Hermenegildo. Non-Strict Independence-Based Program Parallelization Using Sharing and Freeness Information. Theoretical Computer Science, Vol. 410, Núm. 46, páginas 4704--4723, Elsevier Science, Octubre 2009.
  135. Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk. Certificate Translation for Optimizing Compilers. ACM Trans. Program. Lang. Syst., Vol. 31, Núm. 5, ACM, Julio 2009.
  136. Elvira Albert, John P. Gallagher, Miguel Gómez-Zamalloa, Germán Puebla. Type-based homeomorphic embedding for online termination. Inf. Process. Lett., Vol. 109, Núm. 15, páginas 879--886, Elsevier, Julio 2009.
  137. 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, Núm. 2, páginas 137--161, Marzo 2009.
  138. Julio Mariño, Juan José Moreno-Navarro, Susana Muñoz Hernández. Implementing Constructive Intensional Negation. New Generation Computing, Vol. 27, Núm. 1, páginas 25--56, Enero 2009.
  139. D. Basin, M. Clavel, J. Doser, M. Egea. Automated Analysis of Security-Design Models. Information & Software Technology, Vol. 51, Núm. 5, páginas 815--831, 2009.
  140. E. Albert, G. Puebla, M. V. Hermenegildo. Abstraction-Carrying Code: A Model for Mobile Code Safety. New Generation Computing, Vol. 26, Núm. 2, páginas 171--204, Marzo 2008.
  141. Julio Mariño, Ángel Herranz, Juan José Moreno-Navarro. Demandedness Analysis with Partial Predicates. Theory and Practice of Logic Programming, Vol. 7, Núm. 1-2, páginas 153--182, Enero 2007.
  142. 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, Núm. 1-2, páginas 70--91, 2007.


Artículos en Congresos con Revisión Estricta

  1. N. Stulova, J. F. Morales, M. V. Hermenegildo. Exploiting Term Hiding to Reduce Run-time Checking Overhead. 20th International Symposium on Practical Aspects of Declarative Languages (PADL 2018), LNCS, 16 páginas, Springer-Verlag, Enero 2018. (To appear).
  2. Pierre Ganty, Boris Köpf, Pedro Valero. A Language-Theoretic View on Network Protocols. Proc. of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017), LNCS, Vol. 10482, páginas 363--379, Springer, Octubre 2017.
  3. Graeme Gange, Pierre Ganty, Peter J. Stuckey. Fixing the State Budget: Approximation of Regular Languages with Small DFAs. Proc. of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017), LNCS, Vol. 10482, páginas 67--83, Springer, Octubre 2017.
  4. Manuel Barbosa, Dario Catalano, Dario Fiore. Labeled Homomorphic Encryption: Scalable and Privacy-Preserving Processing of Outsourced Data. Proc. of the 22nd European Symposium on Research in Computer Security (ESORICS 2017), LNCS, Vol. 10492, páginas 146--166, Springer, Septiembre 2017.
  5. Pierre Ganty, Elena Gutiérrez. Parikh Image of Pushdown Automata. Proc. of the 21st International Symposium on Fundamentals of Computation Theory (FCT 2017), LNCS, Vol. 10472, páginas 271--283, Springer, Septiembre 2017.
  6. Carmen Elisabetta Zaira Baltico, Dario Catalano, Dario Fiore, Romain Gay. Practical Functional Encryption for Quadratic Functions with Applications to Predicate Encryption. Advances in Cryptology: Proc. of the 37th Annual Cryptology Conference (CRYPTO 2017), LNCS, Vol. 10401, páginas 67--98, Springer, Agosto 2017.
  7. Platon Kotzias, Juan Caballero. An Analysis of Pay-per-Install Economics Using Entity Graphs. 16th Annual Workshop on the Economics of Information Security, Junio 2017.
  8. Vitalii Avdiienko, Konstantin Kuznetsov, Isabelle Rommelfanger, Andreas Rau, Alessandra Gorla, Andreas Zeller. Detecting behavior anomalies in graphical user interfaces. Proc. of the 39th International Conference on Software Engineering (ICSE 2017), páginas 201--203, IEEE Computer Society, Mayo 2017.
  9. Paolo Calciati, Alessandra Gorla. How do apps evolve in their permission requests?: a preliminary study. Proc. of the 14th International Conference on Mining Software Repositories (MSR 2017), páginas 37--41, IEEE Computer Society, Mayo 2017.
  10. Chaz Lever, Platon Kotzias, Davide Balzarotti, Juan Caballero, Manos Antonakakis. A Lustrum of Malware Network Communication: Evolution and Insights. Proceedings of the 38th IEEE Symposium on Security and Privacy, Mayo 2017.
  11. Oliver Kennedy, D. Richard Hipp, Stratos Idreos, Amélie Marian, Arnab Nandi, Carmela Troncoso, Eugene Wu. Small Data. Proc. of the 33rd IEEE International Conference on Data Engineering (ICDE 2017), páginas 1475--1476, IEEE Computer Society, Abril 2017.
  12. Alessio Gambi, Alessandra Gorla, Andreas Zeller. O!Snap: Cost-Efficient Testing in the Cloud. Proc. of the IEEE International Conference on Software Testing, Verification and Validation (ICST 2017), páginas 454--459, IEEE Computer Society, Marzo 2017.
  13. Simon Oya, Fernando Pérez-González, Carmela Troncoso. Filter design for delay-based anonymous communications. Proc. of the 42nd IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP 2017), páginas 2107--2111, IEEE, Marzo 2017.
  14. Vitalii Avdiienko, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller, Steven Arzt, Siegfried Rasthofer, Eric Bodden. AppMining. Software Engineering 2017, LNI, Vol. P-267, páginas 113--114, GI, Febrero 2017.
  15. Srdjan Matic, Carmela Troncoso, Juan Caballero. Dissecting Tor Bridges: a Security Evaluation of their Private and Public Infrastructures. Proceedings of the Network and Distributed System Security Symposium, Febrero 2017. To appear.
  16. Srdjan Matic, Carmela Troncoso, Juan Caballero. Dissecting Tor Bridges: a Security Evaluation of their Private and Public Infrastructures. Proceedings of the Network and Distributed System Security Symposium, Febrero 2017.
  17. Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Concurrent Data Structures Linked in Time. European Conference on Object-Oriented Programming (ECOOP), páginas 1--30, 2017.
  18. Alexey Gotsman, Sebastian Burckhardt. Consistency models with global operation sequencing and their composition. DISC'17: International Symposium on Distributed Computing, LIPICS, Vol. 91, páginas 1--16, Dagstuhl, 2017.
  19. Andrea Cerone, Alexey Gotsman, Hongseok Yang. Algebraic laws for weak consistency. CONCUR'17: International Conference on Concurrency Theory, LIPICS, Vol. 85, páginas 1--18, Dagstuhl, 2017.
  20. Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson. Proving linearizability using partial orders. ESOP'17: European Symposium on Programming, Uppsala, Sweden, LNCS, Vol. 10201, páginas 639--667, Springer, 2017.
  21. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub. Jasmin: High-Assurance and High-Speed Cryptography. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30-November 3, 2017, páginas 1807--1823, ACM, 2017.
  22. Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee. Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30-November 3, 2017, páginas 647--664, ACM, 2017.
  23. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira. A Fast and Verified Software Stack for Secure Function Evaluation. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30-November 3, 2017, páginas 1989--2006, ACM, 2017.
  24. Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu. Verified Translation Validation of Static Analyses. 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, August 21-25, 2017, páginas 405--419, IEEE Computer Society, 2017.
  25. Miguel Ambrona, Gilles Barthe, Benedikt Schmidt. Generic Transformations of Predicate Encodings: Constructions and Applications. Advances in Cryptology - CRYPTO 2017 - 37th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 20-24, 2017, Proceedings, Part I, Lecture Notes in Computer Science, Vol. 10401, páginas 36--66, Springer, 2017.
  26. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. Proving uniformity and independence by self-composition and coupling. LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7-12th May 2017, EPiC Series, Vol. 46, páginas 385--403, EasyChair, 2017.
  27. Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub. *-Liftings for Differential Privacy. 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, LIPIcs, Vol. 80, páginas 1--12, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
  28. Martín Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, Vijay Ganesh. Reasoning about Probabilistic Defense Mechanisms against Remote Attacks. 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, April 26-28, 2017, páginas 499--513, IEEE, 2017.
  29. Gilles Barthe, Francois Dupressoir, Sebastian Faust, Benjamin Grégoire, Francois-Xavier Standaert, Pierre-Yves Strub. Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, April 30 - May 4, 2017, Proceedings, Part I, Lecture Notes in Computer Science, Vol. 10210, páginas 535--566, 2017.
  30. Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns. Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs. Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Lecture Notes in Computer Science, Vol. 10201, páginas 83--110, 2017.
  31. Ezgi Cicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann. Relational cost analysis. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, páginas 316--329, ACM, 2017.
  32. Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. Coupling proofs are probabilistic product programs. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, páginas 161--174, ACM, 2017.
  33. Pepe Vila, Boris Köpf. Loophole: Timing Attacks on Shared Event Loops in Chrome. 26th USENIX Security Symposium, USENIX Association, 2017.
  34. Goran Doychev, Boris Köpf. Rigorous Analysis of Software Countermeasures against Cache Attacks. 38th ACM SIGPLAN Conference on Programming Language Design and Implementations (PLDI), ACM, 2017.
  35. Heiko Mantel, Alexandra Weber, Boris Köpf. A Systematic Study of Cache Side Channels across AES Implementations. Proc. 9th International Symposium on Engineering Secure Software and Systems (ESSoS '17), Springer, 2017.
  36. Pablo Cañones, Boris Köpf, Jan Reineke. Security Analysis of Cache Replacement Polices. Proc. 6th Conference on Principles of Security and Trust (POST '17), Springer, 2017.
  37. Simon Oya, Carmela Troncoso, Fernando Pérez-González. Back to the Drawing Board: Revisiting the Design of Optimal Location Privacy-preserving Mechanisms. Proc. of the ACM Conference on Computer and Communications Security (CCS 2017), páginas 1959--1972, ACM, 2017.
  38. Andreas Metzger, Philipp Leitner, Dragan Ivanovic, Eric Schmieders, Rod Franklin, Manuel Carro, Schahram Dustdar, Klaus Pohl. Vergleich und Kombination von Techniken des Predictive Business Process Monitoring. Software Engineering 2017, Fachtagung des GI-Fachbereichs Softwaretechnik, 21.-24. Februar 2017, Hannover, Deutschland, páginas 79--80, 2017.
  39. Yevgeniy Dodis, Dario Fiore. Unilaterally-Authenticated Key Exchange. Financial Cryptography and Data Security 2017, Proceedings, LNCS, Springer, 2017.
  40. Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub. Computer-aided verification in mechanism design. Proceedings of the 12th Conference on Web and Internet Economics (WINE 2016), Lecture Notes in Computer Science, Vol. 10123, páginas 279--293, Springer, Diciembre 2016.
  41. Antonio Nappa, Rana Faisal Munir, Irfan Khan Tanoli, Christian Kreibich, Juan Caballero. RevProbe: Detecting Silent Reverse Proxies in Malicious Server Infrastructures. Proceedings of the 2016 Annual Computer Security Applications Conference, Diciembre 2016.
  42. J. Arias, M. Carro. Description and Evaluation of a Generic Design to Integrate CLP and Tabled Execution. 18th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'16), páginas 10--23, ACM Press, Septiembre 2016.
  43. N. Stulova, J. F. Morales, M. V. Hermenegildo. Reducing the Overhead of Assertion Run-time Checks via Static Analysis. 18th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'16), páginas 90--103, ACM Press, Septiembre 2016.
  44. Marcos Sebastián, Richard Rivera, Platon Kotzias, Juan Caballero. AVClass: A Tool for Massive Malware Labeling. Proceedings of the 19th International Symposium on Research in Attacks, Intrusions and Defenses, Septiembre 2016.
  45. Alejandro Calleja, Juan Tapiador, Juan Caballero. A Look into 30 Years of Malware Development from a Software Metrics Perspective. Proceedings of the 19th International Symposium on Research in Attacks, Intrusions and Defenses, Septiembre 2016.
  46. Platon Kotzias, Leyla Bilge, Juan Caballero. Measuring PUP Prevalence and PUP Distribution through Pay-Per-Install Services. Proceedings of the 25th USENIX Security Symposium, Agosto 2016.
  47. R. Haemmerlé, P. Lopez-Garcia, U. Liqat, M. Klemen, J. P. Gallagher, M. V. Hermenegildo. A Transformational Approach to Parametric Accumulated-cost Static Profiling. 13th International Symposium on Functional and Logic Programming (FLOPS 2016), LNCS, Vol. 9613, páginas 163--180, Springer, Marzo 2016.
  48. Sergey, Ilya, Nanevski, Aleksandar, Banerjee, Anindya, Delbianco, Germán Andrés. Hoare-style Specifications As Correctness Conditions for Non-linearizable Concurrent Objects. International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), páginas 92--110, 2016.
  49. Goffi, Alberto, Gorla, Alessandra, Ernst, Michael D., Pezz`e, Mauro. Automatic Generation of Oracles for Exceptional Behaviors. Proceedings of the 25th International Symposium on Software Testing and Analysis, ISSTA 2016, páginas 213--224, ACM, 7 2016.
  50. Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, Marek Zawirski. Specification and Complexity of Collaborative Text Editing. PODC'16: Symposium on Principles of Distributed Computing, páginas 259--268, ACM Press, 2016.
  51. Andrea Cerone, Alexey Gotsman. Analysing Snapshot Isolation. PODC'16: Symposium on Principles of Distributed Computing, páginas 55--64, ACM Press, 2016.
  52. Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson. A Generic Logic for Proving Linearizability. FM'16: International Symposium on Formal Methods, LNCS, Vol. 9995, páginas 426--443, Springer, 2016.
  53. Giovanni Bernardi, Alexey Gotsman. Robustness against Consistency Models with Atomic Visibility. CONCUR'16: International Conference on Concurrency Theory, LIPICS, Vol. 59, páginas 1--15, Dagstuhl, 2016.
  54. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro. 'Cause I'm strong enough: reasoning about consistency choices in distributed systems. POPL'16: Symposium on Principles of Programming Languages, St. Petersburg, FL, USA, páginas 371--384, ACM Press, 2016.
  55. Torben Amtoft, Anindya Banerjee. A Theory of Slicing for Probabilistic Control Flow Graphs. Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, páginas 180--196, 2016.
  56. Anindya Banerjee, David A. Schmidt, Mohammad Nikouei. Relational Logic with Framing and Hypotheses. Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2016.
  57. Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. Proving Differential Privacy via Probabilistic Couplings. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, NY, USA, July 5-8, 2016, páginas 749--758, ACM, 2016.
  58. Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. Advanced Probabilistic Couplings for Differential Privacy. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, páginas 55--67, ACM, 2016.
  59. Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub. Differentially Private Bayesian Programming. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, páginas 68--79, ACM, 2016.
  60. Gilles Barthe, Sonia Belaïd, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini. Strong Non-Interference and Type-Directed Higher-Order Masking. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, páginas 116--129, ACM, 2016.
  61. Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns. Facets of Software Doping. Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II, Lecture Notes in Computer Science, Vol. 9953, páginas 601--608, Springer, 2016.
  62. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Michael Emmi. Verifying Constant-Time Implementations. 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10-12, 2016, páginas 53--70, USENIX Association, 2016.
  63. Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. A Program Logic for Union Bounds. 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, LIPIcs, Vol. 55, páginas 1--15, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
  64. Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu. Synthesizing Probabilistic Invariants via Doob's Decomposition. Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Lecture Notes in Computer Science, Vol. 9779, páginas 43--61, Springer, 2016.
  65. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. Fast Software Encryption - 23rd International Conference, FSE 2016, Bochum, Germany, March 20-23, 2016, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 9783, páginas 163--184, Springer, 2016.
  66. Christian Meurisch, Usman Naeem, Muhammad Awais Azam, Frederik Janssen, Benedikt Schmidt, Max Mühlhäuser. Smarticipation: intelligent personal guidance of human behavior utilizing anticipatory models. Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing, UbiComp Adjunct 2016, Heidelberg, Germany, September 12-16, 2016, páginas 1227--1230, ACM, 2016.
  67. Alexander Seeliger, Timo Nolle, Benedikt Schmidt, Max Mühlhäuser. Process Compliance Checking using Taint Flow Analysis. Proceedings of the International Conference on Information Systems - Digital Innovation at the Crossroads, ICIS 2016, Dublin, Ireland, December 11-14, 2016, Association for Information Systems, 2016.
  68. Alexander Seeliger, Benedikt Schmidt, Immanuel Schweizer, Max Mühlhäuser. What Belongs Together Comes Together: Activity-centric Document Clustering for Information Work. Proceedings of the 21st International Conference on Intelligent User Interfaces, IUI 2016, Sonoma, CA, USA, March 07 - 10, 2016, páginas 60--70, ACM, 2016.
  69. Marc Fischlin, Felix Günther, Benedikt Schmidt, Bogdan Warinschi. Key Confirmation in Key Exchange: A Formal Treatment and Implications for TLS 1.3. IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, May 22-26, 2016, páginas 452--469, IEEE Computer Society, 2016.
  70. Raúl Pardo, Ivana Kellyerova, César Sánchez, Gerardo Schneider. Specification of Evolving Privacy Policies for Online Social Networks. Proc. of the 23rd Int'l Symp. on Temporal Representation and Reasoning (TIME'16), páginas 70--79, IEEE Computer Society Press, 2016.
  71. Dario Fiore, Cédric Fournet, Esha Gosh, Markulf Kohlweiss, Olga Ohrimenko, Bryan Parno. Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data. ACM CCS 2016 -- 23rd ACM Conference on Computer and Communication Security, páginas 1304--1316, 2016.
  72. Dario Fiore, Aikaterini Mitrokotsa, Luca Nizzardo, Elena Pagnin. Multi-Key Homomorphic Authenticators. ASIACRYPT 2016: 22nd Annual International Conference on the Theory and Applications of Cryptology and Information Security, LNCS, Springer, 2016.
  73. Dario Fiore, Anca Nitulescu. On the (In)security of SNARKs in the Presence of Oracles. TCC 2016-B: 14th Theory of Cryptography Conference, LNCS, Springer, 2016.
  74. Johannes Krupp, Dominique Schroeder, Mark Simkin, Dario Fiore, Giuseppe Ateniese, Stefan Nuernberger. Nearly Optimal Verifiable Data Streaming. PKC 2016: 19th International Workshop on Theory and Practice in Public Key Cryptography, LNCS, Springer, 2016.
  75. Bishoksan Kafle, John P. Gallagher, José F. Morales. Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Lecture Notes in Computer Science, Vol. 9779, páginas 261--268, Springer, 2016.
  76. Xueliang Li, John P. Gallagher. Fine-Grained Energy Modeling for the Source Code of a Mobile Application. Proceedings of the 13th International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services, MobiQuitous 2016, Hiroshima, Japan, November 28 - December 1, 2016, páginas 180--189, ACM, 2016.
  77. Xueliang Li, John P. Gallagher. A Source-level Energy Optimization Framework for Mobile Applications. 16th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2016), 2016.
  78. Dario Fiore, Aikaterini Mitrokotsa, Luca Nizzardo, Elena Pagnin. Multi-Key Homomorphic Authenticators. ASIACRYPT 2016: 22nd Annual International Conference on the Theory and Applications of Cryptology and Information Security, LNCS, Springer, 2016.
  79. Michael Emmi, Constantin Enea. Symbolic Abstract Data Type Inference. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, Florida, United States, January 20-22, 2016, páginas 513--525, ACM, 2016.
  80. Miguel Ambrona, Gilles Barthe, Benedikt Schmidt. Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. Advances in Cryptology - EUROCRYPT 2016 - 35th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Lecture Notes in Computer Science, Vol. 9666, páginas 822--851, Springer, 2016.
  81. Pavithra Prabhakar, Miriam García Soto, Ratan Lal. Verification Techniques for Hybrid Systems. Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II, páginas 833--842, 2016.
  82. Pavithra Prabhakar, Miriam García Soto. An Algorithmic Approach to Global Asymptotic Stability Verification of Hybrid Systems. Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016, páginas 1--10, ACM, 2016.
  83. Pavithra Prabhakar, Miriam García Soto. Counterexample Guided Abstraction Refinement for Stability Analysis. Computer Aided Verification - 28th International Conference, CAV 2016, Lecture Notes in Computer Science, Vol. 9779, páginas 495--512, Springer, 2016.
  84. Pavithra Prabhakar, Miriam García Soto. Hybridization for Stability Analysis of Switched Linear Systems. Proc. of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, páginas 71--80, ACM, 2016.
  85. Javier Esparza, Pierre Ganty, Jér^ome Leroux, Rupak Majumdar. Model Checking Population Protocols. 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 65, páginas 1--14, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016.
  86. Pierre Ganty, Damir Valput. Bounded-oscillation Pushdown Automata. Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016, EPTCS, Vol. 226, páginas 178--197, 2016.
  87. Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub. Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, páginas 76--87, ACM, 2016.
  88. Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin. Dependent types and multi-monadic effects in F. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, páginas 256--270, ACM, 2016.
  89. Mila Dalla Preda, Roberto Giacobazzi, Isabella Mastroeni. Completeness in Approximate Transduction. Proceedings of the 23rd International Symposium on Static Analysis (SAS), Lecture Notes in Computer Science, Vol. 9837, páginas 126--146, Springer, 2016.
  90. Sandrine Blazy, Vincent Laporte, David Pichardie. An abstract memory functor for verified C static analyzers. Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, páginas 325--337, 2016.
  91. Cédric Fournet, Chantal Keller, Vincent Laporte. A Certified Compiler for Verifiable Computing. IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016, páginas 268--280, 2016.
  92. Shauvik Roy Choudhary, Alessandra Gorla, Alessandro Orso. Automated Test Input Generation for Android: Are We There Yet?. Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, páginas 429--440, Noviembre 2015.
  93. Irfan Ul Haq, Juan Caballero, Michael D. Ernst. Ayudante: Identifying Undesired Variable Interactions. Proceedings of the 13th International Workshop on Dynamic Analysis, Octubre 2015.
  94. Platon Kotzias, Srdjan Matic, Richard Rivera, Juan Caballero. Certified PUP: Abuse in Authenticode Code Signing. Proceedings of the 22nd ACM Conference on Computer and Communication Security, Octubre 2015.
  95. Srdjan Matic, Platon Kotzias, Juan Caballero. CARONTE: Detecting Location Leaks for Deanonymizing Tor Hidden Services. Proceedings of the 22nd ACM Conference on Computer and Communication Security, Octubre 2015.
  96. Salvador Tamarit, Guillermo Vigueras, Manuel Carro, Julio Mariño. A Haskell Implementation of a Rule-Based Program Transformation for C Programs. International Symposium on Practical Aspects of Declarative Languages, LNCS, Núm. 9131, páginas 105--114, Springer-Verlag, Junio 2015.
  97. Vitalii Avdiienko, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller, Steven Arzt, Siegfried Rasthofer, Eric Bodden. Mining Apps for Abnormal Usage of Sensitive Data. Proceedings of the 37th International Conference on Software Engineering, ICSE 2015, páginas 426--436, ACM, Mayo 2015.
  98. Kurt Thomas, Elie Bursztein, Nav Jagpal, Moheeb Abu, Niels Provos, Paul Pearce, Grant Hoand Damon McCoy, Chris Grier, Vern Paxson, Antonio Nappa, Alexandros Kapravelos. Ad Injection at Scale: Assessing Deceptive Advertisement Modifications. Proceedings of the 36th IEEE Symposium on Security and Privacy, páginas 151--167, IEEE Computer Society, Mayo 2015.
  99. Antonio Nappa, Richard Johnson, Leyla Bilge, Juan Caballero, Tudor Dimitras. The Attack of the Clones: A Study of the Impact of Shared Code on Vulnerability Patching. Proceedings of the 36th IEEE Symposium on Security and Privacy, Mayo 2015.
  100. Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Mechanized Verification of Fine-grained Concurrent Programs. Conference on Programming Language Design and Implementation (PLDI), páginas 77--87, 2015.
  101. Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. European Symposium on Programming (ESOP), páginas 333--358, 2015.
  102. Andrea Mattavelli, Alberto Goffi, Alessandra Gorla. Synthesis of Equivalent Method Calls in Guava. Proceedings of the 7th International Symposium on Search-Based Software Engineering, SSBSE 2015, páginas 248--254, Springer, 2015.
  103. Andrea Cerone, Alexey Gotsman, Hongseok Yang. Transaction chopping for parallel snapshot isolation. DISC'15: International Symposium on Distributed Computing, Tokyo, Japan, LNCS, Vol. 9363, páginas 388--404, Springer, 2015.
  104. Andrea Cerone, Giovanni Bernardi, Alexey Gotsman. A framework for transactional consistency models with atomic visibility. CONCUR'15: International Conference on Concurrency Theory, Madrid, Spain, LIPICS, Vol. 42, páginas 58--71, Dagstuhl, 2015.
  105. Alexey Gotsman, Hongseok Yang. Composite replicated data types. ESOP'15: European Symposium on Programming, London, UK, LNCS, Vol. 9032, páginas 585--609, Springer, 2015.
  106. Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt. Automated Proofs of Pairing-based Cryptography. Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, páginas 1156--1168, ACM, 2015.
  107. Gilles Barthe, Sonia Belaïd, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub. Verified Proofs of Higher-Order Masking. Advances in Cryptology - EUROCRYPT 2015 - 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Sofia, Bulgaria, April 26-30, 2015, Proceedings, Part I, Lecture Notes in Computer Science, Vol. 9056, páginas 457--485, Springer, 2015.
  108. Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt. Mind the Gap: Modular Machine-checked Proofs of One-round Key Exchange Protocols. Advances in Cryptology - EUROCRYPT 2015 - 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Lecture Notes in Computer Science, Vol. 9057, páginas 689--718, Springer, 2015.
  109. Patrick Baillot, Gilles Barthe, Ugo Dal Lago. Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, Lecture Notes in Computer Science, Vol. 9450, páginas 203--218, Springer, 2015.
  110. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub. Relational Reasoning via Probabilistic Coupling. Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, Lecture Notes in Computer Science, Vol. 9450, páginas 387--401, Springer, 2015.
  111. Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, páginas 55--68, ACM, 2015.
  112. Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi. Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds. PKC 2015: 18th International Workshop on Theory and Practice in Public Key Cryptography, Lecture Notes in Computer Science, Vol. 9020, páginas 355--376, Springer, 2015.
  113. Boris Köpf. Reasoning about the Trade-off between Security and Performance. Proc. 12th International Conference on Quantitative Evaluation of Systems (QEST '15), Springer, 2015.
  114. Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko. Symbolic Polytopes for Quantitative Interpolation and Verification. Proc. 27th International Conference on Computer Aided Verification (CAV '15), Springer, 2015.
  115. Goran Doychev, Boris Köpf. Rational Protection Against Timing Attacks. Proc. 28th IEEE Computer Security Foundations Symposium (CSF'15), IEEE, 2015.
  116. Bernd Finkbeiner, Markus N. Rabe, César Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL*. Proc. of the 27th Int'l Conf. on Computer Aided Verification (CAV'15), LNCS, Vol. 9206, Springer, 2015.
  117. Z. Banković, U. Liqat, P. López-García. A Practical Approach for Energy Efficient Scheduling in Multicore Environments by combining Evolutionary and YDS Algorithms with Faster Energy Estimation. The 11th International Conference on Artificial Intelligence Applications and Innovations (AIAI'15), IFIP Advances in Information and Communication Technology, Vol. 458, páginas 478--493, Springer, 2015.
  118. Z. Banković, U. Liqat, P. López-García. Trading-off Accuracy vs. Energy in Multicore Processors via Evolutionary Algorithms Combining Loop Perforation and Static Analysis-based Scheduling. Hybrid Artificial Intelligent Systems (HAIS 2015), Lecture Notes in Computer Science, Vol. 9121, páginas 690--701, Springer International Publishing, 2015.
  119. Z. Banković, P. López-García. Improved Energy-aware Stochastic Scheduling based on Evolutionary Algorithms via Copula-based Modeling of Task Dependences. International Conference on Soft Computing Models in Industrial and Environmental Applications (SOCO 2015), Advances in Intelligent Systems and Computing, Vol. 368, páginas 153--163, Springer International Publishing, 2015.
  120. Z. Banković, P. López-García. Energy Efficient Allocation and Scheduling for DVFS-enabled Multicore Environments using a Multiobjective Evolutionary Algorithm. Genetic and Evolutionary Computation Conference (GECCO 2015), páginas 1353--1354, ACM, 2015.
  121. J.F. Morales, M. V. Hermenegildo. Pre-Indexed Terms for Prolog. Proceedings of the 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'14), LNCS, Vol. 8981, páginas 317--331, Springer, 2015.
  122. Dario Catalano, Dario Fiore. Using Linearly-Homomorphic Encryption to Evaluate Degree-2 Functions on Encrypted Data. ACM CCS 2015 -- 22nd ACM Conference on Computer and Communication Security, páginas 1518--1529, 2015.
  123. Dario Catalano, Dario Fiore, Luca Nizzardo. Programmable Hash Functions go Private: Constructions and Application to (Homomorphic) Signatures with Shorter Public Keys. Advances in Cryptology -- CRYPTO 2015 -- 35th Annual Cryptology Conference, Santa Barbara, CA, USA, August 16-20, 2015, Proceedings, Part II, LNCS, Vol. 9216, páginas 254--274, Springer, 2015.
  124. Michael Backes, Manuel Barbosa, Dario Fiore, Raphael M. Reischuk. ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data. 36th IEEE Symposium on Security and Privacy (Oakland) 2015, IEEE Computer Society, 2015.
  125. Jerusalem, Antoine, Vigueras, Guillermo, Sket, Federico, Samaniego, Cristobal, Wu, Ling, Noels, Ludovic, Tjahjanto, Denny, Casoni, Eva, Houzeaux, Guillaume, Makradi, Ahmed, Molina-Aldareguia, Jon M., Vazquez, Mariano. An XFEM/CZM implementation for massively parallel simulations of composites fracture. European Solid Mechanics Conference, ESMC 2015, 2015.
  126. Bishoksan Kafle, John P. Gallagher. Tree automata-based refinement with application to Horn clause verification. Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, Lecture Notes in Computer Science, Vol. 8931, páginas 209--226, Springer, 2015.
  127. Bishoksan Kafle, John P. Gallagher. Constraint Specialisation in Horn Clause Verification. Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015, páginas 85--90, Association for Computing Machinery, 2015.
  128. Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza. On Reducing Linearizability to State Reachability. Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, páginas 95--107, 2015.
  129. Michael Emmi, Constantin Enea, Jad Hamza. Monitoring Refinement via Symbolic Reasoning. Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, Portland, OR, USA, June 15-17, 2015, páginas 260--269, ACM, 2015.
  130. Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric. SMACK+Corral: A Modular Verifier - (Competition Contribution). Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, páginas 451--454, 2015.
  131. Michael Emmi, Pierre Ganty, Rupak Majumdar, Fernando Rosa-Velardo. Analysis of Asynchronous Programs with Event-Based Synchronization. Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, páginas 535--559, 2015.
  132. Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza. Tractable Refinement Checking for Concurrent Objects. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, páginas 651--662, ACM, 2015.
  133. Carolina Dania, Manuel Clavel. Model-Based Formal Reasoning about Data-Management Applications. Fundamental Approaches to Software Engineering - 18th International Conference, FASE 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Lecture Notes in Computer Science, Vol. 9033, páginas 218--232, Springer, 2015.
  134. Miguel Ángel García de Dios, Carolina Dania, Manuel Clavel. Formal Reasoning about Fine-Grained Access Control Policies. 11th Asia-Pacific Conference on Conceptual Modelling, APCCM 2015, Sydney, Australia, January 2015, CRPIT, Vol. 165, páginas 91--100, Australian Computer Society, 2015.
  135. Pavithra Prabhakar, Nima Roohi, Mahesh Viswanathan. Deciding Concurrent Planar Monotonic Linear Hybrid Systems. Formal Modeling and Analysis of Timed Systems - 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings, páginas 256--269, 2015.
  136. Pavithra Prabhakar, Miriam Garcia Soto. Foundations of Quantitative Predicate Abstraction for Stability Analysis of Hybrid Systems. Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, Lecture Notes in Computer Science, Vol. 8931, páginas 318--335, Springer, 2015.
  137. Ganty, Pierre, Genaim, Samir, Lal, Ratan, Prabhakar, Pavithra. From Non-Zenoness Verification to Termination. MEMOCODE '15: 13th ACM-IEEE Int. Conf. on Formal Methods and Models for System Design, IEEE Computer Society, 2015.
  138. Esparza, Javier, Ganty, Pierre, Leroux, Jér^ome, Majumdar, Rupak. Verification of Population Protocols. CONCUR '15: Proc. 26th Int. Conf. on Concurrency Theory, 2015.
  139. Durand-Gasselin, Antoine, Esparza, Javier, Ganty, Pierre, Majumdar, Rupak. Model Checking Parameterized Asynchronous Shared-Memory Systems. CAV '15: Proc. 25th Int. Conf. on Computer Aided Verification, LNCS, Vol. 9206, Springer, 2015.
  140. Ganty, Pierre, Iosif, Radu. Interprocedural Reachability for Flat Integer Programs. FCT '15: Proc. 20th Int. Symp. on Fundamentals of Computation Theory, LNCS, Springer, 2015.
  141. Ratan Lal, Pavithra Prabhakar. Bounded error flowpipe computation of parameterized linear systems. Proceedings of the International Conference on Embedded Software (EMSOFT), ACM, IEEE, 2015.
  142. Julio Mariño, Raúl N.N. Alborodo. A Model-driven Methodology for Generating and Verifying CSP-based Java Code. Communicating Process Architectures 2015, Proceedings of the 37th WoTUG Conference on Concurrent and Parallel Systems, páginas 85--108, Open Channel Publishing Ltd., 2015.
  143. Roberto Giacobazzi, Francesco Logozzo, Francesco Ranzato. Analyzing Program Analyses. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, páginas 261--273, 2015.
  144. Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia, Isabella Mastroeni. Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, páginas 329--341, 2015.
  145. M. Zubair Rafique, Juan Caballero, Christophe Huygens, Wouter Joosen. Network Dialog Minimization and Network Dialog Diffing: Two Novel Primitives for Network Security Applications. Proceedings of the 2014 Annual Computer Security Applications Conference, Diciembre 2014.
  146. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie. System-level Non-interference for Constant-time Cryptography. 21st ACM Conference on Computer and Communications Security (CCS 2014), páginas 1267--1279, ACM, Noviembre 2014.
  147. Gilles Barthe, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz. Synthesis of Fault Attacks on Cryptographic Implementations. 21st ACM Conference on Computer and Communications Security (CCS 2014), páginas 1016--1027, ACM, Noviembre 2014.
  148. Dragan Ivanovic, Manuel Carro. Transforming Service Compositions into Cloud-Friendly Actor Networks. Service-Oriented Computing - 12th International Conference, ICSOC 2014, Paris, France, November 3-6, 2014. Proceedings, LNCS, Vol. 8831, páginas 291--305, Springer Verlag, Noviembre 2014.
  149. Dragan Ivanović, Manuel Carro, Peerachai Kaowichakorn. Towards QoS Prediction Based on Composition Structure Analysis and Probabilistic Models. Service-Oriented Computing - 12th International Conference, ICSOC, LNCS, Vol. 8831, páginas 394--402, Springer Verlag, Noviembre 2014.
  150. Zhaoyan Xu, Antonio Nappa, Robert Baykov, Guangliang Yang, Juan Caballero, Guofei Gu. AutoProbe: Towards Automatic Active Malicious Server Probing Using Dynamic Binary Analysis. Proceedings of the 21st ACM Conference on Computer and Communication Security, Noviembre 2014.
  151. Liang Wang, Antonio Nappa, Juan Caballero, Thomas Ristenpart, Aditya Akella. WhoWas: A Platform for Measuring Web Deployments on IaaS Clouds. Proceedings of the 2014 ACM Internet Measurement Conference, Noviembre 2014.
  152. R. Haemmerlé. On Combining Backward and Forward Chaining in Constraint Logic Programming. 16th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'14), 12 páginas, ACM Press, Septiembre 2014.
  153. N. Stulova, J. F. Morales, M. V. Hermenegildo. Assertion-based Debugging of Higher-Order (C)LP Programs. 16th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'14), páginas 225--235, ACM Press, Septiembre 2014.
  154. David Urbina, Yufei Gu, Juan Caballero, Zhiqiang Lin. SigPath: A Memory Graph Based Approach for Program Data Introspection and Modification. Proceedings of the 19th European Symposium on Research in Computer Security, Septiembre 2014.
  155. Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub. Certified Synthesis of Efficient Batch Verifiers. Computer Security Foundations Symposium (CSF 2014), Julio 2014.
  156. Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub. Proving differential privacy in Hoare logic. Computer Security Foundations Symposium (CSF 2014), Julio 2014. CoRR abs/1407.2988 [cs.LO].
  157. Antonio Nappa, Zhaoyan Xu, Juan Caballero, Guofei Gu. CyberProbe: Towards Internet-Scale Active Detection of Malicious Servers. Proceedings of the Network and Distributed System Security Symposium, Febrero 2014.
  158. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, German Andres Delbianco. Communicating State Transition Systems for Fine-Grained Concurrent Resources. European Symposium on Programming (ESOP), páginas 290--310, 2014.
  159. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv. Modular Reasoning about Heap Paths via Effectively Propositional Formulas. Principles of Programming Languages (POPL), páginas 385--396, 2014.
  160. Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky. Safety of live transactions in transactional memory: TMS is necessary and sufficient. DISC'14: International Symposium on Distributed Computing, Austin, TX, USA, LNCS, Vol. 8784, páginas 376--390, Springer, 2014.
  161. Andrea Cerone, Alexey Gotsman, Hongseok Yang. Parameterised linearisability. ICALP'14: International Colloquium on Automata, Languages, and Programming, Copenhagen, Denmark, LNCS, Vol. 8573, páginas 271--284, Springer, 2014.
  162. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski. Replicated data types: specification, verification, optimality. Proceedings of the 41st ACM Symposium on Principles of Programming Languages (POPL'14), San Diego, CA, USA, páginas 271--284, ACM Press, 2014.
  163. Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey. Deriving Interpretations of the Gradually-Typed Lambda Calculus. Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation, PEPM '14, páginas 157--168, ACM, 2014.
  164. Cerone, Andrea, Hennessy, Matthew. Characterising Testing Preorders for Broadcasting Distributed Systems. Trustworthy Global Computing, páginas 67--81, Springer, 2014.
  165. Anindya Banerjee, David A. Naumann. A Logical Analysis of Framing for Specifications with Pure Method Calls. Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers, páginas 3--20, 2014.
  166. Gilles Barthe, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz. Making RSA-PSS Provably Secure against Non-random Faults. Cryptographic Hardware and Embedded Systems - CHES 2014 - 16th International Workshop, Busan, South Korea, September 23-26, 2014. Proceedings, Lecture Notes in Computer Science, Vol. 8731, páginas 206--222, Springer, 2014.
  167. Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt. Automated Analysis of Cryptographic Assumptions in Generic Group Models. Advances in Cryptology - CRYPTO 2014 - 34th Annual Cryptology Conference, Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part I, Lecture Notes in Computer Science, Vol. 8616, páginas 95--112, Springer, 2014.
  168. Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin. Probabilistic relational verification for cryptographic implementations. The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, páginas 193--206, ACM, 2014.
  169. Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa. Leakage Resilience against Concurrent Cache Attacks. Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, Lecture Notes in Computer Science, Vol. 8414, páginas 140--158, Springer, 2014.
  170. Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. Computer Security Foundations Symposium (CSF 2014), 2014. CoRR abs/1407.6845 [cs.PL].
  171. Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin. Automated Verification of Group Key Agreement Protocols. Proceedings of the 2014 IEEE Symposium on Security and Privacy, SP '14, páginas 179--194, IEEE Computer Society, 2014.
  172. Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa. Leakage Resilience against Concurrent Cache Attacks. Proc. 3rd Conference on Principles of Security and Trust (POST '14), Springer, 2014.
  173. Alejandro Sánchez, César Sánchez. Formal Verification of Skiplists with Arbitrarily Many Levels. Proc. of the 12th Int'l Symp. on Automated Technology for Verification and Analysis (ATVA), LNCS, Vol. 8837, páginas 314--329, Springer, 2014.
  174. Alejandro Sánchez, César Sánchez. Parametrized Verification Diagrams. Proc. of the 21st Int'l Symp. on Temporal Representation and Reasoning (TIME'14), páginas 132--141, IEEE Computer Society Press, 2014.
  175. Laura Bozzelli, César Sánchez. Foundations of Boolean Stream Runtime Verification. LNCS, Vol. 8734, páginas 64--79, Springer, 2014.
  176. Alejandro Sánchez, César Sánchez. LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes. Proc. of the 26th Int'l Conf. on Computer Aided Verification (CAV'14), LNCS, Vol. 8559, páginas 620--627, Springer, 2014.
  177. Laura Bozzelli, César Sánchez. Visibly Linear Temporal Logic. Proc. of the 7th Int'l Joint Conf. on Automated Reasoning (IJCAR'14), LNCS, Vol. 8562, páginas 418--433, Springer, 2014.
  178. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez. Temporal Logics for Hyperproperties. Proc. of the 3rd Conference on Principles of Security and Trust (POST 2014), LNCS, Vol. 8414, páginas 265--284, Springer, 2014.
  179. U. Liqat, S. Kerrison, A. Serrano, K. Georgiou, P. Lopez-Garcia, N. Grech, M. V. Hermenegildo, K. Eder. Energy Consumption Analysis of Programs based on XMOS ISA-Level Models. Logic-Based Program Synthesis and Transformation, 23rd International Symposium, LOPSTR 2013, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 8901, páginas 72--90, Springer, 2014.
  180. Dario Fiore, Rosario Gennaro, Valerio Pastro. Efficiently Verifiable Computation on Encrypted Data. ACM CCS 2014 -- 21th ACM Conference on Computer and Communication Security, páginas 844--855, 2014.
  181. Dario Catalano, Dario Fiore, Bogdan Warinschi. Homomorphic Signatures with Efficient Verification for Polynomial Functions. Advances in Cryptology -- CRYPTO 2014 -- 34th Annual Cryptology Conference, Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part I, LNCS, Vol. 8616, páginas 371--389, Springer, 2014.
  182. Dario Catalano, Dario Fiore, Rosario Gennaro, Luca Nizzardo. Generalizing Homomorphic MACs for Arithmetic Circuits. PKC 2014: 17th International Workshop on Theory and Practice in Public Key Cryptography, LNCS, Vol. 8383, páginas 538--555, Springer, 2014.
  183. Yevgeniy Dodis, Dario Fiore. Interactive Encryption and Message Authentication. Security and Cryptography for Networks - 9th International Conference, SCN 2014, LNCS, Vol. 8642, páginas 494--513, Springer, 2014.
  184. Giovanni Bernardi, Ornela Dardha, Simon J. Gay, Dimitrios Kouzapas. On Duality Relations for Session Types. Trustworthy Global Computing, TGC 2014 Revised Selected Papers, Lecture Notes in Computer Science, páginas 51--66, Springer Berlin Heidelberg, 2014.
  185. Giovanni Bernardi, Matthew Hennessy. Using Higher-Order Contracts to Model Session Types (Extended Abstract). CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, Lecture Notes in Computer Science, Vol. 8704, páginas 387--401, Springer, 2014.
  186. Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones. Modular, higher-order cardinality analysis in theory and practice. Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, páginas 335--348, ACM, 2014.
  187. Zvonimir Rakamaric, Michael Emmi. SMACK: Decoupling Source Language Details from Verifier Implementations. Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Vol. 8559, páginas 106--113, Springer, 2014.
  188. Michael Emmi, Burcu Kulahcioglu Ozkan, Serdar Tasiran. Exploiting synchronization in the analysis of shared-memory asynchronous programs. 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014, páginas 20--29, ACM, 2014.
  189. Marcos Arjona, Carolina Dania, Marina Egea, Antonio Maña. Validation of a Security Metamodel for the Development of Cloud Applications. Proceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014., páginas 33--42, 2014.
  190. Achim D. Brucker, Tony Clark, Carolina Dania, Geri Georg, Martin Gogolla, Frédéric Jouault, Ernest Teniente, Burkhart Wolff. Panel Discussion: Proposals for Improving OCL. Proceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014., páginas 83--99, 2014.
  191. Carolina Dania, Manuel Clavel. Modeling Social Networking Privacy. 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, September 1-3, 2014, páginas 50--57, 2014.
  192. Pavithra Prabhakar, Miriam Garcia Soto. An algorithmic approach to stability verification of polyhedral switched systems. American Control Conference, ACC 2014, Portland, OR, USA, June 4-6, 2014, páginas 2318--2323, IEEE, 2014.
  193. Jun Liu, Pavithra Prabhakar. Switching control of dynamical systems from metric temporal logic specifications. 2014 IEEE International Conference on Robotics and Automation, ICRA 2014, Hong Kong, China, May 31 - June 7, 2014, páginas 5333--5338, IEEE, 2014.
  194. Ganty, Pierre, Rezine, Ahmed. Ordered Counter Abstraction (Refinable Subword Relations for Parameterized Verification). LATA'14, 8th Int. Conf. on Language and Automata Theory and Applications, LNCS, Vol. 8370, páginas 396--407, Springer, 2014.
  195. Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin. Proving the TLS Handshake Secure (As It Is). Advances in Cryptology - CRYPTO 2014 - 34th Annual Cryptology Conference, Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part II, páginas 235--255, 2014.
  196. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub. Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. Proceedings of the 2014 IEEE Symposium on Security and Privacy, SP '14, páginas 98--113, IEEE Computer Society, 2014.
  197. Evmorfia-Iro Bartzia, Pierre-Yves Strub. A Formal Library for Elliptic Curves in the Coq Proof Assistant. Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science, Vol. 8558, páginas 77--92, Springer, 2014.
  198. Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman. Gradual typing embedded securely in JavaScript. The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, páginas 425--438, ACM, 2014.
  199. Zhoulai Fu. Targeted Update - Aggressive Memory Abstraction Beyond Common Sense and Its Application on Static Numeric Analysis. Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, páginas 534--553, 2014.
  200. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella Béguelin. Fully automated analysis of padding-based encryption in the computational model. 2013 ACM SIGSAC Conference on Computer and Communications Security (CCS'13), páginas 1247--1260, ACM, Noviembre 2013.
  201. Martina Lindorfer, Matthias Neumayr, Juan Caballero, Christian Platzer. POSTER: Cross-Platform Malware: Write Once, Infect Everywhere. Proceedings of the 20th ACM Conference on Computer and Communications Security, Noviembre 2013.
  202. M. Zubair Rafique, Juan Caballero. FIRMA: Malware Clustering and Network Signature Generation with Mixed Network Behaviors. Proceedings of the 16th International Symposium on Research in Attacks, Intrusions and Defenses, Octubre 2013.
  203. A. Serrano, P. Lopez-Garcia, F. Bueno, M. V. Hermenegildo. Sized Type Analysis for Logic Programs (Technical Communication). Theory and Practice of Logic Programming, 29th Int'l. Conference on Logic Programming (ICLP'13) Special Issue, On-line Supplement, Vol. 13, Núm. 4-5, páginas 1--14, Cambridge U. Press, Agosto 2013.
  204. Antonio Nappa, M. Zubair Rafique, Juan Caballero. Driving in the Cloud: An Analysis of Drive-by Download Operations and Abuse Reporting. Proceedings of the 10th Conference on Detection of Intrusions and Malware & Vulnerability Assessment, Julio 2013.
  205. 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, Enero 2013.
  206. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. Supporting Pruning in Tabled LP. Practical Aspects of Declarative Languages (PADL'13), LNCS, Springer Verlag, Enero 2013.
  207. Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski. Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures. Principles and Practice of Declarative Programming (PPDP), páginas 145--156, 2013.
  208. Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. Mtac: A Monad for Typed Tactic Programming in Coq. International Conference on Functional Programming (ICFP), páginas 87--100, 2013.
  209. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv. Effectively-Propositional Reasoning about Reachability in Linked Data Structures. Computer Aided Verification (CAV), páginas 756--772, 2013.
  210. Ruy Ley-Wild, Aleksandar Nanevski. Subjective Auxiliary State for Coarse-Grained Concurrency. Principles of Programming Languages (POPL), páginas 561--574, 2013.
  211. Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky. A programming language perspective on transactional memory consistency. Proceedings of the 32nd ACM Symposium on Principles of Distributed Computing (PODC'13), Montreal, Canada, páginas 309--318, ACM Press, 2013.
  212. Alexey Gotsman, Noam Rinetzky, Hongseok Yang. Verifying concurrent memory reclamation algorithms with grace. Proceedings of the 22nd European Symposium on Programming (ESOP'13), Rome, Italy, LNCS, Vol. 7792, páginas 249--269, Springer, 2013.
  213. 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, páginas 235--248, ACM Press, 2013.
  214. Álvaro García-Pérez, Pablo Nogueira, Juan José Moreno-Navarro. Deriving the Full-reducing Krivine Machine from the Small-step Operational Semantics of Normal Order. Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, páginas 85--96, ACM, 2013.
  215. Álvaro García-Pérez, Pablo Nogueira. A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers. Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM '13, páginas 107--116, ACM, 2013.
  216. Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin. Verified Computational Differential Privacy with Applications to Smart Metering. CSF, páginas 287--301, IEEE, 2013.
  217. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. 2013 ACM SIGSAC Conference on Computer and Communications Security (CCS'13), páginas 1217--1230, 2013.
  218. 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, páginas 29--43, Springer, 2013.
  219. 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, páginas 123--134, ACM, 2013.
  220. Simon Meier, Benedikt Schmidt, Cas Cremers, David A. Basin. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, Vol. 8044, páginas 696--701, Springer, 2013.
  221. Boris Köpf, Andrey Rybalchenko. Automation of Quantitative Information-Flow Analysis. 13th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM), LNCS 7938, Springer, 2013.
  222. Goran Doychev, Dominik Feld, Boris Köpf, Laurent Mauborgne, Jan Reineke. CacheAudit: A Tool for the Static Analysis of Cache Side Channels. 22nd USENIX Security Symposium, USENIX, 2013.
  223. Pavithra Prabhakar, Boris Köpf. Verifying Information Flow Properties of Hybrid Systems. Proc. 2nd ACM International Conference on High Confidence Networked Systems (HiCoNS), ACM, 2013.
  224. Michael Backes, Goran Doychev, Boris Köpf. Preventing Side-Channel Leaks in Web Traffic: A Formal Approach. Proc. 20th Network and Distributed Systems Security Symposium (NDSS), Internet Society, 2013.
  225. Z. Banković, P. Lopez-Garcia. Genetic Algorithm-based Allocation and Scheduling for Voltage and Frequency Scalable XMOS Chips. Hybrid Artificial Intelligent Systems (HAIS 2013), Lecture Notes in Computer Science, Vol. 8073, páginas 401--410, Springer, 2013.
  226. Germán Andrés Delbianco, Aleksandar Nanevski. Hoare-style reasoning with (algebraic) continuations. Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, ICFP '13, páginas 363--376, ACM, 2013.
  227. Guillermo Vigueras, Cristobal Samaniego, Guillaume Houzeau, Mariano Vazquez, Antoine Jerusalem. An XFEM Implementation for Fracture Simulations of Composites. International Conference on Computational Plasticity. Fundamentals and Applications. COMPLAS 2013, 2013.
  228. Guillermo Vigueras, Cristobal Samaniego, Eva Casoni, Guillaume Houzeau, Federico Sket, Jon Molina-Aldareguia, Ahmed Makradi, Mariano Vazquez, Antoine Jerusalem. An XFEM-CZM Implementation for Large-Scale Fracture Simulations of Composites Laminates. European Congress and Exhibition on Advanced Materials and Processes. EUROMAT 2013, 2013.
  229. Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens. Fixing idioms: a recursion primitive for applicative DSLs. Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, páginas 97--106, ACM, 2013.
  230. Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens. Monadic abstract interpreters. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, páginas 399--410, ACM, 2013.
  231. Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza. Verifying Concurrent Programs Against Sequential Specifications. ESOP '13: Proc. 22nd European Symposium on Programming, LNCS, Springer, 2013.
  232. Carolina Dania, Manuel Clavel. OCL2FOL+: Coping with Undefinedness. Proceedings of the MODELS 2013 OCL Workshop co-located with the 16th International ACM/IEEE Conference on Model Driven Engineering Languages and Systems (MODELS 2013), Miami, USA, September 30, 2013, CEUR Workshop Proceedings, Vol. 1092, páginas 53--62, CEUR-WS.org, 2013.
  233. Pavithra Prabhakar, Miriam Garcia Soto. Abstraction Based Model-Checking of Stability of Hybrid Systems. CAV, páginas 280--295, 2013.
  234. Pavithra Prabhakar, Jun Liu, Richard M. Murray. Pre-orders for reasoning about stability properties with respect to input of hybrid systems. EMSOFT, páginas 1--10, 2013.
  235. Pavithra Prabhakar, Mahesh Viswanathan. On the decidability of stability of hybrid systems. HSCC, 2013.
  236. Scott C. Livingston, Pavithra Prabhakar, Alex B. Jose, Richard M. Murray. Patching task-level robot controllers based on a local -calculus formula. ICRA, 2013.
  237. Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan. Hybrid Automata based CEGAR for Rectangular Hybrid Automata. VMCAI, 2013.
  238. Javier Esparza, Pierre Ganty, Rupak Majumdar. Parameterized Verification of Asynchronous Shared-Memory Systems. CAV'13: Proc. 23rd Int. Conf. on Computer Aided Verification, LNCS, Vol. 8044, páginas 124--140, Springer, 2013.
  239. Pierre Ganty, Samir Genaim. Proving Termination Starting from the End. CAV'13: Proc. 23rd Int. Conf. on Computer Aided Verification, LNCS, Vol. 8044, páginas 397--412, Springer, 2013.
  240. Pierre Ganty, Radu Iosif, Filip Konecný. Underapproximation of Procedure Summaries for Integer Programs. TACAS'13: Proc. 19th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS, Vol. 7795, páginas 247--261, Springer, 2013.
  241. Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits. Fully abstract compilation to JavaScript. The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, páginas 371--384, ACM, 2013.
  242. Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub. Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security and Privacy, páginas 445--459, IEEE Computer Society, 2013.
  243. D. Ivanovic, M. Carro, M. V. Hermenegildo. A Constraint-Based Approach to Quality Assurance in Service Choreographies. 10th International Conference on Service Oriented Computing, ICSOC'12, LNCS, Vol. 7637, Springer Verlag, Noviembre 2012.
  244. 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, Octubre 2012.
  245. George Bariannys, M. Carro, Dimitris Plexousakis. Deriving Specifications for Composite Web Services. IEEE Signature Conference on Computers, Software, and Applications, IEEE Computer Society, IEEE, Julio 2012.
  246. 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, Julio 2012.
  247. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, P. Stuckey. A General Implementation Framework for Tabled CLP. FLOPS'12, LNCS, Núm. 7294, páginas 104--119, Springer Verlag, Mayo 2012.
  248. P. Chico de Guzmán, A. Casas, M. Carro, M. V. Hermenegildo. A Segment-Swapping Approach for Executing Trapped Computations. PADL'12, LNCS, Vol. 7149, páginas 138--152, Springer Verlag, Enero 2012.
  249. 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, páginas 31--45, Springer, 2012.
  250. 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, páginas 256--271, Springer, 2012.
  251. 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, páginas 87--107, Springer, 2012.
  252. Mark Marron, Ondrej Lhoták, Anindya Banerjee. Programming Paradigm Driven Heap Analysis. 21st International Conference on Compiler Construction (CC 2012), Lecture Notes in Computer Science, Vol. 7210, páginas 41--60, Springer Berlin Heidelberg, 2012.
  253. Stan Rosenberg, Anindya Banerjee, David A. Naumann. Decision Procedures for Region Logic. 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012), Lecture Notes in Computer Science, Vol. 7148, páginas 379--395, Springer Berlin Heidelberg, 2012.
  254. Alexander Malkis, Anindya Banerjee. Verification of Software Barriers. Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel Programming (PPoPP 2012), páginas 313--314, ACM, 2012.
  255. 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, páginas 488--500, 2012.
  256. 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, páginas 724--735, 2012.
  257. 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, páginas 7--8, Springer, 2012.
  258. 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, páginas 186--197, IEEE, 2012.
  259. 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, páginas 354--368, IEEE, 2012.
  260. 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, páginas 11--27, Springer, 2012.
  261. 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, páginas 186--202, Springer, 2012.
  262. 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, páginas 1--6, Springer, 2012.
  263. 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, páginas 1--2, Springer, 2012.
  264. 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, páginas 47--66, Springer, 2012.
  265. 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, páginas 97--110, ACM, 2012.
  266. 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.
  267. 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, páginas 564--580, Springer-Verlag, 2012.
  268. 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), páginas 97--109, ACM, 2012.
  269. 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, páginas 146--163, Springer, 2012.
  270. 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), páginas 13--20, IEEE Computer Society, 2012.
  271. 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, páginas 30--45, Springer, 2012.
  272. Laura Bozzelli, César Sánchez. Visibly Rational Expressions. Proc. of the 32nd Int'l Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), Leibniz International Proceedings in Informatics (LIPIcs), páginas 211--223, Leibniz-Zentrum fuer Informatik, 2012.
  273. Aizatulin, Mihhail, Dupressoir, Francois, Gordon, Andrew D., Jürjens, Jan. Verifying Cryptographic Code in C: Some Experience and the Csec Challenge. Formal Aspects of Security and Trust (FAST), Lecture Notes in Computer Science, Vol. 7140, páginas 1--20, Springer Berlin Heidelberg, 2012. Invited Paper, also appears as tech. rep. MSR-TR-2011-118.
  274. 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.
  275. 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), páginas 13--20, IEEE Computer Society, 2012.
  276. 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, páginas 30--45, Springer, 2012.
  277. Pavithra Prabhakar. Foundations for Approximation Based Analysis of Stability Properties of Hybrid Systems. 50th Annual Allerton Conference on Communication, Control and Computing, 2012.
  278. 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, páginas 101--117, Springer, 2012.
  279. 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, páginas 197--206, ACM, 2012.
  280. 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, páginas 285--294, IEEE Computer Society Press, 2012.
  281. 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, páginas 476--496, Springer, 2012.
  282. D. Ivanović, M. Carro, M. V. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. Service-Oriented Computing -- ICSOC 2011, LNCS, Vol. 7084, páginas 62--76, Springer Verlag, Diciembre 2011. Best paper award.
  283. 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, páginas 122--137, Springer, Noviembre 2011.
  284. 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, páginas 68--83, Springer, Octubre 2011.
  285. 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, páginas 71--90, Springer, Agosto 2011.
  286. Juan Caballero, Chris Grier, Christian Kreibich, Vern Paxson. Measuring Pay-per-Install: The Commoditization of Malware Distribution. Proceedings of the 20th USENIX Security Symposium, Agosto 2011.
  287. J. F. Morales, M. V. Hermenegildo, R. Haemmerlé. Modular Extensions for Modular (Logic) Languages. Proceedings of the 21th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'11), LNCS, Vol. 7225, páginas 139--154, Springer, Julio 2011.
  288. R. Haemmerlé, P. López, M. V. Hermenegildo. CLP Projection for Constraint Handling Rules. Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, páginas 137--148, ACM Press, Julio 2011.
  289. D. Ivanović, M. Carro, M. V. Hermenegildo. Automated Attribute Inference in Complex Service Workflows Based on Sharing Analysis. Proceedings of the 8th IEEE Conference on Services Computing SCC 2011, páginas 120--127, IEEE Press, Julio 2011.
  290. Gilles Barthe, Juan Manuel Crespo, César Kunz. Relational Verification Using Product Programs. FM 2011: 17th International Symposium on Formal Methods, LNCS, Vol. 6664, páginas 200--214, Springer, Junio 2011.
  291. 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, páginas 231--245, Springer, Junio 2011.
  292. David A. Basin, Manuel Clavel, Marina Egea. A decade of model-driven security. SACMAT 2011, 16th ACM Symposium on Access Control Models and Technologies, páginas 1--10, ACM, Junio 2011.
  293. Germán Andrés Delbianco, Mauro Jaskelioff, Alberto Pardo. Applicative Shortcut Fusion. 12th International Symposium on Trends in Functional Programming, TFP'11, Mayo 2011.
  294. 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, Mayo 2011.
  295. 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, páginas 180--196, Springer, Febrero 2011.
  296. E. Mera, T. Trigo, P. López-García, M. V. Hermenegildo. Profiling for Run-Time Checking of Computational Properties and Performance Debugging. Practical Aspects of Declarative Languages (PADL'11), Lecture Notes in Computer Science, Vol. 6539, páginas 38--53, Springer-Verlag, Enero 2011.
  297. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. How to make ad hoc proof automation less ad hoc. International Conference on Functional Programming (ICFP), páginas 163--175, 2011.
  298. 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), páginas 165--179, 2011.
  299. Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski. Partiality, State and Dependent Types. Typed Lambda Calculi and Applications (TLCA), páginas 198--212, 2011.
  300. Alexey Gotsman, Hongseok Yang. Modular verification of preemptive OS kernels. Proceedings of the 16th ACM International Conference on Functional Programming (ICFP'11), Tokyo, Japan, páginas 404--417, ACM Press, 2011.
  301. 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, páginas 453--465, Springer, 2011.
  302. 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.
  303. 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.
  304. Gilles Barthe, Boris Köpf. Information-theoretic Bounds for Differentially Private Mechanisms. Proc. 24rd IEEE Computer Security Foundations Symposium (CSF '11), páginas 191--204, IEEE, 2011.
  305. 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), páginas 367--375, ACM, 2011.
  306. 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, páginas 343--358, Springer, 2011.
  307. M. Carro, D. Karastoyanova, G. A. Lewis, A. Liu. Third International Workshop on Principles of Engineering Service-Oriented Systems (PESOS 2011). ICSE, páginas 1218--1219, 2011.
  308. Dupressoir, Francois, Gordon, Andrew D., Jürjens, Jan, Naumann, David A.. Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. Proceedings of the 2011 IEEE 24th Computer Security Foundations Symposium (CSF), páginas 3--17, IEEE Computer Society, 2011.
  309. 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, páginas 456--472, Springer-Verlag, 2011.
  310. 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, páginas 172--187, Springer, 2011.
  311. 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.
  312. 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, páginas 101--124, Springer, 2011.
  313. 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, páginas 133--142, ACM, 2011.
  314. 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.
  315. 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.
  316. 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, páginas 499--510, ACM Press, 2011.
  317. 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), páginas 43--55, SciTePress, Octubre 2010.
  318. 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, páginas 104--113, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Julio 2010.
  319. 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, páginas 1--38, American Institue of Aeronautics and Astronautics, Abril 2010. AIAA-2010-3385.
  320. Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine. Structuring the verification of heap-manipulating programs. Principles of Programming Languages (POPL), páginas 261--274, 2010.
  321. 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, páginas 356--372, Springer, 2010.
  322. 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, páginas 125--139, Springer, 2010.
  323. David A. Naumann, Anindya Banerjee. Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. ESOP, páginas 2--22, 2010.
  324. Stan Rosenberg, Anindya Banerjee, David A. Naumann. Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. VSTTE, páginas 183--198, 2010.
  325. 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, páginas 72--86, Springer, 2010.
  326. Gilles Barthe, César Kunz. Perspectives in Certificate Translation. Trustworthly Global Computing - 5th International Symposium, TGC 2010, Lecture Notes in Computer Science, Vol. 6084, páginas 23--34, Springer, 2010.
  327. 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, páginas 375--386, ACM, 2010.
  328. 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, páginas 91--106, IEEE Computer Society, 2010.
  329. 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.
  330. 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, páginas 246--260, IEEE Computer Society, 2010.
  331. 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, páginas 115--130, Springer, 2010.
  332. 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, páginas 237--252, Springer, 2010.
  333. 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, Núm. 6037, páginas 173--187, Springer, 2010.
  334. 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), páginas 44--56, IEEE, 2010.
  335. Boris Köpf, Andrey Rybalchenko. Approximation and Randomization for Quantitative Information-Flow Analysis. Proc. 23rd IEEE Computer Security Foundations Symposium (CSF '10), páginas 3--14, IEEE, 2010.
  336. 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, páginas 508--523, Springer, 2010.
  337. Martin Leucker, César Sánchez. Regular Linear-Time Temporal Logic. Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), páginas 3--5, IEEE Computer Society, 2010.
  338. 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, páginas 295--311, Springer, 2010.
  339. 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, páginas 293--307, Springer, 2010.
  340. 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, páginas 74--89, Springer, 2010.
  341. D. Ivanović, M. Carro, M. V. Hermenegildo. Automatic Fragment Identification in Workflows Based on Sharing Analysis. Service-Oriented Computing -- ICSOC 2010, LNCS, Vol. 6470, páginas 350--364, Springer Verlag, 2010.
  342. D. Ivanović, M. Carro, M. V. 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, páginas 107--114, IEEE, 2010.
  343. 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, páginas 27--45, Springer, 2010.
  344. 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, páginas 1--9, 2010.
  345. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. A Scalable Segmented Decision Tree Abstract Domain. Pnueli Festschrift, Lecture Notes in Computer Science, Vol. 6200, páginas 72--95, Springer-Verlag, 2010.
  346. Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur. Shape Analysis with Reference Set Relations. VMCAI, 2010.
  347. 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, páginas 311--312, ACM, 2010.
  348. 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, páginas 201--217, Springer, 2010.
  349. 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.
  350. Pierre Ganty, Benjamin Monmege, Rupak Majumdar. Bounded Underapproximations. CAV'10: Proc. 20th Int. Conf. on Computer Aided Verification, LNCS, Vol. 6174, páginas 600--614, Springer, 2010.
  351. Umut A. Acar, Guy E. Blelloch, Ruy Ley-Wild, Kanat Tangwongsan, Duru Türkoglu. Traceable data types for self-adjusting computation. PLDI, páginas 483--496, 2010.
  352. 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, páginas 102--116, Noviembre 2009.
  353. 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, páginas 149--159, Elsevier, Agosto 2009.
  354. E. Mera, P. López-García, M. V. Hermenegildo. Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework. 25th Int'l. Conference on Logic Programming (ICLP'09), LNCS, Vol. 5649, páginas 281--295, Springer-Verlag, Julio 2009.
  355. 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, Núm. 5649, páginas 190--204, Springer-Verlag, Julio 2009.
  356. V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee. Merlin: specification inference for explicit information flow problems. PLDI, páginas 75--86, Junio 2009.
  357. 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, Junio 2009.
  358. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. Towards a Complete Scheme for Tabled Execution Based on Program Transformation. 11th International Symposium on Practical Aspects of Declarative Languages (PADL'09), LNCS, Núm. 5418, páginas 224--238, Springer-Verlag, Enero 2009.
  359. Avraham Shinnar, Marco Pistoia, Anindya Banerjee. A language for information flow: dynamic tracking in multiple interdependent dimensions. PLAS, páginas 125--131, 2009.
  360. 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, páginas 541--560, Springer, 2009.
  361. 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, páginas 90--101, ACM, 2009.
  362. 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, páginas 237--250, IEEE Computer Society, 2009.
  363. 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.
  364. 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, páginas 55--69, Springer, 2009.
  365. 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.
  366. 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, páginas 380--390, Springer, 2009.
  367. 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, páginas 317--350, 2009.
  368. Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko. Verifying Liveness for Asynchronous Programs. POPL '09: Proc. 36th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, páginas 102--113, ACM Press, 2009.
  369. 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.
  370. 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, páginas 164--178, Springer, 2009.
  371. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo. Negative Ternary Set-Sharing. International Conference on Logic Programming, ICLP, LNCS, Núm. 5366, páginas 301--316, Springer-Verlag, Diciembre 2008.
  372. 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, páginas 795--800, Springer Verlag, Diciembre 2008. Short paper.
  373. A. Casas, M. Carro, M. V. Hermenegildo. A High-Level Implementation of Non-Deterministic, Unrestricted, Independent And-Parallelism. 24th International Conference on Logic Programming (ICLP'08), LNCS, Vol. 5366, páginas 651--666, Springer-Verlag, Diciembre 2008.
  374. 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, Noviembre 2008.
  375. 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, páginas 135--146, Octubre 2008.
  376. 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, Agosto 2008.
  377. J. Morales, M. Carro, M. V. 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), páginas 32--43, ACM Press, Julio 2008.
  378. E. Mera, P. López-García, M. Carro, M. V. 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), páginas 174--184, ACM Press, Julio 2008.
  379. 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 páginas, Springer, Abril 2008.
  380. 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, Núm. 4905, páginas 172--187, Springer-Verlag, Enero 2008.
  381. P. Chico de Guzmán, M. Carro, M. V. 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, páginas 198--213, Springer-Verlag, Enero 2008.
  382. 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, páginas 18--34, Springer Verlag, Enero 2008.
  383. A. Casas, M. Carro, M. V. 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, páginas 230--247, Springer-Verlag, Enero 2008.
  384. P. Pietrzak, J. Correas, G. Puebla, M. V. Hermenegildo. A Practical Type Analysis for Verification of Modular Prolog Programs. ACM SIGPLAN 2008 Workshop on Partial Evaluation and Program Manipulation (PEPM'08), páginas 61--70, ACM Press, Enero 2008.
  385. Anindya Banerjee, Michael Barnett, David A. Naumann. Boogie Meets Regions: A Verification Experience Report. VSTTE, páginas 177--191, 2008.
  386. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Expressive Declassification Policies and Modular Static Enforcement. IEEE Symposium on Security and Privacy, páginas 339--353, 2008.
  387. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Regional Logic for Local Reasoning about Global Invariants. ECOOP, páginas 387--411, 2008.
  388. 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, páginas 75--90, Springer, 2008.
  389. Gilles Barthe, César Kunz. Certificate Translation in Abstract Interpretation. 17th European Symposium on Programming, ESOP 2008, Lecture Notes in Computer Science, Vol. 4960, páginas 368--382, Springer, 2008.
  390. 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, páginas 127--136, IEEE Computer Society, 2008.
  391. Gilles Barthe, Salvador Cavadini, Tamara Rezk. Tractable Enforcement of Declassification Policies. Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, páginas 83--97, IEEE Computer Society, 2008.
  392. 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, páginas 493--507, Springer, 2008.
  393. 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, páginas 83--99, Springer, 2008.
  394. 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, páginas 152--167, Springer, 2008.
  395. 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, páginas 55--70, Springer, 2008.
  396. 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, páginas 682--696, Springer, 2008.
  397. 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, páginas 327--338, Springer-Verlag, 2008.
  398. 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.
  399. P. Pietrzak, M. V. Hermenegildo. Automatic Binding-related Error Diagnosis in Logic Programs. International Conference on Logic Programming (ICLP'07), LNCS, Núm. 4670, páginas 333--347, Springer-Verlag, Septiembre 2007.
  400. 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), Lecture Notes in Computer Science, Núm. 4915, páginas 154--168, Springer-Verlag, Agosto 2007.
  401. A. Casas, M. Carro, M. V. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. 17th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'07), LNCS, Núm. 4915, páginas 138--153, Springer-Verlag, Agosto 2007.
  402. J.F. Morales, M. Carro, M. V. Hermenegildo. Towards Description and Optimization of Abstract Machines in an Extension of Prolog. Logic-Based Program Synthesis and Transformation (LOPSTR'06), LNCS, Núm. 4407, páginas 77--93, Julio 2007.
  403. 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, Junio 2007.
  404. 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, Núm. 4354, páginas 140--154, Springer-Verlag, Enero 2007.
  405. 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.
  406. 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, páginas 420--435, Springer-Verlag, 2007.
  407. 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, páginas 173--178, Springer, 2007.


Libros y Monografías

  1. M. V. Hermenegildo, P. Lopez-Garcia (Eds.). Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers. Lecture Notes in Computer Science, Núm. 10184, 330 páginas, Springer, Julio 2017.
  2. Manuel Carro, Andy King (Eds.). 32nd International Conference on Logic Programming. Vol. 16, Núm. 5-6, Cambridge University Press, Septiembre 2016.
  3. Manuel Carro, Salvador Tamarit, Guillermo Vigueras, Julio Mariño (Eds.). First International Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016). Marzo 2016.
  4. A. Zaks, M. V. Hermenegildo. Proceedings of the 25th International Conference on Compiler Construction (CC 2016). ACM, Marzo 2016.
  5. Antonio Nappa. Defending Against Cybercrime: Advances in the Detection of Malicious Servers and the Analysis of Client-Side Vulnerabilities. Tesis Doctoral, Escuela Técnica Superior de Ingenieros Informáticos, Universidad Politécnica de Madrid, Madrid, Spain, Febrero 2016.
  6. Antonio Nappa. Defending Against Cybercrime: Advances in the Detection of Malicious Servers and the Analysis of Client-Side Vulnerabilities. Tesis Doctoral, Escuela Técnica Superior de Ingenieros Informáticos, Universidad Politécnica de Madrid, Madrid, Spain, Febrero 2016.
  7. Gilles Barthe, Evangelos P. Markatos, Pierangela Samarati (Eds.). Security and Trust Management - 12th International Workshop, STM 2016, Heraklion, Crete, Greece, September 26-27, 2016, Proceedings. Lecture Notes in Computer Science, Vol. 9871, Springer, 2016.
  8. Manuel Carro, Andy King, Neda Saeedloei, Marina De Vos (Eds.). Technical Communications of the 32nd International Conference on Logic Programming. OASICS, Vol. 52, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
  9. John P. Gallagher, Philipp Rümmer (Eds.). Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS (satellite event of ETAPS), Eindhoven, The Netherlands, 3rd April 2016. EPTCS, Vol. 219, 2016.
  10. Juan Caballero, Eric Bodden, Elias Athanasopoulos. Engineering Secure Software and Systems - 8th International Symposium, ESSoS 2016. Proceedings. Lecture Notes in Computer Science, Vol. 9639, Springer, 2016.
  11. Pierre Ganty, Michele Loreti (Eds.). Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015, Revised Selected Papers. Lecture Notes in Computer Science, Vol. 9533, Springer, 2016.
  12. Alejandro Sánchez. Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures. Tesis Doctoral, ETS de Ingenieros Informáticos, Technical University of Madrid, Septiembre 2015.
  13. Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, Annabelle McIver. Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181). Dagstuhl Reports, Vol. 5, Núm. 4, páginas 123--141, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015.
  14. Frank Piessens, Juan Caballero, Nataliia Bielova. Engineering Secure Software and Systems - 7th International Symposium, ESSoS 2015, Milan, Italy, March, 4-6, 2015. Proceedings. Lecture Notes in Computer Science, Vol. 8978, Springer, 2015.
  15. R. Haemmerlé, J. Sneyers. Proceedings of the Eleventh Workshop on Constraint Handling Rules (CHR 2014). CoRR abs/1406.1510, 2014.
  16. Nataliia Stulova. Dynamic Checking of Assertions for Higher-order Predicates. Tesis de Licenciatura, Technical University of Madrid, School of Computer Science, E-28660, Boadilla del Monte, Madrid, Spain, 73 páginas, Julio 2013.
  17. Dragan Ivanovic. Analysis of Service-Oriented Computing Systems. Tesis Doctoral, School of Computer Science, UPM, Enero 2013.
  18. R. Haemmerlé, J.F. Morales. Proceedings of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013). CoRR abs/1308.2055, 2013.
  19. Javier Valdazo. Developing Secure Business Applications from Secure BPMN Models. Tesis de Licenciatura, Universidad Complutense de Madrid, Spain, Septiembre 2012.
  20. Gustavo Grieco. Typegrapher: Inferring the Type Graph of a Binary Program. Tesis de Licenciatura, Facultad de Ciencias Exactas, Ingenieria y Agrimensura, Universidad Nacional de Rosario, Rosario, Argentina, Agosto 2012.
  21. 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.
  22. 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.
  23. Gilles Barthe, Alberto Pardo, Gerardo Schneider. Software Engineering and Formal Methods - 9th International Conference, SEFM 2011. Lecture Notes in Computer Science, Vol. 7041, Springer, Noviembre 2011.
  24. Julián Samborski-Forlese. Two Algorithms for Model Checking of Regular Linear Temporal Logic. Tesis de Licenciatura, Dpto. Sistemas Informáticos y Computación, Universidad Complutense de Madrid, Septiembre 2011.
  25. Alejandro Sánchez. Decision Procedures for the Temporal Verification of Concurrent Data Structures. Tesis de Licenciatura, Dpto. Sistemas Informáticos y Computación, Universidad Complutense de Madrid, Julio 2011.
  26. 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), páginas 429--839, Cambridge University Press, Julio 2011.
  27. 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, Julio 2011.
  28. 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, Marzo 2011.
  29. M. Carro, J.H. Reppy. ACM SIGPLAN Proceedings of the Workshop on Declarative Aspects of Multicore Programming. ACM, Enero 2011.
  30. 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.
  31. M. V. Hermenegildo, T. Schaub. Theory and Practice of Logic Programming. 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue. Vol. 10 (4--6), páginas 361--778, Cambridge University Press, Julio 2010.
  32. M. V. 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, Julio 2010.
  33. J.F. Morales. Advanced Compilation Techniques for Logic Programming. Tesis Doctoral, Universidad Politécnica de Madrid (UPM), Facultad Informática UPM, 28660-Boadilla del Monte, Madrid-Spain, Julio 2010.
  34. G. Barthe, M. Hermenegildo. Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010. LNCS, Núm. 5944, Springer, Enero 2010.
  35. M. V. Hermenegildo, J. Palsberg. Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010). ACM, Enero 2010.
  36. M. Carro, R. Peña-Mar&\acute;i. Practical Aspects of Declarative Languages -- 12th. International Symposium, PADL 2010. LNCS, Vol. 5937, Springer-Verlag, Enero 2010.
  37. Rafael Caballero, John P. Gallagher. Proceedings of the 19th Workshop on Logic-based methods in Programming Environments (WLPE 2009). CoRR, abs/1002.4535, 2010.
  38. 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.
  39. Anindya Banerjee. FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs. ACM, 2009.
  40. 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, páginas 70--76, Springer Berlin / Heidelberg, 2009.
  41. 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.
  42. J. Garrigue, M. V. Hermenegildo. Functional and Logic Programming, 9th International Symposium, FLOPS'08. LNCS, Núm. 4989, Springer, Abril 2008.
  43. M. V. Hermenegildo. ACM SIGPLAN-Intel Workshop on Declarative Aspects of Multicore Programming, DAMP'08, Informal Proceedings. Enero 2008.
  44. 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.
  45. 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.
  46. 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.


Artíulos Invitados y Tutoriales

  1. M. V. Hermenegildo, P. Lopez-Garcia, U. Liqat, M. Klemen. Energy Consumption Analysis and Verification by Transformantion into Horn Clauses and Abstract Interpretation. 5th International Workshop on Verification and Program Transformation (VPT 2017), Vol. 253, páginas 4--6, EPTCS, Abril 2017. (Abstract of invited talk).
  2. Gilles Barthe, Francois Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub. EasyCrypt: A Tutorial. Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures, Lecture Notes in Computer Science, Vol. 8604, páginas 146--166, Springer, 2013.
  3. M. V. Hermenegildo. Conferences vs. Journals in CS, what to do? Evolutionary ways forward and the ICLP/TPLP model. Dagstuhl 12452: Publication Culture in Computing Research -- Position Papers, Núm. 12452, 12 páginas, IBFI -- Dagstuhl, Noviembre 2012. (available online).
  4. D. Ivanović, M. Carro, M. V. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. 22nd Workshop on Logic-based Methods in Programming Environments, 1 páginas, Septiembre 2012. (abstract of invited talk).
  5. 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.
  6. 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, Vol. 6826, páginas 2--3, Springer-Verlag, Julio 2011. (abstract of invited talk).
  7. John P. Gallagher, Michael Gelfond. Introduction to the 27th International Conference on Logic Programming (ICLP'11) Special Issue. Vol. 11, Núm. 4-5, páginas 429--432, Cambridge University Press, Julio 2011.
  8. 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, páginas 1--9, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Julio 2011.
  9. M. V. Hermenegildo, T. Schaub. Introduction to the 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue. Vol. 10, Núm. 4--6, páginas 361--364, Cambridge University Press, Julio 2010.
  10. M. V. 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, páginas 8--11, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Julio 2010.
  11. Anindya Banerjee. Semantics and Enforcement of Expressive Information Flow Policies. Formal Aspects in Security and Trust, Lecture Notes in Computer Science, Vol. 5983, páginas 1--3, Springer Berlin / Heidelberg, 2010.
  12. 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, páginas 1--19, Springer, 2009.
  13. 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.
  14. M. V. 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, páginas 1--1, ACM, Enero 2007. (abstract of invited talk).


Artículos en Libros y Otras Colecciones

  1. P. Lopez-Garcia, M. V. Hermenegildo, M. Klemen, U. Liqat. Energy Consumption Analysis and Verification using CiaoPP. The ALP Newsletter, Vol. 30, Núm. 3, The Association for Logic Programming, Septiembre 2017.
  2. Alberto Goffi, Alessandra Gorla, Andrea Mattavelli, Mauro Pezz`e. Intrinsic Redundancy for Reliability and Beyond. Present and Ulterior Software Engineering, páginas 153--171, Springer, 2017.
  3. Salvador Tamarit, Guillermo Vigueras, Manuel Carro, Julio Mariño. Machine Learning-Driven Automatic Program Transformation to Increase Performance in Heterogeneous Architectures. Tools for High Performance Computing 2016, Springer International Publishing, 2017.
  4. U. Liqat, K. Georgiou, S. Kerrison, P. Lopez-Garcia, M. V. Hermenegildo, J. P. Gallagher, K. Eder. Inferring Parametric Energy Consumption Functions at Different Software Levels: ISA vs. LLVM IR. Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers, Lecture Notes in Computer Science, Vol. 9964, páginas 81--100, Springer, 2016.
  5. Konstantin Kuznetsov, Alessandra Gorla, Ilaria Tavecchia, Florian Gross, Andreas Zeller. Mining Android Apps for Anomalies. The Art and Science of Analyzing Software Data, páginas 257--284, Morgan Kaufmann, 2015.
  6. Barthe, Gilles, Dupressoir, Francois, Grégoire, Benjamin, Schmidt, Benedikt, Strub, Pierre-Yves. Computer-Aided Proofs in Cryptography: An Overview. All about Proofs, Proofs for All (APPA), Mathematical Logic and Foundations, Vol. 55, College Publications, jan 2015.
  7. K. Georgiou, U. Liqat. Towards LLVM-Based Energy Consumption Analysis of Programs. ICT-Energy (Nanoenergy) Letters, Núm. 8, páginas 16--17, Julio 2014.
  8. Miguel Ángel García de Dios, Carolina Dania, David A. Basin, Manuel Clavel. Model-Driven Development of a Secure eHealth Application. Engineering Secure Future Internet Services and Systems - Current Research, páginas 97--118, 2014.
  9. Kerstin Eder, Steve Kerrison, John Gallagher, Pedro Lopez-Garcia. Whole Systems Energy Transparency. Núm. 6, páginas 67--68, Agosto 2013.
  10. Anindya Banerjee, David A. Naumann. State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings. Aliasing in Object-Oriented Programming, Lecture Notes in Computer Science, Vol. 7850, páginas 319--365, Springer, 2013.
  11. Barthe, Gilles, Dupressoir, Francois, Grégoire, Benjamin, Kunz, César, Schmidt, Benedikt, Strub, Pierre-Yves. EasyCrypt: A Tutorial. Foundations of Security Analysis and Design VII (FOSAD), Lecture Notes in Computer Science, Vol. 8604, páginas 146--166, Springer International Publishing, 2013.
  12. Dave Clarke, Johan Östlund, Ilya Sergey, Tobias Wrigstad. Ownership Types: A Survey. Aliasing in Object-Oriented Programming. Types, Analysis and Verification, LNCS, Vol. 7850, páginas 15--58, Springer, 2013.
  13. Juan Caballero, Adam Barth, Dawn Song. Content-Sniffing XSS Attacks: XSS with non-HTML Content. The Death of the Internet, Wiley, Julio 2012.
  14. T. Trigo, P. López-García, S. Muñoz-Hernandez. A Fuzzy Approach to Resource Aware Automatic Parallelization. Computational Intelligence, Studies in Computational Intelligence (SCI), Vol. 399, páginas 229--245, Springer Berlin Heidelberg, 2012.
  15. P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo. Interval-Based Resource Usage Verification: Formalization and Prototype. Foundational and Practical Aspects of Resource Analysis. Second International Workshop FOPARA 2011, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 7177, páginas 54--71, Springer-Verlag, 2012.
  16. V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee. Merlin: specification inference for explicit information flow problems. Mining Software Specifications, páginas 377--410, Chapman & Hall/CRC, Mayo 2011.
  17. M. Carro, M. V. Hermenegildo. Logic Languages. Encyclopedia of Parallel Computing, páginas 1057--1068, Springer, 2011.
  18. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. Logical Abstract Domains and Interpretations. The Future of Software Engineering, páginas 48--71, Springer-Verlag, 2011.
  19. 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, páginas 277--298, Springer, 2011.
  20. 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, Vol. 5065, páginas 209--237, Springer-Verlag, Junio 2008.
  21. 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, páginas 51--95, Springer, 2008.
  22. 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, páginas 100--152, Springer, 2008.
  23. 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, páginas 586--609, Springer-Verlag, 2008.
  24. Ángel Herranz, Juan José Moreno-Navarro. Modeling and Reasoning about Design Patterns in SLAM-SL. Design Pattern Formalization Techniques, IGI Publishing, Marzo 2007.


Publicaciones en Workshops con Revisión

  1. U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo. Inferring Energy Bounds via Static Program Analysis and Evolutionary Modeling of Basic Blocks. Pre-proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'17), Octubre 2017.
  2. Salvador Tamarit, Julio Mariño, Guillermo Vigueras, Manuel Carro. Towards a Semantics-Aware Code Transformation Toolchain for Heterogeneous Systems. Proceedings of XIV Jornadas sobre Programación y Lenguajes (PROLE 2016), EPTCS, Septiembre 2017.
  3. Guillermo Vigueras, Manuel Carro, Salvador Tamarit, Julio Mariño. Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural Code. Proceedings of XIV Jornadas sobre Programación y Lenguajes (PROLE 2016), EPTCS, Septiembre 2017.
  4. N. Stulova. On Improving Run-time Checking in Dynamic Languages. Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017), Vol. 58, 10 páginas, OASIcs, Agosto 2017. CP/ICLP/SAT Doctoral Program 2017 (CP-ICLP-SAT-DP-17) entry (To appear).
  5. N. Stulova, J. F. Morales, M. V. Hermenegildo. Towards Run-time Checks Simplification via Term Hiding (Extended Abstract). Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017), Vol. 58, 3 páginas, OASIcs, Agosto 2017. (To appear).
  6. Simon Oya, Carmela Troncoso, Fernando Pérez-González. Is Geo-Indistinguishability What You Are Looking for?. Proc. of the 16th Workshop on Privacy in the Electronic Society (WPES 2017), páginas 137--140, ACM, 2017.
  7. J. Arias. Tabled CLP for Reasoning over Stream Data. 12th ICLP Doctoral Consortium (DC-ICLP'16), 8 páginas, OASIcs, Octubre 2016.
  8. Jan Kuper, Lutz Schubert, Kilian Kempf, Colin Glas, Daniel Rubio Bonilla, Manuel Carro. Program Transformations in the POLCA Project. Design, Automation, and Testing in Europe, EDAA, Marzo 2016.
  9. Guillermo Vigueras, Manuel Carro, Salvador Tamarit, Julio Mariño. Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural Code. Proceedings of the First International Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016), Marzo 2016.
  10. Salvador Tamarit, Julio Mariño, Guillermo Vigueras, Manuel Carro. Towards a Semantics-Aware Transformation Toolchain for Heterogeneous Systems. Proceedings of the First International Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016), Marzo 2016.
  11. Konstantin Kuznetsov, Vitalii Avdiienko, Alessandra Gorla, Andreas Zeller. Checking App User Interfaces Against App Descriptions. Proceedings of the 1st International Workshop on App Market Analytics, WAMA 2016, páginas 1--7, ACM, 11 2016.
  12. Vitalii Avdiienko, Konstantin Kuznetsov, Paolo Calciati, Juan Carlos Caiza Román, Alessandra Gorla, Andreas Zeller. CALAPPA: a Toolchain for Mining Android Applications. Proceedings of the 1st International Workshop on App Market Analytics, WAMA 2016, páginas 22--25, ACM, 11 2016.
  13. Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira, Marc Shapiro. The CISE tool: proving weakly-consistent applications correct. PAPOC'16: Workshop on the Principles and Practice of Consistency for Distributed Data, páginas 1--3, ACM Press, 2016.
  14. J. Hayes, C. Troncoso, G. Danezis . TASP: Towards Anonymity Sets that Persist. 15th Workshop on Privacy in the Electronic Society, WPES, ACM, 2016.
  15. U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo. Inferring Energy Bounds Statically by Evolutionary Analysis of Basic Blocks. Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES 2016), 2016. arXiv:1601.02800.
  16. Bishoksan Kafle, John P. Gallagher. Interpolant tree automata and their application in Horn clause verification. Proceedings of the Fourth International Workshop on Verification and Program Transformation, VPT 2016, Eindhoven, The Netherlands, 2nd April 2016., EPTCS, Vol. 216, páginas 104--117, 2016.
  17. Bishoksan Kafle, John P. Gallagher, Pierre Ganty. Solving non-linear Horn clauses using a linear Horn clause solver. Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS 2016, satellite event of ETAPS, Eindhoven, The Netherlands, 3rd April 2016, EPTCS, Vol. 219, páginas 33--48, 2016.
  18. R. Haemmerle, M. V. Hermenegildo, M. Klemen, U. Liqat, P. Lopez-Garcia. Energy Analysis and Verification by Translation to Horn Clauses and Abstract Interpretation. Workshop on Horn Clauses for Verification and Synthesis (HCVS'2015), Julio 2015.
  19. S. Gurses, C. Troncoso, C. Diaz. Engineering Privacy by Design Reloaded. Amsterdam Privacy Conference 2015, 21 páginas, 2015.
  20. Joaquín Arias, Manuel Carro. Towards a Generic Interface to Integrate CLP and Tabled Execution (Extended Abstract). Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, August 31 - September 4, 2015., CEUR Workshop Proceedings, Vol. 1433, CEUR-WS.org, 2015. Extended Abstract.
  21. P. Lopez-Garcia, R. Haemmerlé, M. Klemen, U. Liqat, M. V. Hermenegildo. Towards Energy Consumption Verification via Static Analysis. Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES), arXiv:1501.03064, 11 páginas, 2015. arXiv:1512.09369.
  22. Kafle, Bishoksan, Gallagher, John P., Ganty, Pierre. Decomposition by tree dimension in Horn clause verification. VPT '15: 3rd Int. Workshop on Verification and Program Transformation, EPTCS, Vol. 199, páginas 1--14, 2015. arXiv:1512.03862.
  23. J.F. Morales, M. V. Hermenegildo. Pre-Indexed Terms for Prolog. Pre-proceedings of the 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'14), 15 páginas, Septiembre 2014.
  24. J.F. Morales, M. V. Hermenegildo. Towards Pre-Indexed Terms. 14th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS-WLPE 2014), 14 páginas, RWTH Aachen University, Julio 2014. http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2014.
  25. N. Stulova, J. F. Morales, M. V. Hermenegildo. Towards Assertion-based Debugging of Higher-Order (C)LP Programs (Extended Abstract). Theory and Practice of Logic Programming, 30th Int'l. Conference on Logic Programming (ICLP'14) Special Issue, On-line Supplement, Vol. 14, Núm. 4-5, páginas 209--210, Cambridge U. Press, Julio 2014.
  26. Bishoksan Kafle, John P. Gallagher. Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification. Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014, Vol. 169, páginas 53--67, EPTCS, 2014.
  27. U. Liqat, S. Kerrison, A. Serrano, K. Georgiou, P. Lopez-Garcia, N. Grech, M. V. Hermenegildo, K. Eder. Energy Consumption Analysis of Programs based on XMOS ISA-Level Models. Pre-proceedings of the 23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'13), Septiembre 2013.
  28. A. Serrano, P. Lopez-Garcia, M. V. Hermenegildo. Towards an Abstract Domain for Resource Analysis of Logic Programs Using Sized Types. 23rd Workshop on Logic-based Methods in Programming Environments (WLPE 2013), 15 páginas, Agosto 2013. CoRR abs/1308.3940.
  29. Dragan Ivanović. Implementing Constraint Handling Rules as a Domain-Specific Language Embedded in Java. Proceedings of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013), Agosto 2013.
  30. Dragan Ivanović. Implementing Constraint Handling Rules as a Domain-Specific Language Embedded in Java. Proceedings of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013), Agosto 2013.
  31. D. Ivanovic, P. Kaowichakorn, M. Carro. Towards QoS Prediction Based on Composition Structure Analysis and Probabilistic Environment Models. 5th International Workshop on Principles of Engineering Service-Oriented Systems, Mayo 2013.
  32. Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey. Derivación de intérpretes del cálculo lambda con tipos graduales. V Taller de Programación Funcional TPF 2013, September 17 2013. Charla impartida en el V Taller de Programación Funcional TPF 2013.
  33. Javier Reyes, Juan M. Orduña, Guillermo Vigueras, Rafael Tornero. Acceleration of Communication-Aware Task Mapping Techniques through GPU Computing. AINA Workshops, páginas 843--848, 2013.
  34. Julián Samborski-Forlese, César Sánchez. Bounded Model Checking for Regular Linear Temporal Logic (extended abstract). Proceedings of the 24th Nordic Workshop on Programming Theory (NWPT'12), Octubre 2012. Available at (available online).
  35. R. Haemmerlé. Coinductive Proofs over Streams as CHR Confluence Proofs. 9th Int'l Workshop on Constraint Handling Rules (CHR 2012), Septiembre 2012.
  36. 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 páginas, Septiembre 2012.
  37. 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 páginas, Septiembre 2012.
  38. D. Ivanovic, M. Carro, M. V. Hermenegildo. Analyzing Service-Oriented Systems Using Their Data and Structure. European Software Services and Systems Research -- Results and Challenges (ICSE Workshop), Julio 2012.
  39. D. Karastoyanova, Z. Nemeth, M. Carro, D. Ivanovic, C. Pautasso, C. Di Napoli, and M. Giordano. Research Challenges on Service Technology Foundations. European Software Services and Systems Research -- Results and Challenges (ICSE Workshop), Julio 2012.
  40. D. Ivanović, M. Carro, M. V. 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, páginas 931--937, IEEE Press, Junio 2012.
  41. Álvaro García-Pérez, Pablo Nogueira. Enfoque normal y enfoque spine para reducción en el cálculo lambda puro. IV Taller de Programación Funcional TPF 2012, September 17 2012. Charla impartida en el IV Taller de Programación Funcional TPF 2012.
  42. D. Ivanović, M. Carro, M. V. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. XII Jornadas sobre Programación y Lenguajes (PROLE), Universidad de Almería, 2012.
  43. 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.
  44. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, P. Stuckey. A General Implementation Framework for Tabled CLP. XII Jornadas sobre Programaciń y Lenguajes (PROLE), Universidad de Almería, 2012.
  45. Carolina Dania. Modeling Social Networking Privacy. ESSoS-DS 2012. Doctoral Symposium, Workshop Proceedings, Vol. 834, páginas 49--54, CEUR, 2012.
  46. 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, páginas 17--31, Springer, 2012.
  47. 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 páginas, Septiembre 2011.
  48. P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo. Interval-based Resource Usage Verification: Formalization and Prototype. 2nd International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'2011), Mayo 2011.
  49. Álvaro García-Pérez, Pablo Nogueira. Estrategias del cálculo lambda e interderivación de artefactos semánticos. III Taller de Programación Funcional TPF 2011, September 5 2011. Charla impartida en el III Taller de Programación Funcional TPF 2011.
  50. 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 páginas, ACM, 2011.
  51. 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. Proc. Int'l. WS on Scripts to Programs, STOP'11, 4 páginas, ACM, 2011.
  52. D. Ivanović, M. Carro, M. V. 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, Núm. 6275, Springer, Septiembre 2010.
  53. Álvaro García-Pérez. El Cubo Beta. II Taller de Programación Funcional TPF 2010, September 7 2010. Charla impartida en el II Taller de Programación Funcional TPF 2010.
  54. Álvaro García-Pérez, 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), páginas 3--7, July 9 2010.
  55. R. Haemmerlé. (Co)inductive Semantics for Constraint Handling Rules. Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming, 2010.
  56. D. Ivanović, M. Carro, M. V. 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+), Noviembre 2009.
  57. 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), Septiembre 2009.
  58. D. Ivanović, J.F. Morales, M. Carro, M. V. Hermenegildo. Towards Structured State Threading in Prolog. CICLOPS 2009, 15 páginas, Julio 2009.
  59. J. Navas, M. Méndez-Lojo, M. V. 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, Núm. 5, páginas 65--82, Elsevier - North Holland, Marzo 2009.
  60. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. A Program Transformation for Continuation Call-Based Tabled Execution. Colloquium on Implementation of Constraint and LOgic Programming Systems (ICLP associated workshop), 15 páginas, University of Udine, Diciembre 2008.
  61. 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, páginas 245--249, Octubre 2008.
  62. 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), páginas 61--73, ACM Press, Septiembre 2008.
  63. M. Méndez-Lojo, O. Lhoták, M. V. Hermenegildo. Efficient Set Sharing using ZBDDs. 21st Int'l. WS on Languages and Compilers for Parallel Computing (LCPC'08), LNCS, Vol. 5335, páginas 94--108, Springer-Verlag, Agosto 2008.
  64. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo. Two Efficient Representations for Set-Sharing Analysis in Logic Programs . 17th International Workshop on Functional and (Constraint) Logic Programming, WFLP'08, 15 páginas, Julio 2008.
  65. R. Haemmerlé, H. Betz. Verification of Constraint Handling Rules using Liner Logic Phase Semantics. 5th Int'l Workshop on Constraint Handling Rules (CHR 2011), Report Series 08-10, RICS-Linz, Julio 2008.
  66. 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), páginas 29--32, Abril 2008. Extended Abstract.
  67. Gilles Barthe, César Kunz. Certificate Translation for Specification-Preserving Advices. Proceedings of the 7th Workshop on Foundations of Aspect-Oriented Languages, FOAL 2008, páginas 9--18, ACM, 2008.
  68. 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, Septiembre 2007.
  69. P. Chico de Guzmán, M. Carro, M. V. 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 páginas, Universidade do Porto, Septiembre 2007.
  70. A. Casas, M. Carro, M. V. 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 páginas, U. of Evora, Septiembre 2007.
  71. J. Navas, M. Méndez-Lojo, M. V. Hermenegildo. An Efficient, Context and Path Sensitive Analysis Framework for Java Programs. 9th Workshop on Formal Techniques for Java-like Programs FTfJP 2007, 12 páginas, Julio 2007.
  72. A. Casas, M. Carro, M. V. Hermenegildo. Towards A High-Level Implementation of Flexible Parallelism Primitives for Symbolic Languages. Parallel Symbolic Computation (PASCO'07), 2 páginas, ACM Press, Julio 2007. Extended Abstract.
  73. 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, Julio 2007.
  74. M. Méndez-Lojo, J. Navas, M. V. 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, Marzo 2007.


Informes Técnicos y Manuales

  1. N. Stulova, J. F. Morales, M. V. Hermenegildo. Term Hiding and its Impact on Run-time Check Simplification. Núm. CLIP-1/2017.0, 27 páginas, The CLIP Lab, Mayo 2017. CoRR abs/1705.06662 (v2) [cs.PL].
  2. Miguel Ambrona, Gilles Barthe, Benedikt Schmidt. Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. 30 páginas, IACR Cryptology ePrint Archive, 2016.
  3. Miguel Ambrona, Gilles Barthe, Benedikt Schmidt. Generic Transformations of Predicate Encodings: Constructions and Applications. 30 páginas, IACR Cryptology ePrint Archive, 2016.
  4. P. Lopez-Garcia, R. Haemmerlé, U. Liqat, M. Klemen, M. V. Hermenegildo. Parametric Static Profiling. Núm. CLIP-2/2015.0, The CLIP Lab, Abril 2015.
  5. Guillermo Vigueras, Salvador Tamarit, Manuel Carro, Julio Mariño. Towards a Rule-Based Approach to Generate High-Performance Scientific Code. Núm. CLIP1/2015.0, 8 páginas, The CLIP Lab, Marzo 2015. http://cliplab.org/papers/vigueras15-rule-based.pdf.
  6. Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub. Computer-aided Verification in Mechanism Design. 2015. CoRR abs/1502.04052 [cs.GT].
  7. R. Haemmerlé. On the Confluence of the Analytical Semantics of CHR. Núm. CLIP2/2014.0, 12 páginas, Technical University of Madrid (UPM), Julio 2014.
  8. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, Francois Dupressoir, Benjamin Grégoire, Pierre-Yves Strub. Verified Implementations for Secure and Verifiable Computation. Junio 2014. IACR Cryptology ePrint Archive, Report 2014/456.
  9. N. Stulova, J. F. Morales, M. V. Hermenegildo. An Approach to Assertion-based Debugging of Higher-Order (C)LP Programs. Núm. CLIP-1/2014.0, 25 páginas, The CLIP Lab, Enero 2014. CoRR abs/1404.4246 [cs.PL].
  10. Pierre Ganty, Radu Iosif. Generating Bounded Languages Using Bounded Control Sets. 2014.
  11. Juan Caballero, Gustavo Grieco, Mark Marron, Zhiqiang Lin, David Urbina. ARTISTE: Automatic Generation of Hybrid Data Structure Signatures from Binary Code Executions. Núm. TR-IMDEA-SW-2012-001, IMDEA Software Institute, Agosto 2012.
  12. 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).
  13. 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).
  14. 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).
  15. Marianne Busch, Miguel Ángel García de Dios. ActionUWE: Transformation of UWE to ActionGUI Models. Ludwig-Maximilians-Universität München, 2012.
  16. F. Bueno, M. Carro, M. V. Hermenegildo, R. Haemmerlé, P. López-García, E. Mera, and J.F. Morales, G. Puebla-(Eds.). The Ciao System. Ref. Manual (V1.14). Julio 2011. Available at http://ciao-lang.org.
  17. M. V. Hermenegildo, J.F. Morales. The LPdoc Documentation Generator. Ref. Manual (V3.0). Julio 2011. Available at http://ciao-lang.org.
  18. R. Haemmerlé. Toward Observational Equivalences for Linear Logic Concurrent Constraint Languages. Núm. CLIP5/2011.0, 32 páginas, Technical University of Madrid (UPM), Mayo 2011.
  19. P. López-García, L. Darmawan, F. Bueno, M. V. Hermenegildo. Towards Resource Usage Function Verification based on Input Data Size Intervals. Núm. CLIP4/2011.0, Technical University of Madrid (UPM), Abril 2011. Available at http://cliplab.org/papers/resource-verif-11-tr.pdf.
  20. R. Haemmerlé. Towards a Logically Complete Fixpoint Semantics for Constraint Handling Rules. Núm. CLIP3/2011.0, 31 páginas, Technical University of Madrid (UPM), Marzo 2011.
  21. P. Chico de Guzmán, A. Casas, M. Carro, M. V. Hermenegildo. A Simulation Study on Parallel Backtracking with Solution Memoing for Independent And-Parallelism. Núm. CLIP1/2011.0, 12 páginas, Technical University of Madrid (UPM), Enero 2011.
  22. J.F. Morales, M. V. Hermenegildo, R. Haemmerlé. Towards Modular Extensions for a Modular Language. Núm. CLIP2/2011.0, 15 páginas, Technical University of Madrid (UPM), Enero 2011.
  23. Alexander Malkis. On the strength of Owicki-Gries for resources. 2011. Technical report, (available online).
  24. D. Ivanović, M. Carro, M. V. Hermenegildo. Automated Attribute Inference in Complex Service Workflows Based on Sharing Analysis. Núm. CLIP5/2010.0, Technical University of Madrid (UPM), Diciembre 2010.
  25. D. Ivanović, M. Carro, M. V. Hermenegildo. Automatic Fragment Identification in Workflows Based on Sharing Analysis. Núm. CLIP4/2010.0, 15 páginas, Technical University of Madrid (UPM), Junio 2010. Submitted.
  26. E. Mera, T. Trigo, P. López-García, M. V. Hermenegildo. An Approach to Profiling for Run-Time Checking of Computational Properties and Performance Debugging. Núm. CLIP3/2010.0, 29 páginas, Technical University of Madrid (UPM), Marzo 2010.
  27. 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. Núm. CLIP2/2010.0, Technical University of Madrid (UPM), Marzo 2010. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).
  28. D. Ivanović, M. Carro, M. V. Hermenegildo, P. López, E. Mera. Towards Data-Aware Cost-Driven Adaptation for Service Orchestrations. Núm. CLIP5/2009.1, Technical University of Madrid (UPM), Marzo 2010.
  29. P. López-García, L. Darmawan, F. Bueno, M. V. Hermenegildo. Towards a Framework for Resource Usage Verification and Debugging in the CiaoPP System. Núm. CLIP1/2010.0, Technical University of Madrid (UPM), Febrero 2010. Available at http://cliplab.org/papers/resource-verif-10-tr.pdf.
  30. Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger. Parikh's Theorem: A simple and direct construction. 2010.
  31. Pierre Ganty, Rupak Majumdar. Algorithmic Verification of Asynchronous Programs. 2010.
  32. D. Ivanović, M. Carro, M. V. Hermenegildo. Sharing-Based Independence-Driven Fragment Identification for Service Orchestrations. Núm. CLIP7/2009.0, Technical University of Madrid (UPM), Diciembre 2009.
  33. D. Ivanović, M. Carro, M. V. Hermenegildo, P. López, E. Mera. Towards Data-Aware Cost-Driven Adaptation for Service Orchestrations. Núm. CLIP5/2009.0, Technical University of Madrid (UPM), Noviembre 2009. Replaced by a later version.
  34. J.F. Morales, M. Carro, M. V. Hermenegildo. Description and Optimization of Abstract Machines in a Dialect of Prolog. Núm. CLIP4/2009.0, Technical University of Madrid (UPM), Octubre 2009.
  35. D. Ivanović, M. Carro, M. V. Hermenegildo. Towards Data-Aware Resource Analysis for Service Orchestrations. Núm. CLIP3/2009.0, Technical University of Madrid (UPM), Junio 2009.
  36. E. Mera, P. López-García, M. V. Hermenegildo. Towards Integrating Run-Time Checking and Software Testing in a Verification Framework. Núm. CLIP1/2009.0, 19 páginas, Technical University of Madrid (UPM), Marzo 2009.
  37. P. López-García, F. Bueno, M. V. Hermenegildo. Inferring Determinacy and Mutual Exclusion in Logic Programs Using Mode and Type Analysis. Núm. CLIP2/2009.0, Technical University of Madrid (UPM), Febrero 2009.
  38. F. Bueno, D. Cabeza, M. Carro, M. V. Hermenegildo, P. López-García, G. Puebla-(Eds.). The Ciao System. Ref. Manual (V1.13). 2009. Available at http://ciao-lang.org.
  39. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Bounded Underapproximations. 2009.
  40. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo. Efficient Representations for Set-Sharing Analysis. Núm. CLIP9/2008.0, University of New Mexico and Technical University of Madrid, Septiembre 2008.
  41. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. Bridge Program Transformation for the CCall Tabling Scheme. Núm. CLIP6/2008.0, Technical University of Madrid (UPM), Septiembre 2008.
  42. A. Casas, M. Carro, M. V. Hermenegildo. A High-Level Implementation of Non-Deterministic, Unrestricted, Independent And-Parallelism. Núm. TR-CS-2008-10, University of New Mexico (UNM), Septiembre 2008.
  43. J. Navas, E. Mera, P. López-García, M. Hermenegildo. Inference of User-Definable Resource Bounds Usage for Logic Programs and its Applications. Núm. CLIP5/2008.0, Technical University of Madrid (UPM), Julio 2008.
  44. M. Méndez-Lojo, O. Lhoták, M. V. Hermenegildo. Fast Set Sharing using ZBDDs. University of New Mexico, Junio 2008.
  45. 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. Núm. CLIP3/2008.0, Technical University of Madrid (UPM), Abril 2008.
  46. J. Navas, M. Méndez-Lojo, M. V. Hermenegildo. Customizable Resource Usage Analysis for Java Bytecode. Núm. UNM TR-CS-2008-02 - CLIP1/2008.0, University of New Mexico, Enero 2008.
  47. A. Casas, M. Carro, M. V. Hermenegildo. Automatic Unrestricted Independent And-Parallelism in Logic Programs. Núm. CLIP11/2007.0, Technical University of Madrid (UPM), Diciembre 2007. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).
  48. M. Méndez-Lojo, M. Hermenegildo. Precise Set Sharing for Java-style Programs (and proofs). Núm. CLIP2/2007.1, Technical University of Madrid (UPM), Noviembre 2007.
  49. A. Casas, M. Carro, M. V. Hermenegildo. Towards a High-Level Implementation of Execution Primitives for Non-restricted, Independent And-parallelism. Núm. TR-CS-2007-16, University of New Mexico (UNM), Octubre 2007.
  50. A. Casas, M. Carro, M. V. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. Núm. TR-CS-2007-14, University of New Mexico (UNM), Septiembre 2007.
  51. E. Mera, P. López-García, M. Carro, M. V. Hermenegildo. Towards Execution Time Estimation in Abstract Machine-Based (Logic) Languages. Núm. CLIP8/2007.0, Technical University of Madrid (UPM), Agosto 2007.
  52. G. Marpons, J. Mariño, M. Carro, A. Herranz, J.J. Moreno-Navarro, L.Å. Fredlund. Automatic Coding Rule Conformance Checking Using Logic Programming. Núm. CLIP6/2007.0, Technical University of Madrid (UPM), Agosto 2007.
  53. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. An Improved Continuation Call-Based Implementation of Tabling. Núm. CLIP9/2007.0, Technical University of Madrid (UPM), Agosto 2007.
  54. A. Casas, M. Carro, M. V. Hermenegildo. Towards a High-Level Implementation of Execution Primitives for Non-Restricted, Independent And-Parallelism. Núm. CLIP7/2007.0, Technical University of Madrid (UPM), Agosto 2007.
  55. A. Casas, M. Carro, M. V. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. Núm. CLIP5/2007.0, Technical University of Madrid (UPM), Junio 2007.
  56. 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. Núm. CLIP4/2007.0, Technical University of Madrid (UPM), Marzo 2007.
  57. M. Méndez-Lojo, M. Hermenegildo. Precise Set Sharing and Nullity Analysis for Java-style Programs. Núm. CLIP2/2007.0, Technical University of Madrid (UPM), Febrero 2007.
  58. P. López-García, F. Bueno, M. V. Hermenegildo. Inferring Determinacy in Logic Programs Using Mode and Type Information. Núm. CLIP3/2007.0, Technical University of Madrid (UPM), Febrero 2007.