IMDEA initiative

Home > Research > Publications

IMDEA Software Institute's Publications



Articles in Refereed Journals

  1. S. Oya, F. Pérez-González, C. Troncoso. Design of Pool Mixes Against Profiling Attacks in Real Conditions. IEEE/ACM Transactions on Networking, Vol. 24, Num. 6, pages 1--14, November 2016.
  2. 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, pages 278--286, Elsevier, November 2016.
  3. 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. IET Information Security, Vol. 10, Num. 6, pages 358--371, Institution of Engineering and Technology, November 2016.
  4. 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, Num. 5-6, pages 721--737, Cambridge U. Press, October 2016.
  5. 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, Num. 5-6, pages 849--865, Cambridge U. Press, October 2016.
  6. Manuel Carro, Andy King. Introduction to the 32nd International Conference on Logic Programming Special Issue. Theory and Practice of Logic Programming, Vol. 16, Num. 5-6, pages 509--514, Cambridge University Press, September 2016.
  7. 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, Num. 5, pages 457--472, Sage Publications, July 2016.
  8. Juan Caballero, Zhiqiang Lin. Type Inference on Executables. ACM Computing Surveys, Vol. 48, Num. 4, pages 1--35, ACM, May 2016.
  9. Roberto Giacobazzi, Isabella Mastroeni. Making abstract models complete. Mathematical Structures in Computer Science, Vol. 26, Num. 4, pages 658--701, Cambridge University Press, May 2016.
  10. Javier Esparza, Pierre Ganty, Rupak Majumdar. Parameterized Verification of Asynchronous Shared-Memory Systems. J. ACM, Vol. 63, Num. 1, pages 1--48, ACM, March 2016.
  11. 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, Num. 1, pages 1--2, ACM, January 2016.
  12. J.F. Morales, M. Carro, M. Hermenegildo. Description and Optimization of Abstract Machines in a Dialect of Prolog. Theory and Practice of Logic Programming, Vol. 16, pages 1--58, Cambridge University Press, January 2016.
  13. Gilles Barthe, Juan Manuel Crespo, César Kunz. Product programs and relational program logics. J. Log. Algebr. Meth. Program., Vol. 85, Num. 5, pages 847--859, 2016.
  14. Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce. Programming language techniques for differential privacy. SIGLOG News, Vol. 3, Num. 1, pages 34--53, 2016.
  15. 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, pages 88--110, 2016.
  16. Alejandro Sánchez, César Sánchez. Parametrized Verification Diagrams: Temporal Verification of Symmetric Parametrized Concurrent Systems. Annals of Mathematics and Artificial Intelligence, To Appear, 2016.
  17. 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, To Appear, Old City Publishing, 2016.
  18. Giovanni Bernardi, Matthew Hennessy. Using higher-order contracts to model session types. Logical Methods in Computer Science, Vol. 12, Num. 2, 2016.
  19. Guillermo Vigueras, Juan M. Orduña. On the Use of GPU for Accelerating Communication-Aware Mapping Techniques. The Computer Journal, Vol. 59, Num. 6, pages 836--847, 2016.
  20. Á. García-Pérez, P. Nogueira. No solvable lambda-value term left behind. Logical Methods in Computer Science, Vol. 12, Num. 2, pages 1--43, 2016.
  21. 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, To Appear, Springer Berlin Heidelberg, 2016.
  22. Isabella Mastroeni, Roberto Giacobazzi. Weakening Additivity in Adjoining Closures. Order, Vol. 33, Num. 3, pages 503--516, 2016.
  23. Roberto Giacobazzi, Isabella Mastroeni, Mila Dalla Preda. Maximal incompleteness as obfuscation potency. Formal Aspects of Computing, To Appear, 2016.
  24. Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Journal of Automated Reasoning, Vol. 56, Num. 3, pages 283--308, 2016.
  25. Bishoksan Kafle, John P. Gallagher. Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. Computer Languages, Systems & Structures, To Appear, Pergamon, November 2015.
  26. 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, Num. 04-05, pages 726--741, Cambridge U. Press, September 2015.
  27. 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, Num. 1, pages 1--32, ACM, June 2015.
  28. Vigueras, Guillermo, Orduña, Juan M.. On the Use of GPU for Accelerating Communication-Aware Mapping Techniques. The Computer Journal, To Appear, May 2015.
  29. Giovanni Bernardi, Matthew Hennessy. Mutually Testing Processes. Logical Methods in Computer Science, Vol. 11, Num. 2, April 2015.
  30. Zorana Banković, Pedro Lopez-Garcia. Stochastic vs. Deterministic Evolutionary Algorithm-based Allocation and Scheduling for XMOS Chips. Neurocomputing, Vol. 150, pages 82--89, Elsevier, February 2015.
  31. 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, Num. 2, pages 276--290, February 2015.
  32. 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, Num. 1, pages 15--33, Springer Berlin Heidelberg, February 2015.
  33. 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.
  34. 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, Num. 3, pages 1--42, 2015.
  35. Andrea Cerone, Matthew Hennessy, Massimo Merro. Modelling MAC-Layer Communications in Wireless Systems. Logical Methods in Computer Science, Vol. 11, Num. 1, 2015.
  36. Gilles Barthe. High-Assurance Cryptography: Cryptographic Software We can Trust. IEEE Security & Privacy, Vol. 13, Num. 5, pages 86--89, 2015.
  37. Gilles Barthe, Alberto Pardo, Gerardo Schneider. SEFM: Software Engineering and Formal Methods. Software and System Modeling, Vol. 14, Num. 1, pages 3--4, 2015.
  38. Backes, Michael, Köpf, Boris. Quantifying information flow in cryptographic systems. Mathematical Structures in Computer Science, Vol. 25, Num. 2, pages 457--479, 2 2015.
  39. Alejandro Sánchez, César Sánchez. Parametrized Invariance for Infinite State Processes. Acta Informatica, Vol. 52, Num. 6, pages 525--557, 2015.
  40. Dario Catalano, Dario Fiore, Rosario Gennaro, Konstantinos Vamvourellis. Algebraic (trapdoor) one-way functions: Constructions and applications. Theoretical Computer Science, Vol. 592, pages 143--165, Springer, 2015.
  41. 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, Num. 0, pages 542--557, 2015.
  42. Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan. Stability Preserving Simulations and Bisimulations for Hybrid Systems. IEEE Trans. Automat. Contr., Vol. 60, Num. 12, pages 3210--3225, 2015.
  43. Pavithra Prabhakar, Miriam Garcia Soto. AVERIST: An Algorithmic Verifier for Stability. Electr. Notes Theor. Comput. Sci., Vol. 317, pages 133--139, 2015.
  44. Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan. Hybrid automata-based CEGAR for rectangular hybrid systems. Formal Methods in System Design, Vol. 46, Num. 2, pages 105--134, 2015.
  45. Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, Geir E. Dullerud. A decidable class of planar linear hybrid systems. Theoretical Computer Science, Vol. 574, pages 1--17, 2015.
  46. Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray. Unveiling metamorphism by abstract interpretation of code properties. Theor. Comput. Sci., Vol. 577, pages 74--97, 2015.
  47. Gilles Barthe, Delphine Demange, David Pichardie. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst., Vol. 36, Num. 1, pages 1--35, ACM, March 2014.
  48. Á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, pages 176--199, Elsevier, 2014.
  49. Alexander Malkis, Anindya Banerjee. On Automation in the Verification of Software Barriers: Experience Report. J. Autom. Reasoning, Vol. 52, Num. 3, pages 275--329, 2014.
  50. Laura Bozzelli, César Sánchez. Visibly Rational Expressions. Acta Informatica, Vol. 51, Num. 1, pages 25--49, 2014.
  51. 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, Num. 4-5, pages 619--632, Cambridge U. Press, 2014.
  52. A. Serrano, P. Lopez-Garcia, M. 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, Num. 4-5, pages 739--754, Cambridge U. Press, 2014.
  53. Michel Abdalla, Dario Catalano, Dario Fiore. Verifiable Random Functions: Relations to Identity-Based Key-Encapsulation and New Constructions. Journal of Cryptology, Vol. 27, Num. 3, pages 544--593, Springer, 2014.
  54. 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, Num. 5, pages 823--866, IOS Press, 2014. Also appears as tech. rep. MSR-TR-2011-50.
  55. 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, Num. 1, pages 117--134, 2014.
  56. 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, Num. 1, 2014.
  57. J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn. Pushdown flow analysis with abstract garbage collection. J. Funct. Program., Vol. 24, Num. 2-3, pages 218--283, 2014.
  58. John P. Gallagher, Bishoksan Kafle. Analysis and Transformation Tools for Constrained Horn Clause Verification. Theory and Practice of Logic Programming, Vol. 14, Num. 4-5 (supplementary materials), pages 90--101, Cambridge University Press, 2014.
  59. Juan Caballero, Simson Garfinkel. Fourteenth Annual DFRWS Conference. Digital Investigation, Vol. 11, Supplement 2, Num. 0, pages 1--2, 2014. The Proceedings of the 14th Annual Digital Forensics Research Conference.
  60. Ahmed Bouajjani, Michael Emmi. Bounded phase analysis of message-passing programs. STTT, Vol. 16, Num. 2, pages 127--146, 2014.
  61. 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, Num. 4, pages 324--337, 2014.
  62. Javier Esparza, Pierre Ganty, Tomás Poch. Pattern-based Verification for Multithreaded Programs. ACM Transactions on Programming Languages and Systems, Vol. 36, Num. 3, pages 1--29, 2014.
  63. Alexey Gotsman, Hongseok Yang. Linearizability with ownership transfer. Logical Methods in Computer Science, Vol. 9, Num. 3, September 2013.
  64. 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, Num. 4, pages 357--401, July 2013.
  65. 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, Num. 2(6), pages 1--6, July 2013.
  66. Alexey Gotsman, Hongseok Yang. Modular verification of preemptive OS kernels. Journal of Functional Programming, Vol. 23, Num. 4, pages 452--514, Cambridge University Press, July 2013.
  67. D. Ivanovic, M. Carro, M. V. Hermenegildo. A Sharing-Based Approach to Supporting Adaptation in Service Compositions. Computing, Vol. 95, Num. 6, pages 453--492, Springer Wien, June 2013. 10.1007/s00607-012-0230-z.
  68. Vigueras, Guillermo, Orduña, Juan M., Lozano, Miguel, Jégou, Yvon. A Scalable Multiagent System Architecture for Interactive Applications. Sci. Comput. Program., Vol. 78, Num. 6, pages 715--724, Elsevier North-Holland, Inc., June 2013.
  69. Murdoch J. Gabbay, Aleksandar Nanevski. Denotation of syntax and metaprogramming in contextual modal type theory (CMTT). Journal of Applied Logic (JAPPL), Vol. 11, Num. 1, pages 1--29, March 2013.
  70. Juan Caballero, Dawn Song. Automatic Protocol Reverse-Engineering: Message Format Extraction and Field Semantics. Computer Networks, Vol. 57, Num. 2, pages 451--474, Elsevier, February 2013.
  71. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Local Reasoning for Global Invariants, Part I: Region Logic. Journal of the ACM, Vol. 60, Num. 3, pages 1--56, ACM, 2013.
  72. Anindya Banerjee, David A. Naumann. Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. Journal of the ACM, Vol. 60, Num. 3, pages 1--73, ACM, 2013.
  73. 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, Num. 2, pages 1--41, ACM, 2013.
  74. 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, To Appear, ACM, 2013.
  75. Maria-Cristina Marinescu, César Sánchez. Fusing Statecharts and Java. ACM Transactions on Embedded Computing Systems, Vol. 12, pages 1--21, 2013.
  76. Mark Marron, César Sánchez, Zhendong Su, Manuel Fähndrich. Abstracting Runtime Heaps for Program Understanding. IEEE Transactions on Software Engineering, Vol. 39, Num. 6, pages 774--786, IEEE Computer Society, 2013.
  77. M. Carro, Ángel Herranz, Julio Mariño. A Model-Driven Approach to Teaching Concurrency. ACM Transactions on Computer Education, Vol. 13, Num. 1, 2013.
  78. 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, Num. 1, 2013.
  79. 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, Num. 1, pages 156--166, Springer US, 2013.
  80. 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, Num. 2, 2013.
  81. Clay Shields, Juan Caballero. Thirteenth Annual DFRWS Conference. Digital Investigation, Vol. 10, Supplement, Num. 0, pages 1--2, 2013. The Proceedings of the 13th Annual Digital Forensics Research Conference.
  82. Ahmed Bouajjani, Michael Emmi. Analysis of Recursively Parallel Programs. ACM Trans. Program. Lang. Syst., Vol. 35, Num. 3, pages 1--49, 2013.
  83. 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, Num. 4, pages 402--451, 2013.
  84. Marina Zapater, César Sánchez, José L. Ayala, José M. Moya, José L. Risco-Martín. Ubiquitous Green Computing Techniques for High Demand Applications in Smart Environments. Sensors, Vol. 12, Num. 8, pages 10659--10677, August 2012.
  85. Juan Caballero. Understanding the Role of Malware in Cybercrime. ERCIM News, Vol. 2012, Num. 90, pages 15--16, July 2012.
  86. M. V. Hermenegildo, F. Bueno, M. Carro, P. López, E. Mera, J.F. Morales, G. Puebla. An Overview of Ciao and its Design Philosophy. Theory and Practice of Logic Programming, Vol. 12, Num. 1--2, pages 219--252, Cambridge University Press, January 2012. http://arxiv.org/abs/1102.5497.
  87. Gilles Barthe, Jorge Cuéllar, Javier Lopez, Alexander Pretschner. Preface. Journal of Computer Security, Vol. 20, Num. 4, pages 307--308, 2012.
  88. Gilles Barthe, David Pichardie, Tamara Rezk. A Certified Lightweight Non-interference Java Bytecode Verifier. Mathematical Structures in Computer Science, To Appear, Cambridge University Press, 2012.
  89. Boris Köpf, Pasquale Malacaria, Catuscia Palamidessi. Quantitative Security Analysis (Dagstuhl Seminar 12481). Dagstuhl Reports, Vol. 2, Num. 11, pages 135--154, 2012.
  90. 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, Num. 4-5, pages 737--754, Cambridge U. Press, 2012.
  91. J. F. Morales, R. Haemmerlé, M. Carro, M. V. Hermenegildo. Lightweight compilation of (C)LP to JavaScript. Theory and Practice of Logic Programming, 28th Int'l. Conference on Logic Programming (ICLP'12) Special Issue, Vol. 12, Num. 4-5, pages 755--773, Cambridge U. Press, 2012.
  92. E. Albert, P. Arenas, G. Puebla, M. Hermenegildo. Certificate Size Reduction in Abstraction-Carrying Code. Theory and Practice of Logic Programming, Vol. 12, Num. 3, pages 283--318, 2012.
  93. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. Theories, Solvers and Static Analysis by Abstract Interpretation. Journal of the ACM, To Appear, ACM, 2012.
  94. Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir E. Dullerud. Verification of Bounded Discrete Horizon Hybrid Automata. IEEE Transactions on Automatic Control, Vol. 57, Num. 6, pages 1445--1455, 2012.
  95. Ganty, Pierre, Majumdar, Rupak. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., Vol. 34, Num. 1, pages 1--48, ACM, 2012.
  96. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Bounded Underapproximations. Formal Methods in System Design, Vol. 40, Num. 2, pages 206--231, 2012.
  97. Isabella Mastroeni, Anindya Banerjee. Modelling Declassification Policies using Abstract Domain Completeness. Mathematical Structures in Computer Science, Vol. 21, Num. 6, pages 1253--1299, December 2011.
  98. Gilles Barthe, Pedro D'Argenio, Tamara Rezk. Secure Information Flow by Self-Composition. Mathematical Structures in Computer Science, Vol. 21, Num. 6, pages 1207--1252, Cambridge University Press, October 2011.
  99. Gilles Barthe, César Kunz. An Abstract Model of Certificate Translation. ACM Trans. Program. Lang. Syst., Vol. 33, Num. 4, pages 1--13, ACM, July 2011.
  100. P. Chico de Guzmán, A. Casas, M. Carro, M. Hermenegildo. Parallel Backtracking with Answer Memoing for Independent And-Parallelism. Theory and Practice of Logic Programming, 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue, Vol. 11, Num. 4--5, pages 555--574, Cambridge U. Press, July 2011.
  101. 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, Num. 4--5, pages 593--609, Cambridge U. Press, July 2011.
  102. 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, Num. 4--5, pages 469--485, Cambridge U. Press, July 2011.
  103. G. Puebla, E. Albert, M. Hermenegildo. Efficient Local Unfolding with Ancestor Stacks. Theory and Practice of Logic Programming, Vol. 11, Num. 1, pages 1--32, Cambridge U. Press, January 2011.
  104. Julien Bertrane, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, X. Rival. Static Analysis by Abstract Interpretation of Embedded Critical Software. Software Engineering Notes, Vol. 36, Num. 1, pages 1--8, ACM, January 2011.
  105. Boris Köpf, David Basin. Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks. Journal of Computer Security, Vol. 1, pages 1--31, 2011.
  106. Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir E. Dullerud. Specifications for decidable hybrid games. Theoretical Computer Science, Vol. 412, Num. 48, pages 6770--6785, 2011.
  107. Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger. Parikh's Theorem: A simple and direct automaton construction. Information Processing Letters, Vol. 111, pages 614--619, 2011.
  108. Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld. Security of Multithreaded Programs by Compilation. ACM Trans. Inf. Syst. Secur., Vol. 13, Num. 3, 2010.
  109. A. Stivala, P. J. Stuckey, M. García de la Banda, M. Hermenegildo, A. Wirth. Lock-free Parallel Dynamic Programming. Journal of Parallel and Distributed Computing, Vol. 70, Num. 8, pages 839--848, Elsevier, 2010.
  110. P. López-García, F. Bueno, M. Hermenegildo. Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Information. New Generation Computing, Vol. 28, Num. 2, pages 117--206, Ohmsha, Ltd. and Springer, 2010.
  111. M. Egea, V. Rusu. Formal Executable Semantics for Conformance in the MDE Framework. Innovations in Systems and Software Engineering, Vol. 6, pages 73--81, Springer London, 2010.
  112. Pierre Ganty, Nicolas Maquet, Jean-Francois Raskin. Fixed Point Guided Abstraction Refinement for Alternating Automata. Theor. Comput. Sci., Vol. 411, Num. 38-39, pages 3444--3459, 2010.
  113. D. Cabeza, M. Hermenegildo. Non-Strict Independence-Based Program Parallelization Using Sharing and Freeness Information. Theoretical Computer Science, Vol. 410, Num. 46, pages 4704--4723, Elsevier Science, October 2009.
  114. Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk. Certificate Translation for Optimizing Compilers. ACM Trans. Program. Lang. Syst., Vol. 31, Num. 5, ACM, July 2009.
  115. Elvira Albert, John P. Gallagher, Miguel Gómez-Zamalloa, Germán Puebla. Type-based homeomorphic embedding for online termination. Inf. Process. Lett., Vol. 109, Num. 15, pages 879--886, Elsevier, July 2009.
  116. Toufik Taibi, Ángel Herranz, Juan José Moreno-Navarro. Stepwise Refinement Validation of Design Patterns Formalized in TLA+ Using the TLC Model Checker. Journal of Object Technology (JOT, (available online)), Vol. 8, Num. 2, pages 137--161, March 2009.
  117. Julio Mariño, Juan José Moreno-Navarro, Susana Muñoz Hernández. Implementing Constructive Intensional Negation. New Generation Computing, Vol. 27, Num. 1, pages 25--56, January 2009.
  118. D. Basin, M. Clavel, J. Doser, M. Egea. Automated Analysis of Security-Design Models. Information & Software Technology, Vol. 51, Num. 5, pages 815--831, 2009.
  119. E. Albert, G. Puebla, M. Hermenegildo. Abstraction-Carrying Code: A Model for Mobile Code Safety. New Generation Computing, Vol. 26, Num. 2, pages 171--204, March 2008.
  120. Julio Mariño, Ángel Herranz, Juan José Moreno-Navarro. Demandedness Analysis with Partial Predicates. Theory and Practice of Logic Programming, Vol. 7, Num. 1-2, pages 153--182, January 2007.
  121. M. Clavel, J. Meseguer, M. Palomino. Reflection in Membership Equational Logic, Many-Sorted Equational Logic, Horn Logic with Equality, and Rewriting Logic. Theoretical Computer Science, Vol. 373, Num. 1-2, pages 70--91, 2007.


Articles in Refereed Conferences

  1. 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, February 2017. To appear.
  2. Ezgi Cicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann. Relational Cost Analysis. POPL'17, ACM Press, 2017. To appear.
  3. Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. Coupling proofs are probabilistic product programs. POPL'17, ACM Press, 2017. To appear.
  4. 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), Springer-Verlag, December 2016. To appear.
  5. 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, December 2016.
  6. 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), pages 10--23, ACM Press, September 2016.
  7. 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), pages 90--103, ACM Press, September 2016.
  8. 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, September 2016.
  9. 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, September 2016.
  10. Platon Kotzias, Leyla Bilge, Juan Caballero. Measuring PUP Prevalence and PUP Distribution through Pay-Per-Install Services. Proceedings of the 25th USENIX Security Symposium, August 2016.
  11. 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, pages 163--180, Springer, March 2016.
  12. 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), 2016.
  13. 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, pages 213--224, ACM, 7 2016.
  14. 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, pages 259--268, ACM Press, 2016.
  15. Andrea Cerone, Alexey Gotsman. Analysing Snapshot Isolation. PODC'16: Symposium on Principles of Distributed Computing, pages 55--64, ACM Press, 2016.
  16. Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson. A Generic Logic for Proving Linearizability. FM'16: International Symposium on Formal Methods, LNCS, Vol. 9995, pages 426--443, Springer, 2016.
  17. Giovanni Bernardi, Alexey Gotsman. Robustness against Consistency Models with Atomic Visibility. CONCUR'16: International Conference on Concurrency Theory, LIPICS, Vol. 59, pages 1--15, Dagstuhl, 2016.
  18. 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, pages 371--384, ACM Press, 2016.
  19. 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, pages 180--196, 2016.
  20. 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.
  21. 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, pages 749--758, ACM, 2016.
  22. 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, pages 55--67, ACM, 2016.
  23. 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, pages 68--79, ACM, 2016.
  24. 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, pages 116--129, ACM, 2016.
  25. 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, pages 601--608, Springer, 2016.
  26. 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, pages 53--70, USENIX Association, 2016.
  27. 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, pages 1--15, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
  28. 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, pages 43--61, Springer, 2016.
  29. 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, pages 163--184, Springer, 2016.
  30. 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, pages 1227--1230, ACM, 2016.
  31. 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.
  32. 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, pages 60--70, ACM, 2016.
  33. 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, pages 452--469, IEEE Computer Society, 2016.
  34. Dario Fiore, Cdric 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, pages 1304--1316, 2016.
  35. 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.
  36. 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.
  37. 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.
  38. 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, pages 261--268, Springer, 2016.
  39. 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, pages 180--189, ACM, 2016.
  40. 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.
  41. 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.
  42. 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, pages 513--525, ACM, 2016.
  43. 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, pages 822--851, Springer, 2016.
  44. 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, pages 833--842, 2016.
  45. 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, pages 1--10, ACM, 2016.
  46. 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, pages 495--512, Springer, 2016.
  47. 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, pages 71--80, ACM, 2016.
  48. 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, pages 178--197, 2016.
  49. 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, pages 76--87, ACM, 2016.
  50. 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, pages 256--270, ACM, 2016.
  51. 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, pages 126--146, Springer, 2016.
  52. 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, pages 325--337, 2016.
  53. 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, pages 268--280, 2016.
  54. 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, pages 429--440, November 2015.
  55. Irfan Ul Haq, Juan Caballero, Michael D. Ernst. Ayudante: Identifying Undesired Variable Interactions. Proceedings of the 13th International Workshop on Dynamic Analysis, October 2015.
  56. 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, October 2015.
  57. 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, October 2015.
  58. 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, Num. 9131, pages 105--114, Springer-Verlag, June 2015.
  59. 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, pages 426--436, ACM, May 2015.
  60. 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, pages 151--167, IEEE Computer Society, May 2015.
  61. 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, May 2015.
  62. Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Mechanized Verification of Fine-grained Concurrent Programs. Conference on Programming Language Design and Implementation (PLDI), pages 77--87, 2015.
  63. Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. European Symposium on Programming (ESOP), pages 333--358, 2015.
  64. 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, pages 248--254, Springer, 2015.
  65. Andrea Cerone, Alexey Gotsman, Hongseok Yang. Transaction chopping for parallel snapshot isolation. DISC'15: International Symposium on Distributed Computing, Tokyo, Japan, LNCS, Vol. 9363, pages 388--404, Springer, 2015.
  66. 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, pages 58--71, Dagstuhl, 2015.
  67. Alexey Gotsman, Hongseok Yang. Composite replicated data types. ESOP'15: European Symposium on Programming, London, UK, LNCS, Vol. 9032, pages 585--609, Springer, 2015.
  68. 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, pages 1156--1168, ACM, 2015.
  69. 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, pages 457--485, Springer, 2015.
  70. 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, pages 689--718, Springer, 2015.
  71. 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, pages 203--218, Springer, 2015.
  72. 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, pages 387--401, Springer, 2015.
  73. 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, pages 55--68, ACM, 2015.
  74. 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, pages 355--376, Springer, 2015.
  75. 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.
  76. 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.
  77. Goran Doychev, Boris Köpf. Rational Protection Against Timing Attacks. Proc. 28th IEEE Computer Security Foundations Symposium (CSF'15), IEEE, 2015.
  78. 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.
  79. 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, pages 478--493, Springer, 2015.
  80. 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, pages 690--701, Springer International Publishing, 2015.
  81. 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, pages 153--163, Springer International Publishing, 2015.
  82. 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), pages 1353--1354, ACM, 2015.
  83. 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, pages 317--331, Springer, 2015.
  84. 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, pages 1518--1529, 2015.
  85. 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, pages 254--274, Springer, 2015.
  86. 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.
  87. 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.
  88. 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, pages 209--226, Springer, 2015.
  89. 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, pages 85--90, Association for Computing Machinery, 2015.
  90. 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, pages 95--107, 2015.
  91. 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, pages 260--269, ACM, 2015.
  92. 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, pages 451--454, 2015.
  93. 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, pages 535--559, 2015.
  94. 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, pages 651--662, ACM, 2015.
  95. 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, pages 218--232, Springer, 2015.
  96. 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, pages 91--100, Australian Computer Society, 2015.
  97. 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, pages 256--269, 2015.
  98. 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, pages 318--335, Springer, 2015.
  99. 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.
  100. Esparza, Javier, Ganty, Pierre, Leroux, Jér^ome, Majumdar, Rupak. Verification of Population Protocols. CONCUR '15: Proc. 26th Int. Conf. on Concurrency Theory, 2015.
  101. 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.
  102. Ganty, Pierre, Iosif, Radu. Interprocedural Reachability for Flat Integer Programs. FCT '15: Proc. 20th Int. Symp. on Fundamentals of Computation Theory, LNCS, Springer, 2015.
  103. Ratan Lal, Pavithra Prabhakar. Bounded error flowpipe computation of parameterized linear systems. Proceedings of the International Conference on Embedded Software (EMSOFT), ACM, IEEE, 2015.
  104. 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, pages 85--108, Open Channel Publishing Ltd., 2015.
  105. 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, pages 261--273, 2015.
  106. 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, pages 329--341, 2015.
  107. 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, December 2014.
  108. 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), pages 1267--1279, ACM, November 2014.
  109. 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), pages 1016--1027, ACM, November 2014.
  110. 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, pages 291--305, Springer Verlag, November 2014.
  111. 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, pages 394--402, Springer Verlag, November 2014.
  112. 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, November 2014.
  113. 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, November 2014.
  114. 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 pages, ACM Press, September 2014.
  115. 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), 15 pages, ACM Press, September 2014.
  116. 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, September 2014.
  117. 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), July 2014.
  118. 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), July 2014. CoRR abs/1407.2988 [cs.LO].
  119. 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, Cambridge U. Press, July 2014.
  120. 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, February 2014.
  121. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, German Andres Delbianco. Communicating State Transition Systems for Fine-Grained Concurrent Resources. European Symposium on Programming (ESOP), pages 290--310, 2014.
  122. 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), pages 385--396, 2014.
  123. 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, pages 376--390, Springer, 2014.
  124. Andrea Cerone, Alexey Gotsman, Hongseok Yang. Parameterised linearisability. ICALP'14: International Colloquium on Automata, Languages, and Programming, Copenhagen, Denmark, LNCS, Vol. 8573, pages 271--284, Springer, 2014.
  125. 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, pages 271--284, ACM Press, 2014.
  126. Á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, pages 157--168, ACM, 2014.
  127. Cerone, Andrea, Hennessy, Matthew. Characterising Testing Preorders for Broadcasting Distributed Systems. Trustworthy Global Computing, pages 67--81, Springer, 2014.
  128. 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, pages 3--20, 2014.
  129. 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, pages 206--222, Springer, 2014.
  130. 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, pages 95--112, Springer, 2014.
  131. 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, pages 193--206, ACM, 2014.
  132. 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, pages 140--158, Springer, 2014.
  133. 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].
  134. 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, pages 179--194, IEEE Computer Society, 2014.
  135. 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.
  136. 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, pages 314--329, Springer, 2014.
  137. Alejandro Sánchez, César Sánchez. Parametrized Verification Diagrams. Proc. of the 21st Int'l Symp. on Temporal Representation and Reasoning (TIME'14), pages 132--141, IEEE Computer Society Press, 2014.
  138. Laura Bozzelli, César Sánchez. Foundations of Boolean Stream Runtime Verification. LNCS, Vol. 8734, pages 64--79, Springer, 2014.
  139. 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, pages 620--627, Springer, 2014.
  140. 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, pages 418--433, Springer, 2014.
  141. 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, pages 265--284, Springer, 2014.
  142. 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, pages 72--90, Springer, 2014.
  143. Dario Fiore, Rosario Gennaro, Valerio Pastro. Efficiently Verifiable Computation on Encrypted Data. ACM CCS 2014 -- 21th ACM Conference on Computer and Communication Security, pages 844--855, 2014.
  144. 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, pages 371--389, Springer, 2014.
  145. 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, pages 538--555, Springer, 2014.
  146. Yevgeniy Dodis, Dario Fiore. Interactive Encryption and Message Authentication. Security and Cryptography for Networks - 9th International Conference, SCN 2014, LNCS, Vol. 8642, pages 494--513, Springer, 2014.
  147. 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, pages 51--66, Springer Berlin Heidelberg, 2014.
  148. 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, pages 387--401, Springer, 2014.
  149. 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, pages 335--348, ACM, 2014.
  150. 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, pages 106--113, Springer, 2014.
  151. 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, pages 20--29, ACM, 2014.
  152. 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., pages 33--42, 2014.
  153. 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., pages 83--99, 2014.
  154. Carolina Dania, Manuel Clavel. Modeling Social Networking Privacy. 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, September 1-3, 2014, pages 50--57, 2014.
  155. 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, pages 2318--2323, IEEE, 2014.
  156. 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, pages 5333--5338, IEEE, 2014.
  157. 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, pages 396--407, Springer, 2014.
  158. 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, pages 235--255, 2014.
  159. 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, pages 98--113, IEEE Computer Society, 2014.
  160. 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, pages 77--92, Springer, 2014.
  161. 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, pages 425--438, ACM, 2014.
  162. 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, pages 534--553, 2014.
  163. 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), pages 1247--1260, ACM, November 2013.
  164. 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, November 2013.
  165. 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, October 2013.
  166. A. Serrano, P. Lopez-Garcia, F. Bueno, M. 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, Num. 4-5, pages 1--14, Cambridge U. Press, August 2013.
  167. 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, July 2013.
  168. Z. Drey, J. F. Morales, M. V. Hermenegildo, M. Carro. Reversible Language Extensions and their Application in Debugging. Practical Aspects of Declarative Languages (PADL'13), LNCS, Vol. 7752, Springer, January 2013.
  169. P. Chico de Guzmán, M. Carro, M. Hermenegildo. Supporting Pruning in Tabled LP. Practical Aspects of Declarative Languages (PADL'13), LNCS, Springer Verlag, January 2013.
  170. 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), pages 145--156, 2013.
  171. 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), pages 87--100, 2013.
  172. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv. Effectively-Propositional Reasoning about Reachability in Linked Data Structures. Computer Aided Verification (CAV), pages 756--772, 2013.
  173. Ruy Ley-Wild, Aleksandar Nanevski. Subjective Auxiliary State for Coarse-Grained Concurrency. Principles of Programming Languages (POPL), pages 561--574, 2013.
  174. 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, pages 309--318, ACM Press, 2013.
  175. 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, pages 249--269, Springer, 2013.
  176. 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, pages 235--248, ACM Press, 2013.
  177. Á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, pages 85--96, ACM, 2013.
  178. Á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, pages 107--116, ACM, 2013.
  179. Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin. Verified Computational Differential Privacy with Applications to Smart Metering. CSF, pages 287--301, IEEE, 2013.
  180. 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), pages 1217--1230, 2013.
  181. Gilles Barthe, Juan Manuel Crespo, César Kunz. Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. Logical Foundations of Computer Science, International Symposium, LFCS 2013, Lecture Notes in Computer Science, Vol. 7734, pages 29--43, Springer, 2013.
  182. Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron. From Relational Verification to SIMD Loop Synthesis. ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '13, pages 123--134, ACM, 2013.
  183. 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, pages 696--701, Springer, 2013.
  184. 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.
  185. 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.
  186. 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.
  187. 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.
  188. 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, pages 401--410, Springer, 2013.
  189. 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, pages 363--376, ACM, 2013.
  190. 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.
  191. 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.
  192. 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, pages 97--106, ACM, 2013.
  193. 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, pages 399--410, ACM, 2013.
  194. 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.
  195. 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, pages 53--62, CEUR-WS.org, 2013.
  196. Pavithra Prabhakar, Miriam Garcia Soto. Abstraction Based Model-Checking of Stability of Hybrid Systems. CAV, pages 280--295, 2013.
  197. Pavithra Prabhakar, Jun Liu, Richard M. Murray. Pre-orders for reasoning about stability properties with respect to input of hybrid systems. EMSOFT, pages 1--10, 2013.
  198. Pavithra Prabhakar, Mahesh Viswanathan. On the decidability of stability of hybrid systems. HSCC, 2013.
  199. Scott C. Livingston, Pavithra Prabhakar, Alex B. Jose, Richard M. Murray. Patching task-level robot controllers based on a local -calculus formula. ICRA, 2013.
  200. Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan. Hybrid Automata based CEGAR for Rectangular Hybrid Automata. VMCAI, 2013.
  201. 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, pages 124--140, Springer, 2013.
  202. Pierre Ganty, Samir Genaim. Proving Termination Starting from the End. CAV'13: Proc. 23rd Int. Conf. on Computer Aided Verification, LNCS, Vol. 8044, pages 397--412, Springer, 2013.
  203. 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, pages 247--261, Springer, 2013.
  204. 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, pages 371--384, ACM, 2013.
  205. Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub. Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security and Privacy, pages 445--459, IEEE Computer Society, 2013.
  206. 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, November 2012.
  207. Chris Grier, Lucas Ballard, Juan Caballero, Neha Chachra, Christian J. Dietrich, Kirill Levchenko, Panayiotis Mavrommatis, Damon McCoy, Antonio Nappa, Andreas Pitsillidis, Niels Provos, M. Zubair Rafique, Moheeb Abu Rajab, Christian Rossow, Kurt Thomas, Vern Paxson, Stefan Savage, Geoffrey M. Voelker. Manufacturing Compromise: The Emergence of Exploit-as-a-Service. Proceedings of the 19th ACM Conference on Computer and Communication Security, October 2012.
  208. George Bariannys, M. Carro, Dimitris Plexousakis. Deriving Specifications for Composite Web Services. IEEE Signature Conference on Computers, Software, and Applications, IEEE Computer Society, IEEE, July 2012.
  209. Juan Caballero, Gustavo Grieco, Mark Marron, Antonio Nappa. Early Detection of Dangling Pointers in Use-After-Free and Double-Free Vulnerabilities. Proceedings of the 2012 International Symposium on Software Testing and Analysis, July 2012.
  210. P. Chico de Guzmán, M. Carro, M. Hermenegildo, P. Stuckey. A General Implementation Framework for Tabled CLP. FLOPS'12, LNCS, Num. 7294, pages 104--119, Springer Verlag, May 2012.
  211. P. Chico de Guzmán, A. Casas, M. Carro, M. Hermenegildo. A Segment-Swapping Approach for Executing Trapped Computations. PADL'12, LNCS, Vol. 7149, pages 138--152, Springer Verlag, January 2012.
  212. Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang. Show no weakness: sequentially consistent specifications of TSO libraries. Proceedings of the International Symposium on Distributed Computing (DISC'12), Salvador, Bahia, Brazil, LNCS, Vol. 7611, pages 31--45, Springer, 2012.
  213. Alexey Gotsman, Hongseok Yang. Linearizability with ownership transfer. Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), Newcastle upon Tyne, UK, LNCS, Vol. 7454, pages 256--271, Springer, 2012.
  214. Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang. Concurrent library correctness on the TSO memory model. Proceedings of the 21st European Symposium on Programming (ESOP'12), Tallinn, Estonia, LNCS, Vol. 7211, pages 87--107, Springer, 2012.
  215. 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, pages 41--60, Springer Berlin Heidelberg, 2012.
  216. 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, pages 379--395, Springer Berlin Heidelberg, 2012.
  217. Alexander Malkis, Anindya Banerjee. Verification of Software Barriers. Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel Programming (PPoPP 2012), pages 313--314, ACM, 2012.
  218. José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin. Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. ACM Conference on Computer and Communications Security, pages 488--500, 2012.
  219. Gilles Barthe, David Pointcheval, Santiago Zanella Béguelin. Verified Security of Redundancy-Free Encryption from Rabin and RSA. ACM Conference on Computer and Communications Security, pages 724--735, 2012.
  220. Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. Certified Programs and Proofs - Second International Conference, CPP 2012, Lecture Notes in Computer Science, Vol. 7679, pages 7--8, Springer, 2012.
  221. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna. Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. 25th IEEE Computer Security Foundations Symposium, CSF 2012, pages 186--197, IEEE, 2012.
  222. Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin. Verified Security of Merkle-Damgrd. 25th IEEE Computer Security Foundations Symposium, CSF 2012, pages 354--368, IEEE, 2012.
  223. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin. Computer-Aided Cryptographic Proofs. Interactive Theorem Proving - Third International Conference, ITP 2012, Lecture Notes in Computer Science, Vol. 7406, pages 11--27, Springer, 2012.
  224. Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas. Secure Multi-Execution through Static Program Transformation. Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Lecture Notes in Computer Science, Vol. 7273, pages 186--202, Springer, 2012.
  225. Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. Mathematics of Program Construction - 11th International Conference, MPC 2012, Lecture Notes in Computer Science, Vol. 7342, pages 1--6, Springer, 2012.
  226. Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin. Computer-Aided Cryptographic Proofs. Static Analysis - 19th International Symposium, SAS 2012, Lecture Notes in Computer Science, Vol. 7460, pages 1--2, Springer, 2012.
  227. Gilles Barthe, Delphine Demange, David Pichardie. A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. 21st European Symposium on Programming, ESOP 2012, Lecture Notes in Computer Science, Vol. 7211, pages 47--66, Springer, 2012.
  228. Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pages 97--110, ACM, 2012.
  229. 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.
  230. Boris Köpf, Laurent Mauborgne, Martín Ochoa. Automatic Quantification of Cache Side-Channels. 24th International Conference on Computer Aided Verification (CAV '12), Lecture Notes in Computer Science, Vol. 7358, pages 564--580, Springer-Verlag, 2012.
  231. Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin. Probabilistic Relational Reasoning for Differential Privacy. Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12), pages 97--109, ACM, 2012.
  232. Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, Bor-Yuh Evan Chang. Invariant Generation for Parametrized Systems Using Self-reflection. Proc. of the 19th International Symposium on Static Analysis (SAS'12), LNCS, Vol. 7460, pages 146--163, Springer, 2012.
  233. César Sánchez, Julián Samborski-Forlese. Efficient Regular Linear Temporal Logic Using Dualization and Stratification. Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME'12), pages 13--20, IEEE Computer Society, 2012.
  234. César Sánchez, Julián Samborski-Forlese. How to Translate Efficiently Extensions of Temporal Logics into Alternating Automata. Proceedings of The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC'12), LNCS, Vol. 7521, pages 30--45, Springer, 2012.
  235. 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), pages 211--223, Leibniz-Zentrum fuer Informatik, 2012.
  236. 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, pages 1--20, Springer Berlin Heidelberg, 2012. Invited Paper, also appears as tech. rep. MSR-TR-2011-118.
  237. 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.
  238. César Sánchez, Julián Samborski-Forlese. Efficient Regular Linear Temporal Logic Using Dualization and Stratification. Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME'12), pages 13--20, IEEE Computer Society, 2012.
  239. César Sánchez, Julián Samborski-Forlese. How to Translate Efficiently Extensions of Temporal Logics into Alternating Automata. Proceedings of The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC'12), LNCS, Vol. 7521, pages 30--45, Springer, 2012.
  240. Pavithra Prabhakar. Foundations for Approximation Based Analysis of Stability Properties of Hybrid Systems. 50th Annual Allerton Conference on Communication, Control and Computing, 2012.
  241. Pavithra Prabhakar, Mahesh Viswanathan. Conformance Testing of Boolean Programs with Multiple Faults. Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings, Lecture Notes in Computer Science, Vol. 7273, pages 101--117, Springer, 2012.
  242. Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan. Pre-orders for reasoning about stability. Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC'12, Beijing, China, April 17-19, 2012, pages 197--206, ACM, 2012.
  243. 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, pages 285--294, IEEE Computer Society Press, 2012.
  244. Ruy Ley-Wild, Umut A. Acar, Guy Blelloch. Non-Monotonic Self-Adjusting Computation. European Symposium on Programming, ESOP 2012, Lecture Notes in Computer Science, Vol. 7211, pages 476--496, Springer, 2012.
  245. D. Ivanović, M. Carro, M. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. Service-Oriented Computing -- ICSOC 2011, LNCS, Vol. 7084, pages 62--76, Springer Verlag, December 2011. Best paper award.
  246. Juan Manuel Crespo, César Kunz. A Machine-Checked Framework for Relational Separation Logic. Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, LNCS, Vol. 7041, pages 122--137, Springer, November 2011.
  247. Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin. Verifiable Security of Boneh-Franklin Identity-Based Encryption. 5th International Conference on Provable Security -- ProvSec 2011, Lecture Notes in Computer Science, Vol. 6980, pages 68--83, Springer, October 2011.
  248. Barthe, Gilles, Grégoire, Benjamin, Heraud, Sylvain, Zanella Béguelin, Santiago. Computer-Aided Security Proofs for the Working Cryptographer. Advances in Cryptology -- CRYPTO 2011, Lecture Notes in Computer Science, Vol. 6841, pages 71--90, Springer, August 2011.
  249. Juan Caballero, Chris Grier, Christian Kreibich, Vern Paxson. Measuring Pay-per-Install: The Commoditization of Malware Distribution. Proceedings of the 20th USENIX Security Symposium, August 2011.
  250. 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, pages 139--154, Springer, July 2011.
  251. R. Haemmerlé, P. López, M. Hermenegildo. CLP Projection for Constraint Handling Rules. Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 137--148, ACM Press, July 2011.
  252. 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, pages 120--127, IEEE Press, July 2011.
  253. Gilles Barthe, Juan Manuel Crespo, César Kunz. Relational Verification Using Product Programs. FM 2011: 17th International Symposium on Formal Methods, LNCS, Vol. 6664, pages 200--214, Springer, June 2011.
  254. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna. Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. FM 2011: 17th International Symposium on Formal Methods, LNCS, Vol. 6664, pages 231--245, Springer, June 2011.
  255. David A. Basin, Manuel Clavel, Marina Egea. A decade of model-driven security. SACMAT 2011, 16th ACM Symposium on Access Control Models and Technologies, pages 1--10, ACM, June 2011.
  256. Germán Andrés Delbianco, Mauro Jaskelioff, Alberto Pardo. Applicative Shortcut Fusion. 12th International Symposium on Trends in Functional Programming, TFP'11, May 2011.
  257. Noah M. Johnson, Juan Caballero, Kevin Chen, Stephen McCamant, Pongsin Poosankam, Daniel Reynaud, Dawn Song. Differential Slicing: Identifying Causal Execution Differences for Security Applications. Proceedings of the IEEE Symposium on Security and Privacy, May 2011.
  258. Barthe, Gilles, Grégoire, Benjamin, Lakhnech, Yassine, Zanella Béguelin, Santiago. Beyond Provable Security Verifiable IND-CCA Security of OAEP. Topics in Cryptology --- CT-RSA 2011, Lecture Notes in Computer Science, Vol. 6558, pages 180--196, Springer, February 2011.
  259. E. Mera, T. Trigo, P. López-García, M. Hermenegildo. Profiling for Run-Time Checking of Computational Properties and Performance Debugging. Practical Aspects of Declarative Languages (PADL'11), Lecture Notes in Computer Science, Vol. 6539, pages 38--53, Springer-Verlag, January 2011.
  260. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. How to make ad hoc proof automation less ad hoc. International Conference on Functional Programming (ICFP), pages 163--175, 2011.
  261. Aleksandar Nanevski, Anindya Banerjee, Deepak Garg. Verification of Information Flow and Access Control Policies with Dependent Types. IEEE Symposium on Security and Privacy (S&P), pages 165--179, 2011.
  262. Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski. Partiality, State and Dependent Types. Typed Lambda Calculi and Applications (TLCA), pages 198--212, 2011.
  263. Alexey Gotsman, Hongseok Yang. Modular verification of preemptive OS kernels. Proceedings of the 16th ACM International Conference on Functional Programming (ICFP'11), Tokyo, Japan, pages 404--417, ACM Press, 2011.
  264. Alexey Gotsman, Hongseok Yang. Liveness-Preserving Atomicity Abstraction. Proceedings of the 38th International Colloquium on Automata, Languages and Programming, (ICALP'11), Zurich, Switzerland, LNCS, Vol. 6756, pages 453--465, Springer, 2011.
  265. 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.
  266. 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.
  267. Gilles Barthe, Boris Köpf. Information-theoretic Bounds for Differentially Private Mechanisms. Proc. 24rd IEEE Computer Security Foundations Symposium (CSF '11), pages 191--204, IEEE, 2011.
  268. Michael Backes, Matthias Berg, Boris Köpf. Non-Uniform Distributions in Quantitative Information-Flow. Proc. 6th ACM Conference on Information, Computer and Communications Security (ASIACCS '11), pages 367--375, ACM, 2011.
  269. Alejandro Sánchez, César Sánchez. A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes. Proc. of the 3rd NASA Formal Methods Symposium (NFM'11), LNCS, Vol. 6447, pages 343--358, Springer, 2011.
  270. M. Carro, D. Karastoyanova, G. A. Lewis, A. Liu. Third International Workshop on Principles of Engineering Service-Oriented Systems (PESOS 2011). ICSE, pages 1218--1219, 2011.
  271. 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), pages 3--17, IEEE Computer Society, 2011.
  272. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. The Reduced Product of Abstract Domains and the Combination of Decision Procedures. 14th International Conference on Fondations of Software Science and Computation Structures (FoSSaCS 2011), Lecture Notes in Computer Science, Vol. 6604, pages 456--472, Springer-Verlag, 2011.
  273. Alexander Malkis, Laurent Mauborgne. On the Strength of Owicki-Gries for Resources. 9th Asian Symposium on Programming Languages and Systems (APLAS 2011), Lecture Notes in Computer Science, Vol. 7078, pages 172--187, Springer, 2011.
  274. 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.
  275. David A. Basin, Manuel Clavel, Marina Egea, Miguel Angel García de Dios, Carolina Dania, Gonzalo Ortiz, Javier Valdazo. Model-Driven Development of Security-Aware GUIs for Data-Centric Applications. Foundations of Security Analysis and Design VI (FOSAD 2010), LNCS, Vol. 6858, pages 101--124, Springer, 2011.
  276. Pavithra Prabhakar, Mahesh Viswanathan. A dynamic algorithm for approximate flow computations. Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pages 133--142, ACM, 2011.
  277. 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.
  278. 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.
  279. Javier Esparza, Pierre Ganty. Complexity of Pattern-based Verification for Multithreaded Programs. POPL '11: Proc. 38th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pages 499--510, ACM Press, 2011.
  280. T. Trigo, P. López-García, S. Muñoz-Hernandez. Towards Fuzzy Granularity Control in Parallel/Distributed Computing. International Conference on Fuzzy Computation (ICFC 2010), pages 43--55, SciTePress, October 2010.
  281. P. López-García, L. Darmawan, F. Bueno. A Framework for Verification and Debugging of Resource Usage Properties. Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 7, pages 104--113, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2010.
  282. Julien Bertrane, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, X. Rival. Static Analysis and Verification of Aerospace Software by Abstract Interpretation. AIAA InfotechAerospace 2010, pages 1--38, American Institue of Aeronautics and Astronautics, April 2010. AIAA-2010-3385.
  283. Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine. Structuring the verification of heap-manipulating programs. Principles of Programming Languages (POPL), pages 261--274, 2010.
  284. Alexander Malkis, Andreas Podelski, Andrey Rybalchenko. Thread-Modular Counterexample-Guided Abstraction Refinement. Static Analysis - 17th International Symposium, SAS 2010, Lecture Notes in Computer Science, Vol. 6337, pages 356--372, Springer, 2010.
  285. Moritz Y. Becker, Alexander Malkis, Laurent Bussard. A Practical Generic Privacy Language. Information Systems Security - 6th International Conference, ICISS 2010, Lecture Notes in Computer Science, Vol. 6503, pages 125--139, Springer, 2010.
  286. David A. Naumann, Anindya Banerjee. Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. ESOP, pages 2--22, 2010.
  287. Stan Rosenberg, Anindya Banerjee, David A. Naumann. Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. VSTTE, pages 183--198, 2010.
  288. Gilles Barthe, Pablo Buiras, César Kunz. A Functional Framework for Result Checking. Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Lecture Notes in Computer Science, Vol. 6009, pages 72--86, Springer, 2010.
  289. Gilles Barthe, César Kunz. Perspectives in Certificate Translation. Trustworthly Global Computing - 5th International Symposium, TGC 2010, Lecture Notes in Computer Science, Vol. 6084, pages 23--34, Springer, 2010.
  290. Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech. Computational Indistinguishability Logic. Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, pages 375--386, ACM, 2010.
  291. Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi. Robustness Guarantees for Anonymity. Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pages 91--106, IEEE Computer Society, 2010.
  292. 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.
  293. Barthe, Gilles, Hedin, Daniel, Zanella Béguelin, Santiago, Gregoire, Benjamin, Heraud, Sylvain. A Machine-Checked Formalization of Sigma-Protocols. 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pages 246--260, IEEE Computer Society, 2010.
  294. Barthe, Gilles, Grégoire, Benjamin, Zanella Béguelin, Santiago. Programming Language Techniques for Cryptographic Proofs. 1st International Conference on Interactive Theorem Proving, ITP 2010, Lecture Notes in Computer Science, Vol. 6172, pages 115--130, Springer, 2010.
  295. César Kunz. Certificate Translation for the Verification of Concurrent Programs. Trustworthly Global Computing - 5th International Symposium, TGC 2010, Lecture Notes in Computer Science, Vol. 6084, pages 237--252, Springer, 2010.
  296. L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo. Program Parallelization using Synchronized Pipelining. Proceedings of the 19th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'09), LNCS, Num. 6037, pages 173--187, Springer, 2010.
  297. Boris Köpf, Geoffrey Smith. Vulnerability Bounds and Leakage Resilience of Blinded Cryptography under Timing Attacks. Proc 23rd. IEEE Computer Security Foundations Symposium (CSF '10), pages 44--56, IEEE, 2010.
  298. Boris Köpf, Andrey Rybalchenko. Approximation and Randomization for Quantitative Information-Flow Analysis. Proc. 23rd IEEE Computer Security Foundations Symposium (CSF '10), pages 3--14, IEEE, 2010.
  299. Michael Backes, Goran Doychev, Markus Dürmuth, Boris Köpf. Speaker Recognition in Encrypted Voice Streams. Proc. 15th European Symposium on Research in Computer Security (ESORICS '10), LNCS 6345, pages 508--523, Springer, 2010.
  300. Martin Leucker, César Sánchez. Regular Linear-Time Temporal Logic. Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), pages 3--5, IEEE Computer Society, 2010.
  301. César Sánchez, Martin Leucker. Regular Linear Temporal Logic with Past. Proc. of the 11th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation, (VMCAI'10), LNCS, Vol. 5944, pages 295--311, Springer, 2010.
  302. Krishnendu Chatterjee, Luca de Alfaro, Vishwanath Raman, César Sánchez. Analyzing the Impact of Change in Multi-threaded Programs. Proc. of the 13th Int'l Conf. on Fundamental Approaches to Software Engineering (FASE'10), LNCS, Vol. 6013, pages 293--307, Springer, 2010.
  303. Alejandro Sánchez, César Sánchez. Decision Procedures for the Temporal Verification of Concurrent Lists. Proc. of the 12th Int'l Conf. on Formal Engineering Methods (ICFEM'10), LNCS, Vol. 6447, pages 74--89, Springer, 2010.
  304. D. Ivanović, M. Carro, M. V. Hermenegildo. Automatic Fragment Identification in Workflows Based on Sharing Analysis. Service-Oriented Computing -- ICSOC 2010, LNCS, Vol. 6470, pages 350--364, Springer Verlag, 2010.
  305. D. Ivanović, M. Carro, M. Hermenegildo. Towards Data-Aware QoS-Driven Adaptation for Service Orchestrations. Proceedings of the 2010 IEEE International Conference on Web Services (ICWS 2010), Miami, FL, USA, 5-10 July 2010, pages 107--114, IEEE, 2010.
  306. Gourinath Banda, John P. Gallagher. Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation. Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 6355, pages 27--45, Springer, 2010.
  307. Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival. Astrée: Proving the Absence of Runtime Errors. Embedded Real Time Software and Systems - ERTSS 2010, pages 1--9, 2010.
  308. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. A Scalable Segmented Decision Tree Abstract Domain. Pnueli Festschrift, Lecture Notes in Computer Science, Vol. 6200, pages 72--95, Springer-Verlag, 2010.
  309. Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur. Shape Analysis with Reference Set Relations. VMCAI, 2010.
  310. M. A. García de Dios, C. Dania, M. Schläpfer, D. Basin, M. Clavel, M. Egea. SSG: a Model-Based Development Environment for Smart, Security-Aware GUIs. Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, ICSE 2010, Cape Town, South Africa, 1-8 May 2010, pages 311--312, ACM, 2010.
  311. D. Basin, M. Clavel, M. Egea, M. Schläpfer. Automatic Generation of Smart, Security-Aware GUI Models. Engineering Secure Software and Systems, 2nd International Symposium, ESSoS 2010, Pisa, Italy, February 3-4, 2010. Proceedings, Lecture Notes in Computer Science, Vol. 5965, pages 201--217, Springer, 2010.
  312. 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.
  313. Pierre Ganty, Benjamin Monmege, Rupak Majumdar. Bounded Underapproximations. CAV'10: Proc. 20th Int. Conf. on Computer Aided Verification, LNCS, Vol. 6174, pages 600--614, Springer, 2010.
  314. Umut A. Acar, Guy E. Blelloch, Ruy Ley-Wild, Kanat Tangwongsan, Duru Türkoglu. Traceable data types for self-adjusting computation. PLDI, pages 483--496, 2010.
  315. A. Herranz, J. Mariño, M. Carro, J.J. Moreno-Navarro. Modeling Concurrent Systems with Shared Resources. 14th International Workshop on Formal Methods for Industrial Critical Systems, Lecture Notes in Computer Science, Vol. 5825, pages 102--116, November 2009.
  316. G. Marpons, J. Mariño, M. Carro, A. Herranz, L.Å. Fredlund, J.J. Moreno-Navarro, A. Polo. A Coding Rule Conformance Checker Integrated into GCC. Spanish Conference on Programming and Computer Languages (PROLE'09), ENTCS, Vol. 258, pages 149--159, Elsevier, August 2009.
  317. E. Mera, P. López-García, M. 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, pages 281--295, Springer-Verlag, July 2009.
  318. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. A Tabling Implementation Based on Variables with Multiple Bindings. International Conference on Logic Programming (ICLP 2009), LNCS, Num. 5649, pages 190--204, Springer-Verlag, July 2009.
  319. V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee. Merlin: specification inference for explicit information flow problems. PLDI, pages 75--86, June 2009.
  320. Mark Marron, Deepak Kapur, Manuel Hermenegildo. Identification of Logically Related Heap Regions. ISMM'09: Proceedings of the 8th international symposium on Memory management, ACM Press, June 2009.
  321. P. Chico de Guzmán, M. Carro, M. Hermenegildo. Towards a Complete Scheme for Tabled Execution Based on Program Transformation. 11th International Symposium on Practical Aspects of Declarative Languages (PADL'09), LNCS, Num. 5418, pages 224--238, Springer-Verlag, January 2009.
  322. Avraham Shinnar, Marco Pistoia, Anindya Banerjee. A language for information flow: dynamic tracking in multiple interdependent dimensions. PLAS, pages 125--131, 2009.
  323. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet. Implementing a Direct Method for Certificate Translation. Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Lecture Notes in Computer Science, Vol. 5885, pages 541--560, Springer, 2009.
  324. Barthe, G., Grégoire, B., Zanella Béguelin, S.. Formal Certification of Code-Based Cryptographic Proofs. 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pages 90--101, ACM, 2009.
  325. Zanella Béguelin, S., Grégoire, B., Barthe, G., Olmedo, F.. Formally Certifying the Security of Digital Signature Schemes. 30th IEEE Symposium on Security and Privacy, S&P 2009, pages 237--250, IEEE Computer Society, 2009.
  326. 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.
  327. Henning Christiansen, John P. Gallagher. Non-discriminating Arguments and Their Uses. Logic Programming, 25th International Conference, ICLP 2009, Pasadena, CA, USA, July 14-17, 2009. Proceedings, Lecture Notes in Computer Science, Vol. 5649, pages 55--69, Springer, 2009.
  328. 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.
  329. M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. L. Talcott. Unification and Narrowing in Maude 2.4. Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, Lecture Notes in Computer Science, Vol. 5595, pages 380--390, Springer, 2009.
  330. Vlad Rusu, Manuel Clavel. Vérification d'invariants pour des syst`emes spécifiés en logique de réécriture. Vingti`emes Journées Francophones des Langages Applicatifs (JFLA 2009), Studia Informatica Universalis, Vol. 7.2, pages 317--350, 2009.
  331. Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko. Verifying Liveness for Asynchronous Programs. POPL '09: Proc. 36th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pages 102--113, ACM Press, 2009.
  332. 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.
  333. Pierre Ganty, Rupak Majumdar. Analyzing Real-time Event-driven Programs. FORMATS '09: Proc. 7th Int. Conf. on Formal Modelling and Analysis of Timed Systems, LNCS, Vol. 5813, pages 164--178, Springer, 2009.
  334. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo. Negative Ternary Set-Sharing. International Conference on Logic Programming, ICLP, LNCS, Num. 5366, pages 301--316, Springer-Verlag, December 2008.
  335. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. A Sketch of a Complete Scheme for Tabled Execution Based on Program Transformation. Int'l. Conference on Logic Programming, LNCS, Vol. 5366, pages 795--800, Springer Verlag, December 2008. Short paper.
  336. A. Casas, M. Carro, M. Hermenegildo. A High-Level Implementation of Non-Deterministic, Unrestricted, Independent And-Parallelism. 24th International Conference on Logic Programming (ICLP'08), LNCS, Vol. 5366, pages 651--666, Springer-Verlag, December 2008.
  337. Mark Marron, Mario Méndez-Lojo, Manuel Hermenegildo and Darko Stefanovic, Deepak Kapur. Sharing Analysis of Arrays, Collections, and Recursive Structures. ACM WS on Program Analysis for Software Tools and Engineering (PASTE'08), ACM, November 2008.
  338. Iván Pérez, Ángel Herranz, Susana Muñoz, Juan José Moreno-Navarro. Modelling Mash-Up Resources. 13th Conference on Software Engineering and Databases, JISBD'08, pages 135--146, October 2008.
  339. Mark Marron, Darko Stefanovic, Deepak Kapur, Manuel Hermenegildo. Identification of Heap-Carried Data Dependence Via Explicit Store Heap Models. 21st Int'l. WS on Languages and Compilers for Parallel Computing (LCPC'08), LNCS, Springer-Verlag, August 2008.
  340. J. Morales, M. Carro, M. Hermenegildo. Comparing Tag Scheme Variations Using an Abstract Machine Generator. 10th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), pages 32--43, ACM Press, July 2008.
  341. E. Mera, P. López-García, M. Carro, M. Hermenegildo. Towards Execution Time Estimation in Abstract Machine-Based Languages. 10th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), pages 174--184, ACM Press, July 2008.
  342. Mark Marron, Manuel Hermenegildo, Darko Stefanovic, Deepak Kapur. Efficient Context-Sensitive Shape Analysis with Graph-Based Heap Models. International Conference on Compiler Construction (CC 2008), Lecture Notes in Computer Science, 15 pages, Springer, April 2008.
  343. M. Méndez-Lojo, M. Hermenegildo. Precise Set Sharing Analysis for Java-style Programs. 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'08), LNCS, Num. 4905, pages 172--187, Springer-Verlag, January 2008.
  344. P. Chico de Guzmán, M. Carro, M. Hermenegildo, Claudio Silva, Ricardo Rocha. An Improved Continuation Call-Based Implementation of Tabling. 10th International Symposium on Practical Aspects of Declarative Languages (PADL'08), LNCS, Vol. 4902, pages 198--213, Springer-Verlag, January 2008.
  345. G. Marpons, J. Mariño, M. Carro, A. Herranz, J.J. Moreno-Navarro, L.Å. Fredlund. Automatic Coding Rule Conformance Checking Using Logic Programming. 10th International Symposium on Practical Aspects of Declarative Languages (PADL'08), LNCS, Vol. 4902, pages 18--34, Springer Verlag, January 2008.
  346. A. Casas, M. Carro, M. Hermenegildo. Towards a High-Level Implementation of Execution Primitives for Non-restricted, Independent And-parallelism. 10th International Symposium on Practical Aspects of Declarative Languages (PADL'08), LNCS, Vol. 4902, pages 230--247, Springer-Verlag, January 2008.
  347. P. Pietrzak, J. Correas, G. Puebla, M. Hermenegildo. A Practical Type Analysis for Verification of Modular Prolog Programs. ACM SIGPLAN 2008 Workshop on Partial Evaluation and Program Manipulation (PEPM'08), pages 61--70, ACM Press, January 2008.
  348. Anindya Banerjee, Michael Barnett, David A. Naumann. Boogie Meets Regions: A Verification Experience Report. VSTTE, pages 177--191, 2008.
  349. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Expressive Declassification Policies and Modular Static Enforcement. IEEE Symposium on Security and Privacy, pages 339--353, 2008.
  350. Anindya Banerjee, David A. Naumann, Stan Rosenberg. Regional Logic for Local Reasoning about Global Invariants. ECOOP, pages 387--411, 2008.
  351. Gilles Barthe, César Kunz, Jorge Luis Sacchini. Certified Reasoning in Memory Hierarchies. Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Lecture Notes in Computer Science, Vol. 5356, pages 75--90, Springer, 2008.
  352. Gilles Barthe, César Kunz. Certificate Translation in Abstract Interpretation. 17th European Symposium on Programming, ESOP 2008, Lecture Notes in Computer Science, Vol. 4960, pages 368--382, Springer, 2008.
  353. Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese. Preservation of Proof Obligations for Hybrid Verification Methods. Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, pages 127--136, IEEE Computer Society, 2008.
  354. Gilles Barthe, Salvador Cavadini, Tamara Rezk. Tractable Enforcement of Declassification Policies. Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, pages 83--97, IEEE Computer Society, 2008.
  355. Gilles Barthe, Benjamin Grégoire, Colin Riba. Type-Based Termination with Sized Products. Computer Science Logic, 22nd International Workshop, CSL 2008, Lecture Notes in Computer Science, Vol. 5213, pages 493--507, Springer, 2008.
  356. Gilles Barthe, Benjamin Grégoire, Mariela Pavlova. Preservation of Proof Obligations from Java to the Java Virtual Machine. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Lecture Notes in Computer Science, Vol. 5195, pages 83--99, Springer, 2008.
  357. Tom Schrijvers, Maurice Bruynooghe, John P. Gallagher. From Monomorphic to Polymorphic Well-Typings and Beyond. Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 5438, pages 152--167, Springer, 2008.
  358. Gourinath Banda, John P. Gallagher. Analysis of Linear Hybrid Systems in CLP. Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers, Lecture Notes in Computer Science, pages 55--70, Springer, 2008.
  359. John P. Gallagher, Mads Rosendahl. Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation. Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, Lecture Notes in Computer Science, Vol. 5330, pages 682--696, Springer, 2008.
  360. M. Clavel, V. Silva, C. Braga, M. Egea. Model-Driven Security in Practice: An Industrial Experience. Proceedings of Model Driven Architecture - Industrial Track ECMDA-FA '08, Lecture Notes in Computer Science, Vol. 5095, pages 327--338, Springer-Verlag, 2008.
  361. 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.
  362. P. Pietrzak, M. Hermenegildo. Automatic Binding-related Error Diagnosis in Logic Programs. International Conference on Logic Programming (ICLP'07), LNCS, Num. 4670, pages 333--347, Springer-Verlag, September 2007.
  363. 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, Num. 4915, pages 154--168, Springer-Verlag, August 2007.
  364. A. Casas, M. Carro, M. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. 17th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'07), LNCS, Num. 4915, pages 138--153, Springer-Verlag, August 2007.
  365. J.F. Morales, M. Carro, M. Hermenegildo. Towards Description and Optimization of Abstract Machines in an Extension of Prolog. Logic-Based Program Synthesis and Transformation (LOPSTR'06), LNCS, Num. 4407, pages 77--93, July 2007.
  366. Mark Marron, Darko Stefanovic, Manuel Hermenegildo, Deepak Kapur. Heap Analysis in the Presence of Collection Libraries. ACM WS on Program Analysis for Software Tools and Engineering (PASTE'07), ACM, June 2007.
  367. E. Mera, P. López-García, G. Puebla, M. Carro, M. Hermenegildo. Combining Static Analysis and Profiling for Estimating Execution Times. Ninth International Symposium on Practical Aspects of Declarative Languages (PADL'07), LNCS, Num. 4354, pages 140--154, Springer-Verlag, January 2007.
  368. 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.
  369. D. Basin, M. Clavel, J. Doser, M. Egea. A Metamodel-Based Approach for Analyzing Security-Design Models. Proceedings of the Tenth International Conference on Model Driven Engineering Languages and Systems, MODELS '07, Lecture Notes in Computer Science, Vol. 4735, pages 420--435, Springer-Verlag, 2007.
  370. M. Clavel, F. Durán, J. Hendrix, S. Lucas, J. Meseguer, P. C. Ölveczky. The Maude Formal Tool Environment. Algebra and Coalgebra in Computer Science, 2nd International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, Lecture Notes in Computer Science, Vol. 4624, pages 173--178, Springer, 2007.


Books and Monographs

  1. Manuel Carro, Andy King (Eds.). 32nd International Conference on Logic Programming. Vol. 16, Num. 5-6, Cambridge University Press, September 2016.
  2. Manuel Carro, Salvador Tamarit, Guillermo Vigueras, Julio Mariño (Eds.). First International Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016). March 2016.
  3. A. Zaks, M.V. Hermenegildo. Proceedings of the 25th International Conference on Compiler Construction (CC 2016). ACM, March 2016.
  4. Antonio Nappa. Defending Against Cybercrime: Advances in the Detection of Malicious Servers and the Analysis of Client-Side Vulnerabilities. Ph.D. Thesis, Escuela Técnica Superior de Ingenieros Informáticos, Universidad Politécnica de Madrid, Madrid, Spain, February 2016.
  5. 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.
  6. 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.
  7. Juan Caballero, Urko Zurutuza, Ricardo J. Rodríguez. Detection of Intrusions and Malware, and Vulnerability Assessment - 13th International Conference, DIMVA 2016, San Sebastián, Spain, July 7-8, 2016, Proceedings. Lecture Notes in Computer Science, Vol. 9721, Springer, 2016.
  8. 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.
  9. 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.
  10. Alejandro Sánchez. Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures. Ph.D. Thesis, ETS de Ingenieros Informáticos, Technical University of Madrid, September 2015.
  11. Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, Annabelle McIver. Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181). Dagstuhl Reports, Vol. 5, Num. 4, pages 123--141, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015.
  12. 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.
  13. R. Haemmerlé, J. Sneyers. Proceedings of the Eleventh Workshop on Constraint Handling Rules (CHR 2014). CoRR abs/1406.1510, 2014.
  14. Nataliia Stulova. Dynamic Checking of Assertions for Higher-order Predicates. Ms. Thesis, Technical University of Madrid, School of Computer Science, E-28660, Boadilla del Monte, Madrid, Spain, 73 pages, July 2013.
  15. Dragan Ivanovic. Analysis of Service-Oriented Computing Systems. Ph.D. Thesis, School of Computer Science, UPM, January 2013.
  16. R. Haemmerlé, J.F. Morales. Proceedings of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013). CoRR abs/1308.2055, 2013.
  17. Javier Valdazo. Developing Secure Business Applications from Secure BPMN Models. Ms. Thesis, Universidad Complutense de Madrid, Spain, September 2012.
  18. Gustavo Grieco. Typegrapher: Inferring the Type Graph of a Binary Program. Ms. Thesis, Facultad de Ciencias Exactas, Ingenieria y Agrimensura, Universidad Nacional de Rosario, Rosario, Argentina, August 2012.
  19. 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.
  20. 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.
  21. Gilles Barthe, Alberto Pardo, Gerardo Schneider. Software Engineering and Formal Methods - 9th International Conference, SEFM 2011. Lecture Notes in Computer Science, Vol. 7041, Springer, November 2011.
  22. Julián Samborski-Forlese. Two Algorithms for Model Checking of Regular Linear Temporal Logic. Ms. Thesis, Dpto. Sistemas Informáticos y Computación, Universidad Complutense de Madrid, September 2011.
  23. Alejandro Sánchez. Decision Procedures for the Temporal Verification of Concurrent Data Structures. Ms. Thesis, Dpto. Sistemas Informáticos y Computación, Universidad Complutense de Madrid, July 2011.
  24. John P. Gallagher, Michael Gelfond. Theory and Practice of Logic Programming. 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue. Vol. 11 (4--5), pages 429--839, Cambridge University Press, July 2011.
  25. John P. Gallagher, Michael Gelfond. Technical Communications of the 27th International Conference on Logic Programming (ICLP'11). Leibniz International Proceedings in Informatics (LIPIcs), Vol. 11, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2011.
  26. Gilles Barthe. Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011. Lecture Notes in Computer Science, Vol. 6602, Springer, March 2011.
  27. M. Carro, J.H. Reppy. ACM SIGPLAN Proceedings of the Workshop on Declarative Aspects of Multicore Programming. ACM, January 2011.
  28. 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.
  29. M. Hermenegildo, T. Schaub. Theory and Practice of Logic Programming. 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue. Vol. 10 (4--6), pages 361--778, Cambridge University Press, July 2010.
  30. M. Hermenegildo, T. Schaub. Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10). Leibniz International Proceedings in Informatics (LIPIcs), Vol. 7, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2010.
  31. J.F. Morales. Advanced Compilation Techniques for Logic Programming. Ph.D. Thesis, Universidad Politécnica de Madrid (UPM), Facultad Informática UPM, 28660-Boadilla del Monte, Madrid-Spain, July 2010.
  32. G. Barthe, M. Hermenegildo. Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010. LNCS, Num. 5944, Springer, January 2010.
  33. M.V. Hermenegildo, J. Palsberg. Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010). ACM, January 2010.
  34. M. Carro, R. Peña-Mar&\acute;i. Practical Aspects of Declarative Languages -- 12th. International Symposium, PADL 2010. LNCS, Vol. 5937, Springer-Verlag, January 2010.
  35. Rafael Caballero, John P. Gallagher. Proceedings of the 19th Workshop on Logic-based methods in Programming Environments (WLPE 2009). CoRR, abs/1002.4535, 2010.
  36. 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.
  37. Anindya Banerjee. FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs. ACM, 2009.
  38. Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary Leavens, Peter Müller, Tobias Wrigstad. Formal Techniques for Java-Like Programs. Lecture Notes in Computer Science, Vol. 5475, pages 70--76, Springer Berlin / Heidelberg, 2009.
  39. 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.
  40. J. Garrigue, M. Hermenegildo. Functional and Logic Programming, 9th International Symposium, FLOPS'08. LNCS, Num. 4989, Springer, April 2008.
  41. M. Hermenegildo. ACM SIGPLAN-Intel Workshop on Declarative Aspects of Multicore Programming, DAMP'08, Informal Proceedings. January 2008.
  42. 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.
  43. 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.
  44. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. L. Talcott. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. Lecture Notes in Computer Science, Vol. 4350, Springer, 2007.


Invited Papers and Tutorials

  1. 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, pages 146--166, Springer, 2013.
  2. M. 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, Num. 12452, 12 pages, IBFI -- Dagstuhl, November 2012. (available online).
  3. D. Ivanović, M. Carro, M. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. 22nd Workshop on Logic-based Methods in Programming Environments, 1 pages, September 2012. (abstract of invited talk).
  4. 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.
  5. 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, pages 2--3, Springer-Verlag, July 2011. (abstract of invited talk).
  6. John P. Gallagher, Michael Gelfond. Introduction to the 27th International Conference on Logic Programming (ICLP'11) Special Issue. Vol. 11, Num. 4-5, pages 429--432, Cambridge University Press, July 2011.
  7. John P. Gallagher, Michael Gelfond. Introduction to Technical Communications of the 27th Int'l. Conference on Logic Programming (ICLP'11). Technical Communications of the 27th International Conference on Logic Programming (ICLP'11), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 11, pages 1--9, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2011.
  8. M. Hermenegildo, T. Schaub. Introduction to the 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue. Vol. 10, Num. 4--6, pages 361--364, Cambridge University Press, July 2010.
  9. M. Hermenegildo, T. Schaub. Introduction to Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10). Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 7, pages 8--11, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2010.
  10. Anindya Banerjee. Semantics and Enforcement of Expressive Information Flow Policies. Formal Aspects in Security and Trust, Lecture Notes in Computer Science, Vol. 5983, pages 1--3, Springer Berlin / Heidelberg, 2010.
  11. Barthe, Gilles, Grégoire, Benjamin, Heraud, Sylvain, Zanella Béguelin, Santiago. Formal Certification of ElGamal Encryption. A Gentle Introduction to CertiCrypt. 5th International workshop on Formal Aspects in Security and Trust, FAST 2008, Lecture Notes in Computer Science, Vol. 5491, pages 1--19, Springer, 2009.
  12. 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.
  13. M. Hermenegildo, F. Bueno, A. Casas, J. Navas, E. Mera, M. Carro, P. López-García. Automatic Granularity-Aware Parallelization of Programs with Predicates, Functions, and Constraints. DAMP'07, ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, pages 1--1, ACM, January 2007. (abstract of invited talk).


Articles in Books and Other Collections

  1. 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, pages 81--100, Springer, 2016.
  2. Konstantin Kuznetsov, Alessandra Gorla, Ilaria Tavecchia, Florian Gross, Andreas Zeller. Mining Android Apps for Anomalies. The Art and Science of Analyzing Software Data, pages 257--284, Morgan Kaufmann, 2015.
  3. Barthe, Gilles, Dupressoir, François, 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.
  4. K. Georgiou, U. Liqat. Towards LLVM-Based Energy Consumption Analysis of Programs. ICT-Energy (Nanoenergy) Letters, Num. 8, pages 16--17, July 2014.
  5. 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, pages 97--118, 2014.
  6. Kerstin Eder, Steve Kerrison, John Gallagher, Pedro Lopez-Garcia. Whole Systems Energy Transparency. Num. 6, pages 67--68, August 2013.
  7. 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, pages 319--365, Springer, 2013.
  8. Barthe, Gilles, Dupressoir, François, 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, pages 146--166, Springer International Publishing, 2013.
  9. Dave Clarke, Johan Östlund, Ilya Sergey, Tobias Wrigstad. Ownership Types: A Survey. Aliasing in Object-Oriented Programming. Types, Analysis and Verification, LNCS, Vol. 7850, pages 15--58, Springer, 2013.
  10. Juan Caballero, Adam Barth, Dawn Song. Content-Sniffing XSS Attacks: XSS with non-HTML Content. The Death of the Internet, Wiley, July 2012.
  11. 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, pages 229--245, Springer Berlin Heidelberg, 2012.
  12. P. Lopez-Garcia, L. Darmawan, F. Bueno, M. Hermenegildo. Interval-Based Resource Usage Verification: Formalization and Prototype. Foundational and Practical Aspects of Resource Analysis. Second International Workshop FOPARA 2011, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 7177, pages 54--71, Springer-Verlag, 2012.
  13. V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee. Merlin: specification inference for explicit information flow problems. Mining Software Specifications, pages 377--410, Chapman & Hall/CRC, May 2011.
  14. M. Carro, M. V. Hermenegildo. Logic Languages. Encyclopedia of Parallel Computing, pages 1057--1068, Springer, 2011.
  15. Patrick Cousot, Radhia Cousot, Laurent Mauborgne. Logical Abstract Domains and Interpretations. The Future of Software Engineering, pages 48--71, Springer-Verlag, 2011.
  16. Manuel Clavel, Narciso Martí-Oliet, Miguel Palomino. Parameterized Metareasoning in Membership Equational Logic. Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, LNCS, Vol. 7000, pages 277--298, Springer, 2011.
  17. 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, pages 209--237, Springer-Verlag, June 2008.
  18. Gilles Barthe, César Kunz. An Introduction to Certificate Translation. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, Lecture Notes in Computer Science, Vol. 5705, pages 51--95, Springer, 2008.
  19. Gilles Barthe, Benjamin Grégoire, Colin Riba. A Tutorial on Type-Based Termination. Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Lecture Notes in Computer Science, Vol. 5520, pages 100--152, Springer, 2008.
  20. César Sánchez, Matteo Slanina, Henny B. Sipma, Zohar Manna. The Reaction Algebra: A Formal Language for Event Correlation. Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, LNCS, Vol. 4800, pages 586--609, Springer-Verlag, 2008.
  21. Ángel Herranz, Juan José Moreno-Navarro. Modeling and Reasoning about Design Patterns in SLAM-SL. Design Pattern Formalization Techniques, IGI Publishing, March 2007.


Publications in Refereed Workshops

  1. J. Arias. Tabled CLP for Reasoning over Stream Data. 12th ICLP Doctoral Consortium (DI-ICLP'16), 8 pages, OASIcs, October 2016.
  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), September 2016.
  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), September 2016.
  4. 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, March 2016.
  5. 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), March 2016.
  6. 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), March 2016.
  7. 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, pages 1--7, ACM, 11 2016.
  8. 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, pages 22--25, ACM, 11 2016.
  9. 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, pages 1--3, ACM Press, 2016.
  10. J. Hayes, C. Troncoso, G. Danezis . TASP: Towards Anonymity Sets that Persist. 15th Workshop on Privacy in the Electronic Society, WPES, ACM, 2016.
  11. 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.
  12. 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, pages 104--117, 2016.
  13. 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, pages 33--48, 2016.
  14. S. Gurses, C. Troncoso, C. Diaz. Engineering Privacy by Design Reloaded. Amsterdam Privacy Conference 2015, 21 pages, 2015.
  15. 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.
  16. 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 pages, 2015. arXiv:1512.09369.
  17. 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, pages 1--14, 2015. arXiv:1512.03862.
  18. 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 pages, September 2014.
  19. 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 pages, RWTH Aachen University, July 2014. http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2014.
  20. 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, pages 53--67, EPTCS, 2014.
  21. 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), September 2013.
  22. A. Serrano, P. Lopez-Garcia, M. 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 pages, August 2013. CoRR abs/1308.3940.
  23. 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), August 2013.
  24. 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), August 2013.
  25. 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, May 2013.
  26. Á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.
  27. Javier Reyes, Juan M. Orduña, Guillermo Vigueras, Rafael Tornero. Acceleration of Communication-Aware Task Mapping Techniques through GPU Computing. AINA Workshops, pages 843--848, 2013.
  28. 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), October 2012. Available at (available online).
  29. R. Haemmerlé. Coinductive Proofs over Streams as CHR Confluence Proofs. 9th Int'l Workshop on Constraint Handling Rules (CHR 2012), September 2012.
  30. Z. Drey, J.F. Morales, M. V. Hermenegildo. Reversible Language Extensions and their Application in Debugging. 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS 2012), 15 pages, September 2012.
  31. E.J. Gallego Arias, R. Haemmerlé, M. V. Hermenegildo, J.F. Morales . The Ciao CLP(FD) Library: A Modular CLP Extension for Prolog. 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS 2012), 15 pages, September 2012.
  32. 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), July 2012.
  33. 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), July 2012.
  34. 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, pages 931--937, IEEE Press, June 2012.
  35. Á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.
  36. D. Ivanović, M. Carro, M. Hermenegildo. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations. XII Jornadas sobre Programación y Lenguajes (PROLE), Universidad de Almería, 2012.
  37. 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.
  38. P. Chico de Guzmán, M. Carro, M. Hermenegildo, P. Stuckey. A General Implementation Framework for Tabled CLP. XII Jornadas sobre Programaciń y Lenguajes (PROLE), Universidad de Almería, 2012.
  39. Carolina Dania. Modeling Social Networking Privacy. ESSoS-DS 2012. Doctoral Symposium, Workshop Proceedings, Vol. 834, pages 49--54, CEUR, 2012.
  40. Fangzhe Chang, Pavithra Prabhakar, Ramesh Viswanathan. Behavior Based Service Composition. Web Services and Formal Methods - 8th International Workshop, WS-FM 2011, Clermont-Ferrand, France, September 1-2, 2011, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 7176, pages 17--31, Springer, 2012.
  41. F. Bueno, M. García de la Banda, M. V. Hermenegildo, P. López-García, E. Mera, P. J. Stuckey. Towards Resource Usage Analysis of MiniZinc Models. MiniZinc Workshop (MZN'11), 15 pages, September 2011.
  42. P. Lopez-Garcia, L. Darmawan, F. Bueno, M. Hermenegildo. Interval-based Resource Usage Verification: Formalization and Prototype. 2nd International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'2011), May 2011.
  43. Á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.
  44. M. V. Hermenegildo, F. Bueno, M. Carro, P. López, E. Mera, J.F. Morales, G. Puebla. The Ciao Approach to the Dynamic vs. Static Language Dilemma. Proceedings for the International Workshop on Scripts to Programs, STOP'11, 4 pages, ACM, 2011.
  45. D. Ivanović, M. Carro, M. Hermenegildo. An Initial Proposal for Data-Aware Resource Analysis of Orchestrations with Applications to Predictive Monitoring. International Workshops, ICSOC/ServiceWave 2009, Revised Selected Papers, LNCS, Num. 6275, Springer, September 2010.
  46. Á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.
  47. Á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), pages 3--7, July 9 2010.
  48. R. Haemmerlé. (Co)inductive Semantics for Constraint Handling Rules. Annual ERCIM Workshop on Constraint Solving and Constraint Logic Programming, 2010.
  49. D. Ivanović, M. Carro, M. Hermenegildo. An Initial Proposal for Data-Aware Resource Analysis of Orchestrations with Applications to Proactive Monitoring. Pre-proceedings of the 2nd Workshop on Monitoring, Adaptation and Beyond (MONA+), November 2009.
  50. L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo. Program Parallelization using Synchronized Pipelining. Pre-proceedings of the 19th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'09), September 2009.
  51. D. Ivanović, J.F. Morales, M. Carro, M. Hermenegildo. Towards Structured State Threading in Prolog. CICLOPS 2009, 15 pages, July 2009.
  52. J. Navas, M. Méndez-Lojo, M. Hermenegildo. User-Definable Resource Usage Bounds Analysis for Java Bytecode. Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09), Electronic Notes in Theoretical Computer Science, Vol. 253, Num. 5, pages 65--82, Elsevier - North Holland, March 2009.
  53. P. Chico de Guzmán, M. Carro, M. Hermenegildo. A Program Transformation for Continuation Call-Based Tabled Execution. Colloquium on Implementation of Constraint and LOgic Programming Systems (ICLP associated workshop), 15 pages, University of Udine, December 2008.
  54. G. Marpons, J. Mariño, M. Carro, A. Herranz, L.Å. Fredlund, J.J. Moreno-Navarro, A. Polo. A Coding Rule Conformance Checker Integrated into GCC. VIII Jornadas sobre Programación y Lenguajes, PROLE 2008, pages 245--249, October 2008.
  55. Pablo Nogueira, Juan José Moreno-Navarro. Bialgebra Views: A Way for Polytypic Programming to Cohabit with Data Abstraction. Proceedings of the 2nd ACM SIGPLAN Workshop on Generic Programming (ICFP-WGP'08), pages 61--73, ACM Press, September 2008.
  56. M. Méndez-Lojo, O. Lhoták, M. Hermenegildo. Efficient Set Sharing using ZBDDs. 21st Int'l. WS on Languages and Compilers for Parallel Computing (LCPC'08), LNCS, Springer-Verlag, August 2008.
  57. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo. Two Efficient Representations for Set-Sharing Analysis in Logic Programs . 17th International Workshop on Functional and (Constraint) Logic Programming, WFLP'08, 15 pages, July 2008.
  58. 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, July 2008.
  59. 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), pages 29--32, April 2008. Extended Abstract.
  60. Gilles Barthe, César Kunz. Certificate Translation for Specification-Preserving Advices. Proceedings of the 7th Workshop on Foundations of Aspect-Oriented Languages, FOAL 2008, pages 9--18, ACM, 2008.
  61. G. Marpons-Ucero, J. Mariño, A. Herranz, L.Å. Fredlund, M. Carro, J.J. Moreno-Navarro. Automatic Coding Rule Conformance Checking Using Logic Programs. 17th Workshop on Logic-based methods in Programming Environments, WLPE 2007, September 2007.
  62. P. Chico de Guzmán, M. Carro, M. Hermenegildo, Claudio Silva, Ricardo Rocha. Some Improvements over the Continuation Call Tabling Implementation Technique. Colloquium on Implementation of Constraint and LOgic Programming Systems (ICLP associated workshop), 15 pages, Universidade do Porto, September 2007.
  63. A. Casas, M. Carro, M. Hermenegildo. Towards High-Level Execution Primitives for And-Parallelism: Preliminary Results. Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS'07, ICLP associated workshop), 15 pages, U. of Evora, September 2007.
  64. J. Navas, M. Méndez-Lojo, M. Hermenegildo. An Efficient, Context and Path Sensitive Analysis Framework for Java Programs. 9th Workshop on Formal Techniques for Java-like Programs FTfJP 2007, 12 pages, July 2007.
  65. A. Casas, M. Carro, M. Hermenegildo. Towards A High-Level Implementation of Flexible Parallelism Primitives for Symbolic Languages. Parallel Symbolic Computation (PASCO'07), 2 pages, ACM Press, July 2007. Extended Abstract.
  66. M. Hermenegildo, The Ciao Development Team. An Overview of The Ciao Multiparadigm Language and Program Development Environment and its Design Philosophy. ECOOP Workshop on Multiparadigm Programming with Object-Oriented Languages MPOOL 2007, July 2007.
  67. M. Méndez-Lojo, J. Navas, M. Hermenegildo. An Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode. ETAPS Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2007), Electronic Notes in Theoretical Computer Science, Elsevier - North Holland, March 2007.


Technical Reports and Manuals

  1. Pierre Ganty, Boris Köpf, Pedro Valero. A Language-theoretic View on Network Protocols. 2016.
  2. Goran Doychev, Boris Köpf. Rigorous Analysis of Software Countermeasures against Cache Attacks. 2016.
  3. Miguel Ambrona, Gilles Barthe, Benedikt Schmidt. Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. 30 pages, IACR Cryptology ePrint Archive, 2016.
  4. P. Lopez-Garcia, R. Haemmerlé, U. Liqat, M. Klemen, M. V. Hermenegildo. Parametric Static Profiling. Num. CLIP-2/2015.0, The CLIP Lab, April 2015.
  5. Guillermo Vigueras, Salvador Tamarit, Manuel Carro, Julio Mariño. Towards a Rule-Based Approach to Generate High-Performance Scientific Code. Num. CLIP1/2015.0, 8 pages, The CLIP Lab, March 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. Num. CLIP2/2014.0, 12 pages, Technical University of Madrid (UPM), July 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. June 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. Num. CLIP-1/2014.0, 25 pages, The CLIP Lab, January 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. Num. TR-IMDEA-SW-2012-001, IMDEA Software Institute, August 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. Hermenegildo, R. Haemmerlé, P. López-García, E. Mera, and J.F. Morales, G. Puebla-(Eds.). The Ciao System. Ref. Manual (V1.14). July 2011. Available at http://ciao-lang.org.
  17. M. Hermenegildo, J.F. Morales. The LPdoc Documentation Generator. Ref. Manual (V3.0). July 2011. Available at http://ciao-lang.org.
  18. R. Haemmerlé. Toward Observational Equivalences for Linear Logic Concurrent Constraint Languages. Num. CLIP5/2011.0, 32 pages, Technical University of Madrid (UPM), May 2011.
  19. P. López-García, L. Darmawan, F. Bueno, M. Hermenegildo. Towards Resource Usage Function Verification based on Input Data Size Intervals. Num. CLIP4/2011.0, Technical University of Madrid (UPM), April 2011. Available at http://cliplab.org/papers/resource-verif-11-tr.pdf.
  20. R. Haemmerlé. Towards a Logically Complete Fixpoint Semantics for Constraint Handling Rules. Num. CLIP3/2011.0, 31 pages, Technical University of Madrid (UPM), March 2011.
  21. P. Chico de Guzmán, A. Casas, M. Carro, M. Hermenegildo. A Simulation Study on Parallel Backtracking with Solution Memoing for Independent And-Parallelism. Num. CLIP1/2011.0, 12 pages, Technical University of Madrid (UPM), January 2011.
  22. J.F. Morales, M. Hermenegildo, R. Haemmerlé. Towards Modular Extensions for a Modular Language. Num. CLIP2/2011.0, 15 pages, Technical University of Madrid (UPM), January 2011.
  23. Alexander Malkis. On the strength of Owicki-Gries for resources. 2011. Technical report, (available online).
  24. D. Ivanović, M. Carro, M. Hermenegildo. Automated Attribute Inference in Complex Service Workflows Based on Sharing Analysis. Num. CLIP5/2010.0, Technical University of Madrid (UPM), December 2010.
  25. D. Ivanović, M. Carro, M. V. Hermenegildo. Automatic Fragment Identification in Workflows Based on Sharing Analysis. Num. CLIP4/2010.0, 15 pages, Technical University of Madrid (UPM), June 2010. Submitted.
  26. E. Mera, T. Trigo, P. López-García, M. Hermenegildo. An Approach to Profiling for Run-Time Checking of Computational Properties and Performance Debugging. Num. CLIP3/2010.0, 29 pages, Technical University of Madrid (UPM), March 2010.
  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. Num. CLIP2/2010.0, Technical University of Madrid (UPM), March 2010. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).
  28. D. Ivanović, M. Carro, M. Hermenegildo, P. López, E. Mera. Towards Data-Aware Cost-Driven Adaptation for Service Orchestrations. Num. CLIP5/2009.1, Technical University of Madrid (UPM), March 2010.
  29. P. López-García, L. Darmawan, F. Bueno, M. Hermenegildo. Towards a Framework for Resource Usage Verification and Debugging in the CiaoPP System. Num. CLIP1/2010.0, Technical University of Madrid (UPM), February 2010. Available at http://cliplab.org/papers/resource-verif-10-tr.pdf.
  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. Hermenegildo. Sharing-Based Independence-Driven Fragment Identification for Service Orchestrations. Num. CLIP7/2009.0, Technical University of Madrid (UPM), December 2009.
  33. D. Ivanović, M. Carro, M. Hermenegildo, P. López, E. Mera. Towards Data-Aware Cost-Driven Adaptation for Service Orchestrations. Num. CLIP5/2009.0, Technical University of Madrid (UPM), November 2009. Replaced by a later version.
  34. J.F. Morales, M. Carro, M. Hermenegildo. Description and Optimization of Abstract Machines in a Dialect of Prolog. Num. CLIP4/2009.0, Technical University of Madrid (UPM), October 2009.
  35. D. Ivanović, M. Carro, M. Hermenegildo. Towards Data-Aware Resource Analysis for Service Orchestrations. Num. CLIP3/2009.0, Technical University of Madrid (UPM), June 2009.
  36. E. Mera, P. López-García, M. Hermenegildo. Towards Integrating Run-Time Checking and Software Testing in a Verification Framework. Num. CLIP1/2009.0, 19 pages, Technical University of Madrid (UPM), March 2009.
  37. P. López-García, F. Bueno, M. Hermenegildo. Inferring Determinacy and Mutual Exclusion in Logic Programs Using Mode and Type Analysis. Num. CLIP2/2009.0, Technical University of Madrid (UPM), February 2009.
  38. F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. López-García, G. Puebla-(Eds.). The Ciao System. Ref. Manual (V1.13). 2009. Available at http://ciao-lang.org.
  39. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Bounded Underapproximations. 2009.
  40. E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo. Efficient Representations for Set-Sharing Analysis. Num. CLIP9/2008.0, University of New Mexico and Technical University of Madrid, September 2008.
  41. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. Bridge Program Transformation for the CCall Tabling Scheme. Num. CLIP6/2008.0, Technical University of Madrid (UPM), September 2008.
  42. A. Casas, M. Carro, M. Hermenegildo. A High-Level Implementation of Non-Deterministic, Unrestricted, Independent And-Parallelism. Num. TR-CS-2008-10, University of New Mexico (UNM), September 2008.
  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. Num. CLIP5/2008.0, Technical University of Madrid (UPM), July 2008.
  44. M. Méndez-Lojo, O. Lhoták, M. Hermenegildo. Fast Set Sharing using ZBDDs. University of New Mexico, June 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. Num. CLIP3/2008.0, Technical University of Madrid (UPM), April 2008.
  46. J. Navas, M. Méndez-Lojo, M. Hermenegildo. Customizable Resource Usage Analysis for Java Bytecode. Num. UNM TR-CS-2008-02 - CLIP1/2008.0, University of New Mexico, January 2008.
  47. A. Casas, M. Carro, M. Hermenegildo. Automatic Unrestricted Independent And-Parallelism in Logic Programs. Num. CLIP11/2007.0, Technical University of Madrid (UPM), December 2007. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).
  48. M. Méndez-Lojo, M. Hermenegildo. Precise Set Sharing for Java-style Programs (and proofs). Num. CLIP2/2007.1, Technical University of Madrid (UPM), November 2007.
  49. A. Casas, M. Carro, M. Hermenegildo. Towards a High-Level Implementation of Execution Primitives for Non-restricted, Independent And-parallelism. Num. TR-CS-2007-16, University of New Mexico (UNM), October 2007.
  50. A. Casas, M. Carro, M. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. Num. TR-CS-2007-14, University of New Mexico (UNM), September 2007.
  51. E. Mera, P. López-García, M. Carro, M. Hermenegildo. Towards Execution Time Estimation in Abstract Machine-Based (Logic) Languages. Num. CLIP8/2007.0, Technical University of Madrid (UPM), August 2007.
  52. G. Marpons, J. Mariño, M. Carro, A. Herranz, J.J. Moreno-Navarro, L.Å. Fredlund. Automatic Coding Rule Conformance Checking Using Logic Programming. Num. CLIP6/2007.0, Technical University of Madrid (UPM), August 2007.
  53. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo. An Improved Continuation Call-Based Implementation of Tabling. Num. CLIP9/2007.0, Technical University of Madrid (UPM), August 2007.
  54. A. Casas, M. Carro, M. V. Hermenegildo. Towards a High-Level Implementation of Execution Primitives for Non-Restricted, Independent And-Parallelism. Num. CLIP7/2007.0, Technical University of Madrid (UPM), August 2007.
  55. A. Casas, M. Carro, M. Hermenegildo. Annotation Algorithms for Unrestricted Independent And-Parallelism in Logic Programs. Num. CLIP5/2007.0, Technical University of Madrid (UPM), June 2007.
  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. Num. CLIP4/2007.0, Technical University of Madrid (UPM), March 2007.
  57. M. Méndez-Lojo, M. Hermenegildo. Precise Set Sharing and Nullity Analysis for Java-style Programs. Num. CLIP2/2007.0, Technical University of Madrid (UPM), February 2007.
  58. P. López-García, F. Bueno, M. Hermenegildo. Inferring Determinacy in Logic Programs Using Mode and Type Information. Num. CLIP3/2007.0, Technical University of Madrid (UPM), February 2007.