Articles in Refereed Journals (219)

1. A decade of code comment quality assessment: A systematic literature review
   Pooja Rani, Arianna Blasi, Nataliia Stulova, Sebastiano Panichella, Alessandra Gorla, Oscar Nierstrasz.
   Journal of Systems and Software 195, 111515. 2023.
2. On Composing Finite Forests with Modal Logics
   Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti.
   ACM Transactions on Computational Logic. 2023.
3. Safe Couplings: Coupled Refinement Types
   Elizaveta Vasilenko, Niki Vazou, Gilles Barthe.
   Proceedings of the ACM on Programming Languages 6 (ICFP). Association for Computing Machinery, August 2022.
4. Protecting Software and the Systems that use it Against Cyber Threats
   Juan Caballero, Alessandra Gorla, Marco Guarnieri.
   Notiweb, 12-16. June 2022.
5. Fifty Years of Prolog and Beyond
   Philipp Körner, Michael Leuschel, João Barbosa, Vítor Santos-Costa, Verónica Dahl, Manuel V. Hermenegildo, Jose F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu, Giovanni Ciatto.
   Theory and Practice of Logic Programming FirstView, 1–86. Cambridge U. Press, May 2022.
6. Parallel Logic Programming: A Sequel
   Agostino Dovier, Andrea Formisano, Gopal Gupta, Manuel V. Hermenegildo, Enrico Pontelli, Ricardo Rocha.
   Theory and Practice of Logic Programming FirstView, 1–69. Cambridge U. Press, March 2022.
7. Visibility Reasoning for Concurrent Snapshot Algorithms
   Joakim Öhman, Aleksandar Nanevski.
   Proceedings of the ACM on Programming Languages 6 (POPL). Association for Computing Machinery, January 2022.
8. CoqQ: Foundational Verification of Quantum Programs
   Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying.
   ACM SIGACT Symposium on Principles of Programming Languages abs/2207.11350. 2022.
9. A formal treatment of the role of verified compilers in secure computation
   José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela.
   J. Log. Algebraic Methods Program. 125, 100736. 2022.
10. Universal Equivalence and Majority of Probabilistic Programs over Finite Fields
    Gilles Barthe, Charlie Jacomme, Steve Kremer.
    ACM Transactions on Computational Logic 23 (1), 5:1–5:42. 2022.
11. Anonymity and rewards in peer rating systems
    Lydia Garms, Siaw-Lynn Ng, Elizabeth A. Quaglia, Giulia Traverso.
    Journal of Computer Security 30 (1), 109–165. IOS Press, 2022.
12. Combatting Energy Issues for Mobile Applications
    Xueliang Li, Junyang Chen, Yepang Liu, Kaishun Wu, John P. Gallagher.
    ACM Transactions on Software Engineering and Methodology 32 (1), 1–44. Association for Computing Machinery, 2022.
13. Making Byzantine consensus live
    Manuel Bravo, Gregory Chockler, Alexey Gotsman.
    Distributed Computing 35 (6), 503–532. Springer, 2022.
14. Building Information Modeling Using Constraint Logic Programming
    Joaquín Arias, Seppo Törmä, Manuel Carro, Gopal Gupta.
    Theory and Practice of Logic Programming 22 (5), 723–738. 2022.
15. REST: Integrating Term Rewriting with Program Verification (Artifact)
    Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers.
    Dagstuhl Artifacts Series 8 (2), 12:1–12:2. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022.
16. An Auxiliary Logic on Trees: on the Tower-hardness of Logics Featuring Reachability and Submodel Reasoning
    Alessio Mansutti.
    Information and Computation. 2022.
17. Introduction to the 38th International Conference on Logic Programming Special Issue
    Yuliya Lierler, José F. Morales.
    Theory and Practice of Logic Programming 22 (4), 499–504. 2022.
18. Introduction to the 38th International Conference on Logic Programming Special Issue II
    Yuliya Lierler, José F. Morales.
    Theory and Practice of Logic Programming 22 (5), 640–640. 2022.
19. Replicomment: identifying clones in code comments
    Arianna Blasi, Nataliia Stulova, Alessandra Gorla, Oscar Nierstrasz.
    Journal of Systems and Software 182. December 2021.
20. MeMo: Automatically identifying metamorphic relations in Javadoc comments for test automation
    Arianna Blasi, Alessandra Gorla, Michael D. Ernst, Mauro Pezzè, Antonio Carzaniga.
    Journal of Systems and Software 181. November 2021.
21. Complete Abstractions for Checking Language Inclusion
    Pierre Ganty, Francesco Ranzato, Pedro Valero.
    ACM Transactions on Computational Logic 22 (4). Association for Computing Machinery, September 2021.
22. VeriFly: On-the-fly Assertion Checking via Incrementality
    M.A. Sanchez-Ordaz, I. Garcia-Contreras, V. Perez-Carrasco, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
    Theory and Practice of Logic Programming 21 (6), 768–784. Cambridge U. Press, September 2021.
23. Contextual Modal Types for Algebraic Effects and Handlers
    Nikita Zyuzin, Aleksandar Nanevski.
    International Conference on Functional Programming 5 (ICFP). Association for Computing Machinery, August 2021.
24. A Survey of Binary Code Similarity
    Irfan Ul Haq, Juan Caballero.
    ACM Computing Surveys 54 (3). April 2021.
25. Incremental and Modular Context-sensitive Analysis
    I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
    Theory and Practice of Logic Programming 21 (2), 196–243. January 2021.
26. Hardware security without secure hardware: How to decrypt with a password and a server
    Olivier Blazy, Laura Brouilhet, Celine Chevalier, Patrick Towa, Ida Tucker, Damien Vergnaud.
    Electronic Notes in Theoretical Computer Science 895, 178-211. 2021.
27. A note on secure multiparty computation via higher residue symbols
    Ignacio Cascudo, Reto Schnyder.
    Journal of Mathematical Cryptology 15 (1), 284–297. 2021.
28. A pre-expectation calculus for probabilistic sensitivity
    Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.
    ACM SIGACT Symposium on Principles of Programming Languages 5 ({POPL}), 1–28. 2021.
29. Higher-order probabilistic adversarial computations: categorical semantics and program logics
    Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato.
    Proceedings of the ACM on Programming Languages 5 ({ICFP}), 1–30. 2021.
30. On algebraic abstractions for concurrent separation logics
    Františsek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas.
    ACM SIGACT Symposium on Principles of Programming Languages 5 ({POPL}), 1–32. 2021.
31. Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification
    Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth.
    IACR Trans. Cryptogr. Hardw. Embed. Syst. 2021 (2), 189–228. 2021.
32. Analysis and Transformation of Constrained Horn Clauses for Program Verification
    Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, Maurizio Proietti.
    Theory and Practice of Logic Programming First view, 1–69. Cambridge University Press, 2021.
33. Preface
    John P. Gallagher, Martin Sulzmann.
    Science of Computer Programming 202, 102577. 2021.
34. Controlled Functional Encryption Revisited: Multi-Authority Extensions and Efficient Schemes for Quadratic Functions
    Miguel Ambrona, Dario Fiore, Claudio Soriente.
    Privacy Enhancing Technologies Symposium 2021 (1), 21 - 42. Sciendo, 2021.
35. Refinement Types: A Tutorial
    Ranjit Jhala, Niki Vazou.
    Foundations and Trends® in Programming Languages 6 (3–4), 159-317. 2021.
36. A compiler for multi-key homomorphic signatures for Turing machines
    Somayeh Dolatnezhad Samarin, Dario Fiore, Daniele Venturi, Morteza Amini.
    Electronic Notes in Theoretical Computer Science 889, 145-170. 2021.
37. Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming
    Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
    Theory and Practice of Logic Programming, 1–30. Cambridge University Press, 2021.
38. Multi-Shot Distributed Transaction Commit
    Gregory Chockler, Alexey Gotsman.
    Distributed Computing 34 (4), 301–318. Springer, 2021.
39. Specification and Space Complexity of Collaborative Text Editing
    Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, Marek Zawirski.
    Electronic Notes in Theoretical Computer Science 855, 141–160. Elsevier, 2021.
40. Stream runtime verification of real-time event streams with the Striver language
    Felipe Gorostiaga, César Sánchez.
    International Journal on Software Tools for Technology Transfer 23, 157–183. 2021.
41. Symbolic AI for XAI: Evaluating LFIT Inductive Programming for Explaining Biases in Machine Learning
    Alfonso Ortega, Julian Fierrez, Aythami Morales, Zilong Wang, Marina de la Cruz, César Luis Alonso, Tony Ribeiro.
    Computers 10 (11), 154. Multidisciplinary Digital Publishing Institute, 2021.
42. Weakest Preconditions in Fibrations
    Alejandro Aguirre, Shin-ya Katsumata.
    Mathematical Structures in Computer Science 352, 5–27. 2020.
43. Squares of matrix-product codes
    Ignacio Cascudo, Jaron Skovsted Gundersen, Diego Ruano.
    Finite Fields and Their Applications 62. 2020.
44. Decentralized Privacy-Preserving Proximity Tracing
    Carmela Troncoso, Mathias Payer, Jean-Pierre Hubaux, Marcel Salathé, James R. Larus, Wouter Lueks, Theresa Stadler, Apostolos Pyrgelis, Daniele Antonioli, Ludovic Barman, Sylvain Chatel, Kenneth G. Paterson, Srdjan Capkun, David A. Basin, Jan Beutel, Dennis Jackson, Marc Roeschlin, Patrick Leu, Bart Preneel, Nigel P. Smart, Aysajan Abidin, Seda Gurses, Michael Veale, Cas Cremers, Michael Backes, Nils Ole Tippenhauer, Reuben Binns, Ciro Cattuto, Alain Barrat, Dario Fiore, Manuel Barbosa, Rui Oliveira, José Pereira.
    IEEE Data Engineering Bulletin 43 (2), 36–66. 2020.
45. System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory
    Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie.
    Journal of Automated Reasoning 64 (8), 1685–1729. 2020.
46. Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations
    Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub.
    Journal of Cryptographic Engineering 10 (1), 17–26. 2020.
47. Privacy Profiles and Amplification by Subsampling
    Borja Balle, Gilles Barthe, Marco Gaboardi.
    Journal of Privacy and Confidentiality 10 (1). 2020.
48. Formal verification of a constant-time preserving C compiler
    Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu.
    ACM SIGACT Symposium on Principles of Programming Languages 4 ({POPL}), 7:1–7:30. 2020.
49. A probabilistic separation logic
    Gilles Barthe, Justin Hsu, Kevin Liao.
    ACM SIGACT Symposium on Principles of Programming Languages 4 ({POPL}), 55:1–55:30. 2020.
50. Relational proofs for quantum programs
    Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou.
    ACM SIGACT Symposium on Principles of Programming Languages 4 ({POPL}), 21:1–21:29. 2020.
51. Liquidate your assets: reasoning about resource usage in liquid Haskell
    Martin A. T. Handley, Niki Vazou, Graham Hutton.
    ACM SIGACT Symposium on Principles of Programming Languages 4 ({POPL}), 24:1–24:27. 2020.
52. Preface, Special Issue on LOPSTR 2017
    Fabio Fioravanti, John P. Gallagher, Maurizio Proietti.
    Fundam. Inform. 173 (4). 2020.
53. Stream Runtime Verification of Real-Time Event-Streams with the Striver Language
    Felipe Gorostiaga, César Sánchez.
    International Journal on Software Tools for Technology Transfer. 2020.
54. Runtime verification of real-time event streams under non-synchronized arrival
    Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, Alexander Schramm.
    Software Quality Journal 28 (2), 745–787. 2020.
55. Verifying replicated data types with typeclass refinements in Liquid Haskell
    Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou.
    ACM Conference on Object Oriented Programming Systems Languages and Applications 4 (OOPSLA), 1–30. ACM New York, NY, USA, 2020.
56. Fireplug: Efficient and Robust Geo-Replication of Graph Databases
    R. Neiheiser, L. Rech, M. Bravo, L. Rodrigues, M. Correia.
    IEEE Transactions on Parallel and Distributed Systems 31 (8), 1942–1953. 2020.
57. Proving Highly-Concurrent Traversals Correct
    Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham.
    ACM Conference on Object Oriented Programming Systems Languages and Applications 4 ({OOPSLA}), 128:1–128:29. 2020.
58. Gray-Box Monitoring of Hyperproperties with an Application to Privacy
    Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonarkdarpour.
    Formal Methods in System Design, 1–36. 2020.
59. The MalSource Dataset: Quantifying Complexity and Code Reuse in Malware Development
    Alejandro Calleja, Juan Tapiador, Juan Caballero.
    IEEE Transactions on Information Forensics and Security 14 (12), 3175-3190. IEEE, December 2019.
60. A survey of challenges for runtime verification from advanced application domains (beyond software)
    César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yliès Falcone, Adrian Francalanza, Srdan Krstic, João M. Lourenço, Dejan Nickovic, Gordon J. Pace, José Rufino, Julien Signoles, Dmitriy Traytel, Alexander Weiss.
    Formal Methods in System Design 54 (3), 279–335. November 2019.
61. Specifying concurrent programs in separation logic: morphisms and simulations
    Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas.
    ACM Conference on Object Oriented Programming Systems Languages and Applications 3 ({OOPSLA}), 1–30. ACM, October 2019.
62. Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis
    Jesús J. Doménech, John P. Gallagher, Samir Genaim.
    Theory and Practice of Logic Programming 19 (5-6), 990–1005. Cambridge University Press, September 2019.
63. Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP
    Joaquín Arias, Manuel Carro.
    Theory and Practice of Logic Programming 19 (5-6), 1107–1123. September 2019.
64. Multi-key homomorphic authenticators
    Dario Fiore, Aikaterini Mitrokotsa, Luca Nizzardo, Elena Pagnin.
    IET Information Security 13 (6), 618–638. Institution of Engineering and Technology, April 2019.
65. Automated Analysis of Cryptographic Assumptions in Generic Group Models
    Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt.
    Journal of Cryptology 32 (2), 324–360. April 2019.
66. On the Incomparability of Cache Algorithms in Terms of Timing Leakage
    Pablo Cañones, Boris Köpf, Jan Reineke.
    Logical Methods in Computer Science 15 (1). March 2019.
67. A^2I: abstract^2 interpretation
    Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato.
    ACM SIGACT Symposium on Principles of Programming Languages 3 ({POPL}), 1–31. ACM, January 2019.
68. Costly Freeware: A Systematic Analysis of Abuse in Download Portals
    Richard Rivera, Platon Kotzias, Avinash Sudhodanan, Juan Caballero.
    IET Information Security 13 (1), 27–35. IET, January 2019.
69. When Are Prime Formulae Characteristic?
    Luca Aceto, Dario Della Monica, Ignacio Fábregas, Anna Ingólfsdóttir.
    Electronic Notes in Theoretical Computer Science 777, 3–31. 2019.
70. Logical characterisations, rule formats and compositionality for input-output conformance simulation
    Luca Aceto, Ignacio Fábregas, Carlos Gregorio-Rodríguez, Anna Ingólfsdóttir.
    Journal of Logical and Algebraic Methods in Programming 106, 78–106. 2019.
71. Rule Formats for Nominal Process Calculi
    Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, Yolanda Ortega-Mallén.
    Logical Methods in Computer Science 15 (4). 2019.
72. Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
    Patrick Baillot, Gilles Barthe, Ugo Dal Lago.
    Journal of Automated Reasoning 63 (4), 813–855. 2019.
73. System-Level Non-interference of Constant-Time Cryptography. Part I: Model
    Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna.
    Journal of Automated Reasoning 63 (1), 1–51. 2019.
74. A relational logic for higher-order programs
    Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
    Journal of Functional Programming 29, e16. 2019.
75. Program for TPDP 2016
    Gilles Barthe, Christos Dimitrakakis, Marco Gaboardi, Andreas Haeberlen, Aaron Roth, Aleksandra B. Slavkovic.
    Journal of Privacy and Confidentiality 9 (1). 2019.
76. Relational ⋆-Liftings for differential privacy
    Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub.
    Logical Methods in Computer Science 15 (4). 2019.
77. LWeb: information flow security for multi-tier web applications
    James Parker, Niki Vazou, Michael Hicks.
    ACM SIGACT Symposium on Principles of Programming Languages 3 ({POPL}), 1–30. 2019.
78. Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization
    Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.
    ACM SIGACT Symposium on Principles of Programming Languages 3 ({POPL}), 38:1–38:30. 2019.
79. Synthesis of verifiable concurrent Java components from formal models
    Julio Mariño, Raúl N. N. Alborodo, Lars-Åke Fredlund, Ángel Herranz-Nieva.
    Software and Systems Modeling 18 (1), 71–105. 2019.
80. The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus
    Álvaro García-Pérez, Pablo Nogueira.
    Journal of Functional Programming 29 (E7), 1–38. Cambridge University Press, 2019.
81. doppioDB 1.0: Machine Learning inside a Relational Engine
    Gustavo Alonso, Zsolt Istvan, Kaan Kara, Muhsen Owaida, David Sidler.
    IEEE Data Engineering Bulletin 42 (2), 19–31. 2019.
82. The Glass Half Full: Using Programmable Hardware Accelerators in Analytics
    Zsolt István.
    IEEE Data Engineering Bulletin 42 (1), 49–60. 2019.
83. I Can't Believe It's Not (Only) Software! Bionic Distributed Storage for Parquet Files
    Lucas Kuhring, Zsolt István.
    International Conference on Very Large Databases 12 (12), 1838–1841. VLDB Endowment, 2019.
84. A General Methodology for Energy-efficient Scheduling in Multicore Environments based on Evolutionary Algorithms
    Zorana Banković, Umer Liqat, Pedro Lopez-Garcia.
    Journal of Multiple-Valued Logic and Soft Computing 32 (3-4), 313–341. Old City Publishing, 2019.
85. Code obfuscation against abstraction refinement attacks
    Roberto Bruni, Roberto Giacobazzi, Roberta Gori.
    Formal Aspects of Computing: applicable formal methods 30 (6), 685–711. November 2018.
86. Homomorphic signatures with sublinear public keys via asymmetric programmable hash functions
    Dario Catalano, Dario Fiore, Nizzardo Luca.
    Design, Codes and Cryptography 86 (10), 2197–2246. October 2018.
87. Malware Lineage in the Wild
    Irfan Ul Haq, Sergio Chica, Juan Caballero, Somesh Jha.
    Computers and Security 78, 347–363. Elsevier, August 2018.
88. Active Pages 20 Years Later: Active Storage for the Cloud
    Zsolt István, David Sidler, Gustavo Alonso.
    IEEE Internet Computing 22 (4), 6–14. July 2018.
89. A Logical Analysis of Framing for Specifications with Pure Method Calls
    Anindya Banerjee, David A. Naumann, Mohammad Nikouei.
    ACM Transactions on Programming Languages and Systems 40 (2), 1–90. ACM, May 2018.
90. Some Trade-offs in Reducing the Overhead of Assertion Run-time Checks via Static Analysis
    N. Stulova, J. F. Morales, M. V. Hermenegildo.
    Science of Computer Programming 155, 3–26. Elsevier, April 2018.
91. Tree dimension in verification of constrained Horn clauses
    Bishoksan Kafle, John P. Gallagher, Pierre Ganty.
    Theory and Practice of Logic Programming 18 (2), 224–251. March 2018.
92. Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption
    P. Lopez-Garcia, L. Darmawan, M. Klemen, U. Liqat, F. Bueno, M. V. Hermenegildo.
    Theory and Practice of Logic Programming 18, 167–223. Cambridge U. Press, March 2018.
93. Analysing snapshot isolation
    Andrea Cerone, Alexey Gotsman.
    Journal of the ACM 65 (2), 1-41. ACM Press, March 2018.
94. Optimised determinisation and completion of finite tree automata
    John P. Gallagher, Mai Ajspur, Bishoksan Kafle.
    Journal of Logical and Algebraic Methods in Programming 95, 1–16. February 2018.
95. Abstract Non-Interference: A Unifying Framework for Weakening Information-flow
    Roberto Giacobazzi, Isabella Mastroeni.
    ACM Transactions on Information and System Security 21 (2), 1–31. ACM, February 2018.
96. Decidability of conversion for type theory in type theory
    Andreas Abel, Joakim Öhman, Andrea Vezzosi.
    ACM SIGACT Symposium on Principles of Programming Languages 2 ({POPL}), 1–29. ACM, January 2018.
97. Characterizing transactional memory consistency conditions using observational refinement
    Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky.
    Journal of the ACM 65 (1), 1-44. ACM Press, January 2018.
98. Proving expected sensitivity of probabilistic programs
    Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
    ACM SIGACT Symposium on Principles of Programming Languages 2 ({POPL}), 1–29. 2018.
99. Monadic refinements for relational cost analysis
    Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
    ACM SIGACT Symposium on Principles of Programming Languages 2 (POPL), 1–32. 2018.
100. Gradual liquid type inference
     Niki Vazou, Éric Tanter, David Van Horn.
     ACM Conference on Object Oriented Programming Systems Languages and Applications 2 ({OOPSLA}), 1–25. 2018.
101. An iterative approach to precondition inference using constrained Horn clauses
     Bishoksan Kafle, John P. Gallagher, Graeme Gange, Peter Schachte, Harald Søndergaard, Peter J. Stuckey.
     Theory and Practice of Logic Programming 18 (3-4), 553–570. 2018.
102. Practical Homomorphic Message Authenticators for Arithmetic Circuits
     Dario Catalano, Dario Fiore.
     Journal of Cryptology 31 (1), 23–59. Springer, 2018.
103. Introduction to the special issue on runtime verification
     Yliès Falcone, César Sánchez.
     Formal Methods in System Design 53 (1), 1–5. 2018.
104. Constraint Answer Set Programming without Grounding
     J. Arias, M. Carro, E. Salazar, K. Marple, G. Gupta.
     Theory and Practice of Logic Programming. Cambridge U. Press, 2018.
105. Description, Implementation, and Evaluation of a Generic Design for Tabled CLP
     J. Arias, M. Carro.
     Theory and Practice of Logic Programming. Cambridge U. Press, 2018.
106. An Evolutionary Scheduling Approach for Trading-off Accuracy vs. Verifiable Energy in Multicore Processors
     U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
     Logic Journal of the IGPL 25 (6), 1006–1019. Oxford Academic Press, December 2017.
107. A relational logic for higher-order programs
     Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
     Proceedings of the ACM on Programming Languages 1, 1–29. ACM, August 2017.
108. Parametrized Verification Diagrams: Temporal Verification of Symmetric Parametrized Concurrent Systems
     Alejandro Sánchez, César Sánchez.
     Annals of Mathematics and Artificial Intelligence 80 (3–4), 249–282. August 2017.
109. A Certificateless Approach to Onion Routing
     Dario Catalano, Dario Fiore, Rosario Gennaro.
     International Journal of Intelligent Systems 16 (3), 327–343. Springer, June 2017.
110. Partitioned Group Password-Based Authenticated Key Exchange
     Dario Fiore, María Isabel González Vasco, Claudio Soriente.
     The Computer Journal 60 (12), 1912–1922. 2017.
111. A messy state of the union: taming the composite state machines of TLS
     Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue.
     Communications of the ACM 60 (2), 99–107. 2017.
112. Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
     Bishoksan Kafle, John P. Gallagher.
     Computer Languages, Systems & Structures 47, 2–18. 2017.
113. Constraint specialisation in Horn clause verification
     Bishoksan Kafle, John P. Gallagher.
     Science of Computer Programming 137, 125–140. 2017.
114. What Does The Crowd Say About You? Evaluating Aggregation-based Location Privacy
     Apostolos Pyrgelis, Carmela Troncoso, Emiliano De Cristofaro.
     Privacy Enhancing Technologies Symposium 2017 (4), 156–176. 2017.
115. Privacy Games Along Location Traces: A Game-Theoretic Framework for Optimizing Location Privacy
     Reza Shokri, George Theodorakopoulos, Carmela Troncoso.
     ACM Transactions on Information and System Security 19 (4), 1–31. 2017.
116. Systematizing Decentralization and Privacy: Lessons from 15 years of research and deployments
     Carmela Troncoso, George Danezis, Marios Isaakidis, Harry Halpin.
     Privacy Enhancing Technologies Symposium 2017 (4), 404–426. 2017.
117. ENTRA: Whole-Systems Energy Transparency
     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.
     Microprocessors and Microsystems - Embedded Hardware Design 47, Part B, 278–286. Elsevier, November 2016.
118. A General Framework for Static Profiling of Parametric Resource Usage
     P. Lopez-Garcia, M. Klemen, U. Liqat, M. V. Hermenegildo.
     Theory and Practice of Logic Programming 16 (5-6), 849–865. Cambridge U. Press, October 2016.
119. Mobile Collaborative Learning Systems with Augmented Reality
     Veronica Mendoza, Richard Rivera, J.J. Barriga-Andrade.
     Revista Politécnica 38 (1), 71-80. Escuela Politécnica Nacional, September 2016.
120. Introduction to the 32nd International Conference on Logic Programming Special Issue
     Manuel Carro, Andy King.
     Theory and Practice of Logic Programming 16 (5-6), 509-514. Cambridge University Press, September 2016.
121. Semantic Code Browsing
     I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
     Theory and Practice of Logic Programming 16 (5-6), 721–737. CUP, September 2016.
122. A testing-based approach to ensure the safety of shared resource concurrent systems
     Lars-Åke Fredlund, Julio Mariño, Raúl N.N. Alborodo, Angel Herranz.
     Journal of Risk and Reliability, Proceedings of the Institution of Mechanical Engineers, Part O 230 (5), 457–472. Sage Publications, July 2016.
123. Making abstract models complete
     Roberto Giacobazzi, Isabella Mastroeni.
     Mathematical Structures in Computer Science 26 (4), 658–701. Cambridge University Press, May 2016.
124. Type Inference on Executables
     Juan Caballero, Zhiqiang Lin.
     ACM Computing Surveys 48 (4), 1–35. ACM, May 2016.
125. Parameterized Verification of Asynchronous Shared-Memory Systems
     Javier Esparza, Pierre Ganty, Rupak Majumdar.
     Journal of the ACM 63 (1), 1–48. ACM, March 2016.
126. Building Resource Adaptive Software Systems (BRASS): Objectives and System Evaluation
     J. Hughes, C. Sparks, A. Stoughton, R. Parikh, A. Reuther, S. Jagannathan.
     ACM SIGSOFT Software Engineering Notes 41 (1), 1–2. ACM, January 2016.
127. Description and Optimization of Abstract Machines in a Dialect of Prolog
     J.F. Morales, M. Carro, M. V. Hermenegildo.
     Theory and Practice of Logic Programming 16 (1), 1–58. Cambridge University Press, January 2016.
128. No solvable lambda-value term left behind
     Á. García-Pérez, P. Nogueira.
     Logical Methods in Computer Science 12 (2), 1-43. 2016.
129. A rapid-prototyping framework for extracting small-scale incident-related information in microblogs: Application of multi-label classification on tweets
     Axel Schulz, Eneldo Loza Mencía, Benedikt Schmidt.
     IEEE International Conference on Intelligent Systems 57, 88–110. 2016.
130. Product programs and relational program logics
     Gilles Barthe, Juan Manuel Crespo, César Kunz.
     Journal of Logical and Algebraic Methods in Programming 85 (5), 847–859. 2016.
131. Programming language techniques for differential privacy
     Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce.
     ACM SIGLOG News 3 (1), 34–53. 2016.
132. Model checking parameterized asynchronous shared-memory systems
     Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
     Formal Methods in System Design, 1–28. 2016.
133. Verification of population protocols
     Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
     Acta Informatica, 1–25. 2016.
134. Maximal incompleteness as obfuscation potency
     Roberto Giacobazzi, Isabella Mastroeni, Mila Dalla Preda.
     Formal Aspects of Computing: applicable formal methods. 2016.
135. Underapproximation of procedure summaries for integer programs
     Pierre Ganty, Radu Iosif, Filip Konečný.
     International Journal on Software Tools for Technology Transfer, 1–20. 2016.
136. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
     Sandrine Blazy, Vincent Laporte, David Pichardie.
     Journal of Automated Reasoning 56 (3), 283–308. 2016.
137. Weakening Additivity in Adjoining Closures
     Isabella Mastroeni, Roberto Giacobazzi.
     Order - A Journal on the Theory of Ordered Sets and its Applications 33 (3), 503–516. 2016.
138. Design of Pool Mixes Against Profiling Attacks in Real Conditions
     S. Oya, F. Pérez-González, C. Troncoso.
     IEEE ACM Transactions on Networking 24 (6), 3662–3675. 2016.
139. Foundations of Boolean Stream Runtime Verification
     Laura Bozzelli, César Sánchez.
     Electronic Notes in Theoretical Computer Science 631, 118–138. 2016.
140. Special issue on Rich Models, EU-COST Action IC0901 Rich-Model Toolkit
     Bernd Finkbeiner, César Sánchez.
     Acta Informatica 53 (4), 325–326. 2016.
141. Special issue on temporal representation and reasoning (TIME'13)
     César Sánchez, Kristen Brent Venable, Esteban Zimányi.
     Acta Informatica 53 (2), 87–88. 2016.
142. Practical Run-time Checking via Unobtrusive Property Caching
     N. Stulova, J.F. Morales, M.V. Hermenegildo.
     Theory and Practice of Logic Programming 15 (04-05), 726-741. CUP, September 2015.
143. CacheAudit: A Tool for the Static Analysis of Cache Side Channels
     Goran Doychev, Boris Köpf, Laurent Mauborgne, Jan Reineke.
     ACM Transactions on Information and System Security 18 (1), 1–32. ACM, June 2015.
144. On the Use of GPU for Accelerating Communication-Aware Mapping Techniques
     Guillermo Vigueras, Juan M. Orduña.
     The Computer Journal. May 2015.
145. Quantifying information flow in cryptographic systems
     Michael Backes, Boris Köpf.
     Mathematical Structures in Computer Science 25 (2), 457–479. February 2015.
146. The MALICIA Dataset: Identification and Analysis of Drive-by Download Operations
     Antonio Nappa, M. Zubair Rafique, Juan Caballero.
     International Journal of Information Security 14 (1), 15-33. Springer Berlin Heidelberg, February 2015.
147. Comparing and Combining Predictive Business Process Monitoring Techniques
     Andreas Metzger, Philip Leitner, Dragan Ivanovic, Eric Schmieders, Roslin Franklin, Manuel Carro, Schahram Dustdar, Klaus Pohl.
     IEEE Transactions on Human-Machine Systems 45 (2), 276-290. February 2015.
148. Automatic Workarounds: Exploiting the Intrinsic Redundancy of Web Applications
     Antonio Carzaniga, Alessandra Gorla, Nicolò Perino, Mauro Pezzè.
     ACM Transactions on Software Engineering and Methodology 24 (3), 1–42. 2015.
149. AVERIST: An Algorithmic Verifier for Stability
     Pavithra Prabhakar, Miriam Garcia Soto.
     Electronic Notes in Theoretical Computer Science 317, 133–139. 2015.
150. Hybrid automata-based CEGAR for rectangular hybrid systems
     Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan.
     Formal Methods in System Design 46 (2), 105–134. 2015.
151. High-Assurance Cryptography: Cryptographic Software We can Trust
     Gilles Barthe.
     IEEE Security and Privacy Magazine 13 (5), 86–89. 2015.
152. SEFM: Software Engineering and Formal Methods
     Gilles Barthe, Alberto Pardo, Gerardo Schneider.
     Software and Systems Modeling 14 (1), 3–4. 2015.
153. Stability Preserving Simulations and Bisimulations for Hybrid Systems
     Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan.
     IEEE Transactions on Automatic Control 60 (12), 3210–3225. 2015.
154. A decidable class of planar linear hybrid systems
     Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, Geir E. Dullerud.
     Electronic Notes in Theoretical Computer Science 574, 1–17. 2015.
155. Unveiling metamorphism by abstract interpretation of code properties
     Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray.
     Electronic Notes in Theoretical Computer Science 577, 74–97. 2015.
156. Algebraic (trapdoor) one-way functions: Constructions and applications
     Dario Catalano, Dario Fiore, Rosario Gennaro, Konstantinos Vamvourellis.
     Electronic Notes in Theoretical Computer Science 592, 143–165. Springer, 2015.
157. Parametrized Invariance for Infinite State Processes
     Alejandro Sánchez, César Sánchez.
     Acta Informatica 52 (6), 525–557. 2015.
158. Stochastic vs. Deterministic Evolutionary Algorithm-based Allocation and Scheduling for XMOS Chips
     Z. Banković, P. Lopez-Garcia.
     Neurocomputing 150, 82–89. Elsevier, 2015.
159. An XFEM/CZM implementation for massively parallel simulations of composites fracture
     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.
     Composite Structures 125 (0), 542-557. 2015.
160. Mtac: A Monad for Typed Tactic Programming in Coq
     Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
     Journal of Functional Programming 25. 2015.
161. Formal Verification of an SSA-Based Middle-End for CompCert
     Gilles Barthe, Delphine Demange, David Pichardie.
     ACM Transactions on Programming Languages and Systems 36 (1), 1–35. ACM, March 2014.
162. A Model-Driven Methodology for Developing Secure Data-Management Applications
     David A. Basin, Manuel Clavel, Marina Egea, Miguel Ángel García de Dios, Carolina Dania.
     IEEE Transactions on Software Engineering 40 (4), 324–337. 2014.
163. On Automation in the Verification of Software Barriers: Experience Report
     Alexander Malkis, Anindya Banerjee.
     Journal of Automated Reasoning 52 (3), 275–329. 2014.
164. On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines
     Álvaro García-Pérez, Pablo Nogueira.
     Science of Computer Programming 95, 176–199. Elsevier, 2014.
165. Verifiable Random Functions: Relations to Identity-Based Key-Encapsulation and New Constructions
     Michel Abdalla, Dario Catalano, Dario Fiore.
     Journal of Cryptology 27 (3), 544–593. Springer, 2014.
166. Pushdown flow analysis with abstract garbage collection
     J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn.
     Journal of Functional Programming 24 (2-3), 218–283. 2014.
167. Visibly Rational Expressions
     Laura Bozzelli, César Sánchez.
     Acta Informatica 51 (1), 25–49. 2014.
168. On Termination, Confluence and Consistent CHR-based Type Inference
     G.J. Duck, R. Haemmerlé, M. Sulzmann.
     Theory and Practice of Logic Programming 14 (4-5), 619-632. Cambridge U. Press, 2014.
169. Pattern-based Verification for Multithreaded Programs
     Javier Esparza, Pierre Ganty, Tomás Poch.
     ACM Transactions on Programming Languages and Systems 36 (3), 1–29. 2014.
170. Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols
     François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann.
     Journal of Computer Security 22 (5), 823–866. IOS Press, 2014.
171. Bounded phase analysis of message-passing programs
     Ahmed Bouajjani, Michael Emmi.
     International Journal on Software Tools for Technology Transfer 16 (2), 127–146. 2014.
172. Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types
     A. Serrano, P. Lopez-Garcia, M. V. Hermenegildo.
     Theory and Practice of Logic Programming 14 (4-5), 739-754. CUP, 2014.
173. Accelerating collision detection for large-scale crowd simulation on multi-core and many-core architectures
     Guillermo Vigueras, Juan M. Orduña, Miguel Lozano, Jose M. Cecilia, Jose M. Garcia.
     International Journal of High Performance Computing Applications 28 (1). 2014.
174. Toward GPGPU accelerated human electromechanical cardiac simulations
     Guillermo Vigueras, Ishani Roy, Andrew Cookson, Jack Lee, Nicolas Smith, David Nordsletten.
     International Journal for Numerical Methods in Biomedical Engineering 30 (1), 117–134. 2014.
175. A Certified Lightweight Non-interference Java Bytecode Verifier
     Gilles Barthe, David Pichardie, Tamara Rezk.
     Mathematical Structures in Computer Science 23 (5), 1032–1081. Cambridge University Press, October 2013.
176. How to make ad hoc proof automation less ad hoc
     Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
     Journal of Functional Programming 23 (4), 357–401. July 2013.
177. Modular verification of preemptive OS kernels
     Alexey Gotsman, Hongseok Yang.
     Journal of Functional Programming 23 (4), 452–514. Cambridge University Press, July 2013.
178. A Scalable Multiagent System Architecture for Interactive Applications
     Guillermo Vigueras, Juan M. Orduña, Miguel Lozano, Yvon Jégou.
     Science of Computer Programming 78 (6), 715–724. Elsevier North-Holland, Inc., June 2013.
179. A Sharing-Based Approach to Supporting Adaptation in Service Compositions
     D. Ivanovic, M. Carro, M. V. Hermenegildo.
     Computing 95 (6), 453-492. Springer Wien, June 2013.
180. Automatic Protocol Reverse-Engineering: Message Format Extraction and Field Semantics
     Juan Caballero, Dawn Song.
     Computer Networks 57 (2), 451-474. Elsevier, February 2013.
181. Local Reasoning for Global Invariants, Part II: Dynamic Boundaries
     Anindya Banerjee, David A. Naumann.
     Journal of the ACM 60 (3), 1–73. ACM, 2013.
182. Local Reasoning for Global Invariants, Part I: Region Logic
     Anindya Banerjee, David A. Naumann, Stan Rosenberg.
     Journal of the ACM 60 (3), 1–56. ACM, 2013.
183. Secure distributed programming with value-dependent types
     Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang.
     Journal of Functional Programming 23 (4), 402-451. 2013.
184. Dependent Type Theory for Verification of Information Flow and Access Control Policies
     Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
     ACM Transactions on Programming Languages and Systems 35 (2), 1–41. ACM, 2013.
185. A Model-Driven Approach to Teaching Concurrency
     M. Carro, Ángel Herranz, Julio Mariño.
     ACM Transactions on Computing Education 13 (1). 2013.
186. Analysis of Recursively Parallel Programs
     Ahmed Bouajjani, Michael Emmi.
     ACM Transactions on Programming Languages and Systems 35 (3), 1–49. 2013.
187. A Survey on Service Quality Description
     Kyriakos Kritikos, Barbara Pernici, Pierluigi Plebani, Cinzia Cappiello, Marco Comuzzi, Salima Benbernou, Ivona Brandic, Attila Kertesz, Michael Parkin, M. Carro.
     ACM Computing Surveys 46 (1). 2013.
188. Fusing Statecharts and Java
     Maria-Cristina Marinescu, César Sánchez.
     ACM Transactions on Embedded Computing Systems 12, 1–21. 2013.
189. A computationally efficient framework for the simulation of cardiac perfusion using a multi-compartment Darcy porous-media flow model
     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.
     International Journal of Numerical Methods in Biomedical Engineering 29 (2). 2013.
190. A Read-Copy Update based parallel server for distributed crowd simulations
     Guillermo Vigueras, Juan M. Orduña, Miguel Lozano.
     Journal of Supercomputing 64 (1), 156–166. Springer US, 2013.
191. Ubiquitous Green Computing Techniques for High Demand Applications in Smart Environments
     Marina Zapater, César Sánchez, José L. Ayala, José M. Moya, José L. Risco-Martín.
     Sensors 12 (8), 10659–10677. August 2012.
192. Understanding the Role of Malware in Cybercrime
     Juan Caballero.
     ERCIM News 2012 (90), 15-16. July 2012.
193. Certificate Size Reduction in Abstraction-Carrying Code
     E. Albert, P. Arenas, G. Puebla, M. Hermenegildo.
     Theory and Practice of Logic Programming 12 (3), 283–318. 2012.
194. Lightweight compilation of (C)LP to JavaScript
     J. F. Morales, R. Haemmerlé, M. Carro, M. V. Hermenegildo.
     Theory and Practice of Logic Programming 12 (4-5), 755-773. Cambridge U. Press, 2012.
195. Algorithmic verification of asynchronous programs
     Pierre Ganty, Rupak Majumdar.
     ACM Transactions on Programming Languages and Systems 34 (1), 1–48. ACM, 2012.
196. Bounded Underapproximations
     Pierre Ganty, Rupak Majumdar, Benjamin Monmege.
     Formal Methods in System Design 40 (2), 206-231. 2012.
197. An Overview of Ciao and its Design Philosophy
     M.V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, E. Mera, J.F. Morales, G. Puebla.
     Theory and Practice of Logic Programming 12 (1–2), 219–252. Cambridge Univ Press, 2012.
198. Quantitative Security Analysis (Dagstuhl Seminar 12481)
     Boris Köpf, Pasquale Malacaria, Catuscia Palamidessi.
     Dagstuhl Reports 2 (11), 135-154. 2012.
199. Abstracting Runtime Heaps for Program Understanding
     Mark Marron, César Sánchez, Zhendong Su, Manuel Fähndrich.
     IEEE Transactions on Software Engineering 99. IEEE Computer Society, 2012.
200. Verification of Bounded Discrete Horizon Hybrid Automata
     Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir E. Dullerud.
     IEEE Transactions on Automatic Control 57 (6), 1445-1455. 2012.
201. Modelling Declassification Policies using Abstract Domain Completeness
     Isabella Mastroeni, Anindya Banerjee.
     Mathematical Structures in Computer Science 21 (6), 1253-1299. December 2011.
202. Secure Information Flow by Self-Composition
     Gilles Barthe, Pedro D'Argenio, Tamara Rezk.
     Mathematical Structures in Computer Science 21 (6), 1207-1252. Cambridge University Press, October 2011.
203. An Abstract Model of Certificate Translation
     Gilles Barthe, César Kunz.
     ACM Transactions on Programming Languages and Systems 33 (4), 1–13. ACM, July 2011.
204. Parallel Backtracking with Answer Memoing for Independent And-Parallelism
     P. Chico de Guzmán, A. Casas, M. Carro, M. V. Hermenegildo.
     Theory and Practice of Logic Programming. Cambridge U. Press, July 2011.
205. Efficient Local Unfolding with Ancestor Stacks
     G. Puebla, E. Albert, M. V. Hermenegildo.
     Theory and Practice of Logic Programming 11 (1), 1–32. Cambridge U. Press, January 2011.
206. Parikh's Theorem: A simple and direct automaton construction
     Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger.
     Information Processing Letters 111, 614-619. 2011.
207. Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks
     Boris Köpf, David Basin.
     Journal of Computer Security 1, 1–31. 2011.
208. Security of Multithreaded Programs by Compilation
     Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld.
     ACM Transactions on Information and System Security 13 (3). 2010.
209. Formal Executable Semantics for Conformance in the MDE Framework
     M. Egea, V. Rusu.
     Innovations in Systems and Software Engineering 6, 73-81. Springer London, 2010.
210. Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Analyses
     P. Lopez-Garcia, F. Bueno, M. V. Hermenegildo.
     New Generation Computing: computing paradigms and computational intelligence 28 (2), 117–206. 2010.
211. Fixed Point Guided Abstraction Refinement for Alternating Automata
     Pierre Ganty, Nicolas Maquet, Jean-François Raskin.
     Electronic Notes in Theoretical Computer Science 411 (38-39), 3444-3459. 2010.
212. Lock-free Parallel Dynamic Programming
     A. Stivala, P. J. Stuckey, M. García de la Banda, M. V. Hermenegildo, A. Wirth.
     Journal of Parallel and Distributed Computing 70 (8), 839-848. Elsevier, 2010.
213. Non-Strict Independence-Based Program Parallelization Using Sharing and Freeness Information
     D. Cabeza, M. Hermenegildo.
     Electronic Notes in Theoretical Computer Science 410 (46), 4704–4723. Elsevier Science, October 2009.
214. Type-based homeomorphic embedding for online termination
     Elvira Albert, John P. Gallagher, Miguel Gómez-Zamalloa, Germán Puebla.
     Information Processing Letters 109 (15), 879-886. Elsevier, July 2009.
215. Certificate Translation for Optimizing Compilers
     Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk.
     ACM Transactions on Programming Languages and Systems 31 (5). ACM, July 2009.
216. Stepwise Refinement Validation of Design Patterns Formalized in TLA+ Using the TLC Model Checker
     Toufik Taibi, Ángel Herranz, Juan José Moreno-Navarro.
     Journal of Object Technology 8 (2), 137-161. March 2009.
217. Implementing Constructive Intensional Negation
     Julio Mariño, Juan José Moreno-Navarro, Susana Muñoz Hernández.
     New Generation Computing: computing paradigms and computational intelligence 27 (1), 25-56. January 2009.
218. Automated Analysis of Security-Design Models
     D. Basin, M. Clavel, J. Doser, M. Egea.
     Information and Software Technology 51 (5), 815-831. 2009.
219. Abstraction-Carrying Code: A Model for Mobile Code Safety
     E. Albert, G. Puebla, M. V. Hermenegildo.
     New Generation Computing: computing paradigms and computational intelligence 26 (2). 2008.

Articles in Refereed Conferences (622)

1. One Size Does not Fit All: Quantifying the Risk of Malicious App Encounters for Different Android User Profiles
   Savino Dambra, Leyla Bilge, Platon Kotzias, Yun Shen, Juan Caballero.
   Usenix Security Symposium (USENIX-Security). August 2023.
2. ACoRe: Automated Goal-Conflict Resolution
   Luiz Carvalho, Renzo Degiovanni, Matías Brizzio, Maxime Cordy, Nazareno Aguirre, Yves Le Traon, Mike Papadakis.
   Fundamental Approaches to Software Engineering: 26th International Conference, FASE 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings. 2023.
3. Efficient Bounded Exhaustive Input Generation from Program APIs
   Mariano Politano, Valeria S. Bengolea, Facundo Molina, Nazareno Aguirre, Marcelo F. Frias, Pablo Ponzio.
   Fundamental Approaches to Software Engineering (FASE). 2023.
4. Get Me Out of This Payment! Bailout: An HTLC Re-routing Protocol
   Oguzhan Ersoy, Pedro Moreno-Sanchez, Stefanie Roos.
   Financial Cryptography and Data Security Conference (FC). 2023.
5. Breaking and Fixing Virtual Channels: Domino Attack and Donner
   Lukas Aumayr, Pedro Moreno-Sanchez, Aniket Kate, Matteo Maffei.
   Network and Distributed System Security Symposium (NDSS). 2023.
6. Antichains Algorithms for the Inclusion Problem Between ω-VPL
   Kyveli Doveri, Pierre Ganty, Luka Hadži-Đokić.
   International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2023.
7. Tableaux for Realizability of Safety Specifications
   Monserrat Hermo, Paqui Lucio, César Sánchez.
   International Symposium on Formal Methods (FM). 2023.
8. The complexity of Presburger arithmetic with power or powers
   Michael Benedikt, Dmitry Chistikov, Alessio Mansutti.
   Automata, Languages and Programming – ICALP. 2023.
9. Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing
   Oleksii Oleksenko, Marco Guarnieri, Boris Köpf, Mark Silberstein.
   Proceedings of the 44th IEEE Symposium on Security and Privacy. 2023.
10. Cryptographic Oracle-Based Conditional Payments
    Varun Madathil, Sri Aravinda Krishnan Thyagarajan, Dimitrios Vasilopoulos, Lloyd Fournier, Giulio Malavolta, Pedro Moreno-Sanchez.
    Network and Distributed System Security Symposium (NDSS). 2023.
11. Efficient Modular SMT-Based Model Checking of Pointer Programs
    I. Garcia-Contreras, A. Gurfinkel, J. A. Navas.
    Static Analysis Symposium (SAS). December 2022.
12. Watch Your Back: Identifying Cybercrime Financial Relationships in Bitcoin through Back-and-Forth Exploration
    Gibran Gomez, Pedro Moreno-Sanchez, Juan Caballero.
    ACM Conference on Computer and Communications Security (CCS). November 2022.
13. Call Me Maybe: Using NLP to Automatically Generate Unit Test Cases Compliant with Temporal Constraints
    Arianna Blasi, Alessandra Gorla, Michael D. Ernst, Mauro Pezzè.
    International Conference on Automated Software Engineering (ASE). October 2022.
14. LISSA: Lazy Initialization with Specialized Solver Aid
    Juan Manuel Copia, Pablo Ponzio, Nazareno Aguirre, Alessandra Gorla, Marcelo Frias.
    International Conference on Automated Software Engineering (ASE). October 2022.
15. On the Usage of Programming Languages in the iOS Ecosystem
    Daniel Dominguez, Alessandra Gorla, Juan Caballero.
    IEEE Working Conference on Source Code Analysis and Manipulation (SCAM). October 2022.
16. Deep dive into the IoT backend ecosystem
    Said Jawad Saidi, Srdjan Matic, Georgios Smaragdakis, Oliver Gasser, Anja Feldmann.
    Internet Measurement Conference (IMC). October 2022.
17. Measuring Web Cookies in Governmental Websites
    Matthias Götze, Srdjan Matic, Costas Iordanou, Georgios Smaragdakis, Nikolaos Laoutaris.
    Web Science Conference (WebSci). June 2022.
18. ReChan: An Automated Analysis of Android App Release Notes to Report Inconsistencies
    Daniel Domínguez-Álvarez, Daniel Tomic, Alessandra Gorla.
    International Conference on Mobile Software Engineering and Systems (MOBILESoft). May 2022.
19. Use of Test Doubles in Android Testing: An In-Depth Investigation
    Mattia Fazzini, Chase Choi, Juan Manuel Copia, Gabriel Lee, Yoshiki Kakehi, Alessandra Gorla, Alessandro Orso.
    International Conference on Software Engineering (ICSE). May 2022.
20. Universal Atomic Swaps: Secure Exchange of Coins Across All Blockchains
    Sri Aravinda Krishnan Thyagarajan, Giulio Malavolta, Pedro Moreno-Sanchez.
    IEEE Symposium on Security and Privacy (SP). May 2022.
21. ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
    Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker.
    ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2022.
22. How to Safely Use Extensionality in Liquid Haskell
    Niki Vazou, Michael Greenberg.
    ACM SIGPLAN International Symposium on Haskell (Haskell). 2022.
23. Liquid Proof Macros
    Henry Blanchette, Niki Vazou, Leonidas Lampropoulos.
    ACM SIGPLAN International Symposium on Haskell (Haskell). 2022.
24. Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
    Lykourgos Mastorou, Nikolaos Papaspyrou, Niki Vazou.
    ACM SIGPLAN International Symposium on Haskell (Haskell). 2022.
25. YOLO YOSO: Fast and Simple Encryption and Secret Sharing in the YOSO Model
    Ignacio Cascudo, Bernardo David, Lydia Garms, Anders Konring.
    International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). 2022.
26. Additive-Homomorphic Functional Commitments and Applications to Homomorphic Signatures
    Dario Catalano, Dario Fiore, Ida Tucker.
    International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). 2022.
27. Progressive And Efficient Verification For Digital Signatures
    Cecilia Boschini, Dario Fiore, Elena Pagnin.
    International Conference on Applied Cryptography and Network Security (ACNS). 2022.
28. Succinct Zero-Knowledge Batch Proofs for Set Accumulators
    Matteo Campanelli, Dario Fiore, Semin Han, Jihye Kim, Dimitris Kolonelos, Hyunok Oh.
    ACM Conference on Computer and Communications Security (CCS). 2022.
29. Efficient Zero-Knowledge Proofs on Signed Data with Applications to Verifiable Computation on Data Streams
    Dario Fiore, Ida Tucker.
    ACM Conference on Computer and Communications Security (CCS). 2022.
30. Subversion-Resilient Enhanced Privacy ID
    Antonio Faonio, Dario Fiore, Luca Nizzardo, Claudio Soriente.
    The Cryptographer’s Track at RSA Conference (CT-RSA). 2022.
31. Symbolic Synthesis of Indifferentiability Attacks
    Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe.
    Asia Conference on Information, Computer and Communications Security (AsiaCCS). 2022.
32. Tidy: Symbolic Verification of Timed Cryptographic Protocols
    Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, Itsaka Rakotonirina.
    ACM Conference on Computer and Communications Security (CCS). 2022.
33. Enforcing Fine-grained Constant-time Policies
    Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya.
    ACM Conference on Computer and Communications Security (CCS). 2022.
34. Efficient Proofs of Knowledge for Threshold Relations
    Gennaro Avitabile, Vincenzo Botta, Daniele Friolo, Ivan Visconti.
    European Symposium On Research In Computer Security (ESORICS). 2022.
35. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
    Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying.
    IEEE Symposium on Logic in Computer Science (LICS). 2022.
36. Towards Dynamic Consistency Checking in Goal-Directed Predicate Answer Set Programming
    Joaquín Arias, Manuel Carro, Gopal Gupta.
    Practical Aspects of Declarative Languages (PADL). 2022.
37. Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs
    Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe.
    Static Analysis Symposium (SAS). 2022.
38. SoK: Practical Foundations for Software Spectre Defenses
    Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan.
    IEEE Symposium on Security and Privacy (SP). 2022.
39. They're not that hard to mitigate: What Cryptographic Library Developers Think About Timing Attacks
    Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar.
    IEEE Symposium on Security and Privacy (SP). 2022.
40. Deciding program properties via complete abstractions on bounded domains
    Roberto Bruni, Roberta Gori, Nicolas Manini.
    Static Analysis Symposium (SAS). 2022.
41. Ring Signatures with User-Controlled Linkability
    Dario Fiore, Lydia Garms, Dimitris Kolonelos, Claudio Soriente, Ida Tucker.
    European Symposium On Research In Computer Security (ESORICS). 2022.
42. On Interactive Oracle Proofs for Boolean R1CS Statements
    Ignacio Cascudo, Emanuele Giunta.
    Financial Cryptography and Data Security Conference (FC). 2022.
43. Adaptively Secure Single Secret Leader Election from DDH
    Dario Catalano, Dario Fiore, Emanuele Giunta.
    ACM Symposium on Principles of Distributed Computing (PODC). 2022.
44. Inner Product Functional Commitments with Constant-Size Public Parameters and Openings
    Hien Chu, Dario Fiore, Dimitris Kolonelos, Dominique Schröder.
    Conference on Security and Cryptography for Networks (SCN). 2022.
45. Vector Commitments over Rings and Compressed Σ-Protocols
    Thomas Attema, Ignacio Cascudo, Ronald Cramer, Ivan Damgård, Daniel Escudero.
    Theory of Cryptography Conference (TCC). 2022.
46. On the Impossibility of Algebraic Vector Commitments in Pairing-Free Groups
    Dario Catalano, Dario Fiore, Rosario Gennaro, Emanuele Giunta.
    Theory of Cryptography Conference (TCC). 2022.
47. Acuerdo: Fast atomic broadcast over RDMA
    Joseph Izraelevitz, Gaukas Wang, Rhett Hanscom, Kayli Silvers, Tamara Silbergleit Lehman, Gregory Chockler, Alexey Gotsman.
    International Conference on Parallel Processing (ICPP). 2022.
48. Measuring the Adoption and Actual Privacy of Decentralized CoinJoin Implementations in the Bitcoin Ecosystem
    Rainer Stütz, Johann Stockinger, Bernhard Haslhofer, Pedro Moreno-Sanchez, Matteo Maffei.
    Conference on Advances in Financial Technologies (AFT). 2022.
49. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
    Laura Bozzelli, Adriano Peron, César Sánchez.
    International Conference on Concurrency Theory (CONCUR). 2022.
50. Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers
    Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Antonio Russo, César Sánchez.
    IEEE International Conference on Blockchain (Blockchain). 2022.
51. Transaction Monitoring of Smart Contracts
    Margarita Capretto, Martín Ceresa, César Sánchez.
    International Conference on Runtime Verification (RV). 2022.
52. Foundations of Coin Mixing Services
    Noemi Glaeser, Matteo Maffei, Giulio Malavolta, Pedro Moreno-Sanchez, Erkan Tairi, Sri Aravinda Krishnan Thyagarajan.
    ACM Conference on Computer and Communications Security (CCS). 2022.
53. FORQ-Based Language Inclusion Formal Testing
    Kyveli Doveri, Pierre Ganty, Nicolas Mazzocchi.
    Computer Aided Verification (CAV). 2022.
54. Automatic Detection of Speculative Execution Combinations
    Xaver Fabian, Marco Guarnieri, Marco Patrignani.
    ACM Conference on Computer and Communications Security (CCS). 2022.
55. Quantifier elimination for counting extensions of Presburger arithmetic
    Dmitry Chistikov, Christoph Haase, Alessio Mansutti.
    Foundations of Software Science and Computational Structures (FOSSACS). 2022.
56. Modal Logics and Local Quantifiers: A Zoo in the Elementary Hierarchy
    Raul Fervari, Alessio Mansutti.
    Foundations of Software Science and Computational Structures (FOSSACS). 2022.
57. Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification
    Felipe Gorostiaga, Sebastián Zudaire, César Sánchez, Gerardo Schneider, Sebastián Uchitel.
    International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). 2022.
58. Monitorability of Expressive Verdicts
    Felipe Gorostiaga, César Sánchez.
    NASA Formal Methods (NFM). 2022.
59. Anticipatory Recurrent Monitoring with Uncertainty and Assumptions
    Hannes Kallwies, Martin Leucker, César Sánchez, Torben Scheffel.
    International Conference on Runtime Verification (RV). 2022.
60. Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions
    Hannes Kallwies, Martin Leucker, César Sánchez.
    International Symposium on Automated Technology for Verification and Analysis (ATVA). 2022.
61. Geometric decision procedures and the VC dimension of linear arithmetic theories
    Dmitry Chistikov, Christoph Haase, Alessio Mansutti.
    IEEE Symposium on Logic in Computer Science (LICS). 2022.
62. Proceedings 38th International Conference on Logic Programming
    Yuliya Lierler, José F. Morales, Carmine Dodaro, Verónica Dahl, Martin Gebser, Tuncay Tekle.
    CoRR. 2022.
63. Higher-Order Quantified Boolean Satisfiability
    Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, Alessio Mansutti.
    International Symposium on Mathematical Foundations of Computer Science (MFCS). 2022.
64. Liveness and latency of Byzantine state-machine replication
    Manuel Bravo, Gregory Chockler, Alexey Gotsman.
    International Symposium on Distributed Computing (DISC). 2022.
65. Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Lukas Aumayr, Sri Aravinda Krishnan Thyagarajan, Giulio Malavolta, Pedro Moreno-Sanchez, Matteo Maffei.
    ACM Conference on Computer and Communications Security (CCS). 2022.
66. Lunar: a Toolbox for More Efficient Universal and Updatable zkSNARKs and Commit-and-Prove Extensions
    Matteo Campanelli, Antonio Faonio, Dario Fiore, Anaïs Querol, Hadrián Rodriguez.
    International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). December 2021.
67. Generalized Bitcoin-Compatible Channels
    Lukas Aumayr, Oguzhan Ersoy, Andreas Erwig, Sebastian Faust, Kristina Hostáková, Matteo Maffei, Pedro Moreno-Sanchez, Siavash Riahi.
    International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). December 2021.
68. Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
    Lukas Aumayr, Pedro Moreno-Sanchez, Aniket Kate, Matteo Maffei.
    Usenix Security Symposium (USENIX-Security). August 2021.
69. STORM: Refinement Types for Secure Web Applications
    Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala.
    Usenix Symposium on Operating Systems Design and Implementation (OSDI). July 2021.
70. A2L: Anonymous Atomic Locks for Scalability and Interoperability in Payment Channel Hubs
    Erkan Tairi, Pedro Moreno-Sanchez, Matteo Maffei.
    IEEE Symposium on Security and Privacy (SP). May 2021.
71. How Did That Get In My Phone? Unwanted App Distribution on Android Devices
    Platon Kotzias, Juan Caballero, Leyla Bilge.
    IEEE Symposium on Security and Privacy (SP). May 2021.
72. Bitcoin-Compatible Virtual Channels
    Lukas Aumayr, Oguzhan Ersoy, Andreas Erwig, Sebastian Faust, Kristina Hostáková, Matteo Maffei, Pedro Moreno-Sanchez, Siavash Riahi.
    IEEE Symposium on Security and Privacy (SP). May 2021.
73. EasyPQC: Verifying Post-Quantum Cryptography
    Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou.
    ACM Conference on Computer and Communications Security (CCS). 2021.
74. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability
    Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub.
    ACM Conference on Computer and Communications Security (CCS). 2021.
75. Structured Leakage and Applications to Cryptographic Constant-Time and Cost
    Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya.
    ACM Conference on Computer and Communications Security (CCS). 2021.
76. Secure Compilation of Constant-Resource Programs
    Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie.
    IEEE Computer Security Foundations Symposium (CSF). 2021.
77. A Quantum Interpretation of Bunched Logic & Quantum Separation Logic
    Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu.
    IEEE Symposium on Logic in Computer Science (LICS). 2021.
78. SoK: Computer-Aided Cryptography
    Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno.
    IEEE Symposium on Security and Privacy (SP). 2021.
79. High-Assurance Cryptography in the Spectre Era
    Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe.
    IEEE Symposium on Security and Privacy (SP). 2021.
80. Zero-Knowledge Proofs for Set Membership: Efficient, Succinct, Modular
    Daniel Benarroch, Matteo Campanelli, Dario Fiore, Kobi Gurkan, Dimitris Kolonelos.
    Financial Cryptography and Data Security Conference (FC). 2021.
81. Selectively Linkable Group Signatures - Stronger Security and Preserved Verifiability
    Ashley Fraser, Lydia Garms, Anja Lehmann.
    International Conference on Cryptology and Network Security (CANS). 2021.
82. Decomposing Permutation Automata
    Ismaël Jecker, Nicolas Mazzocchi, Petra Wolf.
    International Conference on Concurrency Theory (CONCUR). 2021.
83. Regular Path Clauses and Their Application in Solving Loops
    Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro López-García, José F. Morales.
    Computing Research Repository (CoRR). 2021.
84. Flexible and Efficient Verifiable Computation on Encrypted Data
    Alexandre Bois, Ignacio Cascudo, Dario Fiore, Dongwoo Kim.
    International Conference on Practice and Theory in Public Key Cryptography (PKC). 2021.
85. Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
    Joaquín Arias, Mar Moreno-Rebato, Jose A. Rodriguez-García, Sascha Ossowski.
    International Conference on Logic Programming (ICLP). 2021.
86. I Told You Tomorrow: Practical Time-Locked Secrets Using Smart Contracts
    Enrico Bacis, Dario Facchinetti, Marco Guarnieri, Marco Rosa, Matthew Rossi, Stefano Paraboschi.
    International Conference on Availability, Reliability and Security (ARES). 2021.
87. Knowledge-driven Natural Language Understanding of English Text and its Applications
    Kinjal Basu, Sarat Varanasi, Farhad Shakerin, Joaquin Arias, Gopal Gupta.
    National Conference of the American Association for Artificial Intelligence (AAAI). 2021.
88. A Temporal Logic for Asynchronous Hyperproperties
    Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez.
    Computer Aided Verification (CAV). 2021.
89. Asynchronous Extensions of HyperLTL
    Laura Bozzelli, Adriano Peron, César Sánchez.
    IEEE Symposium on Logic in Computer Science (LICS). 2021.
90. UniStore: A fault-tolerant marriage of causal and strong consistency
    Manuel Bravo, Alexey Gotsman, Borja de Régil, Hengfeng Wei.
    Usenix Annual Technical Conference (USENIX). 2021.
91. An Experimental Framework for Improving the Performance of BFT Consensus for Future Permissioned Blockchains
    Man-Kit Sit, Manuel Bravo, Zsolt István.
    Proceedings of the 15th ACM International Conference on Distributed and Event-Based Systems. 2021.
92. Inclusion Testing of Büchi Automata Based on Well-Quasiorders
    Kyveli Doveri, Pierre Ganty, Francesco Parolini, Francesco Ranzato.
    International Conference on Concurrency Theory (CONCUR). 2021.
93. Post-Quantum Adaptor Signature for Privacy-Preserving Off-Chain Payments
    Erkan Tairi, Pedro Moreno-Sanchez, Matteo Maffei.
    Financial Cryptography and Data Security Conference (FC). 2021.
94. Cross-Layer Deanonymization Methods in the Lightning Protocol
    Matteo Romiti, Friedhelm Victor, Pedro Moreno-Sanchez, Bernhard Haslhofer, Matteo Maffei.
    Financial Cryptography and Data Security Conference (FC). 2021.
95. SoK: Communication Across Distributed Ledgers
    Alexei Zamyatin, Mustafa Al-Bassam, Dionysis Zindros, Elefterios Kokoris-Kogias, Pedro Moreno-Sanchez, Aggelos Kiayias, William Knottenbelt.
    Financial Cryptography and Data Security Conference (FC). 2021.
96. An application of KLEE to aerospace industrial software
    Juan Francisco García, Daniel Jurjo, Fernando Macías, Jose F. Morales, Alessandra Gorla.
    2021.
97. HLola: a Very Functional Tool for Extensible Stream Runtime Verification
    Felipe Gorostiaga, César Sánchez.
    International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2021.
98. HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams
    Felipe Gorostiaga, César Sánchez.
    International Symposium on Formal Methods (FM). 2021.
99. Nested Monitors: Monitors as Expressions to Build Monitors
    Felipe Gorostiaga, César Sánchez.
    International Conference on Runtime Verification (RV). 2021.
100. Hardware-Software Contracts for Secure Speculation
     Marco Guarnieri, Boris Köpf, Jan Reineke, Pepe Vila.
     IEEE Symposium on Security and Privacy (SP). 2021.
101. Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming
     Brendan Hall, Sarat Chandra Varanasi, Jan Fiedor, Joaquín Arias, Kinjal Basu, Fang Li, Devesh Bhatt, Kevin Driscoll, Elmer Salazar, Gopal Gupta.
     Computing Research Repository (CoRR). 2021.
102. Bounded Model Checking for Hyperproperties
     Tzu-Han Hsu, César Sánchez, Borzoo Bonakdarpour.
     International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2021.
103. Exorcising Spectres with Secure Compilers
     Marco Patrignani, Marco Guarnieri.
     ACM Conference on Computer and Communications Security (CCS). 2021.
104. Synchronous and asynchronous stream runtime verification
     César Sánchez.
     International Symposium on Software Testing and Analysis (ISSTA). 2021.
105. Efficient replication via timestamp stability
     Vitor Enes, Carlos Baquero, Alexey Gotsman, Pierre Sutra.
     Eurosys Conference (EuroSys). 2021.
106. Testing Your (Static Analysis) Truths
     Ignacio Casso, José F. Morales, Pedro López-García, Manuel V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2021.
107. Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions
     Sebastián Zudaire, Felipe Gorostiaga, César Sánchez, Gerardo Schneider, Sebastián Uchitel.
     IEEE International Conference on Robotics and Automation (ICRA). 2021.
108. Incrementally Aggregatable Vector Commitments and Applications to Verifiable Decentralized Storage
     Matteo Campanelli, Dario Fiore, Nicola Grego, Dimitris Kolonelos, Luca Nizzardo.
     International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). December 2020.
109. ALBATROSS: Publicly AttestabLe BATched Randomness Based On Secret Sharing
     Ignacio Cascudo, Bernardo David.
     International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). December 2020.
110. A Secret-Sharing Based MPC Protocol for Boolean Circuits with Good Amortized Complexity
     Ignacio Cascudo, Jaron Skovsted Gundersen.
     Theory of Cryptography Conference (TCC). December 2020.
111. AVClass2: Massive Malware Tag Extraction from AV Labels
     Silvia Sebastián, Juan Caballero.
     Annual Computer Security Applications Conference (ACSAC). December 2020.
112. Towards Attribution in Mobile Markets: Identifying Developer Account Polymorphism
     Silvia Sebastián, Juan Caballero.
     ACM Conference on Computer and Communications Security (CCS). November 2020.
113. Implementation Correctness for Replicated Data Types, Categorically
     Fabio Gadducci, Hernán C. Melgratti, Christian Roldán, Matteo Sammartino.
     International Colloquium on Theoretical Aspects of Computing, ICTAC 2020. November 2020.
114. Towards Detecting Inconsistent Comments in Java Source Code Automatically
     Nataliia Stulova, Arianna Blasi, Alessandra Gorla, Oscar Nierstrasz.
     IEEE Working Conference on Source Code Analysis and Manipulation (SCAM). October 2020.
115. A Framework for Automated Test Mocking of Mobile Apps
     Mattia Fazzini, Alessandra Gorla, Alessandro Orso.
     Automated Software Engineering Conference (ASE). September 2020.
116. Automatically Granted Permissions in Android apps: An Empirical Study on their Prevalence and on the Potential Threats for Privacy
     Paolo Calciati, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller.
     IEEE International Working Conference on Mining Software Repositories (MSR). June 2020.
117. Computing Abstract Distances in Logic Programs
     I. Casso, J. F. Morales, P. Lopez-Garcia, R. Giacobazzi, M. V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). April 2020.
118. A General Framework for Static Cost Analysis of Parallel Logic Programs
     M. Klemen, P. Lopez-Garcia, J. Gallagher, J.F. Morales, M. V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). April 2020.
119. An Integrated Approach to Assertion-Based Random Testing in Prolog
     I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). April 2020.
120. Cross-Origin State Inference (COSI) Attacks: Leaking Web Site States through XS-Leaks
     Avinash Sudhodanan, Soheil Khodayari, Juan Caballero.
     Network and Distributed System Security Symposium (NDSS). February 2020.
121. Abstract Extensionality – On the Properties of Incomplete Abstract Interpretations
     R. Bruni, R. Giacobazzi, R. Gori, I. Garcia-Contreras, D. Pavlovic.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). January 2020.
122. Improving the Efficiency of Re-Randomizable and Replayable CCA Secure Public Key Encryption
     Antonio Faonio, Dario Fiore.
     International Conference on Applied Cryptography and Network Security (ACNS). 2020.
123. Hypothesis Testing Interpretations and Renyi Differential Privacy
     Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato.
     International Conference on Artificial Intelligence and Statistics (AISTATS). 2020.
124. Model-Agnostic Counterfactual Explanations for Consequential Decisions
     Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera.
     International Conference on Artificial Intelligence and Statistics (AISTATS). 2020.
125. On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem
     Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo.
     European Symposium on Programming (ESOP). 2020.
126. Genetic algorithm for the weight maximization problem on weighted automata
     Elena Gutiérrez, Takamasa Okudono, Masaki Waga, Ichiro Hasuo.
     Genetic and Evolutionary Computations (GECCO). 2020.
127. Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira.
     International Conference on Cryptology in India (INDOCRYPT). 2020.
128. Deciding Differential Privacy for Programs with Finite Inputs and Outputs
     Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan.
     IEEE Symposium on Logic in Computer Science (LICS). 2020.
129. Universal equivalence and majority of probabilistic programs over finite fields
     Gilles Barthe, Charlie Jacomme, Steve Kremer.
     IEEE Symposium on Logic in Computer Science (LICS). 2020.
130. Modeling and Reasoning in Event Calculus Using Goal-Directed Constraint Answer Set Programming
     Joaquín Arias, Zhuo Chen, Manuel Carro, Gopal Gupta.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2020.
131. slepice: Towards a Verified Implementation of Type Theory in Type Theory
     František Farka.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2020.
132. A Quasiorder-Based Perspective on Residual Automata
     Pierre Ganty, Elena Gutiérrez, Pedro Valero.
     International Symposium on Mathematical Foundations of Computer Science (MFCS). 2020.
133. Constant-time foundations for the new spectre era
     Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2020.
134. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub.
     IEEE Symposium on Security and Privacy (SP). 2020.
135. Angel or Devil? A Privacy Study of Mobile Parental Control Apps
     Alvaro Feal, Paolo Calciati, Narseo Vallina-Rodriguez, Carmela Troncoso, Alessandra Gorla.
     Privacy Enhancing Technologies Symposium (PETS). 2020.
136. An Experiment Combining Specialization with Abstract Interpretation
     John P. Gallagher, Robert Glück.
     Computing Research Repository (CoRR). 2020.
137. From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation
     John P. Gallagher, Manuel V. Hermenegildo, Bishoksan Kafle, Maximiliano Klemen, Pedro López-García, José F. Morales.
     Computing Research Repository (CoRR). 2020.
138. Unifying the Time-Event Spectrum for Stream Runtime Verification
     Felipe Gorostiaga, Luis Miguel Danielsson, César Sánchez.
     International Conference on Runtime Verification (RV). 2020.
139. MonZa: Fast Maliciously Secure Two Party Computation on Z2k
     Dario Catalano, Mario Di Raimondo, Dario Fiore, Irene Giacomelli.
     International Conference on Practice and Theory in Public Key Cryptography (PKC). 2020.
140. Boosting Verifiable Computation on Encrypted Data
     Dario Fiore, Anca Nitulescu, David Pointcheval.
     International Conference on Practice and Theory in Public Key Cryptography (PKC). 2020.
141. Detecting and Diagnosing Energy Issues for Mobile Applications
     Xueliang Li, Yuming Yang, Yepang Liu, John P. Gallagher, Kaishun Wu.
     International Symposium on Software Testing and Analysis (ISSTA). 2020.
142. State-machine replication for planet-scale systems
     Vitor Enes, Carlos Baquero, Tuanir França Rezende, Alexey Gotsman, Matthieu Perrin, Pierre Sutra.
     Eurosys Conference (EuroSys). 2020.
143. From big-step to small-step semantics and back with interpreter specialization
     J. Gallagher, M. V. Hermenegildo, B. Kafle, M. Klemen, P. Lopez-Garcia, J.F. Morales.
     VPT 2020. 2020.
144. Model Checking Timed Hyperproperties in Discrete-Time Systems
     Borzoo Bonakdarpour, Pavithra Prabhakar, César Sánchez.
     NASA Formal Methods (NFM). 2020.
145. Combining High Throughput and Low Migration Latency for Consistent Data Storage on the Edge
     Nuno Afonso, Manuel Bravo, Luís Rodrigues.
     International Conference on Computer Communication and Networks (ICCCN). 2020.
146. Declarative Stream Runtime Verification (hLola)
     Martín Ceresa, Felipe Gorostiaga, César Sánchez.
     ASIAN Symposium on Programming Languages and Systems (APLAS). 2020.
147. Spectector: Principled detection of speculative information flows
     Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, Andrés Sánchez.
     IEEE Symposium on Security and Privacy (SP). 2020.
148. A Quasiorder-Based Perspective on Residual Automata
     Pierre Ganty, Elena Gutiérrez, Pedro Valero.
     International Symposium on Mathematical Foundations of Computer Science (MFCS). 2020.
149. Incremental Analysis of Logic Programs with Assertions and Open Predicates
     I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2020.
150. Reliable Smart Contracts
     Gordon J. Pace, César Sánchez, Gerardo Schneider.
     International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). 2020.
151. Cost Analysis of Smart Contracts via Parametric Resource Analysis
     V. Perez-Carrasco, M. Klemen, P. Lopez-Garcia, J.F. Morales, M. V. Hermenegildo.
     Static Analysis Symposium (SAS). 2020.
152. CacheQuery: Learning Replacement Policies from Hardware Caches
     Pepe Vila, Pierre Ganty, Marco Guarnieri, Boris Köpf.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2020.
153. Structure-Preserving and Re-randomizable RCCA-secure Public Key Encryption and its Applications
     Antonio Faonio, Dario Fiore, Javier Herranz, Carla Ràfols.
     International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). November 2019.
154. LegoSNARK: Modular Design and Composition of Succinct Zero-Knowledge Proofs
     Matteo Campanelli, Dario Fiore, Anaïs Querol.
     ACM Conference on Computer and Communications Security (CCS). November 2019.
155. Efficient UC Commitment Extension with Homomorphism for Free (and Applications)
     Ignacio Cascudo, Ivan Damgård, Bernardo David, Nico Döttling, Rafael Dowsley, Irene Giacomelli.
     International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). November 2019.
156. Abstract Interpretation of Indexed Grammars
     Marco Campion, Mila Dalla Preda, Roberto Giacobazzi.
     Static Analysis Symposium (SAS). October 2019.
157. Runtime Verification for Timed Event Streams with Partial Information
     Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, Daniel Thoma.
     International Conference on Runtime Verification (RV). October 2019.
158. Privatization-safe transactional memories
     Artem Khyzha, Hagit Attiya, Alexey Gotsman.
     International Symposium on Distributed Computing (DISC). October 2019.
159. Towards Computing Abstract Distances in Logic Programs
     I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
     ICLP Tech. Comms.. September 2019.
160. Towards a General Framework for Static Cost Analysis of Parallel Logic Programs
     M. Klemen, P. Lopez-Garcia, J. Gallagher, J.F. Morales, M. V. Hermenegildo.
     ICLP, Tech. Comms.. September 2019.
161. Can I Opt Out Yet?: GDPR and the Global Illusion of Cookie Control
     Iskander Sánchez-Rola, Matteo Dell'Amico, Platon Kotzias, Davide Balzarotti, Leyla Bilge, Pierre-Antoine Vervier, Igor Santos.
     ACM Conference on Computer and Communications Security (CCS). July 2019.
162. White-box atomic multicast
     Alexey Gotsman, Anatole Lefort, Gregory Chockler.
     IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). June 2019.
163. Theory and Practice of Finding Eviction Sets
     Pepe Vila, Boris Köpf, Jose Morales.
     IEEE Symposium on Security and Privacy (SP). May 2019.
164. Polyvariant Program Specialisation with Property-based Abstraction
     John P. Gallagher.
     Computing Research Repository (CoRR). April 2019.
165. Mind your Own Business: A Longitudinal Study of Threats and Vulnerabilities in Enterprises
     Platon Kotzias, Leyla Bilge, Pierre-Antoine Vervier, Juan Caballero.
     Network and Distributed System Security Symposium (NDSS). February 2019.
166. Orion: A distributed file system for non-volatile main memory and RDMA-capable networks
     Jian Yang, Joseph Izraelevitz, Steven Swanson.
     Conference on File and Storage Technologies (FAST). February 2019.
167. Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP
     Joaquín Arias, Manuel Carro.
     Practical Aspects of Declarative Languages (PADL). January 2019.
168. Multivariant Assertion-based Guidance in Abstract Interpretation
     I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). January 2019.
169. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3
     José Bacelar Almeida, Cecile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub.
     ACM Conference on Computer and Communications Security (CCS). 2019.
170. A Machine-Checked Proof of Security for AWS Key Management Service
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran.
     ACM Conference on Computer and Communications Security (CCS). 2019.
171. GALACTICS: Gaussian Sampling for Lattice-Based Constant- Time Implementation of Cryptographic Signatures, Revisited
     Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Mélissa Rossi, Mehdi Tibouchi.
     ACM Conference on Computer and Communications Security (CCS). 2019.
172. Symbolic Methods in Computational Cryptography Proofs
     Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub.
     IEEE Computer Security Foundations Symposium (CSF). 2019.
173. maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults
     Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert.
     European Symposium On Research In Computer Security (ESORICS). 2019.
174. Verifying Relational Properties using Trace Logic
     Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei.
     Formal Methods in Computer-Aided Design (FMCAD). 2019.
175. Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy
     Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata.
     IEEE Symposium on Logic in Computer Science (LICS). 2019.
176. A Congruence-based Perspective on Automata Minimization Algorithms
     Pierre Ganty, Elena Gutiérrez, Pedro Valero.
     International Symposium on Mathematical Foundations of Computer Science (MFCS). 2019.
177. Privacy Amplification by Mixing and Diffusion Mechanisms
     Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek.
     Advances in Neural Information Processing Systems (NeurIPS). 2019.
178. FaCT: a DSL for timing-sensitive computation
     Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2019.
179. Bidirectional type checking for relational properties
     Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2019.
180. Type-level computations for Ruby libraries
     Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2019.
181. Decentralized Stream Runtime Verification
     Luis Miguel Danielsson, César Sánchez.
     International Conference on Runtime Verification (RV). 2019.
182. Language Inclusion Algorithms as Complete Abstract Interpretations
     Pierre Ganty, Francesco Ranzato, Pedro Valero.
     Static Analysis Symposium (SAS). 2019.
183. Deconstructing Stellar Consensus
     Álvaro García-Pérez, Maria A. Schett.
     International Conference on Principles of Distributed Systems (OPODIS). 2019.
184. Design Patterns for Code Reuse in HLS Packet Processing Pipelines
     Haggai Eran, Lior Zeno, Zsolt István, Mark Silberstein.
     IEEE Symposium on Field Programmable Custom Computing Machines (FCCM). 2019.
185. Storing Parquet Tile by Tile: Application-Aware Storage with Deduplication
     Lucas Kuhring, Zsolt István.
     International Conference on Field-Programmable Logic and Applications (FPL). 2019.
186. Reconfigurable Atomic Transaction Commit
     Manuel Bravo, Alexey Gotsman.
     ACM Symposium on Principles of Distributed Computing (PODC). 2019.
187. Verifying Hyperliveness
     Norine Coenen, Bernd Finkbeiner, César Sánchez, Leander Tentrup.
     Computer Aided Verification (CAV). 2019.
188. Regular Expression Search on Compressed Text
     Pierre Ganty, Pedro Valero.
     Data Compression Conference (DCC). 2019.
189. Information-flow Control for Database-backed Applications
     Marco Guarnieri, Musard Balliu, Daniel Schoepe, David Basin, Andrei Sabelfeld.
     IEEE European Symposium on Security and Privacy (EuroS&P). 2019.
190. Hourglass: Leveraging Transient Resources for Time-Constrained Graph Processing in the Cloud
     Pedro Joaquim, Manuel Bravo, Luís Rodrigues, Miguel Matos.
     Eurosys Conference (EuroSys). 2019.
191. Gray-Box Monitoring of Hyperproperties
     Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonakdarpour.
     International Symposium on Formal Methods (FM). 2019.
192. Striver: Stream Runtime Verification for Real-Time Event-Streams
     Felipe Gorostiaga, César Sánchez.
     International Conference on Runtime Verification (RV). November 2018.
193. K-Hunt: Pinpointing Insecure Cryptographic Keys from Execution Traces
     Juanru Li, Zhiqiang Lin, Juan Caballero, Yuanyuan Zhang, Dawu Gu.
     ACM Conference on Computer and Communications Security (CCS). October 2018.
194. Ido: Compiler-directed failure atomicity for nonvolatile memory
     Qingrui Liu, Joseph Izraelevitz, Se Kwon Lee, Michael L. Scott, Sam H. Noh, Changhee Jung.
     International Symposium on Microarchitecture (MICRO). October 2018.
195. Coming of Age: A Longitudinal Study of TLS Deployment
     Platon Kotzias, Abbas Razaghpanah, Johanna Amann, Kenneth G. Paterson, Narseo Vallina-Rodriguez, Juan Caballero.
     Internet Measurement Conference (IMC). October 2018.
196. Matrioska: A Compiler for Multi-Key Homomorphic Signatures
     Dario Fiore, Elena Pagnin.
     Conference on Security and Cryptography for Networks (SCN). September 2018.
197. Static Performance Guarantees for Programs with Run-time Checks
     M. Klemen, N. Stulova, P. Lopez-Garcia, J. F. Morales, M. V. Hermenegildo.
     International Conference on Principles and Practice of Declarative Programming (PPDP). September 2018.
198. Multi-Input Functional Encryption for Inner Products: Function-Hiding Realizations and Constructions without Pairings
     Michel Abdalla, Dario Catalano, Dario Fiore, Romain Gay, Bogdan Ursu.
     Advances in Cryptology (CRYPTO). August 2018.
199. A Flexible K-Means Operator for Hybrid Databases
     Zhenhao He, David Sidler, Zsolt István, Gustavo Alonso.
     International Conference on Field-Programmable Logic and Applications (FPL). August 2018.
200. Providing Multi-tenant Services with FPGAs: Case Study on a Key-Value Store
     Zsolt István, Gustavo Alonso, Ankit Singla.
     International Conference on Field-Programmable Logic and Applications (FPL). August 2018.
201. Translating Code Comments to Procedure Specifications
     Arianna Blasi, Alberto Goffi, Konstantin Kuznetsov, Alessandra Gorla, Michael D. Ernst, Mauro Pezzè, Sergio Delgado Castellanos.
     International Symposium on Software Testing and Analysis (ISSTA). July 2018.
202. Pipekit: A Deployment Tool with Advanced Scheduling and Inter-Service Communication for Multi-Tier Applications
     P. Chico de Guzmán, F. Gorostiaga, C. Sánchez.
     IEEE International Conference on Web Services (ICWS). July 2018.
203. Towards Incremental and Modular Context-sensitive Analysis
     I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
     International Conference on Logic Programming (ICLP). July 2018.
204. On the Security Notions for Homomorphic Signatures
     Dario Catalano, Dario Fiore, Nizzardo Luca.
     International Conference on Applied Cryptography and Network Security (ACNS). June 2018.
205. BCD: Decomposing Binary Code Into Components Using Graph-Based Clustering
     Vishal Karande, Swarup Chandra, Zhiqiang Lin, Juan Caballero, Latifur Khan, Kevin Hamlen.
     Asia Conference on Information, Computer and Communications Security (AsiaCCS). June 2018.
206. RepliComment: Identifying Clones in Code Comments
     Arianna Blasi, Alessandra Gorla.
     IEEE International Conference on Program Comprehension (ICPC). May 2018.
207. What did Really Change with the new Release of the App?
     Paolo Calciati, Konstantin Kuznetsov, Alessandra Gorla.
     IEEE International Working Conference on Mining Software Repositories (MSR). May 2018.
208. Analyzing the User Interface of Android Apps
     Konstantin Kuznetsov, Vitalii Avdiienko, Alessandra Gorla, Andreas Zeller.
     International Conference on Mobile Software Engineering and Systems (MOBILESoft). May 2018.
209. TARANET: Traffic-Analysis Resistant Anonymity at the NETwork layer
     Chen Chen, Daniele E. Asoni, Adrian Perrig, David Barrera, George Danezis, Carmela Troncoso.
     IEEE European Symposium on Security and Privacy (EuroS&P). April 2018.
210. Interval-based memory reclamation
     Haosen Wen, Joseph Izraelevitz, Wentao Cai, H. Alan Beadle, Michael L. Scott.
     Principles and Practice of Parallel Programming (PPoPP). February 2018.
211. Exploiting Term Hiding to Reduce Run-time Checking Overhead
     N. Stulova, J. F. Morales, M. V. Hermenegildo.
     Practical Aspects of Declarative Languages (PADL). January 2018.
212. Sound up-to techniques and Complete abstract domains
     Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic.
     IEEE Symposium on Logic in Computer Science (LICS). 2018.
213. Code Obfuscation Against Abstract Model Checking Attacks
     Roberto Bruni, Roberto Giacobazzi, Roberta Gori.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2018.
214. Program Analysis Is Harder Than Verification: A Computability Perspective
     Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato.
     Computer Aided Verification (CAV). 2018.
215. Symbolic Proofs for Lattice-Based Cryptography
     Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi.
     ACM Conference on Computer and Communications Security (CCS). 2018.
216. Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela.
     IEEE Computer Security Foundations Symposium (CSF). 2018.
217. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic Constant-Time
     Gilles Barthe, Benjamin Grégoire, Vincent Laporte.
     IEEE Computer Security Foundations Symposium (CSF). 2018.
218. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
     Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg.
     European Symposium on Programming (ESOP). 2018.
219. An Assertion-Based Program Logic for Probabilistic Programs
     Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
     European Symposium on Programming (ESOP). 2018.
220. Masking the GLP Lattice-Based Signature Scheme at Any Order
     Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi.
     International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt). 2018.
221. Almost Sure Productivity
     Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva.
     International Colloquium on Automata Languages and Programming (ICALP). 2018.
222. Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences
     Borja Balle, Gilles Barthe, Marco Gaboardi.
     Advances in Neural Information Processing Systems (NeurIPS). 2018.
223. Lower Bounds on Structure-Preserving Signatures for Bilateral Messages
     Masayuki Abe, Miguel Ambrona, Miyako Ohkubo, Mehdi Tibouchi.
     Conference on Security and Cryptography for Networks (SCN). 2018.
224. i2kit: A Deployment Tool with the Simplicity of Containers and the Security of Virtual Machines
     Pablo Chico de Guzmán, Felipe Gorostiaga, César Sánchez.
     International Conference on Web Information Systems Engineering (WISE). 2018.
225. Knock Knock, Who's There? Membership Inference on Aggregate Location Data
     Apostolos Pyrgelis, Carmela Troncoso, Emiliano De Cristofaro.
     Network and Distributed System Security Symposium (NDSS). 2018.
226. Averist: Algorithmic Verifier for Stability of Linear Hybrid Systems
     Miriam García Soto, Pavithra Prabhakar.
     International Conference on Hybrid Systems: Computation and Control (HSCC). 2018.
227. Inferring Energy Bounds via Static Program Analysis and Evolutionary Modeling of Basic Blocks
     U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2018.
228. Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification
     Borzoo Bonakdarpour, César Sánchez, Gerardo Schneider.
     International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). 2018.
229. Fine-Grained Secure Computation
     Matteo Campanelli, Rosario Gennaro.
     Theory of Cryptography Conference (TCC). 2018.
230. COST Action IC1402 Runtime Verification Beyond Monitoring
     Christian Colombo, Yliés Falcone, Martin Leucker, Giles Reger, César Sánchez, Gerardo Schneider, Volker Stolz.
     International Conference on Runtime Verification (RV). 2018.
231. Multi-Shot Distributed Transaction Commit
     Gregory Chockler, Alexey Gotsman.
     International Symposium on Distributed Computing (DISC). 2018.
232. Compositional verification of compiler optimisations on relaxed memory
     Mike Dodds, Mark Batty, Alexey Gotsman.
     European Symposium on Programming (ESOP). 2018.
233. Verification of Immediate Observation Population Protocols
     Javier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy.
     International Conference on Concurrency Theory (CONCUR). 2018.
234. The Parikh Property for Weighted Context-Free Grammars
     Pierre Ganty, Elena Gutiérrez.
     Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2018.
235. TeSSLa: Runtime Verification of Non-synchronized Real-Time Streams
     Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, Alexander Schramm.
     ACM Symposium on Applied Computing (SAC). 2018.
236. Timed Epistemic Knowledge Bases for Social Networks
     Raúl Pardo, César Sánchez, Gerardo Schneider.
     International Symposium on Formal Methods (FM). 2018.
237. Paxos consensus, deconstructed and abstracted
     Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey.
     European Symposium on Programming (ESOP). 2018.
238. Safe privatization in transactional memory
     Artem Khyzha, Hagit Attiya, Alexey Gotsman, Noam Rinetzky.
     Principles and Practice of Parallel Programming (PPoPP). 2018.
239. Automatic Verification of RMA Programs via Abstraction Extrapolation
     Cedric Baumann, Andrei Marian Dan, Yuri Meshman, Torsten Hoefler, Martin T. Vechev.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2018.
240. Online and Offline Stream Runtime Verification of Synchronous Systems
     César Sánchez.
     International Conference on Runtime Verification (RV). 2018.
241. Reliable Smart Contracts: State-of-the-Art, Applications, Challenges and Future Directions
     César Sánchez, Gerardo Schneider, Martin Leucker.
     International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). 2018.
242. Federated Byzantine quorum systems
     Álvaro García-Pérez, Alexey Gotsman.
     International Conference on Principles of Distributed Systems (OPODIS). 2018.
243. Distributed Transactional Reads: The Strong, the Quick, the Fresh & the Impossible
     Alejandro Z. Tomsic, Manuel Bravo, Marc Shapiro.
     ACM/IFIP/USENIX International Middleware Conference (Middleware). 2018.
244. Fixing the State Budget: Approximation of Regular Languages with Small DFAs
     Graeme Gange, Pierre Ganty, Peter J. Stuckey.
     International Symposium on Automated Technology for Verification and Analysis (ATVA). October 2017.
245. A Language-Theoretic View on Network Protocols
     Pierre Ganty, Boris Köpf, Pedro Valero.
     International Symposium on Automated Technology for Verification and Analysis (ATVA). October 2017.
246. Towards formal model-based analysis and testing of Android's security mechanisms
     G. Betarte, J. Campo, M. Cristiá, F. Gorostiaga, C. Luna, C. Sanz.
     Conferencia Latinoamericana En Informatica (CLEI). September 2017.
247. Labeled Homomorphic Encryption: Scalable and Privacy-Preserving Processing of Outsourced Data
     Manuel Barbosa, Dario Catalano, Dario Fiore.
     European Symposium On Research In Computer Security (ESORICS). September 2017.
248. Parikh Image of Pushdown Automata
     Pierre Ganty, Elena Gutiérrez.
     International Symposium on Fundamentals of Computation Theory (FCT). September 2017.
249. Practical Functional Encryption for Quadratic Functions with Applications to Predicate Encryption
     Carmen Elisabetta Zaira Baltico, Dario Catalano, Dario Fiore, Romain Gay.
     Advances in Cryptology (CRYPTO). August 2017.
250. Detecting behavior anomalies in graphical user interfaces
     Vitalii Avdiienko, Konstantin Kuznetsov, Isabelle Rommelfanger, Andreas Rau, Alessandra Gorla, Andreas Zeller.
     International Conference on Software Engineering (ICSE). May 2017.
251. How Do Apps Evolve in Their Permission Requests?: A Preliminary Study
     Paolo Calciati, Alessandra Gorla.
     IEEE International Working Conference on Mining Software Repositories (MSR). May 2017.
252. A Lustrum of Malware Network Communication: Evolution and Insights
     Chaz Lever, Platon Kotzias, Davide Balzarotti, Juan Caballero, Manos Antonakakis.
     IEEE Symposium on Security and Privacy (SP). May 2017.
253. Small Data
     Oliver Kennedy, D. Richard Hipp, Stratos Idreos, Amélie Marian, Arnab Nandi, Carmela Troncoso, Eugene Wu.
     International Conference on Data Engineering (ICDE). April 2017.
254. O!Snap: Cost-Efficient Testing in the Cloud
     Alessio Gambi, Alessandra Gorla, Andreas Zeller.
     International Conference on Software Testing, Verification and Validation (ICST). March 2017.
255. Filter design for delay-based anonymous communications
     Simon Oya, Fernando Pérez-González, Carmela Troncoso.
     IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP). March 2017.
256. App Mining
     Vitalii Avdiienko, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller, Steven Arzt, Siegfried Rasthofer, Eric Bodden.
     Systems Engineering. February 2017.
257. Vergleich und Kombination von Techniken des Predictive Business Process Monitoring
     Andreas Metzger, Philipp Leitner, Dragan Ivanovic, Eric Schmieders, Rod Franklin, Manuel Carro, Schahram Dustdar, Klaus Pohl.
     Systems Engineering. February 2017.
258. Dissecting Tor Bridges: a Security Evaluation of their Private and Public Infrastructures
     Srdjan Matic, Carmela Troncoso, Juan Caballero.
     Network and Distributed System Security Symposium (NDSS). February 2017.
259. Rule Formats for Nominal Process Calculi
     Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, Yolanda Ortega-Mallén.
     International Conference on Concurrency Theory (CONCUR). 2017.
260. A Fast and Verified Software Stack for Secure Function Evaluation
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira.
     ACM Conference on Computer and Communications Security (CCS). 2017.
261. Jasmin: High-Assurance and High-Speed Cryptography
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub.
     ACM Conference on Computer and Communications Security (CCS). 2017.
262. Zero-knowledge contingent payments revisited: Attacks and payments for services
     Matteo Campanelli, Rosario Gennaro, Steven Goldfeder, Luca Nizzardo.
     ACM Conference on Computer and Communications Security (CCS). 2017.
263. Verified Translation Validation of Static Analyses
     Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu.
     IEEE Computer Security Foundations Symposium (CSF). 2017.
264. Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions
     Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee.
     ACM Conference on Computer and Communications Security (CCS). 2017.
265. Generic Transformations of Predicate Encodings: Constructions and Applications
     Miguel Ambrona, Gilles Barthe, Benedikt Schmidt.
     Advances in Cryptology (CRYPTO). 2017.
266. Is Your Software on Dope? - Formal Analysis of Surreptitiously enhanced Programs
     Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns.
     European Symposium on Programming (ESOP). 2017.
267. Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
     Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub.
     International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt). 2017.
268. Reasoning about Probabilistic Defense Mechanisms against Remote Attacks
     Martín Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, Vijay Ganesh.
     IEEE European Symposium on Security and Privacy (EuroS&P). 2017.
269. Parikh Image of Pushdown Automata
     Pierre Ganty, Elena Gutiérrez.
     International Symposium on Fundamentals of Computation Theory (FCT). 2017.
270. Formal Synthesis of Stabilizing Controllers for Switched Systems
     Pavithra Prabhakar, Miriam García Soto.
     International Conference on Hybrid Systems: Computation and Control (HSCC). 2017.
271. *-Liftings for Differential Privacy
     Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub.
     International Colloquium on Automata Languages and Programming (ICALP). 2017.
272. Proving uniformity and independence by self-composition and coupling
     Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
     Logic Programming and Automated Reasoning (LPAR). 2017.
273. SQL-PL4OCL: An Automatic Code Generator from OCL to SQL Procedural Language
     Marina Egea, Carolina Dania.
     International Conference on Model Driven Engineering Languages and Systems (MODELS). 2017.
274. Coupling proofs are probabilistic product programs
     Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2017.
275. Relational cost analysis
     Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2017.
276. Machine-Checked Proofs of Privacy for Electronic Voting Protocols
     Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi.
     IEEE Symposium on Security and Privacy (SP). 2017.
277. Unilaterally-Authenticated Key Exchange
     Yevgeniy Dodis, Dario Fiore.
     Financial Cryptography and Data Security Conference (FC). 2017.
278. Feature importance scores and lossless feature pruning using Banzhaf power indices
     Bogdan Kulynych, Carmela Troncoso.
     NIPS 2017 Symposium on Interpretable Machine Learning. 2017.
279. Back to the Drawing Board: Revisiting the Design of Optimal Location Privacy-preserving Mechanisms
     Simon Oya, Carmela Troncoso, Fernando Pérez-González.
     ACM Conference on Computer and Communications Security (CCS). 2017.
280. Security Analysis of Cache Replacement Policies
     Pablo Cañones, Boris Köpf, Jan Reineke.
     International Conference on Principles of Security and Trust (POST). 2017.
281. Concurrent Data Structures Linked in Time
     Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
     European Conference on Object-Oriented Programming (ECOOP). 2017.
282. Rigorous Analysis of Software Countermeasures against Cache Attacks
     Goran Doychev, Boris Köpf.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2017.
283. Consistency models with global operation sequencing and their composition
     Alexey Gotsman, Sebastian Burckhardt.
     International Symposium on Distributed Computing (DISC). 2017.
284. Proving linearizability using partial orders
     Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson.
     European Symposium on Programming (ESOP). 2017.
285. Loophole: Timing Attacks on Shared Event Loops in Chrome
     Pepe Vila, Boris Köpf.
     Usenix Security Symposium (USENIX-Security). 2017.
286. A Systematic Study of Cache Side Channels across AES Implementations
     Heiko Mantel, Alexandra Weber, Boris Köpf.
     Engineering Secure Software and Systems (ESSoS). 2017.
287. Towards Run-time Checks Simplification via Term Hiding (extended abstract)
     N. Stulova, J.F. Morales, M.V. Hermenegildo.
     Tech. Comm. of ICLP'17. 2017.
288. Algebraic laws for weak consistency
     Andrea Cerone, Alexey Gotsman, Hongseok Yang.
     International Conference on Concurrency Theory (CONCUR). 2017.
289. Computer-aided verification for mechanism design
     Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub.
     International Conference on Web and Internet Economics (WINE). December 2016.
290. RevProbe: Detecting Silent Reverse Proxies in Malicious Server Infrastructures
     Antonio Nappa, Rana Faisal Munir, Irfan Khan Tanoli, Christian Kreibich, Juan Caballero.
     Annual Computer Security Applications Conference (ACSAC). December 2016.
291. Description and Evaluation of a Generic Design to Integrate CLP and Tabled Execution
     Joaquín Arias, Manuel Carro.
     International Conference on Principles and Practice of Declarative Programming (PPDP). September 2016.
292. AVClass: A Tool for Massive Malware Labeling
     Marcos Sebastián, Richard Rivera, Platon Kotzias, Juan Caballero.
     The International Symposium on Research in Attacks, Intrusions and Defenses (RAID). September 2016.
293. A Look into 30 Years of Malware Development from a Software Metrics Perspective
     Alejandro Calleja, Juan Tapiador, Juan Caballero.
     The International Symposium on Research in Attacks, Intrusions and Defenses (RAID). September 2016.
294. Reducing the Overhead of Assertion Run-time Checks via Static Analysis
     N. Stulova, J.F. Morales, M.V. Hermenegildo.
     International Conference on Principles and Practice of Declarative Programming (PPDP). September 2016.
295. Measuring PUP Prevalence and PUP Distribution through Pay-Per-Install Services
     Platon Kotzias, Leyla Bilge, Juan Caballero.
     Usenix Security Symposium (USENIX-Security). August 2016.
296. Automatic Generation of Oracles for Exceptional Behaviors
     Alberto Goffi, Alessandra Gorla, Michael D. Ernst, Mauro Pezzè.
     International Symposium on Software Testing and Analysis (ISSTA). July 2016.
297. A Transformational Approach to Parametric Accumulated-cost Static Profiling
     R. Haemmerlé, P. Lopez-Garcia, U. Liqat, M. Klemen, J. P. Gallagher, M. V. Hermenegildo.
     International Symposium on Functional and Logic Programming (FLOPS). March 2016.
298. Multi-Key Homomorphic Authenticators
     Dario Fiore, Aikaterini Mitrokotsa, Luca Nizzardo, Elena Pagnin.
     International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). 2016.
299. Relational Logic with Framing and Hypotheses
     Anindya Banerjee, David A. Schmidt, Mohammad Nikouei.
     Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2016.
300. Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data
     Dario Fiore, Cédric Fournet, Esha Gosh, Markulf Kohlweiss, Olga Ohrimenko, Bryan Parno.
     ACM Conference on Computer and Communications Security (CCS). 2016.
301. A Certified Compiler for Verifiable Computing
     Cédric Fournet, Chantal Keller, Vincent Laporte.
     IEEE Computer Security Foundations Symposium (CSF). 2016.
302. Synthesizing Probabilistic Invariants via Doob's Decomposition
     Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu.
     Computer Aided Verification (CAV). 2016.
303. Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata
     Bishoksan Kafle, John P. Gallagher, José F. Morales.
     Computer Aided Verification (CAV). 2016.
304. Strong Non-Interference and Type-Directed Higher-Order Masking
     Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini.
     ACM Conference on Computer and Communications Security (CCS). 2016.
305. Differentially Private Bayesian Programming
     Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub.
     ACM Conference on Computer and Communications Security (CCS). 2016.
306. Advanced Probabilistic Couplings for Differential Privacy
     Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
     ACM Conference on Computer and Communications Security (CCS). 2016.
307. Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
     Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub.
     International Conference on Certified Programs and Proofs (CPP). 2016.
308. An Algorithmic Approach to Global Asymptotic Stability Verification of Hybrid Systems
     Pavithra Prabhakar, Miriam García Soto.
     ACM Conference on Embedded Software (EMSOFT). 2016.
309. Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model
     Miguel Ambrona, Gilles Barthe, Benedikt Schmidt.
     International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt). 2016.
310. A Theory of Slicing for Probabilistic Control Flow Graphs
     Torben Amtoft, Anindya Banerjee.
     Foundations of Software Science and Computational Structures (FOSSACS). 2016.
311. Smarticipation: intelligent personal guidance of human behavior utilizing anticipatory models
     Christian Meurisch, Usman Naeem, Muhammad Awais Azam, Frederik Janssen, Benedikt Schmidt, Max Mühlhäuser.
     ACM International Joint Conference on Pervasive and Ubiquitous Computing (UbiComp). 2016.
312. A Program Logic for Union Bounds
     Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
     International Colloquium on Automata Languages and Programming (ICALP). 2016.
313. Process Compliance Checking using Taint Flow Analysis
     Alexander Seeliger, Timo Nolle, Benedikt Schmidt, Max Mühlhäuser.
     International Conference on Information Systems (ICIS). 2016.
314. Facets of Software Doping
     Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns.
     International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). 2016.
315. Verification Techniques for Hybrid Systems
     Pavithra Prabhakar, Miriam García Soto, Ratan Lal.
     International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). 2016.
316. What Belongs Together Comes Together: Activity-centric Document Clustering for Information Work
     Alexander Seeliger, Benedikt Schmidt, Immanuel Schweizer, Max Mühlhäuser.
     International Conference on Intelligent User Interfaces (IUI). 2016.
317. Proving Differential Privacy via Probabilistic Couplings
     Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
     IEEE Symposium on Logic in Computer Science (LICS). 2016.
318. Fine-Grained Energy Modeling for the Source Code of a Mobile Application
     Xueliang Li, John P. Gallagher.
     International Conference on Mobile and Ubiquitous Systems: Networks and Services (Mobiquitous). 2016.
319. OCL2MSFOL: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints
     Carolina Dania, Manuel Clavel.
     International Conference on Model Driven Engineering Languages and Systems (MODELS). 2016.
320. Dependent types and multi-monadic effects in F
     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.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2016.
321. Completeness in Approximate Transduction
     Mila Dalla Preda, Roberto Giacobazzi, Isabella Mastroeni.
     Static Analysis Symposium (SAS). 2016.
322. Key Confirmation in Key Exchange: A Formal Treatment and Implications for TLS 1.3
     Marc Fischlin, Felix Günther, Benedikt Schmidt, Bogdan Warinschi.
     IEEE Symposium on Security and Privacy (SP). 2016.
323. Bounded-oscillation Pushdown Automata
     Pierre Ganty, Damir Valput.
     International Symposium on Games, Automata, Logics and Formal Verification (GandALF). 2016.
324. An abstract memory functor for verified C static analyzers
     Sandrine Blazy, Vincent Laporte, David Pichardie.
     International Conference on Functional Programming (ICFP). 2016.
325. A Source-level Energy Optimization Framework for Mobile Applications
     Xueliang Li, John P. Gallagher.
     IEEE Working Conference on Source Code Analysis and Manipulation (SCAM). 2016.
326. Nearly Optimal Verifiable Data Streaming
     Johannes Krupp, Dominique Schroeder, Mark Simkin, Dario Fiore, Giuseppe Ateniese, Stefan Nuernberger.
     International Conference on Practice and Theory in Public Key Cryptography (PKC). 2016.
327. On the (In)security of SNARKs in the Presence of Oracles
     Dario Fiore, Anca Nitulescu.
     Theory of Cryptography Conference (TCC). 2016.
328. Inferring Energy Bounds Statically by Evolutionary Analysis of Basic Blocks
     U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
     (HIP3ES'16). 2016.
329. Counterexample Guided Abstraction Refinement for Stability Analysis
     Pavithra Prabhakar, Miriam García Soto.
     Computer Aided Verification (CAV). 2016.
330. 'Cause I'm strong enough: reasoning about consistency choices in distributed systems
     Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2016.
331. Symbolic Abstract Data Type Inference
     Michael Emmi, Constantin Enea.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2016.
332. Verifying Constant-Time Implementations
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi.
     Usenix Security Symposium (USENIX-Security). 2016.
333. Specification and Complexity of Collaborative Text Editing
     Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, Marek Zawirski.
     ACM Symposium on Principles of Distributed Computing (PODC). 2016.
334. Model Checking Population Protocols
     Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
     Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2016.
335. Hybridization for Stability Analysis of Switched Linear Systems
     Pavithra Prabhakar, Miriam García Soto.
     International Conference on Hybrid Systems: Computation and Control (HSCC). 2016.
336. Specification of Evolving Privacy Policies for Online Social Networks
     Raúl Pardo, Ivana Kellyerova, César Sánchez, Gerardo Schneider.
     International Symposium on Temporal Representation and Reasoning (TIME). 2016.
337. Robustness against Consistency Models with Atomic Visibility
     Giovanni Bernardi, Alexey Gotsman.
     International Conference on Concurrency Theory (CONCUR). 2016.
338. Hoare-style Specifications As Correctness Conditions for Non-linearizable Concurrent Objects
     Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco.
     ACM Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA). 2016.
339. Analysing Snapshot Isolation
     Andrea Cerone, Alexey Gotsman.
     ACM Symposium on Principles of Distributed Computing (PODC). 2016.
340. A Generic Logic for Proving Linearizability
     Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson.
     International Symposium on Formal Methods (FM). 2016.
341. Automated Test Input Generation for Android: Are We There Yet?
     Shauvik Roy Choudhary, Alessandra Gorla, Alessandro Orso.
     International Conference on Automated Software Engineering (ASE). November 2015.
342. CARONTE: Detecting Location Leaks for Deanonymizing Tor Hidden Services
     Srdjan Matic, Platon Kotzias, Juan Caballero.
     ACM Conference on Computer and Communications Security (CCS). October 2015.
343. Certified PUP: Abuse in Authenticode Code Signing
     Platon Kotzias, Srdjan Matic, Richard Rivera, Juan Caballero.
     ACM Conference on Computer and Communications Security (CCS). October 2015.
344. A Haskell Implementation of a Rule-Based Program Transformation for C Programs
     Salvador Tamarit, Guillermo Vigueras, Manuel Carro, Julio Mariño.
     Practical Aspects of Declarative Languages (PADL). June 2015.
345. Mining Apps for Abnormal Usage of Sensitive Data
     Vitalii Avdiienko, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller, Steven Arzt, Siegfried Rasthofer, Eric Bodden.
     International Conference on Software Engineering (ICSE). May 2015.
346. Ad Injection at Scale: Assessing Deceptive Advertisement Modifications
     Kurt Thomas, Elie Bursztein, Nav Jagpal, Moheeb Abu, Niels Provos, Paul Pearce, Grant Hoand Damon McCoy, Chris Grier, Vern Paxson, Antonio Nappa, Alexandros Kapravelos.
     IEEE Symposium on Security and Privacy (SP). May 2015.
347. The Attack of the Clones: A Study of the Impact of Shared Code on Vulnerability Patching
     Antonio Nappa, Richard Johnson, Leyla Bilge, Juan Caballero, Tudor Dimitras.
     IEEE Symposium on Security and Privacy (SP). May 2015.
348. Automated Proofs of Pairing-based Cryptography
     Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt.
     ACM Conference on Computer and Communications Security (CCS). 2015.
349. Mind the Gap: Modular Machine-checked Proofs of One-round Key Exchange Protocols
     Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt.
     International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt). 2015.
350. Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds
     Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi.
     International Conference on Practice and Theory in Public Key Cryptography (PKC). 2015.
351. Programmable Hash Functions go Private: Constructions and Applications to (Homomorphic) Signatures with Shorter Public Keys
     Dario Catalano, Dario Fiore, Luca Nizzardo.
     Advances in Cryptology (CRYPTO). 2015.
352. Using Linearly-Homomorphic Encryption to Evaluate Degree-2 Functions on Encrypted Data
     Dario Catalano, Dario Fiore.
     ACM Conference on Computer and Communications Security (CCS). 2015.
353. Two Decades of Maude
     Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Martí-Oliet, Carolyn L. Talcott.
     Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday. 2015.
354. Verified Proofs of Higher-Order Masking
     Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub.
     International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt). 2015.
355. Deciding Concurrent Planar Monotonic Linear Hybrid Systems
     Pavithra Prabhakar, Nima Roohi, Mahesh Viswanathan.
     International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). 2015.
356. Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
     Patrick Baillot, Gilles Barthe, Ugo Dal Lago.
     Logic Programming and Automated Reasoning (LPAR). 2015.
357. Relational Reasoning via Probabilistic Coupling
     Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub.
     Logic Programming and Automated Reasoning (LPAR). 2015.
358. Model Checking Parameterized Asynchronous Shared-Memory Systems
     Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
     Computer Aided Verification (CAV). 2015.
359. Model-Based Formal Reasoning about Data-Management Applications
     Carolina Dania, Manuel Clavel.
     Fundamental Approaches to Software Engineering (FASE). 2015.
360. Formal Reasoning about Fine-Grained Access Control Policies
     Miguel Ángel García de Dios, Carolina Dania, Manuel Clavel.
     Asia-Pacific Conference on Conceptual Modelling (APCCM). 2015.
361. Verification of Population Protocols
     Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
     International Conference on Concurrency Theory (CONCUR). 2015.
362. From Non-Zenoness Verification to Termination
     Pierre Ganty, Samir Genaim, Ratan Lal, Pavithra Prabhakar.
     International Conference on Formal Methods and Models for System Design (MEMOCODE). 2015.
363. Interprocedural Reachability for Flat Integer Programs
     Pierre Ganty, Radu Iosif.
     International Symposium on Fundamentals of Computation Theory (FCT). 2015.
364. Analyzing Program Analyses
     Roberto Giacobazzi, Francesco Logozzo, Francesco Ranzato.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2015.
365. Analyzing First-Order Role Based Access Control
     Carlos Cotrini Jiménez, Thilo Weghorn, David A. Basin, Manuel Clavel.
     IEEE Computer Security Foundations Symposium (CSF). 2015.
366. Tree automata-based refinement with application to Horn clause verification
     Bishoksan Kafle, John P. Gallagher.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2015.
367. Synthesis of Equivalent Method Calls in Guava
     Andrea Mattavelli, Alberto Goffi, Alessandra Gorla.
     International Symposium on Search Based Software Engineering (SSBSE). 2015.
368. Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables
     Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia, Isabella Mastroeni.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2015.
369. Bounded error flowpipe computation of parameterized linear systems
     Ratan Lal, Pavithra Prabhakar.
     ACM Conference on Embedded Software (EMSOFT). 2015.
370. ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data
     Michael Backes, Manuel Barbosa, Dario Fiore, Raphael M. Reischuk.
     IEEE Symposium on Security and Privacy (SP). 2015.
371. A Practical Approach for Energy Efficient Scheduling in Multicore Environments by combining Evolutionary and YDS Algorithms with Faster Energy Estimation
     Z. Banković, U. Liqat, P. Lopez-Garcia.
     IFIP TC12 Publications (IFIP12). 2015.
372. Improved Energy-aware Stochastic Scheduling based on Evolutionary Algorithms via Copula-based Modeling of Task Dependences
     Z. Banković, P. Lopez-Garcia.
     Soft Computing Models in Industrial and Environmental Applications (SOCO). 2015.
373. Energy Efficient Allocation and Scheduling for DVFS-enabled Multicore Environments using a Multiobjective Evolutionary Algorithm
     Z. Banković, P. Lopez-Garcia.
     Genetic and Evolutionary Computations (GECCO). 2015.
374. Trading-off Accuracy vs. Energy in Multicore Processors via Evolutionary Algorithms Combining Loop Perforation and Static Analysis-based Scheduling
     Z. Banković, U. Liqat, P. Lopez-Garcia.
     Hybrid Artificial Intelligent Systems (HAIS 2015). 2015.
375. Transaction chopping for parallel snapshot isolation
     Andrea Cerone, Alexey Gotsman, Hongseok Yang.
     International Symposium on Distributed Computing (DISC). 2015.
376. Composite replicated data types
     Alexey Gotsman, Hongseok Yang.
     European Symposium on Programming (ESOP). 2015.
377. Systematic Asynchrony Bug Exploration for Android Apps
     Burcu Kulahcioglu Ozkan, Michael Emmi, Serdar Tasiran.
     Computer Aided Verification (CAV). 2015.
378. Analysis of Asynchronous Programs with Event-Based Synchronization
     Michael Emmi, Pierre Ganty, Rupak Majumdar, Fernando Rosa-Velardo.
     European Symposium on Programming (ESOP). 2015.
379. On Reducing Linearizability to State Reachability
     Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
     International Colloquium on Automata Languages and Programming (ICALP). 2015.
380. Monitoring Refinement via Symbolic Reasoning
     Michael Emmi, Constantin Enea, Jad Hamza.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2015.
381. Tractable Refinement Checking for Concurrent Objects
     Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2015.
382. SMACK+Corral: A Modular Verifier - (Competition Contribution)
     Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric.
     International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2015.
383. Rational Protection Against Timing Attacks
     Goran Doychev, Boris Köpf.
     IEEE Computer Security Foundations Symposium (CSF). 2015.
384. Towards Energy Consumption Verification via Static Analysis
     P. Lopez-Garcia, R. Haemmerlé, M. Klemen, U. Liqat, M. V. Hermenegildo.
     WS on High Perf. Energy Efficient Embedded Sys. (HIP3ES). 2015.
385. Algorithms for Model Checking HyperLTL and HyperCTL*
     Bernd Finkbeiner, Markus N. Rabe, César Sánchez.
     Proc. of the 27th Int’l Conf. on Computer Aided Verification (CAV'15). 2015.
386. A framework for transactional consistency models with atomic visibility
     Andrea Cerone, Giovanni Bernardi, Alexey Gotsman.
     International Conference on Concurrency Theory (CONCUR). 2015.
387. Pre-Indexed Terms for Prolog
     J.F. Morales, M. V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2015.
388. Reasoning about the Trade-off between Security and Performance
     Boris Köpf.
     Proc. 12th International Conference on Quantitative Evaluation of Systems (QEST ‘15). 2015.
389. Symbolic Polytopes for Quantitative Interpolation and Verification
     Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko.
     Computer Aided Verification (CAV). 2015.
390. Foundations of Quantitative Predicate Abstraction for Stability Analysis of Hybrid Systems
     Pavithra Prabhakar, Miriam Garcia Soto.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2015.
391. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
     Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
     European Symposium on Programming (ESOP). 2015.
392. Mechanized Verification of Fine-grained Concurrent Programs
     Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2015.
393. A Model-driven Methodology for Generating and Verifying CSP-based Java Code
     Julio Mariño, Raúl N.N. Alborodo.
     Communicating Process Architectures 2015, Proceedings of the 37th WoTUG Conference on Concurrent and Parallel Systems. 2015.
394. An XFEM/CZM implementation for massively parallel simulations of composites fracture
     Antoine Jerusalem, Guillermo Vigueras, Federico Sket, Cristobal Samaniego, Ling Wu, Ludovic Noels, Denny Tjahjanto, Eva Casoni, Guillaume Houzeaux, Ahmed Makradi, Jon M. Molina-Aldareguia, Mariano Vazquez.
     European Solid Mechanics Conference, ESMC 2015. 2015.
395. Network Dialog Minimization and Network Dialog Diffing: Two Novel Primitives for Network Security Applications
     M. Zubair Rafique, Juan Caballero, Christophe Huygens, Wouter Joosen.
     Annual Computer Security Applications Conference (ACSAC). December 2014.
396. System-level Non-interference for Constant-time Cryptography
     Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie.
     ACM Conference on Computer and Communications Security (CCS). November 2014.
397. AutoProbe: Towards Automatic Active Malicious Server Probing Using Dynamic Binary Analysis
     Zhaoyan Xu, Antonio Nappa, Robert Baykov, Guangliang Yang, Juan Caballero, Guofei Gu.
     ACM Conference on Computer and Communications Security (CCS). November 2014.
398. Synthesis of Fault Attacks on Cryptographic Implementations
     Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz.
     ACM Conference on Computer and Communications Security (CCS). November 2014.
399. Transforming Service Compositions into Cloud-Friendly Actor Networks
     Dragan Ivanovic, Manuel Carro.
     International Conference on Service Oriented Computing (ICSOC). November 2014.
400. Towards QoS Prediction Based on Composition Structure Analysis and Probabilistic Models
     Dragan Ivanović, Manuel Carro, Peerachai Kaowichakorn.
     International Conference on Service Oriented Computing (ICSOC). November 2014.
401. WhoWas: A Platform for Measuring Web Deployments on IaaS Clouds
     Liang Wang, Antonio Nappa, Juan Caballero, Thomas Ristenpart, Aditya Akella.
     Internet Measurement Conference (IMC). November 2014.
402. On Combining Backward and Forward Chaining in Constraint Logic Programming
     R. Haemmerlé.
     International Conference on Principles and Practice of Declarative Programming (PPDP). September 2014.
403. Assertion-based Debugging of Higher-Order (C)LP Programs
     N. Stulova, J.F. Morales, M.V. Hermenegildo.
     International Conference on Principles and Practice of Declarative Programming (PPDP). September 2014.
404. SigPath: A Memory Graph Based Approach for Program Data Introspection and Modification
     David Urbina, Yufei Gu, Juan Caballero, Zhiqiang Lin.
     European Symposium On Research In Computer Security (ESORICS). September 2014.
405. Certified Synthesis of Efficient Batch Verifiers
     Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub.
     IEEE Computer Security Foundations Symposium (CSF). July 2014.
406. Proving differential privacy in Hoare logic
     Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub.
     IEEE Computer Security Foundations Symposium (CSF). July 2014.
407. CyberProbe: Towards Internet-Scale Active Detection of Malicious Servers
     Antonio Nappa, Zhaoyan Xu, Juan Caballero, Guofei Gu.
     Network and Distributed System Security Symposium (NDSS). February 2014.
408. Validation of a Security Metamodel for the Development of Cloud Applications
     Marcos Arjona, Carolina Dania, Marina Egea, Antonio Maña.
     International Conference on Model Driven Engineering Languages and Systems (MODELS). 2014.
409. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
     Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2014.
410. Panel Discussion: Proposals for Improving OCL
     Achim D. Brucker, Tony Clark, Carolina Dania, Geri Georg, Martin Gogolla, Frédéric Jouault, Ernest Teniente, Burkhart Wolff.
     International Conference on Model Driven Engineering Languages and Systems (MODELS). 2014.
411. Homomorphic Signatures with Efficient Verification for Polynomial Functions
     Dario Catalano, Dario Fiore, Bogdan Warinschi.
     Advances in Cryptology (CRYPTO). 2014.
412. Efficiently Verifiable Computation on Encrypted Data
     Dario Fiore, Rosario Gennaro, Valerio Pastro.
     ACM Conference on Computer and Communications Security (CCS). 2014.
413. Using Higher-Order Contracts to Model Session Types (Extended Abstract)
     Giovanni Bernardi, Matthew Hennessy.
     International Conference on Concurrency Theory (CONCUR). 2014.
414. Automated Analysis of Cryptographic Assumptions in Generic Group Models
     Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt.
     Advances in Cryptology (CRYPTO). 2014.
415. Proving the TLS Handshake Secure (As It Is)
     Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin.
     Advances in Cryptology (CRYPTO). 2014.
416. Switching control of dynamical systems from metric temporal logic specifications
     Jun Liu, Pavithra Prabhakar.
     IEEE International Conference on Robotics and Automation (ICRA). 2014.
417. A Formal Library for Elliptic Curves in the Coq Proof Assistant
     Evmorfia-Iro Bartzia, Pierre-Yves Strub.
     Conference on Interactive Theorem Proving (ITP). 2014.
418. Probabilistic relational verification for cryptographic implementations
     Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2014.
419. Gradual typing embedded securely in JavaScript
     Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2014.
420. A Logical Analysis of Framing for Specifications with Pure Method Calls
     Anindya Banerjee, David A. Naumann.
     Verified Software: Theories (VSTTE). 2014.
421. Modeling Social Networking Privacy
     Carolina Dania, Manuel Clavel.
     International Symposium on Theoretical Aspects of Software Engineering (TASE). 2014.
422. Generalizing Homomorphic MACs for Arithmetic Circuits
     Dario Catalano, Dario Fiore, Rosario Gennaro, Luca Nizzardo.
     International Conference on Practice and Theory in Public Key Cryptography (PKC). 2014.
423. Interactive Encryption and Message Authentication
     Yevgeniy Dodis, Dario Fiore.
     Conference on Security and Cryptography for Networks (SCN). 2014.
424. Automated Verification of Group Key Agreement Protocols
     Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin.
     IEEE Symposium on Security and Privacy (SP). 2014.
425. Modular, higher-order cardinality analysis in theory and practice
     Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2014.
426. Characterising Testing Preorders for Broadcasting Distributed Systems
     Andrea Cerone, Matthew Hennessy.
     Trustworthy Global Computing (TGC). 2014.
427. Leakage Resilience against Concurrent Cache Attacks
     Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa.
     International Conference on Principles of Security and Trust (POST). 2014.
428. Visibly Linear Temporal Logic
     Laura Bozzelli, César Sánchez.
     International Joint Conference on Automated Reasoning (IJCAR). 2014.
429. Foundations of Boolean Stream Runtime Verification
     Laura Bozzelli, César Sánchez.
     International Conference on Runtime Verification (RV). 2014.
430. Temporal Logics for Hyperproperties
     Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez.
     International Conference on Principles of Security and Trust (POST). 2014.
431. SMACK: Decoupling Source Language Details from Verifier Implementations
     Zvonimir Rakamaric, Michael Emmi.
     Computer Aided Verification (CAV). 2014.
432. Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS
     Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub.
     IEEE Symposium on Security and Privacy (SP). 2014.
433. Exploiting synchronization in the analysis of shared-memory asynchronous programs
     Michael Emmi, Burcu Kulahcioglu Ozkan, Serdar Tasiran.
     International SPIN Symposium on Model Checking of Software (SPIN). 2014.
434. Replicated data types: specification, verification, optimality
     Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2014.
435. Ordered Counter Abstraction (Refinable Subword Relations for Parameterized Verification)
     Pierre Ganty, Ahmed Rezine.
     International Conference on Language and Automata Theory and Applications (LATA). 2014.
436. Energy Consumption Analysis of Programs based on XMOS ISA-Level Models
     U. Liqat, S. Kerrison, A. Serrano, K. Georgiou, P. Lopez-Garcia, N. Grech, M. V. Hermenegildo, K. Eder.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2014.
437. Modular Reasoning about Heap Paths via Effectively Propositional Formulas
     Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2014.
438. Parameterised linearisability
     Andrea Cerone, Alexey Gotsman, Hongseok Yang.
     International Colloquium on Automata Languages and Programming (ICALP). 2014.
439. Communicating State Transition Systems for Fine-Grained Concurrent Resources
     Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, German Andres Delbianco.
     European Symposium on Programming (ESOP). 2014.
440. An algorithmic approach to stability verification of polyhedral switched systems
     Pavithra Prabhakar, Miriam Garcia Soto.
     American Control Conference (ACC). 2014.
441. Formal Verification of Skiplists with Arbitrarily Many Levels
     Alejandro Sánchez, César Sánchez.
     International Symposium on Automated Technology for Verification and Analysis (ATVA). 2014.
442. LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes
     Alejandro Sánchez, César Sánchez.
     Computer Aided Verification (CAV). 2014.
443. Parametrized Verification Diagrams
     Alejandro Sánchez, César Sánchez.
     International Symposium on Temporal Representation and Reasoning (TIME). 2014.
444. On Duality Relations for Session Types
     Giovanni Bernardi, Ornela Dardha, Simon J. Gay, Dimitrios Kouzapas.
     Trustworthy Global Computing (TGC). 2014.
445. Safety of live transactions in transactional memory: TMS is necessary and sufficient
     Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky.
     International Symposium on Distributed Computing (DISC). 2014.
446. Fully automated analysis of padding-based encryption in the computational model
     Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella Béguelin.
     ACM Conference on Computer and Communications Security (CCS). November 2013.
447. POSTER: Cross-Platform Malware: Write Once, Infect Everywhere
     Martina Lindorfer, Matthias Neumayr, Juan Caballero, Christian Platzer.
     ACM Conference on Computer and Communications Security (CCS). November 2013.
448. FIRMA: Malware Clustering and Network Signature Generation with Mixed Network Behaviors
     M. Zubair Rafique, Juan Caballero.
     The International Symposium on Research in Attacks, Intrusions and Defenses (RAID). October 2013.
449. Sized Type Analysis for Logic Programs
     A. Serrano, P. Lopez-Garcia, F. Bueno, M. V. Hermenegildo.
     TPLP (29th ICLP'13 Special Issue), on-line supplement (technical communication). August 2013.
450. Driving in the Cloud: An Analysis of Drive-by Download Operations and Abuse Reporting
     Antonio Nappa, M. Zubair Rafique, Juan Caballero.
     GI International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA). July 2013.
451. Supporting Pruning in Tabled LP
     P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
     Practical Aspects of Declarative Languages (PADL). January 2013.
452. Reversible Language Extensions and their Application in Debugging
     Z. Drey, J. F. Morales, M. V. Hermenegildo, M. Carro.
     Practical Aspects of Declarative Languages (PADL). January 2013.
453. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir.
     ACM Conference on Computer and Communications Security (CCS). 2013.
454. Verified Computational Differential Privacy with Applications to Smart Metering
     Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin.
     IEEE Computer Security Foundations Symposium (CSF). 2013.
455. Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
     Gilles Barthe, Juan Manuel Crespo, César Kunz.
     Logical Foundations of Computer Science (LFCS). 2013.
456. Fully abstract compilation to JavaScript
     Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2013.
457. From Relational Verification to SIMD Loop Synthesis
     Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron.
     Principles and Practice of Parallel Programming (PPoPP). 2013.
458. Implementing TLS with Verified Cryptographic Security
     Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub.
     IEEE Symposium on Security and Privacy (SP). 2013.
459. OCL2FOL+: Coping with Undefinedness
     Carolina Dania, Manuel Clavel.
     International Conference on Model Driven Engineering Languages and Systems (MODELS). 2013.
460. Hoare-style reasoning with (algebraic) continuations
     Germán Andrés Delbianco, Aleksandar Nanevski.
     International Conference on Functional Programming (ICFP). 2013.
461. Deriving the Full-reducing Krivine Machine from the Small-step Operational Semantics of Normal Order
     Álvaro García-Pérez, Pablo Nogueira, Juan José Moreno-Navarro.
     International Conference on Principles and Practice of Declarative Programming (PPDP). 2013.
462. The TAMARIN Prover for the Symbolic Analysis of Security Protocols
     Simon Meier, Benedikt Schmidt, Cas Cremers, David A. Basin.
     Computer Aided Verification (CAV). 2013.
463. Monadic abstract interpreters
     Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2013.
464. Genetic Algorithm-based Allocation and Scheduling for Voltage and Frequency Scalable XMOS Chips
     Z. Banković, P. Lopez-Garcia.
     International Conference on Hybrid Artificial Intelligence Systems (HAIS). 2013.
465. Preventing Side-Channel Leaks in Web Traffic: A Formal Approach
     Michael Backes, Goran Doychev, Boris Köpf.
     Network and Distributed System Security Symposium (NDSS). 2013.
466. Verifying Concurrent Programs Against Sequential Specifications
     Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
     European Symposium on Programming (ESOP). 2013.
467. Library abstraction for C/C++ concurrency
     Mark Batty, Mike Dodds, Alexey Gotsman.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2013.
468. CacheAudit: A Tool for the Static Analysis of Cache Side Channels
     Goran Doychev, Dominik Feld, Boris Köpf, Laurent Mauborgne, Jan Reineke.
     Usenix Security Symposium (USENIX-Security). 2013.
469. Parameterized Verification of Asynchronous Shared-Memory Systems
     Javier Esparza, Pierre Ganty, Rupak Majumdar.
     Computer Aided Verification (CAV). 2013.
470. Proving Termination Starting from the End
     Pierre Ganty, Samir Genaim.
     Computer Aided Verification (CAV). 2013.
471. Underapproximation of Procedure Summaries for Integer Programs
     Pierre Ganty, Radu Iosif, Filip Konečný.
     International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2013.
472. Effectively-Propositional Reasoning about Reachability in Linked Data Structures
     Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv.
     Computer Aided Verification (CAV). 2013.
473. Automation of Quantitative Information-Flow Analysis
     Boris Köpf, Andrey Rybalchenko.
     School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM). 2013.
474. Subjective Auxiliary State for Coarse-Grained Concurrency
     Ruy Ley-Wild, Aleksandar Nanevski.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2013.
475. Abstraction Based Model-Checking of Stability of Hybrid Systems
     Pavithra Prabhakar, Miriam Garcia Soto.
     Computer Aided Verification (CAV). 2013.
476. Pre-orders for reasoning about stability properties with respect to input of hybrid systems
     Pavithra Prabhakar, Jun Liu, Richard M. Murray.
     ACM Conference on Embedded Software (EMSOFT). 2013.
477. On the decidability of stability of hybrid systems
     Pavithra Prabhakar, Mahesh Viswanathan.
     International Conference on Hybrid Systems: Computation and Control (HSCC). 2013.
478. Patching task-level robot controllers based on a local -calculus formula
     Scott C. Livingston, Pavithra Prabhakar, Alex B. Jose, Richard M. Murray.
     IEEE International Conference on Robotics and Automation (ICRA). 2013.
479. Hybrid Automata based CEGAR for Rectangular Hybrid Automata
     Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2013.
480. Verifying Information Flow Properties of Hybrid Systems
     Pavithra Prabhakar, Boris Köpf.
     High Confidence Networked Systems (HiCoNS). 2013.
481. Verifying concurrent memory reclamation algorithms with grace
     Alexey Gotsman, Noam Rinetzky, Hongseok Yang.
     European Symposium on Programming (ESOP). 2013.
482. Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures
     Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski.
     International Conference on Principles and Practice of Declarative Programming (PPDP). 2013.
483. A programming language perspective on transactional memory consistency
     Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky.
     ACM Symposium on Principles of Distributed Computing (PODC). 2013.
484. An XFEM Implementation for Fracture Simulations of Composites
     Guillermo Vigueras, Cristobal Samaniego, Guillaume Houzeau, Mariano Vazquez, Antoine Jerusalem.
     International Conference on Computational Plasticity. Fundamentals and Applications. COMPLAS 2013. 2013.
485. An XFEM-CZM Implementation for Large-Scale Fracture Simulations of Composites Laminates
     Guillermo Vigueras, Cristobal Samaniego, Eva Casoni, Guillaume Houzeau, Federico Sket, Jon Molina-Aldareguia, Ahmed Makradi, Mariano Vazquez, Antoine Jerusalem.
     European Congress and Exhibition on Advanced Materials and Processes. EUROMAT 2013. 2013.
486. Mtac: A Monad for Typed Tactic Programming in Coq
     Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
     International Conference on Functional Programming (ICFP). 2013.
487. A Constraint-Based Approach to Quality Assurance in Service Choreographies
     D. Ivanovic, M. Carro, M. V. Hermenegildo.
     International Conference on Service Oriented Computing (ICSOC). November 2012.
488. Manufacturing Compromise: The Emergence of Exploit-as-a-Service
     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.
     ACM Conference on Computer and Communications Security (CCS). October 2012.
489. Deriving Specifications for Composite Web Services
     George Bariannys, M. Carro, Dimitris Plexousakis.
     International Computer Software and Applications Conference (COMPSAC). July 2012.
490. Early Detection of Dangling Pointers in Use-After-Free and Double-Free Vulnerabilities
     Juan Caballero, Gustavo Grieco, Mark Marron, Antonio Nappa.
     International Symposium on Software Testing and Analysis (ISSTA). July 2012.
491. A General Implementation Framework for Tabled CLP
     P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, P. Stuckey.
     International Symposium on Functional and Logic Programming (FLOPS). May 2012.
492. A Segment-Swapping Approach for Executing Trapped Computations
     P. Chico de Guzmán, A. Casas, M. Carro, M. V. Hermenegildo.
     Practical Aspects of Declarative Languages (PADL). January 2012.
493. Towards Abstract Interpretation of Epistemic Logic
     Mai Ajspur, John P. Gallagher.
     8th Scandinavian Logic Symposium, 20-21 August 2012, Roskilde University, Denmark. 2012.
494. A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert
     Gilles Barthe, Delphine Demange, David Pichardie.
     European Symposium on Programming (ESOP). 2012.
495. Programming Paradigm Driven Heap Analysis
     Mark Marron, Ondrej Lhoták, Anindya Banerjee.
     International Conference on Compiler Construction (CC). 2012.
496. Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols
     José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin.
     ACM Conference on Computer and Communications Security (CCS). 2012.
497. Verified Security of Redundancy-Free Encryption from Rabin and RSA
     Gilles Barthe, David Pointcheval, Santiago Zanella Béguelin.
     ACM Conference on Computer and Communications Security (CCS). 2012.
498. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs
     Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin.
     International Conference on Certified Programs and Proofs (CPP). 2012.
499. Verified Security of Merkle-Damgård
     Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin.
     IEEE Computer Security Foundations Symposium (CSF). 2012.
500. Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization
     Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna.
     IEEE Computer Security Foundations Symposium (CSF). 2012.
501. Secure Multi-Execution through Static Program Transformation
     Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas.
     IFIP WG 6.1 International Conference on Formal Techniques for (Networked and) Distributed Systems (FORTE). 2012.
502. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs
     Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin.
     Mathematics of Program Construction (MPC). 2012.
503. Verification of Software Barriers
     Alexander Malkis, Anindya Banerjee.
     Principles and Practice of Parallel Programming (PPoPP). 2012.
504. Computer-Aided Cryptographic Proofs
     Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin.
     Static Analysis Symposium (SAS). 2012.
505. Decision Procedures for Region Logic
     Stan Rosenberg, Anindya Banerjee, David A. Naumann.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2012.
506. Verified Indifferentiable Hashing into Elliptic Curves
     Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin.
     International Conference on Principles of Security and Trust (POST). 2012.
507. Probabilistic Relational Reasoning for Differential Privacy
     Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2012.
508. Automatic Quantification of Cache Side-Channels
     Boris Köpf, Laurent Mauborgne, Martín Ochoa.
     Computer Aided Verification (CAV). 2012.
509. Visibly Rational Expressions
     Laura Bozzelli, César Sánchez.
     Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2012.
510. A Perfect Model for Bounded Verification
     Javier Esparza, Pierre Ganty, Rupak Majumdar.
     IEEE Symposium on Logic in Computer Science (LICS). 2012.
511. Non-Monotonic Self-Adjusting Computation
     Ruy Ley-Wild, Umut A. Acar, Guy Blelloch.
     European Symposium on Programming (ESOP). 2012.
512. Linearizability with ownership transfer
     Alexey Gotsman, Hongseok Yang.
     International Conference on Concurrency Theory (CONCUR). 2012.
513. Concurrent library correctness on the TSO memory model
     Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang.
     European Symposium on Programming (ESOP). 2012.
514. Foundations for Approximation Based Analysis of Stability Properties of Hybrid Systems
     Pavithra Prabhakar.
     Allerton Conference on Communication, Control, and Computing (Allerton). 2012.
515. Conformance Testing of Boolean Programs with Multiple Faults
     Pavithra Prabhakar, Mahesh Viswanathan.
     IFIP WG 6.1 International Conference on Formal Techniques for (Networked and) Distributed Systems (FORTE). 2012.
516. Pre-orders for reasoning about stability
     Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan.
     International Conference on Hybrid Systems: Computation and Control (HSCC). 2012.
517. Efficient Regular Linear Temporal Logic Using Dualization and Stratification
     César Sánchez, Julián Samborski-Forlese.
     International Symposium on Temporal Representation and Reasoning (TIME). 2012.
518. How to Translate Efficiently Extensions of Temporal Logics into Alternating Automata
     César Sánchez, Julián Samborski-Forlese.
     International Colloquium on Theoretical Aspects of Computing (ICTAC). 2012.
519. Invariant Generation for Parametrized Systems Using Self-reflection
     Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, Bor-Yuh Evan Chang.
     Static Analysis Symposium (SAS). 2012.
520. Show no weakness: sequentially consistent specifications of TSO libraries
     Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang.
     International Symposium on Distributed Computing (DISC). 2012.
521. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations
     D. Ivanović, M. Carro, M. V. Hermenegildo.
     International Conference on Service Oriented Computing (ICSOC). December 2011.
522. A Machine-Checked Framework for Relational Separation Logic
     Juan Manuel Crespo, César Kunz.
     International Conference on Software Engineering and Formal Methods (SEFM). November 2011.
523. Verifiable Security of Boneh-Franklin Identity-Based Encryption
     Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin.
     International Conference on Provable Security (ProvSec). October 2011.
524. Computer-Aided Security Proofs for the Working Cryptographer
     Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin.
     Advances in Cryptology (CRYPTO). August 2011.
525. Measuring Pay-per-Install: The Commoditization of Malware Distribution
     Juan Caballero, Chris Grier, Christian Kreibich, Vern Paxson.
     Usenix Security Symposium (USENIX-Security). August 2011.
526. CLP Projection for Constraint Handling Rules
     R. Haemmerlé, P. Lopez-Garcia, M. V. Hermenegildo.
     International Conference on Principles and Practice of Declarative Programming (PPDP). July 2011.
527. Modular Extensions for Modular (Logic) Languages
     J. F. Morales, M. V. Hermenegildo, R. Haemmerlé.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). July 2011.
528. Automated Attribute Inference in Complex Service Workflows Based on Sharing Analysis
     D. Ivanović, M. Carro, M. V. Hermenegildo.
     IEEE International Conference on Services Computing (IEEE SCC). July 2011.
529. Formally Verifying Isolation and Availability in an Idealized Model of Virtualization
     Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna.
     International Symposium on Formal Methods (FM). June 2011.
530. Relational Verification Using Product Programs
     Gilles Barthe, Juan Manuel Crespo, César Kunz.
     International Symposium on Formal Methods (FM). June 2011.
531. A decade of model-driven security
     David A. Basin, Manuel Clavel, Marina Egea.
     ACM Symposium on Access Control Models and Technologies (SACMAT). June 2011.
532. Applicative Shortcut Fusion
     Germán Andrés Delbianco, Mauro Jaskelioff, Alberto Pardo.
     Symposium on Trends in Functional Programming (TFP). May 2011.
533. Differential Slicing: Identifying Causal Execution Differences for Security Applications
     Noah M. Johnson, Juan Caballero, Kevin Chen, Stephen McCamant, Pongsin Poosankam, Daniel Reynaud, Dawn Song.
     IEEE Symposium on Security and Privacy (SP). May 2011.
534. Beyond Provable Security Verifiable IND-CCA Security of OAEP
     Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin.
     The Cryptographer’s Track at RSA Conference (CT-RSA). February 2011.
535. Approximating Petri Net Reachability Along Context-free Traces
     Mohamed Faouzi Atig, Pierre Ganty.
     Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2011.
536. Complexity Analysis of the Backward Coverability Algorithm for VASS
     Laura Bozzelli, Pierre Ganty.
     Reachability Problems (RP). 2011.
537. Non-Uniform Distributions in Quantitative Information-Flow
     Michael Backes, Matthias Berg, Boris Köpf.
     ACM Conference on Computer and Communications Security (CCS). 2011.
538. Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language
     Gilles Barthe, Exequiel Rivas.
     Trustworthy Global Computing (TGC). 2011.
539. Information-theoretic Bounds for Differentially Private Mechanisms
     Gilles Barthe, Boris Köpf.
     IEEE Computer Security Foundations Symposium (CSF). 2011.
540. Model-Driven Development of Security-Aware GUIs for Data-Centric Applications
     David A. Basin, Manuel Clavel, Marina Egea, Miguel Angel García de Dios, Carolina Dania, Gonzalo Ortiz, Javier Valdazo.
     Foundations of Security Analysis and Design (FOSAD). 2011.
541. Third International Workshop on Principles of Engineering Service-Oriented Systems (PESOS 2011)
     M. Carro, D. Karastoyanova, G. A. Lewis, A. Liu.
     ICSE. 2011.
542. Precision and the conjunction rule in concurrent separation logic
     Alexey Gotsman, Josh Berdine, Byron Cook.
     Electronic Notes in Theoretical Computer Science (ENTCS). 2011.
543. Complexity of Pattern-based Verification for Multithreaded Programs
     Javier Esparza, Pierre Ganty.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2011.
544. How to make ad hoc proof automation less ad hoc
     Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
     International Conference on Functional Programming (ICFP). 2011.
545. The Ciao Approach to the Dynamic vs. Static Language Dilemma
     M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, E. Mera, J.F. Morales, G. Puebla.
     Proc. Int’l. WS on Scripts to Programs, STOP'11. 2011.
546. Liveness-Preserving Atomicity Abstraction
     Alexey Gotsman, Hongseok Yang.
     International Colloquium on Automata Languages and Programming (ICALP). 2011.
547. On the Strength of Owicki-Gries for Resources
     Alexander Malkis, Laurent Mauborgne.
     ASIAN Symposium on Programming Languages and Systems (APLAS). 2011.
548. Verification of Information Flow and Access Control Policies with Dependent Types
     Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
     IEEE Symposium on Security and Privacy (SP). 2011.
549. Profiling for Run-Time Checking of Computational Properties and Performance Debugging in Logic Programs
     E. Mera, T. Trigo, P. Lopez-Garcia, M. V. Hermenegildo.
     Practical Aspects of Declarative Languages (PADL). 2011.
550. A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes
     Alejandro Sánchez, César Sánchez.
     NASA Formal Methods (NFM). 2011.
551. Modular verification of preemptive OS kernels
     Alexey Gotsman, Hongseok Yang.
     International Conference on Functional Programming (ICFP). 2011.
552. Partiality, State and Dependent Types
     Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski.
     International Conference on Typed Lambda Calculi and Applications (TLCA). 2011.
553. Towards Fuzzy Granularity Control in Parallel/Distributed Computing
     T. Trigo, P. Lopez-Garcia, S. Muñoz-Hernandez.
     International Conference on Fuzzy Computation (ICFC 2010). October 2010.
554. A Framework for Verification and Debugging of Resource Usage Properties: Resource Usage Verification
     P. Lopez-Garcia, L. Darmawan, F. Bueno.
     International Conference on Logic Programming (ICLP). July 2010.
555. Automatic Generation of Smart, Security-Aware GUI Models
     D. Basin, M. Clavel, M. Egea, M. Schläpfer.
     Engineering Secure Software and Systems (ESSoS). 2010.
556. Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation
     Gourinath Banda, John P. Gallagher.
     Logic Programming and Automated Reasoning (LPAR). 2010.
557. A Machine-Checked Formalization of Sigma-Protocols
     Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Gregoire, Sylvain Heraud.
     IEEE Computer Security Foundations Symposium (CSF). 2010.
558. Programming Language Techniques for Cryptographic Proofs
     Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin.
     Conference on Interactive Theorem Proving (ITP). 2010.
559. A Functional Framework for Result Checking
     Gilles Barthe, Pablo Buiras, César Kunz.
     International Symposium on Functional and Logic Programming (FLOPS). 2010.
560. Perspectives in Certificate Translation
     Gilles Barthe, César Kunz.
     Trustworthy Global Computing (TGC). 2010.
561. Computational Indistinguishability Logic
     Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech.
     ACM Conference on Computer and Communications Security (CCS). 2010.
562. Robustness Guarantees for Anonymity
     Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi.
     IEEE Computer Security Foundations Symposium (CSF). 2010.
563. Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions
     David A. Naumann, Anindya Banerjee.
     European Symposium on Programming (ESOP). 2010.
564. A Practical Generic Privacy Language
     Moritz Y. Becker, Alexander Malkis, Laurent Bussard.
     International Conference on Information Systems Security (ICISS). 2010.
565. On the Equality of Probabilistic Terms
     Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte.
     Logic Programming and Automated Reasoning (LPAR). 2010.
566. Thread-Modular Counterexample-Guided Abstraction Refinement
     Alexander Malkis, Andreas Podelski, Andrey Rybalchenko.
     Static Analysis Symposium (SAS). 2010.
567. Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients
     Stan Rosenberg, Anindya Banerjee, David A. Naumann.
     Verified Software: Theories (VSTTE). 2010.
568. SSG: a Model-Based Development Environment for Smart, Security-Aware GUIs
     M. A. García de Dios, C. Dania, M. Schläpfer, D. Basin, M. Clavel, M. Egea.
     International Conference on Software Engineering (ICSE). 2010.
569. Certificate Translation for the Verification of Concurrent Programs
     César Kunz.
     Trustworthy Global Computing (TGC). 2010.
570. Speaker Recognition in Encrypted Voice Streams
     Michael Backes, Goran Doychev, Markus Dürmuth, Boris Köpf.
     European Symposium On Research In Computer Security (ESORICS). 2010.
571. Analyzing the Impact of Change in Multi-threaded Programs
     Krishnendu Chatterjee, Luca de Alfaro, Vishwanath Raman, César Sánchez.
     Fundamental Approaches to Software Engineering (FASE). 2010.
572. Bounded Underapproximations
     Pierre Ganty, Benjamin Monmege, Rupak Majumdar.
     Computer Aided Verification (CAV). 2010.
573. Towards Data-Aware QoS-Driven Adaptation for Service Orchestrations
     D. Ivanović, M. Carro, M. V. Hermenegildo.
     IEEE International Conference on Web Services (ICWS). 2010.
574. Automatic Fragment Identification in Workflows Based on Sharing Analysis
     D. Ivanović, M. Carro, M. V. Hermenegildo.
     International Conference on Service Oriented Computing (ICSOC). 2010.
575. Approximation and Randomization for Quantitative Information-Flow Analysis
     Boris Köpf, Andrey Rybalchenko.
     IEEE Computer Security Foundations Symposium (CSF). 2010.
576. Vulnerability Bounds and Leakage Resilience of Blinded Cryptography under Timing Attacks
     Boris Köpf, Geoffrey Smith.
     IEEE Computer Security Foundations Symposium (CSF). 2010.
577. Regular Linear-Time Temporal Logic
     Martin Leucker, César Sánchez.
     International Symposium on Temporal Representation and Reasoning (TIME). 2010.
578. Shape Analysis with Reference Set Relations
     Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2010.
579. Structuring the verification of heap-manipulating programs
     Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2010.
580. Program Parallelization using Synchronized Pipelining
     L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2010.
581. Traceable data types for self-adjusting computation
     Umut A. Acar, Guy E. Blelloch, Ruy Ley-Wild, Kanat Tangwongsan, Duru Türkoglu.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2010.
582. Decision Procedures for the Temporal Verification of Concurrent Lists
     Alejandro Sánchez, César Sánchez.
     International Conference on Formal Engineering Methods (ICFEM). 2010.
583. Regular Linear Temporal Logic with Past
     César Sánchez, Martin Leucker.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2010.
584. A Coding Rule Conformance Checker Integrated into GCC
     G. Marpons, J. Mariño, M. Carro, A. Herranz, L.Å. Fredlund, J.J. Moreno-Navarro, A. Polo.
     Electronic Notes in Theoretical Computer Science (ENTCS). August 2009.
585. Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework
     E. Mera, P. Lopez-Garcia, M. V. Hermenegildo.
     International Conference on Logic Programming (ICLP). July 2009.
586. Merlin: specification inference for explicit information flow problems
     V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). June 2009.
587. Identification of Logically Related Heap Regions
     Mark Marron, Deepak Kapur, Manuel Hermenegildo.
     International Symposium on Memory Management (ISMM). June 2009.
588. User-Definable Resource Usage Bounds Analysis for Java Bytecode
     J. Navas, M. Méndez-Lojo, M. V. Hermenegildo.
     Electronic Notes in Theoretical Computer Science (ENTCS). March 2009.
589. Towards a Complete Scheme for Tabled Execution Based on Program Transformation
     P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
     Practical Aspects of Declarative Languages (PADL). January 2009.
590. Constraint-Based Abstraction of a Model Checker for Infinite State Systems
     Gourinath Banda, John P. Gallagher.
     (Constraint) Logic Programming (WLP). 2009.
591. Formal Certification of Code-Based Cryptographic Proofs
     G. Barthe, B. Grégoire, S. Zanella Béguelin.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2009.
592. Implementing a Direct Method for Certificate Translation
     Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet.
     International Conference on Formal Engineering Methods (ICFEM). 2009.
593. Unification and Narrowing in Maude 2.4
     M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. L. Talcott.
     International Conference on Rewriting Techniques and Applications (RTA). 2009.
594. Non-discriminating Arguments and Their Uses
     Henning Christiansen, John P. Gallagher.
     International Conference on Logic Programming (ICLP). 2009.
595. A language for information flow: dynamic tracking in multiple interdependent dimensions
     Avraham Shinnar, Marco Pistoia, Anindya Banerjee.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2009.
596. Vérification d'invariants pour des systèmes spécifiés en logique de réécriture
     Vlad Rusu, Manuel Clavel.
     Journées francophones des langages applicatifs (JFLA). 2009.
597. Formally Certifying the Security of Digital Signature Schemes
     S. Zanella Béguelin, B. Grégoire, G. Barthe, F. Olmedo.
     IEEE Symposium on Security and Privacy (SP). 2009.
598. Analyzing Real-time Event-driven Programs
     Pierre Ganty, Rupak Majumdar.
     International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). 2009.
599. Verifying Liveness for Asynchronous Programs
     Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2009.
600. Fixpoint Guided Abstraction Refinement for Alternating Automata
     Pierre Ganty, Nicolas Maquet, Jean-François Raskin.
     International Conference on Implementation and Application of Automata (CIAA). 2009.
601. A Tabling Implementation Based on Variables with Multiple Bindings
     P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
     International Conference on Logic Programming (ICLP). 2009.
602. A Sketch of a Complete Scheme for Tabled Execution Based on Program Transformation
     P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
     International Conference on Logic Programming (ICLP). December 2008.
603. A High-Level Implementation of Non-Deterministic, Unrestricted, Independent And-Parallelism
     A. Casas, M. Carro, M. V. Hermenegildo.
     International Conference on Logic Programming (ICLP). December 2008.
604. Negative Ternary Set-Sharing
     E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo.
     International Conference on Logic Programming (ICLP). December 2008.
605. Towards Execution Time Estimation in Abstract Machine-Based Languages
     E. Mera, P. Lopez-Garcia, M. Carro, M. V. Hermenegildo.
     International Conference on Principles and Practice of Declarative Programming (PPDP). July 2008.
606. Comparing Tag Scheme Variations Using an Abstract Machine Generator
     J. Morales, M. Carro, M. V. Hermenegildo.
     International Conference on Principles and Practice of Declarative Programming (PPDP). July 2008.
607. Safe Upper-bounds Inference of Energy Consumption for Java Bytecode Applications
     J. Navas, M. Méndez-Lojo, M. Hermenegildo.
     NASA LFM'08. April 2008.
608. Efficient Context-Sensitive Shape Analysis with Graph-Based Heap Models
     Mark Marron, Manuel Hermenegildo, Darko Stefanovic, Deepak Kapur.
     International Conference on Compiler Construction (CC). April 2008.
609. Towards a High-Level Implementation of Execution Primitives for Unrestricted, Independent And-parallelism
     A. Casas, M. Carro, M. V. Hermenegildo.
     Practical Aspects of Declarative Languages (PADL). January 2008.
610. An Improved Continuation Call-Based Implementation of Tabling
     P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, Claudio Silva, Ricardo Rocha.
     Practical Aspects of Declarative Languages (PADL). January 2008.
611. Automatic Coding Rule Conformance Checking Using Logic Programming
     G. Marpons, J. Mariño, M. Carro, A. Herranz, J.J. Moreno-Navarro, L.Å. Fredlund.
     Practical Aspects of Declarative Languages (PADL). January 2008.
612. Precise Set Sharing Analysis for Java-style Programs
     M. Méndez-Lojo, M. Hermenegildo.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). January 2008.
613. Analysis of Linear Hybrid Systems in CLP
     Gourinath Banda, John P. Gallagher.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2008.
614. Certificate Translation in Abstract Interpretation
     Gilles Barthe, César Kunz.
     European Symposium on Programming (ESOP). 2008.
615. Certified Reasoning in Memory Hierarchies
     Gilles Barthe, César Kunz, Jorge Luis Sacchini.
     ASIAN Symposium on Programming Languages and Systems (APLAS). 2008.
616. Model-Driven Security in Practice: An Industrial Experience
     M. Clavel, V. Silva, C. Braga, M. Egea.
     European Conference on Model Driven Architecture - Foundations and Applications (ECMDA-FA). 2008.
617. Preservation of Proof Obligations from Java to the Java Virtual Machine
     Gilles Barthe, Benjamin Grégoire, Mariela Pavlova.
     International Conference on Automated Deduction (CADE). 2008.
618. Tractable Enforcement of Declassification Policies
     Gilles Barthe, Salvador Cavadini, Tamara Rezk.
     IEEE Computer Security Foundations Symposium (CSF). 2008.
619. Type-Based Termination with Sized Products
     Gilles Barthe, Benjamin Grégoire, Colin Riba.
     Annual Conference on Computer Science Logic (CSL). 2008.
620. Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation
     John P. Gallagher, Mads Rosendahl.
     Logic Programming and Automated Reasoning (LPAR). 2008.
621. From Monomorphic to Polymorphic Well-Typings and Beyond
     Tom Schrijvers, Maurice Bruynooghe, John P. Gallagher.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2008.
622. Preservation of Proof Pbligations for Hybrid Verification Methods
     Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese.
     International Conference on Software Engineering and Formal Methods (SEFM). 2008.

Publications in Refereed Workshops (119)

1. Challenges in inferring privacy properties of smart devices: towards scalable multi-vantage point testing methods
   Aniketh Girish, Vijay Prakash, Serge Egelman, Joel Reardon, Juan Tapiador, Danny Yuxing Huang, Srdjan Matic, Narseo Vallina-Rodriguez.
   ACM International Conference on Emerging Networking Experiments and Technologies Student Workshop (CoNEXT-SW). December 2022.
2. A SAT-based Efficient Method for the Synthesis from numerical LTL spefications
   Andoni Rodríguez, César Sánchez.
   Jornadas de PROgramación y LEnguajes (PROLE) 2022. September 2022.
3. Reactive Synthesis of LTL specifications with Rich Theories
   Andoni Rodríguez, César Sánchez.
   11th Workshop in Synthesis. August 2022.
4. An s(CASP) In-Browser Playground based on Ciao Prolog
   G. Garcia-Pradales, J.F. Morales, M. V. Hermenegildo, J. Arias, M. Carro.
   International Conference on Logic Programming (ICLP). August 2022.
5. FATR: a Framework for Automated Analysis of Threat Reports
   Juan Caballero, Gibran Gomez, Srdjan Matic, Gustavo Sánchez, Silvia Sebastián, Arturo Villacañas.
   Jornadas Nacionales de Investigación en Ciberseguridad (JNIC). June 2022.
6. Analysis and Improvements of the Sender Keys Protocol for Group Messaging
   David Balbás, Daniel Collins, Phillip Gajland.
   Reunión española sobre criptología y seguridad de la información (RECSI). 2022.
7. Multi: A Formal Playground for Multi-Smart Contract Interaction
   Martín Ceresa, César Sánchez.
   International Workshop on Formal Methods for Blockchains (FMBC). 2022.
8. VeriFly: On-the-fly Assertion Checking with CiaoPP
   M. A. Sanchez-Ordaz, I. Garcia-Contreras, V. Perez-Carrasco, J. F. Morales, P. Lopez-Garcia, M.V. Hermenegildo.
   6th Workshop on Formal Integrated Development Environment (F-IDE 2021). May 2021.
9. Incremental and Modular Context-sensitive Analysis
   I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
   Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021). March 2021.
10. A Short Tutorial on s(CASP), a Goal-directed Execution of Constraint Answer Set Programs
    Joaquín Arias, Gopal Gupta, Manuel Carro.
    International Conference on Logic Programming (ICLP). 2021.
11. s(CASP) for SWI-Prolog
    Jan Wielemaker, Joaquín Arias, Gopal Gupta.
    International Conference on Logic Programming (ICLP). 2021.
12. An application of KLEE to aerospace industrial software
    Juan Francisco García, Daniel Jurjo, Fernando Macías, José Francisco Morales, Alessandra Gorla.
    2nd International KLEE Workshop on Symbolic Execution. 2021.
13. Testing Your (Static Analysis) Truths
    I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). September 2020.
14. Justifications for Goal-Directed Constraint Answer Set Programming
    Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
    Computing Research Repository (CoRR). 2020.
15. Making Byzantine Consensus Live
    Manuel Bravo, Gregory Chockler, Alexey Gotsman.
    Workshop on Distributed Algorithms (WDAG). 2020.
16. Computing Abstract Distances in Logic Programs
    I. Casso, J. F. Morales, P. Lopez-Garcia, R. Giacobazzi, M. V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). November 2019.
17. A General Framework for Static Cost Analysis of Parallel Logic Programs
    M. Klemen, P. Lopez-Garcia, J. Gallagher, J.F. Morales, M. V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). November 2019.
18. An Integrated Approach to Assertion-Based Random Testing in Prolog
    I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). November 2019.
19. Experiments in Context-Sensitive Incremental and Modular Static Analysis in CiaoPP
    I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
    10th Workshop on Tools for Automatic Program Analysis (TAPAS'19). October 2019.
20. Incremental Analysis of Logic Programs with Assertions and Open Predicates
    I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). October 2019.
21. Towards Computing Abstract Distances in Logic Programs
    I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
    Technical Communications of the 35th International Conference on Logic Programming (ICLP 2019). September 2019.
22. Modeling and Reasoning in Event Calculus Using Goal-Directed Constraint Answer Set Programming
    J. Arias, Z. Chen, M. Carro, G. Gupta.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). September 2019.
23. Towards a General Framework for Static Cost Analysis of Parallel Logic Programs
    M. Klemen, P. Lopez-Garcia, J. Gallagher, J.F. Morales, M. V. Hermenegildo.
    Technical Communications of the 35th International Conference on Logic Programming (ICLP 2019). September 2019.
24. Constraint Answer Set Programming without Grounding and its Applications
    Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
    Datalog (Datalog). June 2019.
25. Transferable Anonymous Payments via TumbleBit in Permissioned Blockchains
    Claudio Ferretti, Alberto Leporati, Luca Mariot, Luca Nizzardo.
    Italian Conference on Cybersecurity (ITASEC). 2019.
26. Research on NLP for RE at Università della Svizzera Italiana (USI): A Report
    Arianna Blasi, Mauro Pezzè, Alessandra Gorla, Michael D. Ernst.
    International Workshop on Requirements Engineering: Foundation for Software Quality (REFSQ). 2019.
27. Release practices for iOS and Android apps
    Daniel Domínguez-Álvarez, Alessandra Gorla.
    International Workshop on App Market Analytics (WAMA). 2019.
28. Specialize in Moderation - Building Application-aware Storage Services using FPGAs in the Datacenter
    Lucas Kuhring, Eva Garcia, Zsolt István.
    Hot Topics in Storage and File Systems (HotStorage). 2019.
29. 25 Years of Ciao (abstract of invited tutorial)
    M. V. Hermenegildo, M. Carro, P. Lopez, J.F. Morales, J. Arias, I. Garcia-Contreras, M. Klemen, N. Stulova.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). September 2018.
30. Multivariant Assertion-based Guidance in Abstract Interpretation
    I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). September 2018.
31. Knowledge Problems in Equational Extensions of Subterm Convergent Theories
    Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen.
    32nd International Workshop on Unification. July 2018.
32. A General Framework for Static Profiling of Parametric Resource Usage (extended abstract)
    P. Lopez-Garcia, M. Klemen, U. Liqat, M. V. Hermenegildo.
    19th International Workshop on Logic and Computational Complexity (LCC 2018). July 2018.
33. Towards Incremental and Modular Context-sensitive Analysis
    I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
    International Conference on Logic Programming (ICLP). July 2018.
34. Towards Static Performance Guarantees for Programs with Run-time Checks
    M. Klemen, N. Stulova, P. Lopez-Garcia, J. F. Morales, M. V. Hermenegildo.
    International Conference on Logic Programming (ICLP). July 2018.
35. StreamChain: Do Blockchains Need Blocks?
    Zsolt István, Alessandro Sorniotti, Marko Vukolić.
    ACM/IFIP/USENIX International Middleware Conference (Middleware). 2018.
36. A Deep Learning Approach to Program Similarity
    Niccolò Marastoni, Roberto Giacobazzi, Mila Dalla Preda.
    Automated Software Engineering Conference (ASE). 2018.
37. A certified reference validation mechanism for the permission model of Android
    Gustavo Betarte, Juan Diego Campo, Felipe Gorostiaga, Carlos Luna.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). October 2017.
38. Inferring Energy Bounds via Static Program Analysis and Evolutionary Modeling of Basic Blocks
    U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). October 2017.
39. Towards a Semantics-Aware Code Transformation Toolchain for Heterogeneous Systems
    Salvador Tamarit, Julio Mariño, Guillermo Vigueras, Manuel Carro.
    Computing Research Repository (CoRR). September 2017.
40. An Analysis of Pay-per-Install Economics Using Entity Graphs
    Platon Kotzias, Juan Caballero.
    Workshop on the Economics of Information Security (WEIS). June 2017.
41. Which Broadcast Abstraction Captures k-Set Agreement?
    Damien Imbs, Achour Mostéfaoui, Matthieu Perrin, Michel Raynal.
    Workshop on Distributed Algorithms (WDAG). 2017.
42. Is Geo-Indistinguishability What You Are Looking for?
    Simon Oya, Carmela Troncoso, Fernando Pérez-González.
    Workshop on Privacy in the Electronic Society (WPES). 2017.
43. On Improving Run-time Checking in Dynamic Languages
    Nataliia Stulova.
    Logic Programming Doctoral Consortium (DC-ICLP). 2017.
44. Towards Run-time Checks Simplification via Term Hiding
    N. Stulova, J. F. Morales, M. V. Hermenegildo.
    International Conference on Logic Programming (ICLP). 2017.
45. CALAPPA: a Toolchain for Mining Android Applications
    Vitalii Avdiienko, Konstantin Kuznetsov, Paolo Calciati, Juan Carlos Caiza Román, Alessandra Gorla, Andreas Zeller.
    International Workshop on App Market Analytics (WAMA). November 2016.
46. Checking App User Interfaces Against App Descriptions
    Konstantin Kuznetsov, Vitalii Avdiienko, Alessandra Gorla, Andreas Zeller.
    International Workshop on App Market Analytics (WAMA). November 2016.
47. Tabled CLP for Reasoning over Stream Data
    J. Arias.
    Logic Programming Doctoral Consortium (DC-ICLP). October 2016.
48. Program Transformations in the POLCA Project
    Jan Kuper, Lutz Schubert, Kilian Kempf, Colin Glas, Daniel Rubio Bonilla, Manuel Carro.
    Design, Automation and Test in Europe Conference (DATE). March 2016.
49. Towards a Semantics-Aware Transformation Toolchain for Heterogeneous Systems
    Salvador Tamarit, Julio Mariño, Guillermo Vigueras, Manuel Carro.
    Proceedings of the First International Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016). March 2016.
50. Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural Code
    Guillermo Vigueras, Manuel Carro, Salvador Tamarit, Julio Mariño.
    Computing Research Repository (CoRR). March 2016.
51. Interpolant tree automata and their application in Horn clause verification
    Bishoksan Kafle, John P. Gallagher.
    Computing Research Repository (CoRR). 2016.
52. Solving non-linear Horn clauses using a linear Horn clause solver
    Bishoksan Kafle, John P. Gallagher, Pierre Ganty.
    Workshop on Horn Clauses for Verification and Synthesis (HCVS). 2016.
53. TASP: Towards Anonymity Sets that Persist
    J. Hayes, C. Troncoso, G. Danezis.
    Workshop on Privacy in the Electronic Society (WPES). 2016.
54. Inferring Energy Bounds Statically by Evolutionary Analysis of Basic Blocks
    U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
    Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES). 2016.
55. The CISE tool: proving weakly-consistent applications correct
    Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira, Marc Shapiro.
    Eurosys Conference (EuroSys). 2016.
56. Inferring Parametric Energy Consumption Functions at Different Software Levels: ISA vs. LLVM IR
    U. Liqat, K. Georgiou, S. Kerrison, P. Lopez-Garcia, M. V. Hermenegildo, J. P. Gallagher, K. Eder.
    International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA). 2016.
57. Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC
    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir.
    International Workshop on Fast Software Encryption (FSE). 2016.
58. Ayudante: Identifying Undesired Variable Interactions
    Irfan Ul Haq, Juan Caballero, Michael D. Ernst.
    International Workshop on Dynamic Analysis (WODA). October 2015.
59. Energy Analysis and Verification by Translation to Horn Clauses and Abstract Interpretation
    R. Haemmerle, M. V. Hermenegildo, M. Klemen, U. Liqat, P. Lopez-Garcia.
    Workshop on Horn Clauses for Verification and Synthesis (HCVS). July 2015.
60. Towards a Generic Interface to Integrate CLP and Tabled Execution (Extended Abstract)
    J. Arias, M. Carro.
    International Conference on Logic Programming (ICLP). 2015.
61. Decomposition by tree dimension in Horn clause verification
    Bishoksan Kafle, John P. Gallagher, Pierre Ganty.
    International Workshop on Verification and Program Transformation (VPT). 2015.
62. Constraint Specialisation in Horn Clause Verification
    Bishoksan Kafle, John P. Gallagher.
    ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM). 2015.
63. An Algorithmic Approach to Stability Verification of Hybrid Systems: A Summary
    Pavithra Prabhakar, Miriam García Soto.
    Computer Aided Verification (CAV). 2015.
64. Towards Energy Consumption Verification via Static Analysis
    P. Lopez-Garcia, R. Haemmerlé, M. Klemen, U. Liqat, M. V. Hermenegildo.
    Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES). 2015.
65. A standard theory for the pure lambda-value calculus
    Álvaro García-Pérez, Pablo Nogueira.
    September 2014.
66. Pre-Indexed Terms for Prolog
    J.F. Morales, M. V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). September 2014.
67. Towards Assertion-based Debugging of Higher-Order (C)LP Programs (Extended Abstract)
    N. Stulova, J. F. Morales, M. V. Hermenegildo.
    International Conference on Logic Programming (ICLP). July 2014.
68. Towards Pre-Indexed Terms
    J.F. Morales, M. V. Hermenegildo.
    14th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS-WLPE 2014). July 2014.
69. Making RSA-PSS Provably Secure against Non-random Faults
    Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz.
    Workshop on Cryptographic Hardware and Embedded Systems (CHES). 2014.
70. Deriving interpretations of the gradually-typed lambda calculus
    Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey.
    ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM). 2014.
71. Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
    Bishoksan Kafle, John P. Gallagher.
    Computing Research Repository (CoRR). 2014.
72. Towards an EasyCrypt Formalization of Garbling Schemes
    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub.
    The Workshop on Language Support for Privacy-Enhancing Technology (PETShop). November 2013.
73. Derivación de intérpretes del cálculo lambda con tipos graduales
    Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey.
    September 2013.
74. Energy Consumption Analysis of Programs based on XMOS ISA-Level Models
    U. Liqat, S. Kerrison, A. Serrano, K. Georgiou, P. Lopez-Garcia, N. Grech, M. V. Hermenegildo, K. Eder.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). September 2013.
75. Implementing Constraint Handling Rules as a Domain-Specific Language Embedded in Java
    Dragan Ivanović.
    Proceedings of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013). August 2013.
76. Towards an Abstract Domain for Resource Analysis of Logic Programs Using Sized Types
    A. Serrano, P. Lopez-Garcia, M. V. Hermenegildo.
    23rd Workshop on Logic-based Methods in Programming Environments (WLPE 2013). August 2013.
77. Towards QoS Prediction Based on Composition Structure Analysis and Probabilistic Environment Models
    D. Ivanovic, P. Kaowichakorn, M. Carro.
    International Conference on Software Engineering (ICSE). May 2013.
78. A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers
    Álvaro García-Pérez, Pablo Nogueira.
    ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM). 2013.
79. Fixing idioms: a recursion primitive for applicative DSLs
    Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens.
    ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM). 2013.
80. Acceleration of Communication-Aware Task Mapping Techniques through GPU Computing
    Javier Reyes, Juan M. Orduña, Guillermo Vigueras, Rafael Tornero.
    International Conference on Advanced Information Networking and Applications (AINA). 2013.
81. Bounded Model Checking for Regular Linear Temporal Logic (extended abstract)
    Julián Samborski-Forlese, César Sánchez.
    Proceedings of the 24th Nordic Workshop on Programming Theory (NWPT'12). October 2012.
82. Enfoque normal y enfoque spine para reducción en el cálculo lambda puro
    Álvaro García-Pérez, Pablo Nogueira.
    September 2012.
83. The Ciao CLP(FD) Library: A Modular CLP Extension for Prolog
    E.J. Gallego-Arias, R. Haemmerlé, M. V. Hermenegildo, J.F. Morales.
    12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS 2012). September 2012.
84. Reversible Language Extensions and their Application in Debugging
    Z. Drey, J.F. Morales, M. V. Hermenegildo.
    Practical Aspects of Declarative Languages (PADL). September 2012.
85. Proving Computational Security with a General-Purpose C Verifier
    François Dupressoir, Cédric Fournet, Andrew D. Gordon.
    Workshops on Formal and Computational Cryptography (FCC) and Analysis of Security APIs (ASA). July 2012.
86. Analyzing Service-Oriented Systems Using Their Data and Structure
    D. Ivanovic, M. Carro, M. V. Hermenegildo.
    International Conference on Software Engineering (ICSE). July 2012.
87. Research Challenges on Service Technology Foundations
    D. Karastoyanova, Z. Nemeth, M. Carro, D. Ivanovic, C. Pautasso, C. Di Napoli, M. Giordano.
    International Conference on Software Engineering (ICSE). July 2012.
88. Exploring the Impact of Inaccuracy and Imprecision of QoS Assumptions on Proactive Constraint-Based QoS Prediction for Service Orchestrations
    D. Ivanović, M. Carro, M. V. Hermenegildo.
    International Conference on Software Engineering (ICSE). June 2012.
89. Modeling Social Networking Privacy
    Carolina Dania.
    International Symposium on Theoretical Aspects of Software Engineering (TASE). 2012.
90. A General Implementation Framework for Tabled CLP
    M. Carro, M. V. Hermenegildo, P. Stuckey.
    Jornadas sobre Programación y Lenguajes (PROLE). 2012.
91. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations
    D. Ivanović, M. Carro, M. V. Hermenegildo.
    Jornadas sobre Programación y Lenguajes (PROLE). 2012.
92. Lightweight compilation of (C)LP to JavaScript
    J. F. Morales, R. Haemmerlé, M. Carro, M. V. Hermenegildo.
    Jornadas sobre Programación y Lenguajes (PROLE). 2012.
93. Behavior Based Service Composition
    Fangzhe Chang, Pavithra Prabhakar, Ramesh Viswanathan.
    International Workshop on Web Services and Formal Methods (WS-FM). 2012.
94. Estrategias del cálculo lambda e interderivación de artefactos semánticos
    Álvaro García-Pérez, Pablo Nogueira.
    September 2011.
95. Towards Resource Usage Analysis of MiniZinc Models
    F. Bueno, M. García de la Banda, M. V. Hermenegildo, P. Lopez-Garcia, E. Mera, P. J. Stuckey.
    MiniZinc Workshop (MZN'11). September 2011.
96. Interval-based Resource Usage Verification: Formalization and Prototype
    P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo.
    International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA). May 2011.
97. The Ciao Approach to the Dynamic vs. Static Language Dilemma
    M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, E. Mera, J.F. Morales, G. Puebla.
    Proceedings for the International Workshop on Scripts to Programs (STOP'11). 2011.
98. El Cubo Beta
    Álvaro García-Pérez.
    September 2010.
99. An Initial Proposal for Data-Aware Resource Analysis of Orchestrations with Applications to Predictive Monitoring
    D. Ivanović, M. Carro, M. V. Hermenegildo.
    International Conference on Service Oriented Computing (ICSOC). September 2010.
100. The Beta Cube (Extended Abstract)
     Álvaro García-Pérez, Pablo Nogueira, Emilio Jesús Gallego Arias.
     Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS'10). July 2010.
101. MySQL4OCL: A Stored Procedure-Based MySQL Code Generator for OCL
     M. Egea, C. Dania, M. Clavel.
     Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010). 2010.
102. Modeling Concurrent Systems with Shared Resources
     A. Herranz, J. Mariño, M. Carro, J.J. Moreno-Navarro.
     Int. Workshop on Formal Methods for Industrial Critical Systems (FMICS). November 2009.
103. An Initial Proposal for Data-Aware Resource Analysis of Orchestrations with Applications to Proactive Monitoring
     D. Ivanović, M. Carro, M. V. Hermenegildo.
     Pre-proceedings of the 2nd Workshop on Monitoring, Adaptation and Beyond (MONA+). November 2009.
104. Program Parallelization using Synchronized Pipelining
     L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). September 2009.
105. Towards Structured State Threading in Prolog
     D. Ivanović, J.F. Morales, M. Carro, M. V. Hermenegildo.
     CICLOPS 2009. July 2009.
106. User-Definable Resource Usage Bounds Analysis for Java Bytecode
     J. Navas, M. Méndez-Lojo, M. V. Hermenegildo.
     Electronic Notes in Theoretical Computer Science (ENTCS). March 2009.
107. Checking Unsatisfiability for OCL Constraints
     M. Clavel, M. Egea, M. A. García de Dios.
     Proceedings of the Workshop The Pragmatics of OCL and Other Textual Specification Languages at MoDELS 2009. 2009.
108. A Program Transformation for Continuation Call-Based Tabled Execution
     P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
     Colloquium on Implementation of Constraint and LOgic Programming Systems (ICLP associated workshop). December 2008.
109. Sharing Analysis of Arrays, Collections, and Recursive Structures
     Mark Marron, Mario Méndez-Lojo, Manuel Hermenegildo, Darko Stefanovic, Deepak Kapur.
     Workshop on Program Analysis For Software Tools and Engineering (PASTE). November 2008.
110. A Coding Rule Conformance Checker Integrated into GCC
     G. Marpons, J. Mariño, M. Carro, A. Herranz, L.Å. Fredlund, J.J. Moreno-Navarro, A. Polo.
     Electronic Notes in Theoretical Computer Science (ENTCS). October 2008.
111. Modelling Mash-Up Resources
     Iván Pérez, Ángel Herranz, Susana Muñoz, Juan José Moreno-Navarro.
     Jornadas de Ingeniería del Software y Bases de Datos (JISBD). October 2008.
112. Bialgebra Views: A Way for Polytypic Programming to Cohabit with Data Abstraction
     Pablo Nogueira, Juan José Moreno-Navarro.
     ACM SIGPLAN Workshop on Generic Programming (WGP) (WGP). September 2008.
113. Identification of Heap-Carried Data Dependence Via Explicit Store Heap Models
     Mark Marron, Darko Stefanovic, Deepak Kapur, Manuel Hermenegildo.
     International Workshop on Languages and Compilers for Parallel Computing (LCPC). August 2008.
114. Efficient Set Sharing using ZBDDs
     M. Méndez-Lojo, O. Lhoták, M. V. Hermenegildo.
     International Workshop on Languages and Compilers for Parallel Computing (LCPC). August 2008.
115. Two Efficient Representations for Set-Sharing Analysis in Logic Programs
     E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo.
     17th International Workshop on Functional and (Constraint) Logic Programming, WFLP'08. July 2008.
116. Safe Upper-bounds Inference of Energy Consumption for Java Bytecode Applications
     J. Navas, M. Méndez-Lojo, M. Hermenegildo.
     The Sixth NASA Langley Formal Methods Workshop (LFM 08). April 2008.
117. A Practical Type Analysis for Verification of Modular Prolog Programs
     P. Pietrzak, J. Correas, G. Puebla, M. V. Hermenegildo.
     ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM). January 2008.
118. Certificate Translation for Specification-Preserving Advices
     Gilles Barthe, César Kunz.
     Workshop on Foundations of Aspect-Oriented Languages (FOAL). 2008.
119. ECEASST Building an Efficient Component for OCL Evaluation
     M. Clavel, M. Egea, M. A. García de Dios.
     Proceedings of the 8th International Workshop on OCL Concepts and Tools (OCL 2008) at MoDELS 2008. 2008.

Ph.D. Theses (36)

1. ARCHITECH:Advanced Research of Cryptographic Techniques to build efficient blockchains with privacy and security
   Anaïs Querol Cruz.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Dario Fiore. September 2022.
2. Theory and Practice of Stream Runtime Verification for Sequences and Real-Time Event Based Systems
   Felipe Gorostiaga.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Cesar Sanchez. May 2022.
3. A Scalable Static Analysis Framework for Reliable Program Development Exploiting Incrementality and Modularity
   Isabel García Contreras.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Hermenegildo, Jose Francisco Morales. July 2021.
4. Relational logics for higher-order effectful programs
   Alejandro Aguirre Galindo.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Gilles Barthe. November 2020.
5. A General Framework for Static Resource Analysis and Profiling of (Parallel) Programs and an Application to Runtime Checking
   Maximiliano Klemen.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pedro Lopez-Garcia. November 2020.
6. On the Use of Quasiorders in Formal Language Theory
   Pedro Valero Mejía.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pierre Ganty. July 2020.
7. New Perspectives on Classical Automata Constructions
   Elena Gutiérrez Viedma.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pierre Ganty. June 2020.
8. Learning secrets and models from execution time
   José Vila Bausili.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Boris Koepf. June 2020.
9. Advanced Evaluation Techniques for (Non)-Monotonic Reasoning Using Rules with Constraints
   Joaquín Arias.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro. December 2019.
10. A Model Driven Methodology for the Construction of Reliable Concurrent Software
    Raúl Alborodo.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Julio Mariño Carballo. November 2019.
11. Lineage Inference of Packed Malware using Binary Code Similarity
    Irfan Ul Haq.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero. September 2019.
12. Understanding the Evolution of Android Applications
    Paolo Calciati.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla. September 2019.
13. A Systematic Empirical Analysis of Unwanted Software Abuse, Prevalence, Distribution, and Economics
    Platon Kotzias.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero. May 2019.
14. On the Security of Cache Algorithms
    Pablo Cañones Martín.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Boris Koepf. March 2019.
15. Tools for the Detection and Analysis of Potentially Unwanted Programs
    Richard Rivera Guevara.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero. November 2018.
16. Automated Analysis of Cryptographic Constructions
    Miguel Ambrona.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Gilles Barthe. September 2018.
17. Proving Consistency of Concurrent Data Structures and Transactional Memory Systems
    Artem Khyzha.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alexey Gotsman. July 2018.
18. A Multi-Language and Multi-Platform Framework for Resource Consumption Analysis and its Application to Energy-Efficient Software Development
    Umer Liqat.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pedro Lopez. July 2018.
19. Improving Run-time Checking in Dynamic Programming Languages
    Nataliia Stulova.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Jose Francisco Morales, Manuel Hermenegildo. April 2018.
20. Cryptographic Techniques for the Security of Cloud and Blockchain Systems
    Luca Nizzardo.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Dario Fiore. March 2018.
21. An Algorithmic Approach for Stability Verification of Hybrid Systems
    Miriam García Soto.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pravithra Prabhakar. August 2017.
22. Hoare-style Reasoning with Higher-order Control: Continuations and Concurrency
    Germán Andrés Delbianco.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Aleks Nanevski. July 2017.
23. Mapping OCL as a Query and Constraint Language
    Carolina Inés Dania Flores.
    PhD Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Manuel Clavel, Marina Egea. June 2017.
24. Active Techniques for Revealing and Analyzing the Security of Hidden Servers
    Srdjan Matic.
    PhD Thesis. Universitá degli Studi de Milano (UNIMI). Supervisors: Danilo Bruschi, Juan Caballero. February 2017.
25. Tools for the Evaluation and Choice of Countermeasures against Side-channel Attacks
    Goran Doychev.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Boris Koepf. May 2016.
26. Defending Against Cybercrime: Advances in the Detection of Malicious Servers and the Analysis of Client-Side Vulnerabilities
    Antonio Nappa.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero. February 2016.
27. Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures
    Alejandro Sánchez.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Cesar Sanchez. September 2015.
28. Model-driven Development of Secure Data-Management Applications
    Miguel Ángel García de Dios.
    PhD Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Manuel Clavel. April 2015.
29. Operational Aspects of Full-Reduction in Lambda Calculi
    Álvaro García Pérez.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Jose Moreno, Pablo Nogueira. September 2014.
30. Approximate Relational Reasoning for Probabilistic Programs
    Federico Olmedo.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Gilles Barthe. January 2014.
31. Analysis of Service-Oriented Computing Systems
    Dragan Ivanovic.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro. January 2013.
32. Advanced Evaluation Strategies for Tabling and Parallelism in Logic Programs
    Pablo Chico de Guzmán.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro, Manuel Hermenegildo. November 2012.
33. Formal Certification of Game-Based Cryptographic Proofs
    Santiago Zanella.
    PhD Thesis. École Nationale Supérieure des Mines de Paris (Mines ParisTech). Supervisors: Gilles Barthe. December 2010.
34. Advanced Compilation Techniques for Logic Programming
    José Francisco Morales Caballero.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro, Manuel Hermenegildo. July 2010.
35. Técnicas Avanzadas de Compilación para Programación Lógica
    J.F. Morales.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). July 2010.
36. Certificate Translation alongside Program Transformations
    César Darío Kunz.
    PhD Thesis. École Nationale Supérieure des Mines de Paris (Mines ParisTech). Supervisors: Gilles Barthe. February 2009.

Master's Theses (47)

1. Analysis of the Impact of the Collateral Funds in Payment Channel Networks
   Ana Marija Eres.
   MSc Thesis. University of Zagreb (UniZG). Supervisors: Pedro Moreno-Sanchez, Marina Bagic Babac. July 2022.
2. Hunting for New Threats in a Feed of Malicious Samples
   Kevin van Liebergen Ávila.
   MSc Thesis. Universidad de Alcalá (UAH). Supervisors: Juan Caballero, Javier Junquera Sánchez. July 2022.
3. Forecasting Cloud Resource Utilization Using Machine Learning and Computer Vision
   Javier Galindos.
   MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Thaleia Dimitra Doudali. June 2022.
4. Empirical Analysis of Trace-ability in the Lightning Network
   Meresa Gebrewahd.
   MSc Thesis. Sapienza University of Rome (Sapienza). Supervisors: Pedro Moreno-Sanchez, Angelo Spognardi. October 2021.
5. The Temporal Booleanization Theorem: realizability checking over numerical-LTL industrial requirements
   Andoni Rodriguez.
   MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Cesar Sanchez. September 2021.
6. Analysis of Proof of Assets for Different Cryptocurrencies
   Marta Centellas Nadal.
   MSc Thesis. Universidad Complutense Madrid (UCM). Supervisors: Ignacio Cascudo, Pedro Moreno-Sanchez, Ignacio Luengo Velasco. September 2021.
7. An Integrated Approach to Assertion-Based Random Testing in Logic Languages
   Ignacio Casso.
   MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. July 2021.
8. Improvements to Parametric Cost Analysis and its Application to Smart Contracts
   Víctor Pérez Carrasco.
   MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. July 2021.
9. Auxiliary Oracle IOP and secure, fast reductions of R1CS over binary field.
   Emanuele Giunta.
   MSc Thesis. Università degli Studi di Catania (UNICT). Supervisors: Dario Catalano, Ignacio Cascudo, Dario Catalano. September 2020.
10. Threshold decryption protocols for (replayable) chosen ciphertext secure public key encryption
    Jorge Blázquez Díaz.
    MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Dario Fiore, Antonio Faonio. September 2019.
11. Homomorphic Signatures over Lattices
    Stefano Ottolenghi.
    MSc Thesis. Universita degli Studi di Genova (UNIGE). Supervisors: Dario Fiore, Giovanni Lagorio. September 2019.
12. Automatic Detection of Outdated Comments in Open-Source Java Projects
    Ankita Israel Sadu.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Ana Moreno, Barbara Russo. July 2019.
13. A Proposal of Automatic Quality Evaluator for GIT Commit Messages
    Harry Alberto Carpio Salvatierra.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Sira Vegas. July 2019.
14. An Automated Analysis of the What's New Descriptions of Android Apps
    Daniel Toniuc.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Antti Siirtola, Julio Mariño. June 2019.
15. A Framework for Testing Web Applications for Cross-Origin State Inference (COSI) Attacks
    Soheil Khodayari.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Avinash Sudhodanan, Juan Caballero, Manuel Carro. June 2019.
16. Checking Android Applications Behaviour against Google Play Descriptions at Scale
    Daniel Domínguez Álvarez.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Julio Mariño Carballo. January 2019.
17. Sistemas criptográficos de voto electrónico basados en mix-servers y proceso de implementación
    Mario V. García Roqué.
    MSc Thesis. Universidad Carlos III de Madrid (UC3M). Supervisors: Dario Fiore, Antonio Faonio, Juan Manuel Estevez Tapiador. September 2018.
18. Towards a Stream-Based Monitoring Language for Asynchronous Systems
    Felipe Gorostiaga.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Cesar Sanchez, Lars-Ake Fredlund. July 2018.
19. Detecting and Classifying Malicious TLS Network Traffic using Machine Learning
    Gibran Alberto Gómez Montes.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero, Manuel Carro. July 2018.
20. Decentralised Stream Runtime Verification
    Luis Miguel Danielsson.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Cesar Sanchez, Clara Benac Earle. July 2018.
21. Microarchitecture Simulation for Security
    Paloma Pedregal Helft.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Boris Koepf, Clara Benac. July 2018.
22. Security of Cache Replacement Policies under Side-Channel Attacks
    Felix Schroeder.
    MSc Thesis. Technical University Berlin (TU Berlin). Supervisors: Boris Koepf, Martin Skutella. March 2018.
23. Using Semantic Similarity Analysis of Javadoc Comments to Automatically Generate Test Oracles
    Arianna Blasi.
    MSc Thesis. Universitá degli Studi di Milano Bicocca (UNIMIB). Supervisors: Alessandra Gorla, Mauro Pezze. October 2017.
24. Study on Privacy of Parental Control Mobile Applications
    Álvaro Feal Fajardo.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Carmela Troncoso, Manuel Carro. July 2017.
25. ClaimChain: Decentralized Public Key Infrastructure
    Bogdan Kulynych.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Carmela Troncoso, Manuel Carro. July 2017.
26. Enhancing Online Banking Authentication Using Keystroke Dynamics
    María del Carmen Sánchez Medrano.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero, Manuel Carro. July 2017.
27. Code Search: A Semantic, Abstract-Interpretation Based Approach
    Isabel García Contreras.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Jose Francisco Morales, Manuel Hermenegildo, Manuel Hermenegildo. April 2017.
28. On Fully Homomorphic Encryption from the Learning with Errors Problem
    Chiara Redaelli.
    MSc Thesis. Universitá degli Studi di Milano Bicocca (UNIMIB). Supervisors: Dario Fiore, Luca Nizzardo, Francesca Dalla Volta. March 2017.
29. An Asynchronous Evaluation Engine for Stream Based Specifications
    Alexander Schramm.
    MSc Thesis. Universität zu Lübeck (Luebeck University). Supervisors: Cesar Sanchez, Martin Leucker. November 2016.
30. Code Search: A Semantic, Abstract Interpretation-Based Approach
    Isabel Garcia-Contreras.
    MSc Thesis. Technical University of Madrid, School of Computer Science. July 2016.
31. Implementing a Term Rewriting Engine for the EasyCrypt Framework
    Guillermo Ramos Gutiérrez.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pierre-Yves Strub, Manuel Carro. July 2015.
32. Design and Implementation of a Modular Interface to integrate CLP and Tabled Execution
    Joaquín Arias Herrero.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro. July 2015.
33. Improved Static Analysis and Verification of Energy Consumption and Other Resources via Abstract Interpretation
    Maximiliano Klemen.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pedro Lopez, Manuel Carro. July 2015.
34. A Framework for Implementing Outsourcing Schemes
    Rosario Sebastiano Russo.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Dario Fiore, Manuel Carro. July 2015.
35. Concurrent Library Abstraction Without Information Hiding
    Artem Khyzha.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alexey Gotsman, Manuel Carro. July 2014.
36. Relational Domains for the Quantification of Cache Side Channels
    Dominik Feld.
    MSc Thesis. Saarland University (Saarland University). Supervisors: Boris Koepf, Jan Reineke. September 2013.
37. Dynamic Checking of Assertions for Higher-order Predicates
    Nataliia Stulova.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Jose Francisco Morales, Manuel Hermenegildo, Manuel Hermenegildo. July 2013.
38. Probabilistic Analysis of Quality of Service
    Peerachai Kaowichakorn.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Stefanie Betz/Blekinge Institute of Technology, Manuel Carro. October 2012.
39. Developing Secure Business Applications From Secure BPMN Models
    Javier Valdazo Parnisari.
    MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Manuel Clavel. September 2012.
40. Typegrapher: Inferring the Type Graph of a Binary Program
    Gustavo Grieco.
    MSc Thesis. Universidad Nacional de Rosario (UNR). Supervisors: Juan Caballero. August 2012.
41. Valuation: Developer Support for By-References to By-Value Type Conversion
    Shiva Shabaninejad.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Mark Marron, Manuel Carro. July 2012.
42. Analysis and Mitigation of Information Leaks in Web Browsing Traffic
    Goran Doychev.
    MSc Thesis. Saarland University (Saarland University). Supervisors: Boris Koepf, Michael Backes. June 2012.
43. MySQL4OCL:un compilador de OCL a MySQL
    Carolina Inés Dania Flores.
    MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Marina Egea, Manuel Clavel. November 2011.
44. Two Algorithms for Model Checking of Regular Linear Temporal Logic
    Julián Samborski-Forlese.
    MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Cesar Sanchez, Miguel Palomino Tarjuelo. September 2011.
45. Decision Procedures for the Temporal Verification of Concurrent Data Structures
    Alejandro Sánchez.
    MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Cesar Sanchez, Miguel Palomino Tarjuelo. July 2011.
46. Fuzzy Granularity Control in Parallel/Distributed Computing
    María Teresa Trigo de la Vega.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pedro Lopez. September 2010.
47. Exploring the beta-hypercube
    Álvaro García-Pérez.
    MSc Thesis. Facultad de Informática, Universidad Politécnica de Madrid. September 2009.

Baclelor's Theses (20)

1. Browser Fingerprinting Detection and Mitigation Framework
   Karthik Ramakrishnan.
   BSc Thesis. Manipal Institute of Technology (MIT). Supervisors: Srdjan Matic, Juan Caballero, Sudheesh P G. July 2022.
2. Sistemas de restricciones algebraicas para pruebas criptográficas aplicado a SHA-256
   Miguel Morona Minguez.
   BSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Ignacio Cascudo, Dario Fiore, Ignacio Luengo Velasco. June 2022.
3. A Platform for Automating the Preparation of iOS Apps for Binary Analysis
   Alejandro de la Cruz Alvarado.
   BSc Thesis. Universidad Carlos III de Madrid (UC3M). Supervisors: Juan Caballero, Ana Isabel González-Tablas Ferreres. June 2021.
4. Mejora de un Sistema de Autodocumentación Basado en Comentarios Legibles Mecánicamente y Aserciones.: LPDowner
   Natalia Carpizo.
   BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Hermenegildo, Jose Francisco Morales, Pedro López, Manuel Hermenegildo. June 2020.
5. Analysis of Smart Contracts using Horn Clauses
   Víctor Pérez Carrasco.
   BSc Thesis. Universidad Politécnica de Madrid, ETSII. June 2020.
6. Detecting Speculative Information-Flows in Large Code Bases
   Andrés Sánchez Marín.
   BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Marco Guarnieri, José Francisco Morales, Manuel Carro. June 2019.
7. Análisis de las características de las herramientas de testing automático de aplicaciones Android de la plataforma Androtest on Docker
   Jose Carlos Garde González.
   BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Angel Herranz Nieva. January 2019.
8. Herramienta de Actualización Automática de Tests para Android
   Guillermo Paredes López.
   BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Angel Herranz Nieva. January 2019.
9. Towards Computing Distances Among Abstract Interpretations
   Ignacio Casso San Román.
   BSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Manuel Hermenegildo, Francisco J. López Fraguas. September 2018.
10. Monitorización y Detección de Ataques en Redes Corporativas
    Roberto Daniel Fernández Castro.
    BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero, Manuel Carro. July 2018.
11. Cryptographic Methods for Secure Delegation of Computation in Electronic Voting Applications
    Anaïs Querol Cruz.
    BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Dario Fiore, Manuel Carro. June 2017.
12. Diseño e Implementación de un Módulo para Identificar Código Compartido entre Ejecutables Maliciosos
    Sergio Chica Manjarrez.
    BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero, Manuel Carro. June 2017.
13. ToraDocu – Generacion Automática de Casos de Test con Oráculos
    Sergio Delgado.
    BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Damiano Zanardini. June 2017.
14. Automatic Testing Platform for Android Apps
    Sergio Valverde García.
    BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Manuel Carro. June 2017.
15. Diseño e Implementación de un Módulo para la Detección de Aplicaciones Móviles Maliciosas en Mercados Online
    Silvia Sebastián González.
    BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero, Manuel Carro. June 2017.
16. Pruebas de Primer Orden de Programas Concurrentes
    Víctor de Juan Sanz.
    BSc Thesis. Universidad Autónoma de Madrid (UAM). Supervisors: Cesar Sanchez, Juan de Lara. July 2016.
17. Linearisation of k-Index Bounded Sets of Horn Clauses
    Elena Gutiérrez Viedma.
    BSc Thesis. Universidad Autónoma de Madrid (UAM). Supervisors: Pierre Ganty, Jesús Munárriz Aldaz. May 2016.
18. Languages and Security
    Pedro Valero Mejía.
    BSc Thesis. Universidad Autónoma de Madrid (UAM). Supervisors: Pierre Ganty, Eloy Anguiano Rey. May 2016.
19. Implementing Fully Homomorphic Encryption Schemes in FPGA-based Systems
    Alejandro Ranchal Pedrosa.
    BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Guillermo Vigueras, Dario Fiore, Manuel Carro. January 2016.
20. Design and Implementation of an Endpoint Reputation Module
    Marcos Sebastián Alarcón.
    BSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero, Manuel Carro. January 2015.

Books and Monographs (6)

1. Prolog - The Next 50 Years
   David S. Warren, Veronica Dahl, Thomas Eiter, Manuel Hermenegildo, Robert Kowalski, Francesca Rossi.
   July 2023.
2. Logic-Based Program Synthesis and Transformation (LOPSTR 2016): Revised Selected Papers
   M. V. Hermenegildo, P. Lopez-Garcia.
   July 2017.
3. ICT: Energy Concepts for Energy Efficiency and Sustainability
   Giorgos Fagas, Luca Gammaitoni, John P. Gallagher, Douglas J. Paul.
   March 2017.
4. Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181)
   Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, Annabelle McIver.
   Dagstuhl Reports. 2015.
5. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures
   Alessandro Aldini, Gilles Barthe, Roberto Gorrieri.
   Foundations of Security Analysis and Design. 2009.
6. Formal Techniques for Java-Like Programs
   Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary Leavens, Peter Müller, Tobias Wrigstad.
   Object-Oriented Technology. ECOOP 2008 Workshop Reader. 2009.

Sections of Chapters in a Book (5)

1. Verifiable Computation and Succinct Arguments for NP
   Dario Fiore.
   In Asymmetric Cryptography: Primitives and Protocols. Wiley. 2022.
2. Analysis Based Verification and Debugging of Energy, Performance and Precision Properties
   P. Lopez-Garcia.
   ENTRA Project: Whole-Systems Energy Transparency (FET project 318337). December 2015.
3. Energy Optimization: Basic Static Techniques
   J.P. Gallagher.
   ENTRA Project: Whole-Systems Energy Transparency (FET project 318337). August 2014.
4. Initial Energy Consumption Analysis
   P. Lopez-Garcia.
   ENTRA Project: Whole-Systems Energy Transparency (FET project 318337). April 2014.
5. A General Framework for Resource Consumption Analysis and Verification
   P. Lopez-Garcia.
   ENTRA Project: Whole-Systems Energy Transparency (FET project 318337). November 2013.

Proceedings (53)

1. Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems - Essays Dedicated to Manuel Hermenegildo on the Occasion of His 60th Birthday
   Pedro López-García, John P. Gallagher, Roberto Giacobazzi.
   2023.
2. Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming (PPDP 2022)
   Accottoli B, M. V. Hermenegildo.
   September 2022.
3. Practical Aspects of Declarative Languages - 23rd International Symposium, PADL 2021, Copenhagen, Denmark, January 18-19, 2021, Proceedings
   José F. Morales, Dominic A. Orchard.
   2021.
4. Fundamenta Informaticae, Special Issue on the 26th International Symposium on Logic-Based Program Synthesis and Transformation: LOPSTR 2016
   Manuel V. Hermenegildo, Pedro Lopez-Garcia, Alberto Pettorossi, Maurizio Proietti.
   December 2020.
5. Proc. of Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020
   Alexey Gotsman, Ana Sokolova.
   June 2020.
6. PLAS 2019: ACM SIGSAC Workshop on Programming Languages and Analysis for Security
   Piotr Mardziel, Niki Vazou.
   November 2019.
7. Verification and Evaluation of Computer and Communication Systems - 13th International Conference, VECoS 2019, Proceedings
   Pierre Ganty, Mohamed Kaâniche.
   October 2019.
8. Proceedings of the 12th International Workshop on Search-Based Software Testing, SBST-ICSE 2019
   Alessandra Gorla, José Miguel Rojas.
   2019.
9. Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, December 03-07, 2018
   Juan Caballero, Guofei Gu.
   December 2018.
10. Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings
    John P. Gallagher, Martin Sulzmann.
    2018.
11. Proceedings of the 11th International Workshop on Search-Based Software Testing, ICSE 2018
    Alessandra Gorla, Juan Pablo Galeotti.
    2018.
12. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers
    John P. Gallagher, Fabio Fioravanti.
    2018.
13. LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
    Gilles Barthe, Geoff Sutcliffe, Margus Veanes.
    2018.
14. Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation, MARS/VPT-ETAPS 2018, and Sixth International Workshop on Verification and Program Transformation Thessaloniki, Greece, 20th April 2018
    John P. Gallagher, Rob van Glabbeek, Wendelin Serwe.
    2018.
15. Proceedings of the 33rd Annual Computer Security Applications Conference, Orlando, FL, USA, December 4-8, 2017
    Davide Balzarotti, Juan Caballero.
    December 2017.
16. Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers
    Manuel V. Hermenegildo, Pedro Lopez-Garcia.
    2017.
17. 32nd International Conference on Logic Programming
    Manuel Carro, Andy King.
    September 2016.
18. Detection of Intrusions and Malware, and Vulnerability Assessment - 13th International Conference, DIMVA 2016, San Sebastián, Spain, July 7-8, 2016, Proceedings
    Juan Caballero, Urko Zurutuza, Ricardo J. Rodríguez.
    July 2016.
19. Engineering Secure Software and Systems - 8th International Symposium, ESSoS 2016. Proceedings
    Juan Caballero, Eric Bodden, Elias Athanasopoulos.
    April 2016.
20. Proceedings of the First Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016)
    Manuel Carro, Salvador Tamarit, Guillermo Vigueras, Julio Mariño.
    March 2016.
21. Proceedings of the 25th International Conference on Compiler Construction (CC 2016)
    A. Zaks, M. V. Hermenegildo.
    March 2016.
22. Security and Trust Management - 12th International Workshop, STM 2016, Heraklion, Crete, Greece, September 26-27, 2016, Proceedings
    Gilles Barthe, Evangelos P. Markatos, Pierangela Samarati.
    2016.
23. Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015, Revised Selected Papers
    Pierre Ganty, Michele Loreti.
    2016.
24. Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS (satellite event of ETAPS), Eindhoven, The Netherlands, 3rd April 2016
    John P. Gallagher, Philipp Rümmer.
    2016.
25. Technical Communications of the 32nd International Conference on Logic Programming
    Manuel Carro, Andy King, Neda Saeedloei, Marina De Vos.
    2016.
26. Proceedings of the Eighth European Workshop on System Security, EuroSec 2015, Bordeaux, France, April 21, 2015
    Juan Caballero, Michalis Polychronakis.
    April 2015.
27. Engineering Secure Software and Systems - 7th International Symposium, ESSoS 2015, Milan, Italy, March, 4-6, 2015. Proceedings
    Frank Piessens, Juan Caballero, Nataliia Bielova.
    March 2015.
28. Fourteenth Annual DFRWS Conference
    Juan Caballero, Simson Garfinkel.
    August 2014.
29. Proceedings of the Seventh European Workshop on System Security, EuroSec 2014, April 13, 2014, Amsterdam, The Netherlands
    Davide Balzarotti, Juan Caballero.
    April 2014.
30. Proceedings of the Eleventh Workshop on Constraint Handling Rules (CHR 2014)
    R. Haemmerlé, J. Sneyers.
    2014.
31. Thirteenth Annual DFRWS Conference
    Clay Shields, Juan Caballero.
    August 2013.
32. Proceedings of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013)
    R. Haemmerlé, J.F. Morales.
    2013.
33. Engineering Secure Software and Systems - 4th International Symposium, ESSoS 2012, Eindhoven, The Netherlands, February, 16-17, 2012. Proceedings
    Gilles Barthe, Benjamin Livshits, Riccardo Scandariato.
    2012.
34. Formal Aspects of Security and Trust - 8th International Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected Papers
    Gilles Barthe, Anupam Datta, Sandro Etalle.
    2012.
35. Software Engineering and Formal Methods - 9th International Conference, SEFM 2011
    Gilles Barthe, Alberto Pardo, Gerardo Schneider.
    November 2011.
36. Technical Communications of the 27th International Conference on Logic Programming (ICLP'11)
    John P. Gallagher, Michael Gelfond.
    July 2011.
37. Theory and Practice of Logic Programming. 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue
    John P. Gallagher, Michael Gelfond.
    July 2011.
38. Third International Workshop on Principles of Enginering Service-Oriented Systems (PESOS 2011)
    M. Carro, D. Karastoyanova, G. A. Lewis, A. Liu.
    May 2011.
39. 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
    Gilles Barthe.
    March 2011.
40. ACM SIGPLAN Proceedings of the Workshop on Declarative Aspects of Multicore Programming
    M. Carro, J.H. Reppy.
    January 2011.
41. Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers
    Jorge Cuéllar, Javier Lopez, Gilles Barthe, Alexander Pretschner.
    2011.
42. Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10)
    M. V. Hermenegildo, T. Schaub.
    July 2010.
43. Theory and Practice of Logic Programming. 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue
    M. V. Hermenegildo, T. Schaub.
    July 2010.
44. Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010)
    M. V. Hermenegildo, J. Palsberg.
    January 2010.
45. Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010
    G. Barthe, M. Hermenegildo.
    January 2010.
46. Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010, Madrid, Spain, January 18-19, 2010
    John P. Gallagher, Janis Voigtländer.
    2010.
47. Proceedings of the 19th Workshop on Logic-based methods in Programming Environments (WLPE 2009)
    Rafael Caballero, John P. Gallagher.
    2010.
48. FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs
    Anindya Banerjee.
    2009.
49. Functional and Logic Programming, 9th International Symposium, FLOPS'08
    J. Garrigue, M. V. Hermenegildo.
    April 2008.
50. ACM SIGPLAN-Intel Workshop on Declarative Aspects of Multicore Programming, DAMP'08, Informal Proceedings
    M. V. Hermenegildo.
    January 2008.
51. Functional and Logic Programming, 9th International Symposium, FLOPS 2008, Ise, Japan, April 14-16, 2008. Proceedings
    Jacques Garrigue, Manuel V. Hermenegildo.
    2008.
52. Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings
    Gilles Barthe, Frank S. de Boer.
    2008.
53. Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers
    Gilles Barthe, Cédric Fournet.
    2008.

Technical Reports and Manuals (69)

1. Unsupervised Detection and Clustering of Malicious TLS Flows
   Gibran Gomez, Platon Kotzias, Matteo Dell'Amico, Leyla Bilge, Juan Caballero.
   Computing Research Repository. January 2023.
2. GoodFATR: A Platform for Automated Threat Report Collection and IOC Extraction
   Juan Caballero, Gibran Gomez, Srdjan Matic, Gustavo Sánchez, Silvia Sebastián, Arturo Villacañas.
   Computing Research Repository. 2023.
3. A Rule-based Approach for Designing and Composing Abstract Domains
   D. Jurjo, J. F. Morales, P. Lopez-Garcia, M.V. Hermenegildo.
   CLIP Lab, IMDEA Software Institute. December 2022.
4. A Deep Dive into VirusTotal: Characterizing and Clustering a Massive File Feed
   Kevin van Liebergen, Juan Caballero, Platon Kotzias, Chris Gates.
   Computing Research Repository. October 2022.
5. Automated Approximate Recurrence Solving applied to Static Analysis of Energy Consumption
   L. Rustenholz.
   CLIP Lab, IMDEA Software Institute. August 2022.
6. Flux: Liquid Types for Rust
   Nico Lehmann, Adam Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala.
   Computing Research Repository. 2022.
7. Spectre Declassified: Reading from the Right Place at the Wrong Time
   Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom.
   IACR Cryptology ePrint Archive. 2022.
8. Typing High-Speed Cryptography against Spectre v1
   Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean.
   IACR Cryptology ePrint Archive. 2022.
9. Breaking and Fixing Speculative Load Hardening
   Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom.
   IACR Cryptology ePrint Archive. 2022.
10. A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
    Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu.
    Computing Research Repository. 2021.
11. SoK: Practical Foundations for Spectre Defenses
    Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan.
    Computing Research Repository. 2021.
12. âœTheyâ™re not that hard to mitigateâ157: What Cryptographic Library Developers Think About Timing Attacks
    Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar.
    IACR Cryptology ePrint Archive. 2021.
13. UniStore: A fault-tolerant marriage of causal and strong consistency (extended version)
    Manuel Bravo, Alexey Gotsman, Borja de Régil, Hengfeng Wei.
    Computing Research Repository. 2021.
14. The Ciao Playground
    G. Garcia-Pradales, J.F. Morales, M. V. Hermenegildo.
    Technical University of Madrid (UPM) and IMDEA Software Institute. 2021.
15. A Theoretical Study of (Full) Tabled Constraint Logic Programming
    Joaquín Arias, Manuel Carro.
    arXiv. September 2020.
16. On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
    Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo.
    Computing Research Repository. 2020.
17. LIO*: Low Level Information Flow Control in F
    Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin, Niki Vazou.
    Computing Research Repository. 2020.
18. High-Assurance Cryptography Software in the Spectre Era
    Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe.
    IACR Cryptology ePrint Archive. 2020.
19. Making Byzantine Consensus Live (Extended Version)
    Manuel Bravo, Gregory Chockler, Alexey Gotsman.
    Computing Research Repository. 2020.
20. Towards Improving the Performance of BFT Consensus For Future Permissioned Blockchains
    Manuel Bravo, Zsolt István, Man-Kit Sit.
    Computing Research Repository. 2020.
21. Incrementalizing Context-sensitive Analyses for Modularized Programs
    I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
    arXiv. July 2019.
22. Coupling Techniques for Reasoning about Quantum Programs
    Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou.
    Computing Research Repository. 2019.
23. Kantorovich Continuity of Probabilistic Programs
    Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.
    Computing Research Repository. 2019.
24. Towards Constant-Time Foundations for the New Spectre Era
    Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Deian Stefan, Tamara Rezk, Gilles Barthe.
    Computing Research Repository. 2019.
25. Automated Methods for Checking Differential Privacy
    Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan.
    Computing Research Repository. 2019.
26. Machine-Checked Proofs for Cryptographic Standards
    José Bacelar Almeida, Cecile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub.
    IACR Cryptology ePrint Archive. 2019.
27. GALACTICS: Gaussian Sampling for Lattice-Based Constant-Time Implementation of Cryptographic Signatures, Revisited
    Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Mélissa Rossi, Mehdi Tibouchi.
    IACR Cryptology ePrint Archive. 2019.
28. Reconfigurable Atomic Transaction Commit (Extended Version)
    Manuel Bravo, Alexey Gotsman.
    Computing Research Repository. 2019.
29. An Approach to Incremental and Modular Context-sensitive Analysis of Logic Programs
    I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
    The CLIP Lab, IMDEA Software Institute and T.U. Madrid. April 2018.
30. An Approach to Static Performance Guarantees for Programs with Run-time Checks
    M. Klemen, N. Stulova, P. Lopez-Garcia, J. F. Morales, M. V. Hermenegildo.
    The CLIP Lab, IMDEA Software Institute and T.U. Madrid. April 2018.
31. Formal verification of higher-order probabilistic programs
    Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.
    Computing Research Repository. 2018.
32. Term Hiding and its Impact on Run-time Check Simplification
    N. Stulova, J. F. Morales, M. V. Hermenegildo.
    The CLIP Lab. May 2017.
33. Using higher-order contracts to model session types
    Giovanni Bernardi, Matthew Hennessy.
    Computing Research Repository. 2016.
34. Mutually Testing Processes
    Giovanni Bernardi, Matthew Hennessy.
    Computing Research Repository. April 2015.
35. Parametric Static Profiling
    P. Lopez-Garcia, R. Haemmerlé, U. Liqat, M. Klemen, M. V. Hermenegildo.
    The CLIP Lab. April 2015.
36. Modelling MAC-Layer Communications in Wireless Systems
    Andrea Cerone, Matthew Hennessy, Massimo Merro.
    Computing Research Repository. 2015.
37. Computer-aided Verification in Mechanism Design
    Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub.
    Computing Research Repository. 2015.
38. An Optimised Algorithm for Determinisation and Completion of Finite Tree Automata
    John P. Gallagher, Mai Ajspur, Bishoksan Kafle.
    Computing Research Repository. 2015.
39. A Top-to-Bottom View: Energy Analysis for Mobile Application Source Code
    Xueliang Li, John P. Gallagher.
    Computing Research Repository. 2015.
40. On the Confluence of the Analytical Semantics of CHR
    R. Haemmerlé.
    Technical University of Madrid (UPM). July 2014.
41. Inferring Energy Consumption at Different Software Levels: ISA vs. LLVM IR
    U. Liqat, K. Georgiou, S. Kerrison, P. Lopez-Garcia, M. V. Hermenegildo, J. P. Gallagher, K. Eder.
    ENTRA Project. April 2014.
42. An Approach to Assertion-based Debugging of Higher-Order (C)LP Programs
    N. Stulova, J. F. Morales, M. V. Hermenegildo.
    The CLIP Lab. January 2014.
43. Analysis and Transformation Tools for Constrained Horn Clause Verification
    John P. Gallagher, Bishoksan Kafle.
    Computing Research Repository. 2014.
44. Generating Bounded Languages Using Bounded Control Sets
    Pierre Ganty, Radu Iosif.
    Computing Research Repository. 2014.
45. Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
    Murdoch J. Gabbay, Aleksandar Nanevski.
    Computing Research Repository. March 2013.
46. ARTISTE: Automatic Generation of Hybrid Data Structure Signatures from Binary Code Executions
    Juan Caballero, Gustavo Grieco, Mark Marron, Zhiqiang Lin, David Urbina.
    IMDEA Software Institute. August 2012.
47. ActionUWE: Transformation of UWE to ActionGUI Models
    Marianne Busch, Miguel Ángel García de Dios.
    Ludwig-Maximilians-Universität München. 2012.
48. Structural Analysis: Shape Information via Points-To Computation
    Mark Marron.
    Computing Research Repository. 2012.
49. Automated Analysis and Synthesis of Padding-Based Encryption Schemes
    Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin.
    Cryptology ePrint Archive, Report 2012/695. 2012.
50. The LPdoc Documentation Generator. Ref. Manual (V3.0)
    M. V. Hermenegildo, J.F. Morales.
    UPM. July 2011.
51. Towards Modular Extensions for a Modular Language
    J.F. Morales, M. V. Hermenegildo, R. Haemmerlé.
    Technical University of Madrid (UPM). January 2011.
52. A Simulation Study on Parallel Backtracking with Solution Memoing for Independent And-Parallelism
    P. Chico de Guzmán, A. Casas, M. Carro, M. V. Hermenegildo.
    Technical University of Madrid (UPM). January 2011.
53. Towards Resource Usage Function Verification based on Input Data Size Intervals
    P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo.
    UPM. 2011.
54. Towards Data-Aware Cost-Driven Adaptation for Service Orchestrations
    D. Ivanović, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, E. Mera.
    Technical University of Madrid (UPM). March 2010.
55. An Approach to Profiling for Run-Time Checking of Computational Properties and Performance Debugging
    E. Mera, T. Trigo, P. Lopez-Garcia, M. V. Hermenegildo.
    Technical University of Madrid (UPM). March 2010.
56. Towards a Framework for Resource Usage Verification and Debugging in the CiaoPP System
    P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo.
    Technical University of Madrid (UPM). February 2010.
57. Towards Parameterized Regular Type Inference Using Set Constraints
    Francisco Bueno, Jorge A. Navas, Manuel V. Hermenegildo.
    Computing Research Repository. 2010.
58. Parikh's Theorem: A simple and direct construction
    Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger.
    Computing Research Repository. 2010.
59. Sharing-Based Independence-Driven Fragment Identification for Service Orchestrations
    D. Ivanović, M. Carro, M. V. Hermenegildo.
    Technical University of Madrid (UPM). December 2009.
60. Towards Data-Aware Resource Analysis for Service Orchestrations
    D. Ivanović, M. Carro, M. V. Hermenegildo.
    Technical University of Madrid (UPM). June 2009.
61. Towards Integrating Run-Time Checking and Software Testing in a Verification Framework
    E. Mera, P. Lopez-Garcia, M. V. Hermenegildo.
    T. U. Madrid (UPM). March 2009.
62. Inferring Determinacy and Mutual Exclusion in Logic Programs Using Mode and Type Analysis
    P. Lopez-Garcia, F. Bueno, M. V. Hermenegildo.
    Technical University of Madrid (UPM). February 2009.
63. The Ciao System. Ref. Manual (V1.13)
    F. Bueno, D. Cabeza, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, G. Puebla-.
    UPM. 2009.
64. Bridge Program Transformation for the CCall Tabling Scheme
    P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
    Technical University of Madrid (UPM). September 2008.
65. Efficient Representations for Set-Sharing Analysis
    E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo.
    University of New Mexico and Technical University of Madrid. September 2008.
66. Inference of User-Definable Resource Bounds Usage for Logic Programs and its Applications
    J. Navas, E. Mera, P. Lopez-Garcia, M. Hermenegildo.
    Technical University of Madrid (UPM). July 2008.
67. Fast Set Sharing using ZBDDs
    M. Méndez-Lojo, O. Lhoták, M. V. Hermenegildo.
    University of New Mexico. June 2008.
68. Rigorous Methods for Mobile and Heterogeneous Software Systems – Second Year Report
    M. Hermenegildo, E. Albert, P. Arenas, F. Bueno, M. Carro, A. Casas, P. Chico de Guzmán, J. Correas, S. Genaim, J. Lipton, Pedro Lopez-Garcia, M. Méndez, E. Mera, J. Morales, J. Navas, R. Padilla, P. Pietrzak, G. Puebla, M. Zamalloa, D. Zanardini.
    Technical University of Madrid (UPM). April 2008.
69. Customizable Resource Usage Analysis for Java Bytecode
    J. Navas, M. Méndez-Lojo, M. V. Hermenegildo.
    UNM. 2008.

Articles in Books and Other Collections (28)

1. Teaching Prolog with Active Logic Documents
   J.F. Morales, Salvador Abreu, D. Ferreiro, M.V. Hermenegildo.
   Prolog - The Next 50 Years. July 2023.
2. Types, modes and so much more – the Prolog way
   M.V. Hermenegildo, J.F. Morales, P. Lopez-Garcia, M. Carro.
   Prolog - The Next 50 Years. July 2023.
3. Prolog: Past, Present, and Future
   Gopal Gupta, Elmer Salazar, Joaquín Arias, Kinjal Basu, S Varanasi, M Carro.
   Prolog - The Next 50 Years. July 2023.
4. Some Thoughts on How to Teach Prolog
   M.V. Hermenegildo, J.F. Morales, P. Lopez-Garcia.
   Prolog - The Next 50 Years. July 2023.
5. Runtime Verification for Decentralized and Distributed Systems
   Adrian Francalanza, Jorge A. Perez, César Sánchez.
   Lectures on Runtime Verification – Introductory and Advanced Topics. 2018.
6. Energy Consumption Analysis and Verification using CiaoPP
   P. Lopez-Garcia, M. V. Hermenegildo, M. Klemen, U. Liqat.
   September 2017.
7. Energy-Aware Software Engineering
   Kerstin Eder, John P. Gallagher.
   ICT - Energy Concepts for Energy Efficiency and Sustainability. March 2017.
8. Energy Challenges for ICT
   Giorgos Fagas, John P. Gallagher, Luca Gammaitoni, Douglas J. Paul.
   ICT - Energy Concepts for Energy Efficiency and Sustainability. March 2017.
9. Intrinsic Redundancy for Reliability and Beyond
   Alberto Goffi, Alessandra Gorla, Andrea Mattavelli, Mauro Pezzè.
   Present and Ulterior Software Engineering. 2017.
10. Machine Learning-Driven Automatic Program Transformation to Increase Performance in Heterogeneous Architectures
    Salvador Tamarit, Guillermo Vigueras, Manuel Carro, Julio Mariño.
    Tools for High Performance Computing 2016. 2017.
11. Rule formats for bounded nondeterminism in structural operational semantics
    Luca Aceto, Álvaro García-Pérez, Anna Ingólfsdóttir.
    Semantics, Logics and Calculi—Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. 2016.
12. Computer-Aided Proofs in Cryptography: An Overview
    Gilles Barthe, François Dupressoir, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub.
    All about Proofs, Proofs for All (APPA). January 2015.
13. Mining Android Apps for Anomalies
    Konstantin Kuznetsov, Alessandra Gorla, Ilaria Tavecchia, Florian Gross, Andreas Zeller.
    The Art and Science of Analyzing Software Data. 2015.
14. Towards LLVM-Based Energy Consumption Analysis of Programs
    K. Georgiou, U. Liqat.
    July 2014.
15. Model-Driven Development of a Secure eHealth Application
    Miguel Ángel García de Dios, Carolina Dania, David A. Basin, Manuel Clavel.
    Engineering Secure Future Internet Services and Systems - Current Research. 2014.
16. Whole Systems Energy Transparency
    Kerstin Eder, Steve Kerrison, John Gallagher, Pedro Lopez-Garcia.
    NANOENERGY Letters. August 2013.
17. State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings
    Anindya Banerjee, David A. Naumann.
    Aliasing in Object-Oriented Programming. 2013.
18. Ownership Types: A Survey
    Dave Clarke, Johan Östlund, Ilya Sergey, Tobias Wrigstad.
    Aliasing in Object-Oriented Programming. Types, Analysis and Verification. 2013.
19. Content-Sniffing XSS Attacks: XSS with non-HTML Content
    Juan Caballero, Adam Barth, Dawn Song.
    The Death of the Internet. July 2012.
20. A Fuzzy Approach to Resource Aware Automatic Parallelization
    T. Trigo, P. Lopez-Garcia, S. Muñoz-Hernandez.
    Computational Intelligence. 2012.
21. Interval-Based Resource Usage Verification: Formalization and Prototype
    P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo.
    Proc. of FOPARA. 2012.
22. Merlin: specification inference for explicit information flow problems
    V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee.
    Mining Software Specifications. May 2011.
23. Parameterized Metareasoning in Membership Equational Logic
    Manuel Clavel, Narciso Martí-Oliet, Miguel Palomino.
    Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday. 2011.
24. Logic Languages
    M. Carro, M. V. Hermenegildo.
    Encyclopedia of Parallel Computing. 2011.
25. An Overview of The Ciao Multiparadigm Language and Program Development Environment and its Design Philosophy
    M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, J.F. Morales, G. Puebla.
    Festschrift for Ugo Montanari. June 2008.
26. An Introduction to Certificate Translation
    Gilles Barthe, César Kunz.
    Foundations of Security Analysis and Design. 2008.
27. A Tutorial on Type-Based Termination
    Gilles Barthe, Benjamin Grégoire, Colin Riba.
    EU LerNet ALFA Project. 2008.
28. The Reaction Algebra: A Formal Language for Event Correlation
    César Sánchez, Matteo Slanina, Henny B. Sipma, Zohar Manna.
    Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. 2008.

Invited Papers and Tutorials (22)

1. 50-Years of Prolog and Beyond (invited talk)
   M. V. Hermenegildo.
   November 2022.
2. Some reflections on Prolog's evolution, status, and future on the 50th anniversary of the birth of Prolog (abstract of invited talk)
   M. V. Hermenegildo.
   International Conference on Logic Programming. August 2022.
3. Preface, Fundamenta Informaticae, Special Issue on the 26th International Symposium on Logic-Based Program Synthesis and Transformation: LOPSTR 2016
   Manuel V. Hermenegildo, Pedro Lopez-Garcia, Alberto Pettorossi, Maurizio Proietti.
   Fundamenta Informaticae. December 2020.
4. Cost Analysis of Smart Contracts via Parametric Resource Analysis
   V. Perez-Carrasco, M. Klemen, P. Lopez-Garcia, J.F. Morales, M. V. Hermenegildo.
   Static Analysis Symposium. November 2020.
5. Multivariant Assertion-based Guidance of Top-down Horn Clause-based Analysis in CiaoPP
   M. V. Hermenegildo, I. Garcia-Contreras, J. Morales, P. Lopez-Garcia, M. Klemen, I. Casso.
   Workshop on Declarative Program Analysis (DPA 2019). July 2019.
6. Horn Clause-based Program Analysis and Verification with CiaoPP
   M. V. Hermenegildo, P. Lopez-Garcia, J. Morales, I. Garcia-Contreras, M. Klemen, N. Stulova.
   1st International Workshop on Declarative Program Analysis (DPA 2018). July 2018.
7. Informatics Research Evaluation
   Floriana Esposito, Carlo Ghezzi, Manuel V. Hermenegildo, Helene Kirchner, Luke Ong.
   March 2018.
8. Tutorial: Consistency Choices in Modern Distributed Systems
   Alexey Gotsman.
   ACM Symposium on Principles of Distributed Computing. 2018.
9. Energy Consumption Analysis and Verification by Transformantion into Horn Clauses and Abstract Interpretation
   M. V. Hermenegildo, P. Lopez-Garcia, U. Liqat, M. Klemen.
   International Workshop on Verification and Program Transformation. April 2017.
10. EasyCrypt: A Tutorial
    Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub.
    Foundations of Security Analysis and Design. 2013.
11. Conferences vs. Journals in CS, what to do? Evolutionary ways forward and the ICLP/TPLP model
    M. V. Hermenegildo.
    Dagstuhl 12452: Publication Culture in Computing Research – Position Papers. November 2012.
12. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations
    D. Ivanović, M. Carro, M. V. Hermenegildo.
    22nd Workshop on Logic-based Methods in Programming Environments. September 2012.
13. Program Analysis With Regular Tree Languages
    John P. Gallagher.
    International Symposium on Logic-based Program Synthesis and Transformation. 2012.
14. Verifying Cryptographic Code in C: Some Experience and the Csec Challenge
    Mihhail Aizatulin, François Dupressoir, Andrew D. Gordon, Jan Jürjens.
    Formal Aspects of Security and Trust (FAST). 2012.
15. Introduction to Technical Communications of the 27th Int'l. Conference on Logic Programming (ICLP'11)
    John P. Gallagher, Michael Gelfond.
    International Conference on Logic Programming. July 2011.
16. Introduction to the 27th International Conference on Logic Programming (ICLP'11) Special Issue
    John P. Gallagher, Michael Gelfond.
    International Conference on Logic Programming. July 2011.
17. An Overview of the Ciao System
    M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, R. Haemmerlé, E. Mera, J. F. Morales, G. Puebla.
    International Web Rule Symposium. July 2011.
18. Introduction to Technical Communications of the 26th Int'l. Conference on Logic Programming (ICLP'10)
    M. V. Hermenegildo, T. Schaub.
    International Conference on Logic Programming. July 2010.
19. Introduction to the 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue
    M. V. Hermenegildo, T. Schaub.
    International Conference on Logic Programming. July 2010.
20. Semantics and Enforcement of Expressive Information Flow Policies
    Anindya Banerjee.
    Formal Aspects in Security and Trust. 2010.
21. Formal Certification of ElGamal Encryption. A Gentle Introduction to CertiCrypt
    Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin.
    5th International workshop on Formal Aspects in Security and Trust, FAST 2008. 2009.
22. Certificate Translation
    Gilles Barthe.
    International Conference on Automated Deduction. 2008.