Artículos en Revistas (272)

1. Exploiting Multiple Abstract Call Patterns for Optimizing Run-Time Checks
   Daniela Ferreiro, Daniel Jurjo, Marco Ciccalè, José F. Morales, Pedro López-García, Manuel V. Hermenegildo.
   Theory and Practice of Logic Programming. Cambridge University Press, julio 2026.
2. Abstractions of Sequences, Functions and Operators
   Louis Rustenholz, Pedro Lopez-Garcia, Manuel V. Hermenegildo.
   International Journal on Software Tools for Technology Transfer. Springer, marzo 2026.
3. Network scale-up methods on aggregated relational data to estimate the outcome of elections
   Jorge M. Arevalillo, Juan Marcos Ramírez, Sergio Díaz-Aranda, Jose Aguilar, Antonio Fernández Anta, Rosa E. Lillo.
   Social Networks 86, 312-324. 2026.
4. Analysis of the Quid Pro Quo Mechanism With Correlated Players
   Josu Doncel, A. Cerezo, Agustín Santos, Antonio Fernández Anta.
   IEEE Access 14, 50023–50034. 2026.
5. Byzantine-tolerant distributed grow-only sets: specification and applications
   Vicent Cholvi, Antonio Fernández Anta, Chryssis Georgiou, Nicolas Nicolaou, Michel Raynal, Antonio Russo.
   Distributed Computing 39 (2), 7. 2026.
6. Robust network scale-up method estimators
   Sergio Díaz-Aranda, Juan Marcos Ramirez, José Aguilar, Rosa E. Lillo, Antonio Fernández Anta.
   Soc. Networks 84, 46–61. 2026.
7. Boosting Concurrency and Fault-Tolerance for Reconfigurable Shared Large Objects
   Andria Trigeorgi, Nicolas Nicolaou, Chryssis Georgiou, Antonio Fernández Anta, Theophanis Hadjistasi, Efstathios Stavrakis.
   ACM Transactions on Storage 22 (2), 20:1–20:55. 2026.
8. A dynamic explainability method for fuzzy cognitive maps based on causal and temporal evolution analysis
   D. Benito, J. Aguilar, J. M. Ramírez, M. Mora Cantallops, A. Fernández Anta.
   Applied Soft Computing, 115925. Elsevier, 2026.
9. Web of Shadows: Investigating Malware Abuse of Internet Services
   Mauro Allegretta, Marco Gramaglia, Giuseppe Siracusano, Roberto Gonzalez, Juan Caballero.
   Computers & Security 149 (C). Elsevier, noviembre 2025.
10. Checkification: A Practical Approach for Testing Static Analysis Truths
    Daniela Ferreiro, Ignacio Casso, Pedro Lopez-Garcia, José F. Morales, Manuel V. Hermenegildo.
    Theory and Practice of Logic Programming 25 (5), 829–866. Cambridge U. Press, septiembre 2025.
11. Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
    Marco Ciccalè, Daniel Jurjo, José F. Morales, Pedro López-García, Manuel V. Hermenegildo.
    Theory and Practice of Logic Programming 25 (4), 612-630. Cambridge University Press, septiembre 2025.
12. Circuit Width Estimation via Effect Typing and Linear nbsp;Dependency
    Andrea Colledan, Ugo Dal Lago, Niki Vazou.
    TYPES 47 (3). Association for Computing Machinery, 2025.
13. Social Compliance With NPIs, Mobility Patterns, and Reproduction Number: Lessons From COVID-19 in Europe
    Daniele Baccega, José Aguilar, Carlos Baquero, Antonio Fernández Anta, Juan Marcos Ramirez.
    IEEE Access 13, 134357–134375. 2025.
14. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
    Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying.
    Journal of the ACM 72 (3), 20:1–20:51. 2025.
15. Compact Proofs of Partial Knowledge for Overlapping CNF Formulae
    Gennaro Avitabile, Vincenzo Botta, Daniele Friolo, Daniele Venturi, Ivan Visconti.
    Journal of Cryptology 38 (1), 7. 2025.
16. A Quantitative Probabilistic Relational Hoare Logic
    Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire.
    Proceedings of the ACM on Programming Languages 9 ({POPL}), 1167–1195. 2025.
17. Preservation of Speculative Constant-Time by Compilation
    Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte.
    Proceedings of the ACM on Programming Languages 9 ({POPL}), 1293–1325. 2025.
18. Automating Equational Proofs in Dirac Notation
    Yingte Xu, Gilles Barthe, Li Zhou.
    Proceedings of the ACM on Programming Languages 9 ({POPL}), 1227–1259. 2025.
19. Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code
    Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, Peter Schwabe.
    IACR Trans. Cryptogr. Hardw. Embed. Syst. 2025 (3), 644–667. 2025.
20. Test Oracle Automation in the Era of LLMs
    Facundo Molina, Alessandra Gorla, Marcelo d'Amorim.
    ACM Transactions on Software Engineering and Methodology 34 (5), 150:1–150:24. 2025.
21. Natively Compatible Super-Efficient Lookup Arguments and How to Apply Them
    Matteo Campanelli, Dario Fiore, Rosario Gennaro.
    Journal of Cryptology 38 (1), 14. 2025.
22. MixBuy: Contingent Payment in the Presence of Coin Mixers
    D. Castejon-Molina, D. Vasilopoulos, P. Moreno-Sanchez.
    Privacy Enhancing Technologies Symposium 2025 (1). 2025.
23. Large Elimination and Indexed Types in Refinement Types
    Alessio Ferrarini, Niki Vazou.
    TYPES. 2025.
24. Performance Analysis of NSUM Estimators in Social-Network Topologies
    Sergio Díaz-Aranda, Jose Aguilar, Juan Marcos Ramírez, David Rabanedo, Antonio Fernández Anta, Rosa E Lillo.
    The American Statistician 79 (2), 247–264. Taylor & Francis, 2025.
25. Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
    Xaver Fabian, Marco Patrignani, Marco Guarnieri, Michael Backes.
    Proceedings of the ACM on Programming Languages (PACMPL) 9 ({POPL}). ACM, 2025.
26. The Reachable Simulation Problem
    Pierre Ganty, Nicolas Manini, Francesco Ranzato.
    ACM Transactions on Computational Logic 26 (3), 12:1–12:35. 2025.
27. Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
    Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov.
    Proceedings of the ACM on Programming Languages 9 ({ICFP}), 160–189. 2025.
28. Abstract Environment Trimming
    Daniel Jurjo, José F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo.
    Theory and Practice of Logic Programming 24 (4), 863-884. Cambridge U. Press, octubre 2024.
29. MOSFHET: Optimized Software for FHE over the Torus
    Antonio Guimarães, Edson Borin, Diego F. Aranha.
    Journal of Cryptographic Engineering 14 (3), 577–593. septiembre 2024.
30. Mechanizing Refinement Types
    Michael H. Borkowski, Niki Vazou, Ranjit Jhala.
    Proc. ACM Program. Lang. 8 (POPL). Association for Computing Machinery, enero 2024.
31. Progressive and efficient verification for digital signatures: extensions and experimental results
    Cecilia Boschini, Dario Fiore, Elena Pagnin, Luca Torresetti, Andrea Visconti.
    Journal of Cryptographic Engineering 14 (3), 551–575. 2024.
32. Abstraction-Aware Inference of Metamorphic Relations
    Agustín Nolasco, Facundo Molina, Renzo Degiovanni, Alessandra Gorla, Diego Garbervetsky, Mike Papadakis, Sebastián Uchitel, Nazareno Aguirre, Marcelo F. Frias.
    Proc. ACM Softw. Eng. 1 ({FSE}), 450–472. 2024.
33. BEAPI: A tool for bounded exhaustive input generation from APIs
    Mariano Politano, Valeria S. Bengolea, Facundo Molina, Nazareno Aguirre, Marcelo F. Frias, Pablo Ponzio.
    Science of Computer Programming 238, 103153. 2024.
34. On the Complexity of Proving Polyhedral Reductions
    Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan.
    Fundamenta Informaticae 192 (3-4), 363–394. IOS Press, 2024.
35. Improving Blockchain Scalability with the Setchain Data-Type
    Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Antonio Russo, César Sánchez.
    Distributed Ledger Technology: Research and Practice 3 (1), 1:1–1:2. 2024.
36. Verification-Guided Shielding for Deep Reinforcement Learning
    Davide Corsi, Guy Amir, Andoni Rodríguez, Guy Katz, César Sánchez, Roy Fox.
    Reinforcement Learning Journal 4, 1759–1780. 2024.
37. General monitorability of totally ordered verdict domains
    Felipe Gorostiaga, César Sánchez.
    Innovations in Systems and Software Engineering. 2024.
38. MadQCI: a heterogeneous and scalable SDN-QKD network deployed in production facilities
    Vicente Martin, Juan Pedro Brito, Laura Ortíz, Rubén B. Méndez, Jaime Sáez de Buruaga, Rafael J. Vicente, Alberto Sebastián-Lombraña, David Rincón, Fernando Pérez, César Sánchez, Momtchil Peev, Hans H. Brunner, Chi-Hang Fred Fung, Andreas Poppe, Florian Fröwis, Andrew J. Shields, Robert Ian Woodward, Helmut Griesser, Stefan Roehrich, Fernando de la Iglesia, Carlos Abellán, Michael Hentschel, José Manuel Rivas-Moscoso, Antonio Pastor-Perales, Jesús Folgueira, Diego López.
    NPJ Quantum Information 10 (80). 2024.
39. A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs
    Louis Rustenholz, Maximiliano Klemen, Miguel Ángel Carreira-Perpiñán, Pedro López-García.
    TPLP. 2024.
40. Liveness and latency of Byzantine state-machine replication
    Manuel Bravo, Gregory Chockler, Alexey Gotsman.
    Distributed Computing 37 (2), 177–205. Springer, 2024.
41. Realizability modulo theories
    Andoni Rodríguez, César Sánchez.
    Journal of Logic and Algebraic Methods in Programming 140. 2024.
42. Zero-knowledge proofs for set membership: efficient, succinct, modular
    Daniel Benarroch, Matteo Campanelli, Dario Fiore, Kobi Gurkan, Dimitris Kolonelos.
    Designs, Codes and Cryptography. julio 2023.
43. The Rise of GoodFATR: A Novel Accuracy Comparison Methodology for Indicator Extraction Tools
    Juan Caballero, Gibran Gomez, Srdjan Matic, Gustavo Sánchez, Silvia Sebastián, Arturo Villacañas.
    Future Generation Computer Systems 144, 74-89. Elsevier, julio 2023.
44. Flux: Liquid Types for Rust
    Nico Lehmann, Adam T. Geller, Niki Vazou, Ranjit Jhala.
    Proc. ACM Program. Lang. 7 (PLDI). Association for Computing Machinery, junio 2023.
45. Unsupervised Detection and Clustering of Malicious TLS Flows
    Gibran Gomez, Platon Kotzias, Matteo Dell'Amico, Leyla Bilge, Juan Caballero.
    Security and Communication Networks 2023. enero 2023.
46. Privacy and Integrity Threats in Contact Tracing Systems and Their Mitigations
    Gennaro Avitabile, Vincenzo Botta, Vincenzo Iovino, Ivan Visconti.
    IEEE Internet Computing 27 (2), 13–19. 2023.
47. 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.
48. Decentralized Stream Runtime Verification for Timed Asynchronous Networks
    Luis Miguel Danielsson, César Sánchez.
    IEEE Access 11, 84091–84112. 2023.
49. Runtime verification of real-time event streams using the tool HStriver
    Felipe Gorostiaga, César Sánchez.
    Formal Methods for Systems Design. 2023.
50. On Composing Finite Forests with Modal Logics
    Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti.
    ACM Transactions on Computational Logic. 2023.
51. Safe Couplings: Coupled Refinement Types
    Elizaveta Vasilenko, Niki Vazou, Gilles Barthe.
    Proceedings of the ACM on Programming Languages 6 (ICFP), 596–624. Association for Computing Machinery, agosto 2022.
52. 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.
    TPLP, 20th Anniversary Special Issue 22 (6), 776–858. Cambridge U. Press, mayo 2022.
53. Parallel Logic Programming: A Sequel
    Agostino Dovier, Andrea Formisano, Gopal Gupta, Manuel V. Hermenegildo, Enrico Pontelli, Ricardo Rocha.
    Theory and Practice of Logic Programming 22 (6), 905–973. Cambridge U. Press, marzo 2022.
54. Visibility Reasoning for Concurrent Snapshot Algorithms
    Joakim Öhman, Aleksandar Nanevski.
    Proceedings of the ACM on Programming Languages 6 (POPL), 1–30. Association for Computing Machinery, enero 2022.
55. 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.
56. 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.
57. 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.
58. 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.
59. Making Byzantine consensus live
    Manuel Bravo, Gregory Chockler, Alexey Gotsman.
    Distributed Computing 35 (6), 503–532. Springer, 2022.
60. 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.
61. 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.
62. Introduction to the 38th International Conference on Logic Programming Special Issue
    Yuliya Lierler, José F. Morales.
    Theory Pract. Log. Program. 22 (4), 499–504. 2022.
63. Introduction to the 38th International Conference on Logic Programming Special Issue II
    Yuliya Lierler, José F. Morales.
    Theory Pract. Log. Program. 22 (5), 640–640. 2022.
64. Replicomment: identifying clones in code comments
    Arianna Blasi, Nataliia Stulova, Alessandra Gorla, Oscar Nierstrasz.
    Journal of Systems and Software 182. diciembre 2021.
65. 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. noviembre 2021.
66. Complete Abstractions for Checking Language Inclusion
    Pierre Ganty, Francesco Ranzato, Pedro Valero.
    ACM Transactions on Computational Logic 22 (4). Association for Computing Machinery, septiembre 2021.
67. 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, septiembre 2021.
68. Contextual Modal Types for Algebraic Effects and Handlers
    Nikita Zyuzin, Aleksandar Nanevski.
    Proc. ACM Program. Lang. 5 (ICFP). Association for Computing Machinery, agosto 2021.
69. A Survey of Binary Code Similarity
    Irfan Ul Haq, Juan Caballero.
    ACM Computing Surveys 54 (3). abril 2021.
70. Incremental and Modular Context-sensitive Analysis
    I. Garcia-Contreras, J. F. Morales, M.V. Hermenegildo.
    TPLP 21 (2), 196–243. enero 2021.
71. 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.
    Theoretical Computer Science 895, 178-211. 2021.
72. A note on secure multiparty computation via higher residue symbols
    Ignacio Cascudo, Reto Schnyder.
    Journal of Mathematical Cryptology 15 (1), 284–297. 2021.
73. A pre-expectation calculus for probabilistic sensitivity
    Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.
    Proceedings of the ACM on Programming Languages 5 ({POPL}), 1–28. 2021.
74. 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.
75. On algebraic abstractions for concurrent separation logics
    Františsek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas.
    Proceedings of the ACM on Programming Languages 5 ({POPL}), 1–32. 2021.
76. 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.
77. 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.
78. Preface
    John P. Gallagher, Martin Sulzmann.
    Sci. Comput. Program. 202, 102577. 2021.
79. 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.
80. Refinement Types: A Tutorial
    Ranjit Jhala, Niki Vazou.
    Foundations and Trends® in Programming Languages 6 (3–4), 159-317. 2021.
81. A compiler for multi-key homomorphic signatures for Turing machines
    Somayeh Dolatnezhad Samarin, Dario Fiore, Daniele Venturi, Morteza Amini.
    Theoretical Computer Science 889, 145-170. 2021.
82. 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.
83. Multi-Shot Distributed Transaction Commit
    Gregory Chockler, Alexey Gotsman.
    Distributed Computing 34 (4), 301–318. Springer, 2021.
84. Specification and Space Complexity of Collaborative Text Editing
    Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, Marek Zawirski.
    Theoretical Computer Science 855, 141–160. Elsevier, 2021.
85. 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.
86. 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.
87. Weakest Preconditions in Fibrations
    Alejandro Aguirre, Shin-ya Katsumata.
    Electronic Notes in Theoretical Computer Science 352, 5–27. 2020.
88. Squares of matrix-product codes
    Ignacio Cascudo, Jaron Skovsted Gundersen, Diego Ruano.
    Finite Fields and Their Applications 62. 2020.
89. 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.
90. 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.
91. 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.
92. Privacy Profiles and Amplification by Subsampling
    Borja Balle, Gilles Barthe, Marco Gaboardi.
    Journal of Privacy and Confidentiality 10 (1). 2020.
93. 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.
    Proceedings of the ACM on Programming Languages 4 ({POPL}), 7:1–7:30. 2020.
94. A probabilistic separation logic
    Gilles Barthe, Justin Hsu, Kevin Liao.
    Proceedings of the ACM on Programming Languages 4 ({POPL}), 55:1–55:30. 2020.
95. Relational proofs for quantum programs
    Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou.
    Proceedings of the ACM on Programming Languages 4 ({POPL}), 21:1–21:29. 2020.
96. Liquidate your assets: reasoning about resource usage in liquid Haskell
    Martin A. T. Handley, Niki Vazou, Graham Hutton.
    Proceedings of the ACM on Programming Languages 4 ({POPL}), 24:1–24:27. 2020.
97. Preface, Special Issue on LOPSTR 2017
    Fabio Fioravanti, John P. Gallagher, Maurizio Proietti.
    Fundam. Inform. 173 (4). 2020.
98. 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.
99. 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.
100. Verifying replicated data types with typeclass refinements in Liquid Haskell
     Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou.
     Proceedings of the ACM on Programming Languages 4 (OOPSLA), 1–30. ACM New York, NY, USA, 2020.
101. 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.
102. Proving Highly-Concurrent Traversals Correct
     Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham.
     PACMPL 4 ({OOPSLA}), 128:1–128:29. 2020.
103. Gray-Box Monitoring of Hyperproperties with an Application to Privacy
     Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonarkdarpour.
     Formal Methods in Systems Desing, 1–36. 2020.
104. 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, diciembre 2019.
105. 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. noviembre 2019.
106. Specifying concurrent programs in separation logic: morphisms and simulations
     Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas.
     PACMPL 3 ({OOPSLA}), 1–30. ACM, octubre 2019.
107. 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, septiembre 2019.
108. 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. septiembre 2019.
109. Multi-key homomorphic authenticators
     Dario Fiore, Aikaterini Mitrokotsa, Luca Nizzardo, Elena Pagnin.
     IET Information Security 13 (6), 618–638. Institution of Engineering and Technology, abril 2019.
110. 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. abril 2019.
111. 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). marzo 2019.
112. A^2I: abstract^2 interpretation
     Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato.
     Proceedings of the ACM on Programming Languages 3 ({POPL}), 1–31. ACM, enero 2019.
113. 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, enero 2019.
114. When Are Prime Formulae Characteristic?
     Luca Aceto, Dario Della Monica, Ignacio Fábregas, Anna Ingólfsdóttir.
     Theor. Comput. Sci. 777, 3–31. 2019.
115. Logical characterisations, rule formats and compositionality for input-output conformance simulation
     Luca Aceto, Ignacio Fábregas, Carlos Gregorio-Rodríguez, Anna Ingólfsdóttir.
     J. Log. Algebr. Meth. Program. 106, 78–106. 2019.
116. 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.
117. 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.
118. 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.
119. 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.
120. 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.
121. Relational ⋆-Liftings for differential privacy
     Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub.
     Logical Methods in Computer Science 15 (4). 2019.
122. LWeb: information flow security for multi-tier web applications
     James Parker, Niki Vazou, Michael Hicks.
     Proceedings of the ACM on Programming Languages 3 ({POPL}), 1–30. 2019.
123. 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.
     Proceedings of the ACM on Programming Languages 3 ({POPL}), 38:1–38:30. 2019.
124. 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.
125. 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.
126. doppioDB 1.0: Machine Learning inside a Relational Engine
     Gustavo Alonso, Zsolt Istvan, Kaan Kara, Muhsen Owaida, David Sidler.
     IEEE Data Engineering 42 (2), 19–31. 2019.
127. The Glass Half Full: Using Programmable Hardware Accelerators in Analytics
     Zsolt István.
     IEEE Data Eng. Bull. 42 (1), 49–60. 2019.
128. I Can't Believe It's Not (Only) Software! Bionic Distributed Storage for Parquet Files
     Lucas Kuhring, Zsolt István.
     Proc. VLDB Endow. 12 (12), 1838–1841. VLDB Endowment, 2019.
129. 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 (JMVLSC), SOCO'15 Special Issue 32 (3-4), 313–341. Old City Publishing, 2019.
130. Code obfuscation against abstraction refinement attacks
     Roberto Bruni, Roberto Giacobazzi, Roberta Gori.
     Formal Aspects of Computing 30 (6), 685–711. noviembre 2018.
131. 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. octubre 2018.
132. Malware Lineage in the Wild
     Irfan Ul Haq, Sergio Chica, Juan Caballero, Somesh Jha.
     Computers & Security 78, 347–363. Elsevier, agosto 2018.
133. Active Pages 20 Years Later: Active Storage for the Cloud
     Zsolt István, David Sidler, Gustavo Alonso.
     IEEE Internet Computing 22 (4), 6–14. julio 2018.
134. A Logical Analysis of Framing for Specifications with Pure Method Calls
     Anindya Banerjee, David A. Naumann, Mohammad Nikouei.
     ACM Trans. Program. Lang. Syst. 40 (2), 1–90. ACM, mayo 2018.
135. 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, abril 2018.
136. 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. marzo 2018.
137. 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, marzo 2018.
138. Analysing snapshot isolation
     Andrea Cerone, Alexey Gotsman.
     Journal of the ACM 65 (2), 1-41. ACM Press, marzo 2018.
139. 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. febrero 2018.
140. Abstract Non-Interference: A Unifying Framework for Weakening Information-flow
     Roberto Giacobazzi, Isabella Mastroeni.
     ACM Trans. Priv. Secur. 21 (2), 1–31. ACM, febrero 2018.
141. Decidability of conversion for type theory in type theory
     Andreas Abel, Joakim Öhman, Andrea Vezzosi.
     Proceedings of the ACM on Programming Languages (PACMPL) 2 ({POPL}), 1–29. ACM, enero 2018.
142. 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, enero 2018.
143. Proving expected sensitivity of probabilistic programs
     Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
     Proceedings of the ACM on Programming Languages 2 ({POPL}), 1–29. 2018.
144. Monadic refinements for relational cost analysis
     Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
     Proceedings of the ACM on Programming Languages 2 (POPL), 1–32. 2018.
145. Gradual liquid type inference
     Niki Vazou, Éric Tanter, David Van Horn.
     Proceedings of the ACM on Programming Languages 2 ({OOPSLA}), 1–25. 2018.
146. 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.
147. Practical Homomorphic Message Authenticators for Arithmetic Circuits
     Dario Catalano, Dario Fiore.
     Journal of Cryptology 31 (1), 23–59. Springer, 2018.
148. Introduction to the special issue on runtime verification
     Yliès Falcone, César Sánchez.
     Formal Methods in Systems Design 53 (1), 1–5. 2018.
149. 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.
150. 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.
151. 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, diciembre 2017.
152. 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, agosto 2017.
153. 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. agosto 2017.
154. A Certificateless Approach to Onion Routing
     Dario Catalano, Dario Fiore, Rosario Gennaro.
     International Journal of Intelligent Systems 16 (3), 327–343. Springer, junio 2017.
155. 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.
156. 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.
157. 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.
158. Constraint specialisation in Horn clause verification
     Bishoksan Kafle, John P. Gallagher.
     Science of Computer Programming 137, 125–140. 2017.
159. 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.
160. 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.
161. 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.
162. 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 47, Part B, 278–286. Elsevier, noviembre 2016.
163. 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, octubre 2016.
164. 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, septiembre 2016.
165. 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, septiembre 2016.
166. Semantic Code Browsing
     I. Garcia-Contreras, J. F. Morales, M.V. Hermenegildo.
     TPLP (ICLP'16 Special Issue) 16 (5-6), 721–737. CUP, septiembre 2016.
167. 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, julio 2016.
168. Making abstract models complete
     Roberto Giacobazzi, Isabella Mastroeni.
     Mathematical Structures in Computer Science 26 (4), 658–701. Cambridge University Press, mayo 2016.
169. Type Inference on Executables
     Juan Caballero, Zhiqiang Lin.
     ACM Computing Surveys 48 (4), 1–35. ACM, mayo 2016.
170. Parameterized Verification of Asynchronous Shared-Memory Systems
     Javier Esparza, Pierre Ganty, Rupak Majumdar.
     Journal of the ACM 63 (1), 1–48. ACM, marzo 2016.
171. Building Resource Adaptive Software Systems (BRASS): Objectives and System Evaluation
     J. Hughes, C. Sparks, A. Stoughton, R. Parikh, A. Reuther, S. Jagannathan.
     SIGSOFT Softw. Eng. Notes 41 (1), 1–2. ACM, enero 2016.
172. 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, enero 2016.
173. No solvable lambda-value term left behind
     Á. García-Pérez, P. Nogueira.
     Logical Methods in Computer Science 12 (2), 1-43. 2016.
174. 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.
175. 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.
176. Using higher-order contracts to model session types
     Giovanni Bernardi, Matthew Hennessy.
     Logical Methods in Computer Science 12 (2). 2016.
177. Programming language techniques for differential privacy
     Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce.
     ACM SIGLOG News 3 (1), 34–53. 2016.
178. Model checking parameterized asynchronous shared-memory systems
     Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
     Formal Methods in System Design, 1–28. 2016.
179. Verification of population protocols
     Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
     Acta Informatica, 1–25. 2016.
180. Maximal incompleteness as obfuscation potency
     Roberto Giacobazzi, Isabella Mastroeni, Mila Dalla Preda.
     Formal Aspects of Computing. 2016.
181. 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.
182. 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.
183. Weakening Additivity in Adjoining Closures
     Isabella Mastroeni, Roberto Giacobazzi.
     Order 33 (3), 503–516. 2016.
184. 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.
185. Foundations of Boolean Stream Runtime Verification
     Laura Bozzelli, César Sánchez.
     Theoretical Computer Science 631, 118–138. 2016.
186. 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.
187. 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.
188. Practical Run-time Checking via Unobtrusive Property Caching
     N. Stulova, J.F. Morales, M.V. Hermenegildo.
     TPLP 15 (04-05), 726-741. CUP, septiembre 2015.
189. 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 (TISSEC) 18 (1), 1–32. ACM, junio 2015.
190. On the Use of GPU for Accelerating Communication-Aware Mapping Techniques
     Guillermo Vigueras, Juan M. Orduña.
     The Computer Journal. mayo 2015.
191. Mutually Testing Processes
     Giovanni Bernardi, Matthew Hennessy.
     Logical Methods in Computer Science 11 (2). abril 2015.
192. Quantifying information flow in cryptographic systems
     Michael Backes, Boris Köpf.
     Mathematical Structures in Computer Science 25 (2), 457–479. febrero 2015.
193. 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, febrero 2015.
194. Comparing and Combining Predictive Business Process Monitoring Techniques
     Andreas Metzger, Philip Leitner, Dragan Ivanovic, Eric Schmieders, Roslin Franklin, Manuel Carro, Schahram Dustdar, Klaus Pohl.
     System, Man, and Cybernetics: Systems, IEEE Transactions on 45 (2), 276-290. febrero 2015.
195. Modelling MAC-Layer Communications in Wireless Systems
     Andrea Cerone, Matthew Hennessy, Massimo Merro.
     Logical Methods in Computer Science 11 (1). 2015.
196. Automatic Workarounds: Exploiting the Intrinsic Redundancy of Web Applications
     Antonio Carzaniga, Alessandra Gorla, Nicolò Perino, Mauro Pezzè.
     ACM Transactions on Software Engineering and Methodologies 24 (3), 1–42. 2015.
197. AVERIST: An Algorithmic Verifier for Stability
     Pavithra Prabhakar, Miriam Garcia Soto.
     Electronic Notes in Theoretical Computer Science 317, 133–139. 2015.
198. 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.
199. High-Assurance Cryptography: Cryptographic Software We can Trust
     Gilles Barthe.
     IEEE Security and Privacy Magazine 13 (5), 86–89. 2015.
200. SEFM: Software Engineering and Formal Methods
     Gilles Barthe, Alberto Pardo, Gerardo Schneider.
     Software and Systems Modeling 14 (1), 3–4. 2015.
201. 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.
202. 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.
203. Unveiling metamorphism by abstract interpretation of code properties
     Mila Dalla Preda, Roberto Giacobazzi, Saumya K. Debray.
     Theor. Comput. Sci. 577, 74–97. 2015.
204. 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.
205. Parametrized Invariance for Infinite State Processes
     Alejandro Sánchez, César Sánchez.
     Acta Informatica 52 (6), 525–557. 2015.
206. Stochastic vs. Deterministic Evolutionary Algorithm-based Allocation and Scheduling for XMOS Chips
     Z. Banković, P. Lopez-Garcia.
     Neurocomputing 150, 82–89. Elsevier, 2015.
207. 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.
208. Mtac: A Monad for Typed Tactic Programming in Coq
     Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
     Journal of Functional Programming (JFP) 25. 2015.
209. 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, marzo 2014.
210. 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 Trans. Software Eng. 40 (4), 324–337. 2014.
211. On Automation in the Verification of Software Barriers: Experience Report
     Alexander Malkis, Anindya Banerjee.
     Journal of Automated Reasoning 52 (3), 275–329. 2014.
212. 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.
213. Analysis and Transformation Tools for Constrained Horn Clause Verification
     John P. Gallagher, Bishoksan Kafle.
     Theory and Practice of Logic Programming 14 (4-5 (supplementary materials)), 90–101. Cambridge University Press, 2014.
214. 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.
215. Pushdown flow analysis with abstract garbage collection
     J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn.
     J. Funct. Program. 24 (2-3), 218–283. 2014.
216. Visibly Rational Expressions
     Laura Bozzelli, César Sánchez.
     Acta Informatica 51 (1), 25–49. 2014.
217. 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.
218. 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.
219. 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 (JCS) 22 (5), 823–866. IOS Press, 2014.
220. Bounded phase analysis of message-passing programs
     Ahmed Bouajjani, Michael Emmi.
     International Journal on Software Tools for Technology Transfer 16 (2), 127–146. 2014.
221. Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types
     A. Serrano, P. Lopez-Garcia, M.V. Hermenegildo.
     ICLP. 2014.
222. 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 and Applications 28 (1). 2014.
223. 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.
224. 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, octubre 2013.
225. Linearizability with ownership transfer
     Alexey Gotsman, Hongseok Yang.
     Logical Methods in Computer Science 9 (3). septiembre 2013.
226. 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) 13 (4-5), 1-14. Cambridge U. Press, agosto 2013.
227. How to make ad hoc proof automation less ad hoc
     Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
     Journal of Functional Programming (JFP) 23 (4), 357–401. julio 2013.
228. Modular verification of preemptive OS kernels
     Alexey Gotsman, Hongseok Yang.
     Journal of Functional Programming 23 (4), 452–514. Cambridge University Press, julio 2013.
229. A Scalable Multiagent System Architecture for Interactive Applications
     Guillermo Vigueras, Juan M. Orduña, Miguel Lozano, Yvon Jégou.
     Sci. Comput. Program. 78 (6), 715–724. Elsevier North-Holland, Inc., junio 2013.
230. A Sharing-Based Approach to Supporting Adaptation in Service Compositions
     D. Ivanovic, M. Carro, M.V. Hermenegildo.
     Computing 95 (6), 453-492. Springer Wien, junio 2013.
231. Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
     Murdoch J. Gabbay, Aleksandar Nanevski.
     Journal of Applied Logic (JAPPL) 11 (1), 1–29. marzo 2013.
232. Automatic Protocol Reverse-Engineering: Message Format Extraction and Field Semantics
     Juan Caballero, Dawn Song.
     Computer Networks 57 (2), 451-474. Elsevier, febrero 2013.
233. Local Reasoning for Global Invariants, Part II: Dynamic Boundaries
     Anindya Banerjee, David A. Naumann.
     Journal of the ACM 60 (3), 1–73. ACM, 2013.
234. 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.
235. 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.
236. Dependent Type Theory for Verification of Information Flow and Access Control Policies
     Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
     ACM Trans. Program. Lang. Syst. 35 (2), 1–41. ACM, 2013.
237. A Model-Driven Approach to Teaching Concurrency
     M. Carro, Ángel Herranz, Julio Mariño.
     ACM Transactions on Computing Education 13 (1). 2013.
238. Analysis of Recursively Parallel Programs
     Ahmed Bouajjani, Michael Emmi.
     ACM Transactions on Programming Languages and Systems 35 (3), 1–49. 2013.
239. 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.
240. Fusing Statecharts and Java
     Maria-Cristina Marinescu, César Sánchez.
     ACM Transactions on Embedded Computing Systems 12, 1–21. 2013.
241. 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.
242. A Read-Copy Update based parallel server for distributed crowd simulations
     Guillermo Vigueras, Juan M. Orduña, Miguel Lozano.
     The Journal of Supercomputing 64 (1), 156–166. Springer US, 2013.
243. 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. agosto 2012.
244. Understanding the Role of Malware in Cybercrime
     Juan Caballero.
     ERCIM News 2012 (90), 15-16. julio 2012.
245. Certificate Size Reduction in Abstraction-Carrying Code
     E. Albert, P. Arenas, G. Puebla, M.V. Hermenegildo.
     Theory and Practice of Logic Programming 12 (3), 283–318. 2012.
246. 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.
247. Algorithmic verification of asynchronous programs
     Pierre Ganty, Rupak Majumdar.
     ACM Transactions on Programming Languages and Systems 34 (1), 1–48. ACM, 2012.
248. Bounded Underapproximations
     Pierre Ganty, Rupak Majumdar, Benjamin Monmege.
     Formal Methods in System Design 40 (2), 206-231. 2012.
249. 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.
     TPLP 12 (1–2), 219–252. Cambridge Univ Press, 2012.
250. Quantitative Security Analysis (Dagstuhl Seminar 12481)
     Boris Köpf, Pasquale Malacaria, Catuscia Palamidessi.
     Dagstuhl Reports 2 (11), 135-154. 2012.
251. 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.
252. 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.
253. Modelling Declassification Policies using Abstract Domain Completeness
     Isabella Mastroeni, Anindya Banerjee.
     Mathematical Structures in Computer Science 21 (6), 1253-1299. diciembre 2011.
254. 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, octubre 2011.
255. An Abstract Model of Certificate Translation
     Gilles Barthe, César Kunz.
     ACM Trans. Program. Lang. Syst. 33 (4), 1–13. ACM, julio 2011.
256. Parallel Backtracking with Answer Memoing for Independent And-Parallelism
     P. Chico de Guzmán, A. Casas, M. Carro, M.V. Hermenegildo.
     TPLP. Cambridge U. Press, julio 2011.
257. 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, enero 2011.
258. Parikh's Theorem: A simple and direct automaton construction
     Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger.
     Information Processing Letters 111, 614-619. 2011.
259. Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks
     Boris Köpf, David Basin.
     Journal of Computer Security 1, 1–31. 2011.
260. Security of Multithreaded Programs by Compilation
     Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld.
     ACM Transactions on Information and System Security 13 (3). 2010.
261. 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.
262. 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 28 (2), 117–206. 2010.
263. Fixed Point Guided Abstraction Refinement for Alternating Automata
     Pierre Ganty, Nicolas Maquet, Jean-François Raskin.
     Theor. Comput. Sci. 411 (38-39), 3444-3459. 2010.
264. 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.
265. 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, octubre 2009.
266. 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, julio 2009.
267. Certificate Translation for Optimizing Compilers
     Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk.
     ACM Trans. Program. Lang. Syst. 31 (5). ACM, julio 2009.
268. User-Definable Resource Usage Bounds Analysis for Java Bytecode
     J. Navas, M. Méndez-Lojo, M.V. Hermenegildo.
     ENTCS - BYTECODE'09 253 (5). Elsevier, marzo 2009.
269. 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 (JOT, http://www.jot.fm/general/about/) 8 (2), 137-161. marzo 2009.
270. Implementing Constructive Intensional Negation
     Julio Mariño, Juan José Moreno-Navarro, Susana Muñoz Hernández.
     New Generation Computing 27 (1), 25-56. enero 2009.
271. Automated Analysis of Security-Design Models
     D. Basin, M. Clavel, J. Doser, M. Egea.
     Information & Software Technology 51 (5), 815-831. 2009.
272. Abstraction-Carrying Code: A Model for Mobile Code Safety
     E. Albert, G. Puebla, M.V. Hermenegildo.
     New Generation Computing 26 (2). 2008.

Artículos en Congresos con Revisión Estricta (756)

1. Towards Relating Ciao Assertions and LPTP Theorems
   Marco Pérez, Pedro Lopez-Garcia, Jose F. Morales, Manuel V. Hermenegildo, Fred Mesnard.
   Technical Communications of the 42nd International Conference on Logic Programming (ICLP 2026). julio 2026.
2. An Approach to the Abstract Interpretation of Goal-Directed Answer Set Programming
   Daniel Jurjo, Joaquín Arias, Gopal Gupta, Jose F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo.
   Technical Communications of the 42nd International Conference on Logic Programming (ICLP 2026). julio 2026.
3. StreamCFI: Streamed Per-Input Control-Flow Integrity
   Konstantinos Kleftogiorgos, Cristiano Giuffrida, Georgios Portokalidis.
   Proceedings of the IEEE European Symposium on Security and Privacy. julio 2026.
4. New QUBO Transformations to Improve Quantum and Simulated Annealing Performance for Quadratic Knapsack
   Nicolás Borrajo, Juan Marcos Ramirez, Farzam Nosrati, José Aguilar, Vincenzo Mancuso, Antonio Fernández Anta.
   International Conference on Agents and Artificial Intelligence (ICAART). 2026.
5. Exploiting Multi-Core Parallelism in Blockchain Validation and Construction
   Arivarasan Karmegam, Lucianna Kiffer, Antonio Fernández Anta.
   International Symposium on Experimental Algorithms (SEA). 2026.
6. Multi-Configurable Search Rules in Prolog and Application to Testing
   Daniela Ferreiro, José F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo.
   28th International Symposium on Practical Aspects of Declarative Languages, PADL 2026. 2026.
7. Family Ties: A Close Look at the Influence of Static Features on the Precision of Malware Family Clustering
   Antonino Vitale, Kevin van Liebergen, Juan Caballero, Savino Dambra, Platon Kotzias, Simone Aonzo, Davide Balzarotti.
   APWG Symposium on Electronic Crime Research (eCrime). noviembre 2025.
8. Differential Testing of Bundle Protocol v7 Implementations: A Preliminary Report
   Stephan Havermans, Lars Baumgaertner, Marcus Wallum, Juan Caballero.
   Security for Space Systems Conference. noviembre 2025.
9. Extending the FSyntax/Hiord Approach with Imperative Notation
   Paula Corral, José F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo.
   International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). septiembre 2025.
10. The Polymorphism Maze: Understanding Diversities and Similarities in Malware Families
    Antonino Vitale, Simone Aonzo, Savino Dambra, Nanda Rani, Lorenzo Ippolito, Platon Kotzias, Juan Caballero, Davide Balzarotti.
    European Symposium On Research In Computer Security (ESORICS). septiembre 2025.
11. Your Signal, Their Data: An Empirical Privacy Analysis of Wireless-scanning SDKs in Android
    Aniketh Girish, Joel Reardon, Juan Tapiador, Srdjan Matic, Narseo Vallina-Rodriguez.
    Privacy Enhancing Technologies Symposium (PETS). julio 2025.
12. Tracking Without Borders: Studying the Role of WebViews in Bridging Mobile and Web Tracking
    Nipuna Weerasekara, José Miguel Moreno, Srdjan Matic, Joel Reardon, Juan Tapiador, Narseo Vallina-Rodríguez.
    Privacy Enhancing Technologies Symposium (PETS). julio 2025.
13. Ctrl+Alt+Deceive: Quantifying User Exposure to Online Scams
    Platon Kotzias, Michalis Pachilakis, Javier Aldana Iuit, Juan Caballero, Iskander Sanchez-Rola, Leyla Bilge.
    Network and Distributed System Security Symposium (NDSS). febrero 2025.
14. All your (data)base are belong to us: Characterizing Database Ransom(ware) Attacks
    Kevin van Liebergen, Gibran Gomez, Srdjan Matic, Juan Caballero.
    Network and Distributed System Security Symposium (NDSS). febrero 2025.
15. OBRA: Oracle-Based, Relational, Algorithmic Type Verification
    Elizaveta Vasilenko, Niki Vazou, Gilles Barthe.
    Programming Languages and Systems. 2025.
16. Search-based Inference of Class Invariants
    Juan Manuel Copia, Facundo Molina, Alessandra Gorla, Nazareno Aguirre, Pablo Ponzio.
    Proceedings of the Genetic and Evolutionary Computation Conference Companion. 2025.
17. Lessons Learned from Five Years of Artifact Evaluations at EuroSys
    Daniele Cono D'Elia, Thaleia Dimitra Doudali, Cristiano Giuffrida, Miguel Matos, Mathias Payer, Solal Pirelli, Georgios Portokalidis, Valerio Schiavoni, Salvatore Signorello, Anjo Vahldiek-Oberwagner.
    Proceedings of the 3rd ACM Conference on Reproducibility and Replicability. 2025.
18. Towards Efficient Allocation of Tasks in Dag-Based Workflows Across Federated Fog Systems
    Gayani Gupta, Amisha Gupta, Mohsen Amini Salehi, Antonio Fernández Anta, Sanjukta Bhowmick, Jose Aguilar, Mathieu Kourouma.
    2025 IEEE Cloud Summit. 2025.
19. Homomorphic WiSARDs: Efficient Weightless Neural Network Training over Encrypted Data
    Leonardo Neumann, Antonio Guimarães, Diego F. Aranha, Edson Borin.
    Applied Cryptography and Network Security. 2025.
20. Tight conditions for binary-output tasks under crashes
    Timothé Albouy, Antonio Fernández Anta, Chryssis Georgiou, Nicolas Nicolaou, Junlang Wang.
    Proc. 29th Int’l Conference on Principles of Distributed Systems (OPODIS'25). 2025.
21. Contention-aware cooperation
    Timothé Albouy, Davide Frey, Mathieu Gestin, Michel Raynal, François Taïani.
    Proc. 29th Int’l Conference on Principles of Distributed Systems (OPODIS'25). 2025.
22. Atomic Transfer Graphs: Secure-by-design Protocols for Heterogeneous Blockchain Ecosystems
    S. Duebler, F. Badaloni, P. Moreno-Sanchez, C. Schneidewind.
    Computer Security Foundations Symposium. 2025.
23. BitMLx: Secure Cross-chain Smart Contracts For Bitcoin-style Cryptocurrencies
    F. Badaloni S. Holler, C. Oikonomou, P. Moreno-Sanchez, C. Schneidewind.
    Computer Security Foundations Symposium. 2025.
24. Verifiable Computation for Approximate Homomorphic Encryption Schemes
    Ignacio Cascudo, Anamaria Costache, Daniele Cozzo, Dario Fiore, Antonio Guimarães, Eduardo Soria-Vazquez.
    Advances in Cryptology (CRYPTO). 2025.
25. Fairness Shields: Safeguarding against Biased Decision Makers
    Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, Kaushik Mallik.
    National Conference of the American Association for Artificial Intelligence (AAAI). 2025.
26. Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants)
    Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang.
    Architectural Support for Programming Languages and Operating Systems (ASPLOS). 2025.
27. Efficient Dynamic Shielding for Parametric Safety Specifications
    Davide Corsi, Kaushik Mallik, Andoni Rodríguez, César Sánchez.
    International Symposium on Automated Technology for Verification and Analysis (ATVA). 2025.
28. Supermartingale Certificates for Quantitative Omega-Regular Verification and Control
    Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, Dorde Zikelic.
    Computer Aided Verification (CAV). 2025.
29. D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
    Yingte Xu, Li Zhou, Gilles Barthe.
    Computer Aided Verification (CAV). 2025.
30. The Power of On-line Indirect Surveys to Monitor Society
    Antonio Fernández Anta, Nicolas Nicolaou, Efstathios Stavrakis.
    IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). 2025.
31. New QUBO Transformations to Improve Quantum and Simulated Annealing Performance for Quadratic Knapsack
    Nicolás Borrajo, Juan Marcos Ramirez, Farzam Nosrati, José Aguilar, Vincenzo Mancuso, Antonio Fernández Anta.
    Genetic and Evolutionary Computations (GECCO). 2025.
32. Bidding Games on Markov Decision Processes with Quantitative Reachability Objectives
    Guy Avni, Martin Kurecka, Kaushik Mallik, Petr Novotný, Suman Sadhukhan.
    AAMAS. 2025.
33. Monitoring Robustness and Individual Fairness
    Ashutosh Gupta, Thomas A. Henzinger, Konstantin Kueffner, Kaushik Mallik, David Pape.
    ACM International Conference on Knowledge Discovery and Data Mining (KDD). 2025.
34. Error Bounds for the Network Scale-Up Method
    Sergio Díaz-Aranda, Juan Marcos Ramirez, Mohit Daga, Jaya Prakash Champati, Jose Aguilar, Rosa E. Lillo, Antonio Fernández Anta.
    ACM International Conference on Knowledge Discovery and Data Mining (KDD). 2025.
35. Predictive Monitoring of Black-Box Dynamical Systems
    Thomas A. Henzinger, Fabian Kresse, Kaushik Mallik, Emily Yu, Djordje Zikelic.
    L4DC. 2025.
36. Complete Quantum Relational Hoare Logics from Optimal Transport Duality
    Gilles Barthe, Minbo Gao, Theo Wang, Li Zhou.
    IEEE Symposium on Logic in Computer Science (LICS). 2025.
37. Interpretable Outlier and Anomaly Detection for Mobile Networks from Small Tabular Data
    Juan Marcos Ramirez, Pablo J. Rojo Maroni, Vincenzo Mancuso, Antonio Fernández Anta.
    IFIP International Conference on Networking (Networking). 2025.
38. On Graphs of Incremental Proofs of Sequential Work
    Hamza Abusalah.
    International Conference on Practice and Theory in Public Key Cryptography (PKC). 2025.
39. Auditing without Leaks Despite Curiosity
    Hagit Attiya, Antonio Fernández Anta, Alessia Milani, Alexandre Rapetti, Corentin Travers.
    ACM Symposium on Principles of Distributed Computing (PODC). 2025.
40. Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt
    José Bacelar Almeida, Gustavo Xavier Delerue Marinho Alves, Manuel Barbosa, Gilles Barthe, Luís Esquível, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub.
    IEEE Symposium on Security and Privacy (SP). 2025.
41. Invited Paper: Setchain Algorithms for Blockchain Scalability
    Arivarasan Karmegam, Gabina Luz Bianchi, Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, César Sánchez.
    Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS). 2025.
42. Tetris! Traceable Extendable Threshold Ring Signatures and More
    Gennaro Avitabile, Vincenzo Botta, Dario Fiore.
    European Symposium On Research In Computer Security (ESORICS). 2025.
43. Verification-efficient Homomorphic Signatures for Verifiable Computation over Data Streams
    Gaspard Anthoine, Daniele Cozzo, Dario Fiore.
    Financial Cryptography and Data Security 2025. 2025.
44. AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures
    Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, Gururaj Saileshwar.
    Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. 2025.
45. Algebraic Zero Knowledge Contingent Payment
    J. Gomez-Martinez, D. Vasilopoulos, P. Moreno-Sanchez, D. Fiore.
    International Conference on Applied Cryptography and Network Security (ACNS). 2025.
46. The Cost of Skeletal Call-By-Need, Smoothly
    B. Accattoli, F. Magliocca, L. Peyrot, C. Sacerdoti Coen.
    10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). 2025.
47. How Big Is the Automaton? Certified Lower Bounds on the Size of Presburger DFAs
    Nicolas Amat, Pierre Ganty, Alessio Mansutti.
    International Conference on Automated Software Engineering (ASE). 2025.
48. Mode-Based Reactive Synthesis
    Matías Brizzio, Felipe Gorostiaga, César Sánchez, Renzo Degiovanni.
    Proc. of the 17th Int’l Symp. on NASA Formal Methods (NFM'25). 2025.
49. Polymorphic Records for Dynamic Languages
    G. Castagna, L. Peyrot.
    Proceedings of the ACM on Programming Languages, Volume 9, Issue OOPSLA1. 2025.
50. Making democracy work: Fixing and simplifying Egalitarian Paxos
    Fedor Ryabinin, Alexey Gotsman, Pierre Sutra.
    International Conference on Principles of Distributed Systems (OPODIS). 2025.
51. Brief Announcement: Revisiting Lower Bounds for Two-Step Consensus
    Fedor Ryabinin, Alexey Gotsman, Pierre Sutra.
    Symposium on Principles of Distributed Computing (PODC). 2025.
52. MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
    Felipe Gorostiaga, Martín Ceresa, César Sánchez.
    Proc. of the 27th 27th Int’l Symp. on Practical Aspects of Declarative Languages (PADL'25). 2025.
53. Tight Bounds on Channel Reliability via Generalized Quorum Systems
    Alejandro Naser-Pastoriza, Gregory V. Chockler, Alexey Gotsman, Fedor Ryabinin.
    Symposium on Principles of Distributed Computing (PODC). 2025.
54. Realizable Continuous-Space Shields for Safe Reinforcement Learning
    Kyungmin Kim, Davide Corsi, Andoni Rodríguez, JB Lanier, Benjami Parellada, Pierre Baldi, César Sánchez, Roy Fox.
    Proc. of 7th Annual Learning for Dynamics Control Conference (L4DC'25). 2025.
55. Lite-PoT: Practical Powers-of-Tau Setup Ceremony
    L. NG, P. Moreno-Sanchez, M. Minaei, P. Chatzigiannis, A. Bhat, D. Le.
    ACM Conference on Computer and Communications Security (CCS). 2025.
56. Counter Example Guided Reactive Synthesis for LTL Modulo Theories
    Andoni Rodríguez, Felipe Gorostiaga, César Sánchez.
    Proc. of the 37th Int’l Conf. on Computer Aided Verification (CAV'25), Part IV. 2025.
57. Explanations for Unrealizability of Infinite-State Safety Shields
    Andoni Rodríguez, Irfansha Shaik, Davide Corsi, Roy Fox, César Sánchez.
    Proc. of the 22nd Int’l Conf. on Principles of Knowledge Representation and Reasoning, KR in Planning and Scheduling (KR'25). 2025.
58. Shield Synthesis for LTL Modulo Theories
    Andoni Rodríguez, Guy Amir, Davide Corsi, César Sánchez, Guy Katz.
    Proc. of the 39th AAAI Conf. on Artificial Intelligence (AAAI'25). 2025.
59. A Secure Sequencer and Data Availability Committee for Rollups
    M. Capretto, M. Ceresa, A. Fernadez Anta, P. Moreno-Sanchez, C. Sanchez.
    ACM Conference on Computer and Communications Security (CCS). 2025.
60. TEE Is Not a Healer: Rollback-Resistant Reliable Storage
    Sadegh Keshavarzi, Gregory V. Chockler, Alexey Gotsman.
    Symposium on Distributed Computing (DISC). 2025.
61. Temporal Hyperproperties for Population Protocols
    Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty, César Sánchez.
    Foundations of Software Science and Computational Structures (FOSSACS). 2025.
62. Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors
    Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, Marco Guarnieri.
    Proceedings of the 32nd ACM Conference on Computer and Communications Security. 2025.
63. SIDECAR: Leveraging Debugging Extensions in Commodity Processors to Secure Software
    Konstantinos Kleftogiorgos, Patrick Zielinski, Shan Huang, Jun Xu, Georgios Portokalidis.
    Proceedings of the Annual Computer Security Applications Conference (ACSAC). diciembre 2024.
64. Verifiable Secret Sharing from Symmetric Key Cryptography with Improved Optimistic Complexity
    Ignacio Cascudo, Daniele Cozzo, Emanuele Giunta.
    International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt). 2024.
65. HELIOPOLIS: Verifiable Computation over Homomorphically Encrypted Data from Interactive Oracle Proofs is Practical
    Diego F. Aranha, Anamaria Costache, Antonio Guimarães, Eduardo Soria-Vazquez.
    Advances in Cryptology – ASIACRYPT 2024. 2024.
66. Optimizing Virtual Payment Channel Establishment in the Face of On-Path Adversaries
    Lukas Aumayr, Esra Ceylan, Yannik Kopyciok, Matteo Maffei, Pedro Moreno-Sanchez, Iosif Salem, Stefan Schmid.
    IFIP Networking Conference. 2024.
67. Fully-Succinct Multi-key Homomorphic Signatures from Standard Assumptions
    Gaspard Anthoine, David Balbás, Dario Fiore.
    Advances in Cryptology (CRYPTO). 2024.
68. Limits of Black-Box Anamorphic Encryption
    Dario Catalano, Emanuele Giunta, Francesco Migliaro.
    Annual International Cryptology Conference. 2024.
69. Real-world Universal zkSNARKs are non-malleable
    Antonio Faonio, Dario Fiore, Luigi Russo.
    ACM Conference on Computer and Communications Security (CCS). 2024.
70. Signature-Based Witness Encryption with Compact Ciphertext
    Gennaro Avitabile, Nico Döttling, Bernardo Magri, Christos Sakkas, Stella Wohnig.
    International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). 2024.
71. Verification of Population Protocols with Unordered Data
    Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, Chana Weil-Kennedy.
    International Colloquium on Automata Languages and Programming (ICALP). 2024.
72. Improving Patch Correctness Analysis via Random Testing and Large Language Models
    Facundo Molina, Juan Manuel Copia, Alessandra Gorla.
    International Conference on Software Testing, Verification and Validation (ICST). 2024.
73. FixCheck: A Tool for Improving Patch Correctness Analysis
    Facundo Molina, Juan Manuel Copia, Alessandra Gorla.
    International Symposium on Software Testing and Analysis (ISSTA). 2024.
74. Black-Box Timed Commitments from Time-Lock Puzzles
    Hamza Abusalah, Gennaro Avitabile.
    Theory of Cryptography Conference (TCC). 2024.
75. Publicly Verifiable Secret Sharing Over Class Groups and Applications to DKG and YOSO
    Ignacio Cascudo, Bernardo David.
    International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt). 2024.
76. Anamorphic encryption: New constructions and homomorphic realizations
    Dario Catalano, Emanuele Giunta, Francesco Migliaro.
    Annual International Conference on the Theory and Applications of Cryptographic Techniques. 2024.
77. Unbiasable Verifiable Random Functions
    Emanuele Giunta, Alistair Stewart.
    Annual International Conference on the Theory and Applications of Cryptographic Techniques. 2024.
78. On Sigma-Protocols and (Packed) Black-Box Secret Sharing Schemes
    Claudia Bartoli, Ignacio Cascudo.
    International Conference on Practice and Theory in Public Key Cryptography (PKC). 2024.
79. Lookup Arguments: Improvements, Extensions and Applications to Zero-Knowledge Decision Trees
    Matteo Campanelli, Antonio Faonio, Dario Fiore, Tianyu Li, Helger Lipmaa.
    International Conference on Practice and Theory in Public Key Cryptography (PKC). 2024.
80. Witness Encryption for Succinct Functional Commitments and Applications
    Matteo Campanelli, Dario Fiore, Hamidreza Khoshakhlagh.
    International Conference on Practice and Theory in Public Key Cryptography (PKC). 2024.
81. Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023
    Nicolas Amat, Elvio Amparore, Bernard Berthomieu, Pierre Bouvier, Silvano Dal Zilio, Francis Hulin-Hubard, Peter G. Jensen, Loig Jezequel, Fabrice Kordon, Shuo Li, Emmanuel Paviot-Adet, Laure Petrucci, Jiří Srba, Yann Thierry-Mieg, Karsten Wolf.
    TOOLympics Challenge 2023. 2024.
82. Testing side-channel security of cryptographic implementations against future microarchitectures
    Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom.
    Proceedings of the 31st ACM Conference on Computer and Communications Security. 2024.
83. Unifying Asynchronous Logics for Hyperproperties
    Alberto Bombardelli, Laura Bozzelli, César Sánchez, Stefano Tonetta.
    Proc. of the 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'24). 2024.
84. Monitoring the Future of Smart Contracts
    Margarita Capretto, Martín Ceresa, César Sánchez.
    Proc. of the 27th Int’l Conf. on Fundamental Approaches to Software Engineering (FASE'24). 2024.
85. A Myhill-Nerode Style Characterization for Timed Automata With Integer Resets
    Kyveli Doveri, Pierre Ganty, B. Srivathsan.
    Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2024.
86. A Uniform Framework for Language Inclusion Problems
    Kyveli Doveri, Pierre Ganty, Chana Weil-Kennedy.
    Taming the Infinities of Concurrency: Essays Dedicated to Javier Esparza on the Occasion of His 60th Birthday. 2024.
87. Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems
    Luca Geatti, Alessio Mansutti, Angelo Montanari.
    Foundations of Software Science and Computational Structures – FOSSACS. 2024.
88. Computing Reachable Simulations on Transition Systems
    Pierre Ganty, Nicolas Manini, Francesco Ranzato.
    Reachability Problems (RP). 2024.
89. Learning the State Machine Behind a Modal Text Editor: The (Neo)Vim Case Study
    Pierre Ganty.
    International SPIN Symposium on Model Checking of Software (SPIN). 2024.
90. General Anticipatory Runtime Verification
    Raik Hipler, Hannes Kallwies, Martin Leucker, César Sánchez.
    Proc. of the 36th Int’l Conf. on Computer Aided Verification (CAV'24), Part II. 2024.
91. Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors
    Gideon Mohr, Marco Guarnieri, Jan Reineke.
    Proceedings of the 27th Design, Automation and Test in Europe Conference and Exhibition. 2024.
92. An Order Theory Framework of Recurrence Equations for Static Cost Analysis - Dynamic Inference of Non-Linear Inequality Invariants
    Louis Rustenholz, Pedro Lopez-Garcia, José F. Morales, Manuel V. Hermenegildo.
    SAS. 2024.
93. Vertical Atomic Broadcast and Passive Replication
    Manuel Bravo, Gregory Chockler, Alexey Gotsman, Alejandro Naser-Pastoriza, Christian Roldán.
    Symposium on Distributed Computing (DISC). 2024.
94. Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories
    Andoni Rodríguez, César Sánchez.
    Proc. of the 38th AAAI Conf. on Artificial Intelligence (AAAI'24). 2024.
95. Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
    Andoni Rodríguez, Felipe Gorostiaga, César Sánchez.
    Proc. of the 22nd Int’l Symp for the Automated Technology for Verification and Analysis (ATVA'24), Part II. 2024.
96. Integer Programming with GCD Constraints
    Rémy Défossez, Christoph Haase, Alessio Mansutti, Guillermo A. Pérez.
    ACM-SIAM Symposium on Discrete Algorithms – SODA. 2024.
97. SwiftPaxos: Fast Geo-Replicated State Machines
    Fedor Ryabinin, Alexey Gotsman, Pierre Sutra.
    Symposium on Networked Systems Design and Implementation (NSDI). 2024.
98. LibKit: Detecting Third-Party Libraries in iOS Apps
    Daniel Dominguez Alvarez, Alejandro de la Cruz, Alessandra Gorla, Juan Caballero.
    European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE). diciembre 2023.
99. On the Dual Nature of Necessity in Use of Rust Unsafe Code
    Yuchen Zhang, Ashish Kundu, Georgios Portokalidis, Jun Xu.
    Proceedings of the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) (Industry Track). diciembre 2023.
100. Domain and Website Attribution beyond WHOIS
     Silvia Sebastián, Raluca-Georgia Diugan, Juan Caballero, Iskander Sanchez-Rola, Leyla Bilge.
     Annual Computer Security Applications Conference (ACSAC). diciembre 2023.
101. Cybercrime Bitcoin Revenue Estimations: Quantifying the Impact of Methodology and Coverage
     Gibran Gomez, Kevin van Liebergen, Juan Caballero.
     ACM Conference on Computer and Communications Security (CCS). noviembre 2023.
102. Decoding the Secrets of Machine Learning in Windows Malware Classification: A Deep Dive into Datasets, Features, and Model Performance
     Savino Dambra, Yufei Han, Simone Aonzo, Platon Kotzias, Antonino Vitale, Juan Caballero, Davide Balzarotti, Leyla Bilge.
     ACM Conference on Computer and Communications Security (CCS). noviembre 2023.
103. SysPart: Automated Temporal System Call Filtering for Binaries
     Vidya Lakshmi Rajagopalan, Konstantinos Kleftogiorgos, Enes Göktaş, Jun Xu, Georgios Portokalidis.
     Proceedings of the ACM Conference on Computer and Communications Security (CCS). noviembre 2023.
104. In the Room Where It Happens: Characterizing Local Communication and Threats in Smart Homes
     Aniketh Girish, Tianrui Hu, Vijay Prakash, Daniel J. Dubois, Srdjan Matic, Danny Yuxing Huang, Serge Egelman, Joel Reardon, Juan Tapiador, David R. Choffnes, Narseo Vallina-Rodriguez.
     Internet Measurement Conference (IMC). octubre 2023.
105. A Rule-Based Approach for Designing and Composing Abstract Domains
     Daniel Jurjo, José F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo.
     Proc. of the 33rd Int’l. Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2023. octubre 2023.
106. Cryptographic Administration for Secure Group Messaging
     David Balbás, Daniel Collins, Serge Vaudenay.
     Usenix Annual Technical Conference (USENIX). agosto 2023.
107. 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). agosto 2023.
108. Eliminating Vulnerabilities by Disabling Unwanted Functionality in Binary Programs
     Mohamad Mansouri, Jun Xu, Georgios Portokalidis.
     Proceedings of the ACM ASIA Conference on Computer and Communications Security (ASIACCS). julio 2023.
109. Solving Recurrence Relations using Machine Learning, with Application to Cost Analysis
     M. Klemen, M.Á. Carreira-Perpiñán, P. Lopez-Garcia.
     Technical Communications of the 39th International Conference on Logic Programming (ICLP 2023). julio 2023.
110. A Deep Dive into the VirusTotal File Feed
     Kevin van Liebergen, Juan Caballero, Platon Kotzias, Chris Gates.
     GI International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA). julio 2023.
111. Your Code is 0000: An Analysis of the Disposable Phone Numbers Ecosystem
     José Miguel Moreno, Srdjan Matic, Narseo Vallina-Rodriguez, Juan Tapiador.
     Proceedings of the 7th Network Traffic Measurement and Analysis Conference (TMA). junio 2023.
112. Efficient Reactive Synthesis Using Mode Decomposition
     Matías Brizzio, César Sánchez.
     Theoretical Aspects of Computing – ICTAC 2023. 2023.
113. WhatsUpp with Sender Keys? Analysis, Improvements and Security Proofs
     David Balbás, Daniel Collins, Phillip Gajland.
     International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). 2023.
114. Cuckoo Commitments: Registration-Based Encryption and Key-Value Map Commitments for Large Spaces
     Dario Fiore, Dimitris Kolonelos, Paola de Perthuis.
     International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). 2023.
115. Mt. Random: Multi-tiered Randomness Beacons
     Ignacio Cascudo, Bernardo David, Omer Shlomovits, Denis Varlakov.
     International Conference on Applied Cryptography and Network Security (ACNS). 2023.
116. On the Impossibility of Algebraic NIZK in Pairing-Free Groups
     Emanuele Giunta.
     Advances in Cryptology – CRYPTO 2023. 2023.
117. Modular Sumcheck Proofs with Applications to Machine Learning and Image Processing
     David Balbás, Dario Fiore, María Isabel González Vasco, Damien Robissout, Claudio Soriente.
     ACM Conference on Computer and Communications Security (CCS). 2023.
118. CSI-SharK: CSI-FiSh with Sharing-friendly Keys
     Shahla Atapoor, Karim Baghery, Daniele Cozzo, Robi Pedersen.
     Australasian Conference on Information Security and Privacy (ACISP). 2023.
119. Practical Robust DKG Protocols for CSIDH
     Shahla Atapoor, Karim Baghery, Daniele Cozzo, Robi Pedersen.
     International Conference on Applied Cryptography and Network Security (ACNS). 2023.
120. VSS from Distributed ZK Proofs and Applications
     Shahla Atapoor, Karim Baghery, Daniele Cozzo, Robi Pedersen.
     International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). 2023.
121. An Incremental PoSW for General Weight Distributions
     Hamza Abusalah, Valerio Cini.
     International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt). 2023.
122. 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 (FASE). 2023.
123. 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.
124. Automated Repair of Unrealisable LTL Specifications Guided by Model Counting
     Matías Brizzio, Maxime Cordy, Mike Papadakis, César Sánchez, Nazareno Aguirre, Renzo Degiovanni.
     Genetic and Evolutionary Computations (GECCO). 2023.
125. Precise Lazy Initialization for Programs with Complex Heap Inputs
     Juan Manuel Copia, Facundo Molina, Nazareno Aguirre, Marcelo F. Frias, Alessandra Gorla, Pablo Ponzio.
     International Symposium on Software Reliability Engineering (ISSRE). 2023.
126. Enabling Efficient Assertion Inference
     Aayush Garg, Renzo Degiovanni, Facundo Molina, Maxime Cordy, Nazareno Aguirre, Mike Papadakis, Yves Le Traon.
     International Symposium on Software Reliability Engineering (ISSRE). 2023.
127. EvoSpex: A Search-Based Tool for Postcondition Inference
     Facundo Molina, Pablo Ponzio, Nazareno Aguirre, Marcelo F. Frias.
     International Symposium on Software Testing and Analysis (ISSTA). 2023.
128. SpecFuzzer: A Tool for Inferring Class Specifications via Grammar-Based Fuzzing
     Facundo Molina, Marcelo d'Amorim, Nazareno Aguirre.
     Automated Software Engineering Conference (ASE). 2023.
129. Extendable Threshold Ring Signatures with Enhanced Anonymity
     Gennaro Avitabile, Vincenzo Botta, Dario Fiore.
     International Conference on Practice and Theory in Public Key Cryptography (PKC). 2023.
130. From Polynomial IOP and Commitments to Non-malleable zkSNARKs
     Antonio Faonio, Dario Fiore, Markulf Kohlweiss, Luigi Russo, Michal Zajac.
     Theory of Cryptography Conference (TCC). 2023.
131. Transforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
     John P. Gallagher, Manuel V. Hermenegildo, José F. Morales, Pedro López-García.
     Logic-Based Program Synthesis and Transformation - 33rd International Symposium, LOPSTR 2023, Cascais, Portugal, October 23-24, 2023, Proceedings. 2023.
132. Efficient and universally composable single secret leader election from pairings
     Dario Catalano, Dario Fiore, Emanuele Giunta.
     IACR International Conference on Public-Key Cryptography. 2023.
133. Chainable Functional Commitments for Unbounded-Depth Circuits
     David Balbás, Dario Catalano, Dario Fiore, Russell W. F. Lai.
     Theory of Cryptography Conference (TCC). 2023.
134. Round-Robin is Optimal: Lower Bounds for Group Action Based Protocols
     Daniele Cozzo, Emanuele Giunta.
     Theory of Cryptography Conference. 2023.
135. 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.
136. Fault-Tolerant Computing with Unreliable Channels
     Alejandro Naser-Pastoriza, Gregory V. Chockler, Alexey Gotsman.
     International Conference on Principles of Distributed Systems (OPODIS). 2023.
137. Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack
     Jesús Domínguez, Aleksandar Nanevski.
     International Conference on Concurrency Theory (CONCUR). 2023.
138. 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.
139. Is Machine Learning Necessary for Cloud Resource Usage Forecasting?
     Georgia Christofidi, Konstantinos Papaioannou, Thaleia Dimitra Doudali.
     Proceedings of the 2023 ACM Symposium on Cloud Computing. 2023.
140. 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.
141. Tableaux for Realizability of Safety Specifications
     Monserrat Hermo, Paqui Lucio, César Sánchez.
     Proc. of the 25th International Symposium on Formal Methods (FM'23). 2023.
142. Bounded Model Checking for Asynchronous Hyperproperties
     Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez.
     Proc. of the 29th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23). 2023.
143. Efficient Loop Conditions for Bounded Model Checking Hyperproperties
     Tzu-Han Hsu, Sarai Sheinvald, César Sánchez, Borzoo Bonakdarpour.
     Proc. of the 29th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23). 2023.
144. The complexity of Presburger arithmetic with power or powers
     Michael Benedikt, Dmitry Chistikov, Alessio Mansutti.
     Automata, Languages and Programming – ICALP. 2023.
145. General Anticipatory Monitoring for Temporal Logics on Finite Traces
     Hannes Kallwies, Martin Leuker, César Sánchez.
     Proc. of the 23nd Int’l Conference on Runtime Verification (RV'23). 2023.
146. LedgerLocks: A Security Framework for Blockchain Protocols Based on Adaptor Signatures
     Erkan Tairi, Pedro Moreno-Sanchez, Clara Schneidewind.
     ACM Conference on Computer and Communications Security (CCS). 2023.
147. On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (extended abstract)
     Christoph Haase, Alessio Mansutti, Amaury Pouly.
     Mathematical Foundations of Computer Science – MFCS. 2023.
148. Scalable Off-chain Auction
     M. Minaei, R. Kumaresan, A. Beams, P. Moreno-Sanchez, Y. Yang, S. Raghuraman, P. Chatzigiannis, M. Zamani, D. Le.
     Network and Distributed System Security Symposium (NDSS). 2023.
149. 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.
150. 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.
151. A Stream Runtime Verification Tool with Nested and Retroactive Parametrization
     Paloma Pedregal, Felipe Gorostiaga, César Sánchez.
     Runtime Verification. 2023.
152. Boolean Abstractions for Realizabilty Modulo Theories
     Andoni Rodríguez, César Sánchez.
     Proc. of the 35th International Conference on Computer Aided Verification (CAV'23). 2023.
153. Efficient Modular SMT-Based Model Checking of Pointer Programs
     I. Garcia-Contreras, A. Gurfinkel, J. A. Navas.
     Static Analysis, 29th International Symposium, SAS 2022. diciembre 2022.
154. 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). noviembre 2022.
155. 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). octubre 2022.
156. 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). octubre 2022.
157. 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). octubre 2022.
158. Deep dive into the IoT backend ecosystem
     Said Jawad Saidi, Srdjan Matic, Georgios Smaragdakis, Oliver Gasser, Anja Feldmann.
     Internet Measurement Conference (IMC). octubre 2022.
159. Measuring Web Cookies in Governmental Websites
     Matthias Götze, Srdjan Matic, Costas Iordanou, Georgios Smaragdakis, Nikolaos Laoutaris.
     Web Science Conference (WebSci). junio 2022.
160. 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). mayo 2022.
161. 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.
     ICSE 2022: Proceedings of the 44th International Conference on Software Engineering. mayo 2022.
162. 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). mayo 2022.
163. ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
     Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker.
     Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 2022.
164. How to Safely Use Extensionality in Liquid Haskell
     Niki Vazou, Michael Greenberg.
     Proceedings of the 15th ACM SIGPLAN International Haskell Symposium. 2022.
165. Liquid Proof Macros
     Henry Blanchette, Niki Vazou, Leonidas Lampropoulos.
     Proceedings of the 15th ACM SIGPLAN International Haskell Symposium. 2022.
166. Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
     Lykourgos Mastorou, Nikolaos Papaspyrou, Niki Vazou.
     Proceedings of the 15th ACM SIGPLAN International Haskell Symposium. 2022.
167. 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.
168. 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.
169. Progressive And Efficient Verification For Digital Signatures
     Cecilia Boschini, Dario Fiore, Elena Pagnin.
     International Conference on Applied Cryptography and Network Security (ACNS). 2022.
170. 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.
171. 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.
172. Subversion-Resilient Enhanced Privacy ID
     Antonio Faonio, Dario Fiore, Luca Nizzardo, Claudio Soriente.
     The Cryptographer’s Track at RSA Conference (CT-RSA). 2022.
173. 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.
     2022 IEEE International Conference on Blockchain (Blockchain). 2022.
174. Transaction Monitoring of Smart Contracts
     Margarita Capretto, Martín Ceresa, César Sánchez.
     Runtime Verification. 2022.
175. Symbolic Synthesis of Indifferentiability Attacks
     Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe.
     Asia Conference on Information, Computer and Communications Security (AsiaCCS). 2022.
176. 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.
177. 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.
178. Efficient Proofs of Knowledge for Threshold Relations
     Gennaro Avitabile, Vincenzo Botta, Daniele Friolo, Ivan Visconti.
     European Symposium On Research In Computer Security (ESORICS). 2022.
179. 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.
180. 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.
181. 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.
182. 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.
183. 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.
184. Deciding program properties via complete abstractions on bounded domains
     Roberto Bruni, Roberta Gori, Nicolas Manini.
     Static Analysis Symposium (SAS). 2022.
185. 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.
186. On Interactive Oracle Proofs for Boolean R1CS Statements
     Ignacio Cascudo, Emanuele Giunta.
     Financial Cryptography and Data Security Conference (FC). 2022.
187. Adaptively Secure Single Secret Leader Election from DDH
     Dario Catalano, Dario Fiore, Emanuele Giunta.
     Symposium on Principles of Distributed Computing. 2022.
188. 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.
189. Vector Commitments over Rings and Compressed Σ-Protocols
     Thomas Attema, Ignacio Cascudo, Ronald Cramer, Ivan Damgård, Daniel Escudero.
     Theory of Cryptography Conference (TCC). 2022.
190. On the impossibility of algebraic vector commitments in pairing-free groups
     Dario Catalano, Dario Fiore, Rosario Gennaro, Emanuele Giunta.
     Theory of Cryptography Conference. 2022.
191. Acuerdo: Fast atomic broadcast over RDMA
     Joseph Izraelevitz, Gaukas Wang, Rhett Hanscom, Kayli Silvers, Tamara Silbergleit Lehman, Gregory Chockler, Alexey Gotsman.
     ICPP'22: International Conference on Parallel Processing. 2022.
192. 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.
193. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
     Laura Bozzelli, Adriano Peron, César Sánchez.
     Proc. of the 33rd International Conference on Concurrency Theory (CONCUR'22). 2022.
194. 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.
195. FORQ-Based Language Inclusion Formal Testing
     Kyveli Doveri, Pierre Ganty, Nicolas Mazzocchi.
     Computer Aided Verification (CAV). 2022.
196. Automatic Detection of Speculative Execution Combinations
     Xaver Fabian, Marco Guarnieri, Marco Patrignani.
     Proceedings of the 29th ACM Conference on Computer and Communications Security. 2022.
197. Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification
     Felipe Gorostiaga, Sebastián Zudaire, César Sánchez, Gerardo Schneider, Sebastián Uchitel.
     Proc. of the 11th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2022). Verification Principles. Part I. 2022.
198. Monitorability of Expressive Verdicts
     Felipe Gorostiaga, César Sánchez.
     NASA Formal Methods. 2022.
199. Anticipatory Recurrent Monitoring with Uncertainty and Assumptions
     Hannes Kallwies, Martin Leucker, César Sánchez, Torben Scheffel.
     Proc. of the 22nd Int’l Conference on Runtime Verification (RV'22). 2022.
200. Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions
     Hannes Kallwies, Martin Leucker, César Sánchez.
     Proc. of 20th Int’l Symp. on Automated Technology for Verification and Analysis (ATVA'22). 2022.
201. Liveness and latency of Byzantine state-machine replication
     Manuel Bravo, Gregory Chockler, Alexey Gotsman.
     International Symposium on Distributed Computing (DISC). 2022.
202. 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.
203. 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). diciembre 2021.
204. 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). diciembre 2021.
205. Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
     Lukas Aumayr, Pedro Moreno-Sanchez, Aniket Kate, Matteo Maffei.
     Usenix Security Symposium (USENIX-Security). agosto 2021.
206. STORM: Refinement Types for Secure Web Applications
     Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala.
     15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). julio 2021.
207. 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). mayo 2021.
208. 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). mayo 2021.
209. 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). mayo 2021.
210. 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.
211. 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.
212. 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.
213. Secure Compilation of Constant-Resource Programs
     Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie.
     IEEE Computer Security Foundations Symposium (CSF). 2021.
214. 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.
215. 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.
216. 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.
217. 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.
218. Selectively Linkable Group Signatures - Stronger Security and Preserved Verifiability
     Ashley Fraser, Lydia Garms, Anja Lehmann.
     International Conference on Cryptology and Network Security (CANS). 2021.
219. Decomposing Permutation Automata
     Ismaël Jecker, Nicolas Mazzocchi, Petra Wolf.
     International Conference on Concurrency Theory (CONCUR). 2021.
220. 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.
221. Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
     Joaquín Arias, Mar Moreno-Rebato, Jose A. Rodriguez-García, Sascha Ossowski.
     Advances in Artificial Intelligence, CAEPIA 20/21. 2021.
222. I Told You Tomorrow: Practical Time-Locked Secrets Using Smart Contracts
     Enrico Bacis, Dario Facchinetti, Marco Guarnieri, Marco Rosa, Matthew Rossi, Stefano Paraboschi.
     Proceedings of the 16th International Conference on Availability, Reliability and Security. 2021.
223. Knowledge-driven Natural Language Understanding of English Text and its Applications
     Kinjal Basu, Sarat Varanasi, Farhad Shakerin, Joaquin Arias, Gopal Gupta.
     Proceedings of the AAAI Conference on Artificial Intelligence. 2021.
224. A Temporal Logic for Asynchronous Hyperproperties
     Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez.
     Proc. of the 33rd Int’l Conf. on Computer Aided Verification (CAV'21), Part I. 2021.
225. Asynchronous Extensions of HyperLTL
     Laura Bozzelli, Adriano Peron, César Sánchez.
     Proc. of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'21). 2021.
226. UniStore: A fault-tolerant marriage of causal and strong consistency
     Manuel Bravo, Alexey Gotsman, Borja de Régil, Hengfeng Wei.
     Proceedings of the USENIX Annual Technical Conference. 2021.
227. 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.
228. Reachability in Distributed Memory Automata
     Benedikt Bollig, Fedor Ryabinin, Arnaud Sangnier.
     29th EACSL Annual Conference on Computer Science Logic (CSL 2021). 2021.
229. 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.
230. 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.
231. 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.
232. 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.
233. HLola: a Very Functional Tool for Extensible Stream Runtime Verification
     Felipe Gorostiaga, César Sánchez.
     Proc. of the 27th Int’l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21). Part II. 2021.
234. HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams
     Felipe Gorostiaga, César Sánchez.
     Formal Methods. 2021.
235. Nested Monitors: Monitors as Expressions to Build Monitors
     Felipe Gorostiaga, César Sánchez.
     Runtime Verification. 2021.
236. Hardware-Software Contracts for Secure Speculation
     Marco Guarnieri, Boris Köpf, Jan Reineke, Pepe Vila.
     Proceedings of the 42nd IEEE Symposium on Security and Privacy. 2021.
237. Bounded Model Checking for Hyperproperties
     Tzu-Han Hsu, César Sánchez, Borzoo Bonakdarpour.
     Proc. of the 27th Int’l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21). Part I. 2021.
238. Madrid Quantum Communication Infrastructure: a testbed for assessing QKD technologies into real production networks
     Diego López, Juan Pedro Brito, Antonio Pastor, Vicente Martin, César Sánchez, David Rincon, Victor López.
     Optical Fiber Communication Conference (OFC) 2021. 2021.
239. Exorcising Spectres with Secure Compilers
     Marco Patrignani, Marco Guarnieri.
     Proceedings of the 28th ACM Conference on Computer and Communications Security. 2021.
240. Efficient replication via timestamp stability
     Vitor Enes, Carlos Baquero, Alexey Gotsman, Pierre Sutra.
     EuroSys'21: European Conference on Computer Systems. 2021.
241. 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.
242. 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.
     Proc. of IEEE International Conference on Robotics and Automation (ICRA'21). 2021.
243. 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). diciembre 2020.
244. 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). diciembre 2020.
245. A Secret-Sharing Based MPC Protocol for Boolean Circuits with Good Amortized Complexity
     Ignacio Cascudo, Jaron Skovsted Gundersen.
     Theory of Cryptography Conference (TCC). diciembre 2020.
246. AVClass2: Massive Malware Tag Extraction from AV Labels
     Silvia Sebastián, Juan Caballero.
     Annual Computer Security Applications Conference (ACSAC). diciembre 2020.
247. Towards Attribution in Mobile Markets: Identifying Developer Account Polymorphism
     Silvia Sebastián, Juan Caballero.
     ACM Conference on Computer and Communications Security (CCS). noviembre 2020.
248. 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. noviembre 2020.
249. 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). octubre 2020.
250. A Framework for Automated Test Mocking of Mobile Apps
     Mattia Fazzini, Alessandra Gorla, Alessandro Orso.
     Automated Software Engineering Conference (ASE). septiembre 2020.
251. 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.
     MSR 2020: 17th International Conference on Mining Software Repositories. junio 2020.
252. 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). abril 2020.
253. 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'19). abril 2020.
254. 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). abril 2020.
255. 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). febrero 2020.
256. 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). enero 2020.
257. 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.
258. 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.
259. 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.
260. 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.
261. 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.
262. 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.
263. 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.
264. 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.
265. 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.
266. 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.
267. A Quasiorder-Based Perspective on Residual Automata
     Pierre Ganty, Elena Gutiérrez, Pedro Valero.
     International Symposium on Mathematical Foundations of Computer Science (MFCS). 2020.
268. 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.
269. 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.
270. 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.
271. 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.
272. Boosting Verifiable Computation on Encrypted Data
     Dario Fiore, Anca Nitulescu, David Pointcheval.
     International Conference on Practice and Theory in Public Key Cryptography (PKC). 2020.
273. Detecting and Diagnosing Energy Issues for Mobile Applications
     Xueliang Li, Yuming Yang, Yepang Liu, John P. Gallagher, Kaishun Wu.
     Proc. of the ACM SIGSOFT International Symposium on Software Testing and Analysis. 2020.
274. Justifications for Goal-Directed Constraint Answer Set Programming
     Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
     36th ICLP-TC. 2020.
275. State-machine replication for planet-scale systems
     Vitor Enes, Carlos Baquero, Tuanir França Rezende, Alexey Gotsman, Matthieu Perrin, Pierre Sutra.
     EuroSys'20: European Conference on Computer Systems. 2020.
276. 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.
277. Model Checking Timed Hyperproperties in Discrete-Time Systems
     Borzoo Bonakdarpour, Pavithra Prabhakar, César Sánchez.
     Proc. of the 12th NASA Formal Methods Symposium (NFM'2020). 2020.
278. Making Byzantine Consensus Live
     Manuel Bravo, Gregory Chockler, Alexey Gotsman.
     Proceedings of the 34th International Symposium on Distributed Computing. 2020.
279. Combining High Throughput and Low Migration Latency for Consistent Data Storage on the Edge
     Nuno Afonso, Manuel Bravo, Luís Rodrigues.
     Proceedings of the 29th International Conference on Computer Communications and Networks. 2020.
280. Declarative Stream Runtime Verification (hLola)
     Martín Ceresa, Felipe Gorostiaga, César Sánchez.
     Proc. of the 18th Asian Symposium on Programming Languages and Systems (APLAS'20). 2020.
281. Unifying the Time-Event Spectrum for Stream Runtime Verification
     Felipe Gorostiaga, Luis Miguel Danielsson, César Sánchez.
     Proc. of 20th Int’l Conf. on Runtime Verification (RV'20). 2020.
282. Spectector: Principled detection of speculative information flows
     Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, Andrés Sánchez.
     Proceedings of the 41st IEEE Symposium on Security and Privacy. 2020.
283. A Quasiorder-Based Perspective on Residual Automata
     Pierre Ganty, Elena Gutiérrez, Pedro Valero.
     International Symposium on Mathematical Foundations of Computer Science (MFCS). 2020.
284. Incremental Analysis of Logic Programs with Assertions and Open Predicates
     I. Garcia-Contreras, J.F. Morales, M.V. Hermenegildo.
     LOPSTR'19. 2020.
285. Reliable Smart Contracts
     Gordon J. Pace, César Sánchez, Gerardo Schneider.
     Proc. of the 9th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2020). Verification. Part III. 2020.
286. 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 Simposium (SAS'20). 2020.
287. 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.
288. 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). noviembre 2019.
289. 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). noviembre 2019.
290. 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). noviembre 2019.
291. Abstract Interpretation of Indexed Grammars
     Marco Campion, Mila Dalla Preda, Roberto Giacobazzi.
     Static Analysis Symposium (SAS). octubre 2019.
292. Runtime Verification for Timed Event Streams with Partial Information
     Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, Daniel Thoma.
     Proc. of the 19th Int’l Conf. on Runtime Verification (RV'19). octubre 2019.
293. Privatization-safe transactional memories
     Artem Khyzha, Hagit Attiya, Alexey Gotsman.
     International Symposium on Distributed Computing (DISC). octubre 2019.
294. Towards Computing Abstract Distances in Logic Programs
     I. Casso, J. F. Morales, P. Lopez-Garcia, M.V. Hermenegildo.
     ICLP Tech. Comms.. septiembre 2019.
295. 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.. septiembre 2019.
296. 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). julio 2019.
297. White-box atomic multicast
     Alexey Gotsman, Anatole Lefort, Gregory Chockler.
     DSN'19: International Conference on Dependable Systems and Networks. junio 2019.
298. Theory and Practice of Finding Eviction Sets
     Pepe Vila, Boris Köpf, Jose Morales.
     Proc. 40th IEEE Symposium on Security and Privacy (S& P ‘19). mayo 2019.
299. Polyvariant Program Specialisation with Property-based Abstraction
     John P. Gallagher.
     Computing Research Repository (CoRR). abril 2019.
300. 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). febrero 2019.
301. Orion: A distributed file system for non-volatile main memory and RDMA-capable networks
     Jian Yang, Joseph Izraelevitz, Steven Swanson.
     17th USENIX Conference on File and Storage Technologies. febrero 2019.
302. Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP
     Joaquín Arias, Manuel Carro.
     21st Int’l. Symposium on Practical Aspects of Declarative Languages. enero 2019.
303. Multivariant Assertion-based Guidance in Abstract Interpretation
     I. Garcia-Contreras, J.F. Morales, M.V. Hermenegildo.
     28th Int’l. Symp. on Logic-based Program Synthesis and Transformation (LOPSTR'18). enero 2019.
304. 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.
305. 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.
306. 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.
307. 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.
308. 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.
309. 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.
310. 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.
311. 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.
312. Privacy Amplification by Mixing and Diffusion Mechanisms
     Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek.
     Advances in Neural Information Processing Systems (NeurIPS). 2019.
313. 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.
314. 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.
315. 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.
316. Decentralized Stream Runtime Verification
     Luis Miguel Danielsson, César Sánchez.
     International Conference on Runtime Verification (RV). 2019.
317. Language Inclusion Algorithms as Complete Abstract Interpretations
     Pierre Ganty, Francesco Ranzato, Pedro Valero.
     Static Analysis Symposium (SAS). 2019.
318. Deconstructing Stellar Consensus
     Álvaro García-Pérez, Maria A. Schett.
     International Conference on Principles of Distributed Systems (OPODIS). 2019.
319. Design Patterns for Code Reuse in HLS Packet Processing Pipelines
     Haggai Eran, Lior Zeno, Zsolt István, Mark Silberstein.
     2019 IEEE 27th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). 2019.
320. Storing Parquet Tile by Tile: Application-Aware Storage with Deduplication
     Lucas Kuhring, Zsolt István.
     2019 29th International Conference on Field Programmable Logic and Applications (FPL). 2019.
321. Reconfigurable Atomic Transaction Commit
     Manuel Bravo, Alexey Gotsman.
     Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing. 2019.
322. Verifying Hyperliveness
     Norine Coenen, Bernd Finkbeiner, César Sánchez, Leander Tentrup.
     Proc. of the 31st Int’l Conf. on Computer Aided Verification (CAV'19). 2019.
323. Regular Expression Search on Compressed Text
     Pierre Ganty, Pedro Valero.
     Data Compression Conference (DCC). 2019.
324. Information-flow Control for Database-backed Applications
     Marco Guarnieri, Musard Balliu, Daniel Schoepe, David Basin, Andrei Sabelfeld.
     Proceedings of the 4th IEEE European Symposium on Security and Privacy. 2019.
325. Hourglass: Leveraging Transient Resources for Time-Constrained Graph Processing in the Cloud
     Pedro Joaquim, Manuel Bravo, Luís Rodrigues, Miguel Matos.
     Proceedings of the Fourteenth European Conference on Computer Systems. 2019.
326. Gray-Box Monitoring of Hyperproperties
     Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonakdarpour.
     Formal Methods - The Next 30 Years - Third World Congress, FM 2019. 2019.
327. Striver: Stream Runtime Verification for Real-Time Event-Streams
     Felipe Gorostiaga, César Sánchez.
     18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings. noviembre 2018.
328. 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). octubre 2018.
329. Ido: Compiler-directed failure atomicity for nonvolatile memory
     Qingrui Liu, Joseph Izraelevitz, Se Kwon Lee, Michael L. Scott, Sam H. Noh, Changhee Jung.
     51st IEEE/ACM Intl. Symp. on Microarchitecture. octubre 2018.
330. 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). octubre 2018.
331. Matrioska: A Compiler for Multi-Key Homomorphic Signatures
     Dario Fiore, Elena Pagnin.
     Conference on Security and Cryptography for Networks (SCN). septiembre 2018.
332. 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). septiembre 2018.
333. 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). agosto 2018.
334. A Flexible K-Means Operator for Hybrid Databases
     Zhenhao He, David Sidler, Zsolt István, Gustavo Alonso.
     Proceedings of the International Conference on Field-Programmable Logic and Applications. agosto 2018.
335. Providing Multi-tenant Services with FPGAs: Case Study on a Key-Value Store
     Zsolt István, Gustavo Alonso, Ankit Singla.
     Proceedings of the International Conference on Field-Programmable Logic and Applications. agosto 2018.
336. Translating Code Comments to Procedure Specifications
     Arianna Blasi, Alberto Goffi, Konstantin Kuznetsov, Alessandra Gorla, Michael D. Ernst, Mauro Pezzè, Sergio Delgado Castellanos.
     Proceedings of the 27th International Symposium on Software Testing and Analysis. julio 2018.
337. 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.
     2018 IEEE International Conference on Web Services (ICWS). julio 2018.
338. Towards Incremental and Modular Context-sensitive Analysis
     I. Garcia-Contreras, J. F. Morales, M.V. Hermenegildo.
     ICLP 2018 - TCs. julio 2018.
339. On the Security Notions for Homomorphic Signatures
     Dario Catalano, Dario Fiore, Nizzardo Luca.
     International Conference on Applied Cryptography and Network Security (ACNS). junio 2018.
340. 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). junio 2018.
341. RepliComment: Identifying Clones in Code Comments
     Arianna Blasi, Alessandra Gorla.
     2018 IEEE/ACM 26th International Conference on Program Comprehension (ICPC). mayo 2018.
342. What did Really Change with the new Release of the App?
     Paolo Calciati, Konstantin Kuznetsov, Alessandra Gorla.
     Proceedings of the 15th International Conference on Mining Software Repositories (MSR). mayo 2018.
343. Analyzing the User Interface of Android Apps
     Konstantin Kuznetsov, Vitalii Avdiienko, Alessandra Gorla, Andreas Zeller.
     International Conference on Mobile Software Engineering and Systems (MOBILESoft). mayo 2018.
344. 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). abril 2018.
345. Interval-based memory reclamation
     Haosen Wen, Joseph Izraelevitz, Wentao Cai, H. Alan Beadle, Michael L. Scott.
     23rd ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming. febrero 2018.
346. Exploiting Term Hiding to Reduce Run-time Checking Overhead
     N. Stulova, J. F. Morales, M.V. Hermenegildo.
     Int’l. Symp. on Practical Aspects of Declarative Languages (PADL). enero 2018.
347. 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.
348. Code Obfuscation Against Abstract Model Checking Attacks
     Roberto Bruni, Roberto Giacobazzi, Roberta Gori.
     Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI ‘18. 2018.
349. Program Analysis Is Harder Than Verification: A Computability Perspective
     Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato.
     Computer Aided Verification - 30th International Conference, CAV ‘18. 2018.
350. 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.
351. 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.
352. 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.
353. 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.
354. 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.
355. 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.
356. Almost Sure Productivity
     Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva.
     International Colloquium on Automata Languages and Programming (ICALP). 2018.
357. Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences
     Borja Balle, Gilles Barthe, Marco Gaboardi.
     Advances in Neural Information Processing Systems (NeurIPS). 2018.
358. 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.
359. 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.
     Web Information Systems Engineering – WISE 2018. 2018.
360. 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.
361. Averist: Algorithmic Verifier for Stability of Linear Hybrid Systems
     Miriam García Soto, Pavithra Prabhakar.
     Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week). 2018.
362. Inferring Energy Bounds via Static Program Analysis and Evolutionary Modeling of Basic Blocks
     U. Liqat, Z. Banković, P. Lopez-Garcia, M.V. Hermenegildo.
     Logic-Based Program Synthesis and Transformation - 27th International Symposium. 2018.
363. Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification
     Borzoo Bonakdarpour, César Sánchez, Gerardo Schneider.
     Proc. of the 8th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2018). Verification. Part II. 2018.
364. Fine-Grained Secure Computation
     Matteo Campanelli, Rosario Gennaro.
     Theory of Cryptography Conference. 2018.
365. COST Action IC1402 Runtime Verification Beyond Monitoring
     Christian Colombo, Yliés Falcone, Martin Leucker, Giles Reger, César Sánchez, Gerardo Schneider, Volker Stolz.
     Proc. of the 18th Int’l Conf. on Runtime Verification (RV'18). 2018.
366. Multi-Shot Distributed Transaction Commit
     Gregory Chockler, Alexey Gotsman.
     International Symposium on Distributed Computing (DISC). 2018.
367. Compositional verification of compiler optimisations on relaxed memory
     Mike Dodds, Mark Batty, Alexey Gotsman.
     European Symposium on Programming (ESOP). 2018.
368. Verification of Immediate Observation Population Protocols
     Javier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy.
     International Conference on Concurrency Theory (CONCUR). 2018.
369. The Parikh Property for Weighted Context-Free Grammars
     Pierre Ganty, Elena Gutiérrez.
     Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2018.
370. 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.
371. Timed Epistemic Knowledge Bases for Social Networks
     Raúl Pardo, César Sánchez, Gerardo Schneider.
     Proc. of 22nd Int’l Symposium on Formal Methods (FM'18). 2018.
372. Paxos consensus, deconstructed and abstracted
     Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey.
     European Symposium on Programming (ESOP). 2018.
373. Safe privatization in transactional memory
     Artem Khyzha, Hagit Attiya, Alexey Gotsman, Noam Rinetzky.
     PPoPP'18: Symposium on Principles and Practice of Parallel Programming. 2018.
374. Automatic Verification of RMA Programs via Abstraction Extrapolation
     Cedric Baumann, Andrei Marian Dan, Yuri Meshman, Torsten Hoefler, Martin T. Vechev.
     Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. 2018.
375. Online and Offline Stream Runtime Verification of Synchronous Systems
     César Sánchez.
     Proc. of the 18th Int’l Conf. on Runtime Verification (RV'18). 2018.
376. Reliable Smart Contracts: State-of-the-Art, Applications, Challenges and Future Directions
     César Sánchez, Gerardo Schneider, Martin Leucker.
     Proc. of the 8th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2018). Verification. Part IV. 2018.
377. Federated Byzantine quorum systems
     Álvaro García-Pérez, Alexey Gotsman.
     OPODIS'18: International Conference on Principles of Distributed Systems. 2018.
378. Distributed Transactional Reads: The Strong, the Quick, the Fresh & the Impossible
     Alejandro Z. Tomsic, Manuel Bravo, Marc Shapiro.
     Proceedings of the 19th International Middleware Conference. 2018.
379. 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). octubre 2017.
380. A Language-Theoretic View on Network Protocols
     Pierre Ganty, Boris Köpf, Pedro Valero.
     International Symposium on Automated Technology for Verification and Analysis (ATVA). octubre 2017.
381. Towards formal model-based analysis and testing of Android's security mechanisms
     G. Betarte, J. Campo, M. Cristiá, F. Gorostiaga, C. Luna, C. Sanz.
     2017 XLIII Latin American Computer Conference (CLEI). septiembre 2017.
382. 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). septiembre 2017.
383. Parikh Image of Pushdown Automata
     Pierre Ganty, Elena Gutiérrez.
     International Symposium on Fundamentals of Computation Theory (FCT). septiembre 2017.
384. 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). agosto 2017.
385. Detecting behavior anomalies in graphical user interfaces
     Vitalii Avdiienko, Konstantin Kuznetsov, Isabelle Rommelfanger, Andreas Rau, Alessandra Gorla, Andreas Zeller.
     Proceedings of the 39th International Conference on Software Engineering (ICSE 2017). mayo 2017.
386. How Do Apps Evolve in Their Permission Requests?: A Preliminary Study
     Paolo Calciati, Alessandra Gorla.
     IEEE International Working Conference on Mining Software Repositories (MSR). mayo 2017.
387. 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). mayo 2017.
388. Small Data
     Oliver Kennedy, D. Richard Hipp, Stratos Idreos, Amélie Marian, Arnab Nandi, Carmela Troncoso, Eugene Wu.
     International Conference on Data Engineering (ICDE). abril 2017.
389. O!Snap: Cost-Efficient Testing in the Cloud
     Alessio Gambi, Alessandra Gorla, Andreas Zeller.
     Proceedings of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST). marzo 2017.
390. 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). marzo 2017.
391. App Mining
     Vitalii Avdiienko, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller, Steven Arzt, Siegfried Rasthofer, Eric Bodden.
     Software Engineering 2017. febrero 2017.
392. 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.
     Software Engineering 2017, Fachtagung des GI-Fachbereichs Softwaretechnik. febrero 2017.
393. 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). febrero 2017.
394. Rule Formats for Nominal Process Calculi
     Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, Yolanda Ortega-Mallén.
     28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany. 2017.
395. 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.
396. 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.
397. 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.
398. Verified Translation Validation of Static Analyses
     Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu.
     IEEE 30th Computer Security Foundations Symposium, (CSF). 2017.
399. 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.
400. Generic Transformations of Predicate Encodings: Constructions and Applications
     Miguel Ambrona, Gilles Barthe, Benedikt Schmidt.
     Advances in Cryptology (CRYPTO). 2017.
401. 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.
402. 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.
403. 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.
404. Formal Synthesis of Stabilizing Controllers for Switched Systems
     Pavithra Prabhakar, Miriam García Soto.
     International Conference on Hybrid Systems: Computation and Control (HSCC). 2017.
405. *-Liftings for Differential Privacy
     Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub.
     International Colloquium on Automata Languages and Programming (ICALP). 2017.
406. 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.
407. 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.
408. 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.
409. Relational cost analysis
     Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2017.
410. 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.
411. Unilaterally-Authenticated Key Exchange
     Yevgeniy Dodis, Dario Fiore.
     Financial Cryptography and Data Security Conference (FC). 2017.
412. Feature importance scores and lossless feature pruning using Banzhaf power indices
     Bogdan Kulynych, Carmela Troncoso.
     NIPS 2017 Symposium on Interpretable Machine Learning. 2017.
413. 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.
414. Security Analysis of Cache Replacement Policies
     Pablo Cañones, Boris Köpf, Jan Reineke.
     Proc. 6th Conference on Principles of Security and Trust (POST ‘17). 2017.
415. 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.
416. Rigorous Analysis of Software Countermeasures against Cache Attacks
     Goran Doychev, Boris Köpf.
     38th ACM SIGPLAN Conference on Programming Language Design and Implementations (PLDI). 2017.
417. Consistency models with global operation sequencing and their composition
     Alexey Gotsman, Sebastian Burckhardt.
     International Symposium on Distributed Computing (DISC). 2017.
418. Proving linearizability using partial orders
     Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson.
     European Symposium on Programming (ESOP). 2017.
419. Loophole: Timing Attacks on Shared Event Loops in Chrome
     Pepe Vila, Boris Köpf.
     26th USENIX Security Symposium. 2017.
420. A Systematic Study of Cache Side Channels across AES Implementations
     Heiko Mantel, Alexandra Weber, Boris Köpf.
     Proc. 9th International Symposium on Engineering Secure Software and Systems (ESSoS ‘17). 2017.
421. Towards Run-time Checks Simplification via Term Hiding (extended abstract)
     N. Stulova, J.F. Morales, M.V. Hermenegildo.
     Tech. Comm. of ICLP'17. 2017.
422. Algebraic laws for weak consistency
     Andrea Cerone, Alexey Gotsman, Hongseok Yang.
     CONCUR'17: International Conference on Concurrency Theory. 2017.
423. Computer-aided verification for mechanism design
     Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub.
     Proceedings of the 12th Conference on Web and Internet Economics (WINE 2016). diciembre 2016.
424. 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). diciembre 2016.
425. Description and Evaluation of a Generic Design to Integrate CLP and Tabled Execution
     Joaquín Arias, Manuel Carro.
     Proc. of PPDP'16. septiembre 2016.
426. 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). septiembre 2016.
427. 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). septiembre 2016.
428. Reducing the Overhead of Assertion Run-time Checks via Static Analysis
     N. Stulova, J.F. Morales, M.V. Hermenegildo.
     PPDP'16. septiembre 2016.
429. Measuring PUP Prevalence and PUP Distribution through Pay-Per-Install Services
     Platon Kotzias, Leyla Bilge, Juan Caballero.
     Usenix Security Symposium (USENIX-Security). agosto 2016.
430. Automatic Generation of Oracles for Exceptional Behaviors
     Alberto Goffi, Alessandra Gorla, Michael D. Ernst, Mauro Pezzè.
     Proceedings of the 25th International Symposium on Software Testing and Analysis. julio 2016.
431. 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). marzo 2016.
432. 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.
433. Relational Logic with Framing and Hypotheses
     Anindya Banerjee, David A. Schmidt, Mohammad Nikouei.
     Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 2016.
434. 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.
435. A Certified Compiler for Verifiable Computing
     Cédric Fournet, Chantal Keller, Vincent Laporte.
     IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016. 2016.
436. Synthesizing Probabilistic Invariants via Doob's Decomposition
     Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu.
     Computer Aided Verification (CAV). 2016.
437. 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.
438. 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.
439. 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.
440. 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.
441. 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.
442. An Algorithmic Approach to Global Asymptotic Stability Verification of Hybrid Systems
     Pavithra Prabhakar, Miriam García Soto.
     ACM Conference on Embedded Software (EMSOFT). 2016.
443. 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.
444. A Theory of Slicing for Probabilistic Control Flow Graphs
     Torben Amtoft, Anindya Banerjee.
     Foundations of Software Science and Computational Structures (FOSSACS). 2016.
445. 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.
446. 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.
447. Process Compliance Checking using Taint Flow Analysis
     Alexander Seeliger, Timo Nolle, Benedikt Schmidt, Max Mühlhäuser.
     International Conference on Information Systems (ICIS). 2016.
448. 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.
449. 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.
450. 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.
451. 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.
452. 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.
453. 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.
454. 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.
455. Completeness in Approximate Transduction
     Mila Dalla Preda, Roberto Giacobazzi, Isabella Mastroeni.
     Static Analysis Symposium (SAS). 2016.
456. 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.
457. Bounded-oscillation Pushdown Automata
     Pierre Ganty, Damir Valput.
     International Symposium on Games, Automata, Logics and Formal Verification (GandALF). 2016.
458. An abstract memory functor for verified C static analyzers
     Sandrine Blazy, Vincent Laporte, David Pichardie.
     International Conference on Functional Programming (ICFP). 2016.
459. A Source-level Energy Optimization Framework for Mobile Applications
     Xueliang Li, John P. Gallagher.
     16th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2016). 2016.
460. 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.
461. On the (In)security of SNARKs in the Presence of Oracles
     Dario Fiore, Anca Nitulescu.
     Theory of Cryptography Conference (TCC). 2016.
462. Inferring Energy Bounds Statically by Evolutionary Analysis of Basic Blocks
     U. Liqat, Z. Banković, P. Lopez-Garcia, M.V. Hermenegildo.
     (HIP3ES'16). 2016.
463. Counterexample Guided Abstraction Refinement for Stability Analysis
     Pavithra Prabhakar, Miriam García Soto.
     Computer Aided Verification (CAV). 2016.
464. '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.
465. Symbolic Abstract Data Type Inference
     Michael Emmi, Constantin Enea.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2016.
466. Verifying Constant-Time Implementations
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi.
     25th USENIX Security Symposium. 2016.
467. Specification and Complexity of Collaborative Text Editing
     Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, Marek Zawirski.
     PODC'16: Symposium on Principles of Distributed Computing. 2016.
468. 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.
469. A General Framework for Static Profiling of Parametric Resource Usage
     P. Lopez-Garcia, M. Klemen, U. Liqat, M.V. Hermenegildo.
     ICLP. 2016.
470. Hybridization for Stability Analysis of Switched Linear Systems
     Pavithra Prabhakar, Miriam García Soto.
     Proc. of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016. 2016.
471. 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.
     Proc. of FOPARA. 2016.
472. 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.
473. Robustness against Consistency Models with Atomic Visibility
     Giovanni Bernardi, Alexey Gotsman.
     CONCUR'16: International Conference on Concurrency Theory. 2016.
474. Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC
     José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir.
     23rd International Conference on Fast Software Encryption (FSE). 2016.
475. Hoare-style Specifications As Correctness Conditions for Non-linearizable Concurrent Objects
     Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco.
     International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 2016.
476. Analysing Snapshot Isolation
     Andrea Cerone, Alexey Gotsman.
     PODC'16: Symposium on Principles of Distributed Computing. 2016.
477. A Generic Logic for Proving Linearizability
     Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson.
     FM'16: International Symposium on Formal Methods. 2016.
478. Automated Test Input Generation for Android: Are We There Yet?
     Shauvik Roy Choudhary, Alessandra Gorla, Alessandro Orso.
     International Conference on Automated Software Engineering (ASE). noviembre 2015.
479. CARONTE: Detecting Location Leaks for Deanonymizing Tor Hidden Services
     Srdjan Matic, Platon Kotzias, Juan Caballero.
     ACM Conference on Computer and Communications Security (CCS). octubre 2015.
480. Certified PUP: Abuse in Authenticode Code Signing
     Platon Kotzias, Srdjan Matic, Richard Rivera, Juan Caballero.
     ACM Conference on Computer and Communications Security (CCS). octubre 2015.
481. 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). junio 2015.
482. Mining Apps for Abnormal Usage of Sensitive Data
     Vitalii Avdiienko, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller, Steven Arzt, Siegfried Rasthofer, Eric Bodden.
     Proceedings of the 37th International Conference on Software Engineering. mayo 2015.
483. 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.
     Proceedings of the 36th IEEE Symposium on Security and Privacy. mayo 2015.
484. 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). mayo 2015.
485. Automated Proofs of Pairing-based Cryptography
     Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt.
     Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. 2015.
486. Mind the Gap: Modular Machine-checked Proofs of One-round Key Exchange Protocols
     Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt.
     Advances in Cryptology - EUROCRYPT 2015 - 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques. 2015.
487. 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.
488. 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.
489. 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.
490. 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.
491. 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.
492. 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.
493. 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.
494. 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.
495. Model Checking Parameterized Asynchronous Shared-Memory Systems
     Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
     Computer Aided Verification (CAV). 2015.
496. Model-Based Formal Reasoning about Data-Management Applications
     Carolina Dania, Manuel Clavel.
     Fundamental Approaches to Software Engineering - 18th International Conference, FASE 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 2015.
497. Formal Reasoning about Fine-Grained Access Control Policies
     Miguel Ángel García de Dios, Carolina Dania, Manuel Clavel.
     11th Asia-Pacific Conference on Conceptual Modelling, APCCM 2015, Sydney, Australia, January 2015. 2015.
498. Verification of Population Protocols
     Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
     International Conference on Concurrency Theory (CONCUR). 2015.
499. From Non-Zenoness Verification to Termination
     Pierre Ganty, Samir Genaim, Ratan Lal, Pavithra Prabhakar.
     MEMOCODE ‘15: 13th ACM-IEEE Int. Conf. on Formal Methods and Models for System Design. 2015.
500. Interprocedural Reachability for Flat Integer Programs
     Pierre Ganty, Radu Iosif.
     International Symposium on Fundamentals of Computation Theory (FCT). 2015.
501. Analyzing Program Analyses
     Roberto Giacobazzi, Francesco Logozzo, Francesco Ranzato.
     Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 2015.
502. Analyzing First-Order Role Based Access Control
     Carlos Cotrini Jiménez, Thilo Weghorn, David A. Basin, Manuel Clavel.
     IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015. 2015.
503. Tree automata-based refinement with application to Horn clause verification
     Bishoksan Kafle, John P. Gallagher.
     Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings. 2015.
504. Synthesis of Equivalent Method Calls in Guava
     Andrea Mattavelli, Alberto Goffi, Alessandra Gorla.
     Proceedings of the 7th International Symposium on Search-Based Software Engineering. 2015.
505. Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables
     Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia, Isabella Mastroeni.
     Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 2015.
506. Bounded error flowpipe computation of parameterized linear systems
     Ratan Lal, Pavithra Prabhakar.
     Proceedings of the International Conference on Embedded Software (EMSOFT). 2015.
507. ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data
     Michael Backes, Manuel Barbosa, Dario Fiore, Raphael M. Reischuk.
     36th IEEE Symposium on Security and Privacy (Oakland) 2015. 2015.
508. 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.
     The 11th International Conference on Artificial Intelligence Applications and Innovations (AIAI'15). 2015.
509. Improved Energy-aware Stochastic Scheduling based on Evolutionary Algorithms via Copula-based Modeling of Task Dependences
     Z. Banković, P. Lopez-Garcia.
     International Conference on Soft Computing Models in Industrial and Environmental Applications (SOCO 2015). 2015.
510. Energy Efficient Allocation and Scheduling for DVFS-enabled Multicore Environments using a Multiobjective Evolutionary Algorithm
     Z. Banković, P. Lopez-Garcia.
     Proc. of GECCO ‘15. 2015.
511. 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.
512. Transaction chopping for parallel snapshot isolation
     Andrea Cerone, Alexey Gotsman, Hongseok Yang.
     International Symposium on Distributed Computing (DISC). 2015.
513. Composite replicated data types
     Alexey Gotsman, Hongseok Yang.
     European Symposium on Programming (ESOP). 2015.
514. Systematic Asynchrony Bug Exploration for Android Apps
     Burcu Kulahcioglu Ozkan, Michael Emmi, Serdar Tasiran.
     Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 2015.
515. Analysis of Asynchronous Programs with Event-Based Synchronization
     Michael Emmi, Pierre Ganty, Rupak Majumdar, Fernando Rosa-Velardo.
     European Symposium on Programming (ESOP). 2015.
516. On Reducing Linearizability to State Reachability
     Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
     International Colloquium on Automata Languages and Programming (ICALP). 2015.
517. Monitoring Refinement via Symbolic Reasoning
     Michael Emmi, Constantin Enea, Jad Hamza.
     ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2015.
518. Tractable Refinement Checking for Concurrent Objects
     Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2015.
519. 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.
520. Rational Protection Against Timing Attacks
     Goran Doychev, Boris Köpf.
     Proc. 28th IEEE Computer Security Foundations Symposium (CSF'15). 2015.
521. 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.
522. 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.
523. A framework for transactional consistency models with atomic visibility
     Andrea Cerone, Giovanni Bernardi, Alexey Gotsman.
     International Conference on Concurrency Theory (CONCUR). 2015.
524. Pre-Indexed Terms for Prolog
     J.F. Morales, M.V. Hermenegildo.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). 2015.
525. Reasoning about the Trade-off between Security and Performance
     Boris Köpf.
     Proc. 12th International Conference on Quantitative Evaluation of Systems (QEST ‘15). 2015.
526. Symbolic Polytopes for Quantitative Interpolation and Verification
     Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko.
     Proc. 27th International Conference on Computer Aided Verification (CAV ‘15). 2015.
527. 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.
528. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
     Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
     European Symposium on Programming (ESOP). 2015.
529. Mechanized Verification of Fine-grained Concurrent Programs
     Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
     Conference on Programming Language Design and Implementation (PLDI). 2015.
530. 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.
531. 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.
532. 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). diciembre 2014.
533. System-level Non-interference for Constant-time Cryptography
     Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie.
     21st ACM Conference on Computer and Communications Security (CCS 2014). noviembre 2014.
534. 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). noviembre 2014.
535. Synthesis of Fault Attacks on Cryptographic Implementations
     Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz.
     21st ACM Conference on Computer and Communications Security (CCS 2014). noviembre 2014.
536. Transforming Service Compositions into Cloud-Friendly Actor Networks
     Dragan Ivanovic, Manuel Carro.
     International Conference on Service Oriented Computing (ICSOC). noviembre 2014.
537. Towards QoS Prediction Based on Composition Structure Analysis and Probabilistic Models
     Dragan Ivanović, Manuel Carro, Peerachai Kaowichakorn.
     International Conference on Service Oriented Computing (ICSOC). noviembre 2014.
538. WhoWas: A Platform for Measuring Web Deployments on IaaS Clouds
     Liang Wang, Antonio Nappa, Juan Caballero, Thomas Ristenpart, Aditya Akella.
     Internet Measurement Conference (IMC). noviembre 2014.
539. On Combining Backward and Forward Chaining in Constraint Logic Programming
     R. Haemmerlé.
     International Conference on Principles and Practice of Declarative Programming (PPDP). septiembre 2014.
540. Assertion-based Debugging of Higher-Order (C)LP Programs
     N. Stulova, J.F. Morales, M.V. Hermenegildo.
     PPDP'14. septiembre 2014.
541. 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). septiembre 2014.
542. Certified Synthesis of Efficient Batch Verifiers
     Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub.
     Computer Security Foundations Symposium (CSF 2014). julio 2014.
543. Proving differential privacy in Hoare logic
     Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub.
     Computer Security Foundations Symposium (CSF 2014). julio 2014.
544. CyberProbe: Towards Internet-Scale Active Detection of Malicious Servers
     Antonio Nappa, Zhaoyan Xu, Juan Caballero, Guofei Gu.
     Network and Distributed System Security Symposium (NDSS). febrero 2014.
545. 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.
     Computer Security Foundations Symposium (CSF 2014). 2014.
546. Homomorphic Signatures with Efficient Verification for Polynomial Functions
     Dario Catalano, Dario Fiore, Bogdan Warinschi.
     Advances in Cryptology (CRYPTO). 2014.
547. Efficiently Verifiable Computation on Encrypted Data
     Dario Fiore, Rosario Gennaro, Valerio Pastro.
     ACM Conference on Computer and Communications Security (CCS). 2014.
548. Using Higher-Order Contracts to Model Session Types (Extended Abstract)
     Giovanni Bernardi, Matthew Hennessy.
     International Conference on Concurrency Theory (CONCUR). 2014.
549. 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.
550. 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.
551. Switching control of dynamical systems from metric temporal logic specifications
     Jun Liu, Pavithra Prabhakar.
     IEEE International Conference on Robotics and Automation (ICRA). 2014.
552. A Formal Library for Elliptic Curves in the Coq Proof Assistant
     Evmorfia-Iro Bartzia, Pierre-Yves Strub.
     Conference on Interactive Theorem Proving (ITP). 2014.
553. 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.
554. 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.
555. A Logical Analysis of Framing for Specifications with Pure Method Calls
     Anindya Banerjee, David A. Naumann.
     Verified Software: Theories (VSTTE). 2014.
556. Modeling Social Networking Privacy
     Carolina Dania, Manuel Clavel.
     2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, September 1-3, 2014. 2014.
557. 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.
558. Interactive Encryption and Message Authentication
     Yevgeniy Dodis, Dario Fiore.
     Conference on Security and Cryptography for Networks (SCN). 2014.
559. Automated Verification of Group Key Agreement Protocols
     Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin.
     Proceedings of the 2014 IEEE Symposium on Security and Privacy. 2014.
560. Modular, higher-order cardinality analysis in theory and practice
     Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones.
     Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ‘14. 2014.
561. Characterising Testing Preorders for Broadcasting Distributed Systems
     Andrea Cerone, Matthew Hennessy.
     Trustworthy Global Computing. 2014.
562. Leakage Resilience against Concurrent Cache Attacks
     Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa.
     Proc. 3rd Conference on Principles of Security and Trust (POST ‘14). 2014.
563. Visibly Linear Temporal Logic
     Laura Bozzelli, César Sánchez.
     International Joint Conference on Automated Reasoning (IJCAR). 2014.
564. Foundations of Boolean Stream Runtime Verification
     Laura Bozzelli, César Sánchez.
     International Conference on Runtime Verification (RV). 2014.
565. Temporal Logics for Hyperproperties
     Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez.
     Proc. of the 3rd Conference on Principles of Security and Trust (POST 2014). 2014.
566. SMACK: Decoupling Source Language Details from Verifier Implementations
     Zvonimir Rakamaric, Michael Emmi.
     Computer Aided Verification (CAV). 2014.
567. Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS
     Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub.
     Proceedings of the 2014 IEEE Symposium on Security and Privacy. 2014.
568. 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.
569. Replicated data types: specification, verification, optimality
     Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2014.
570. Ordered Counter Abstraction (Refinable Subword Relations for Parameterized Verification)
     Pierre Ganty, Ahmed Rezine.
     International Conference on Language and Automata Theory and Applications (LATA). 2014.
571. 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.
     LOPSTR. 2014.
572. Modular Reasoning about Heap Paths via Effectively Propositional Formulas
     Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv.
     Principles of Programming Languages (POPL). 2014.
573. Parameterised linearisability
     Andrea Cerone, Alexey Gotsman, Hongseok Yang.
     International Colloquium on Automata Languages and Programming (ICALP). 2014.
574. 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.
575. An algorithmic approach to stability verification of polyhedral switched systems
     Pavithra Prabhakar, Miriam Garcia Soto.
     American Control Conference, ACC 2014, Portland, OR, USA, June 4-6, 2014. 2014.
576. 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.
577. LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes
     Alejandro Sánchez, César Sánchez.
     Computer Aided Verification (CAV). 2014.
578. Parametrized Verification Diagrams
     Alejandro Sánchez, César Sánchez.
     International Symposium on Temporal Representation and Reasoning (TIME). 2014.
579. On Duality Relations for Session Types
     Giovanni Bernardi, Ornela Dardha, Simon J. Gay, Dimitrios Kouzapas.
     Trustworthy Global Computing, TGC 2014 Revised Selected Papers. 2014.
580. 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.
581. 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). noviembre 2013.
582. POSTER: Cross-Platform Malware: Write Once, Infect Everywhere
     Martina Lindorfer, Matthias Neumayr, Juan Caballero, Christian Platzer.
     ACM Conference on Computer and Communications Security (CCS). noviembre 2013.
583. 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). octubre 2013.
584. Sized Type Analysis for Logic Programs
     A. Serrano, P. Lopez-Garcia, F. Bueno, M.V. Hermenegildo.
     International Conference on Logic Programming (ICLP). agosto 2013.
585. 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). julio 2013.
586. Supporting Pruning in Tabled LP
     P. Chico de Guzmán, M. Carro, M.V. Hermenegildo.
     Practical Aspects of Declarative Languages (PADL). enero 2013.
587. Reversible Language Extensions and their Application in Debugging
     Z. Drey, J. F. Morales, M.V. Hermenegildo, M. Carro.
     Practical Aspects of Declarative Languages (PADL). enero 2013.
588. 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.
589. 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.
590. 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.
591. 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.
592. 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.
593. 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.
594. Hoare-style reasoning with (algebraic) continuations
     Germán Andrés Delbianco, Aleksandar Nanevski.
     Proceedings of the 18th ACM SIGPLAN international conference on Functional programming. 2013.
595. 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.
596. The TAMARIN Prover for the Symbolic Analysis of Security Protocols
     Simon Meier, Benedikt Schmidt, Cas Cremers, David A. Basin.
     Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. 2013.
597. Monadic abstract interpreters
     Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens.
     Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ‘13. 2013.
598. Genetic Algorithm-based Allocation and Scheduling for Voltage and Frequency Scalable XMOS Chips
     Z. Banković, P. Lopez-Garcia.
     Hybrid Artificial Intelligent Systems (HAIS 2013). 2013.
599. Preventing Side-Channel Leaks in Web Traffic: A Formal Approach
     Michael Backes, Goran Doychev, Boris Köpf.
     Proc. 20th Network and Distributed Systems Security Symposium (NDSS). 2013.
600. Verifying Concurrent Programs Against Sequential Specifications
     Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
     European Symposium on Programming (ESOP). 2013.
601. Library abstraction for C/C++ concurrency
     Mark Batty, Mike Dodds, Alexey Gotsman.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2013.
602. CacheAudit: A Tool for the Static Analysis of Cache Side Channels
     Goran Doychev, Dominik Feld, Boris Köpf, Laurent Mauborgne, Jan Reineke.
     22nd USENIX Security Symposium. 2013.
603. Parameterized Verification of Asynchronous Shared-Memory Systems
     Javier Esparza, Pierre Ganty, Rupak Majumdar.
     Computer Aided Verification (CAV). 2013.
604. Proving Termination Starting from the End
     Pierre Ganty, Samir Genaim.
     Computer Aided Verification (CAV). 2013.
605. 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.
606. Effectively-Propositional Reasoning about Reachability in Linked Data Structures
     Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv.
     Computer Aided Verification (CAV). 2013.
607. Automation of Quantitative Information-Flow Analysis
     Boris Köpf, Andrey Rybalchenko.
     13th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM). 2013.
608. Subjective Auxiliary State for Coarse-Grained Concurrency
     Ruy Ley-Wild, Aleksandar Nanevski.
     Principles of Programming Languages (POPL). 2013.
609. Abstraction Based Model-Checking of Stability of Hybrid Systems
     Pavithra Prabhakar, Miriam Garcia Soto.
     Computer Aided Verification (CAV). 2013.
610. 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.
611. On the decidability of stability of hybrid systems
     Pavithra Prabhakar, Mahesh Viswanathan.
     International Conference on Hybrid Systems: Computation and Control (HSCC). 2013.
612. 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.
613. 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.
614. Verifying Information Flow Properties of Hybrid Systems
     Pavithra Prabhakar, Boris Köpf.
     High Confidence Networked Systems (HiCoNS). 2013.
615. Verifying concurrent memory reclamation algorithms with grace
     Alexey Gotsman, Noam Rinetzky, Hongseok Yang.
     European Symposium on Programming (ESOP). 2013.
616. Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures
     Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski.
     Principles and Practice of Declarative Programming (PPDP). 2013.
617. 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.
618. 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.
619. 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.
620. 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.
621. A Constraint-Based Approach to Quality Assurance in Service Choreographies
     D. Ivanovic, M. Carro, M.V. Hermenegildo.
     International Conference on Service Oriented Computing (ICSOC). noviembre 2012.
622. 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). octubre 2012.
623. Deriving Specifications for Composite Web Services
     George Bariannys, M. Carro, Dimitris Plexousakis.
     International Computer Software and Applications Conference (COMPSAC). julio 2012.
624. 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). julio 2012.
625. A General Implementation Framework for Tabled CLP
     P. Chico de Guzmán, M. Carro, M.V. Hermenegildo, P. Stuckey.
     Int’l. Symposium on Functional and Logic Programming (FLOPS'12). mayo 2012.
626. 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). enero 2012.
627. Towards Abstract Interpretation of Epistemic Logic
     Mai Ajspur, John P. Gallagher.
     8th Scandinavian Logic Symposium, 20-21 August 2012, Roskilde University, Denmark. 2012.
628. A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert
     Gilles Barthe, Delphine Demange, David Pichardie.
     21st European Symposium on Programming, ESOP 2012. 2012.
629. Programming Paradigm Driven Heap Analysis
     Mark Marron, Ondrej Lhoták, Anindya Banerjee.
     International Conference on Compiler Construction (CC). 2012.
630. 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.
631. 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.
632. 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.
633. 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.
634. 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.
635. 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.
636. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs
     Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin.
     Mathematics of Program Construction (MPC). 2012.
637. Verification of Software Barriers
     Alexander Malkis, Anindya Banerjee.
     Principles and Practice of Parallel Programming (PPoPP). 2012.
638. Computer-Aided Cryptographic Proofs
     Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin.
     Static Analysis Symposium (SAS). 2012.
639. Decision Procedures for Region Logic
     Stan Rosenberg, Anindya Banerjee, David A. Naumann.
     13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012). 2012.
640. Verified Indifferentiable Hashing into Elliptic Curves
     Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin.
     1st Conference on Principles of Security and Trust, POST 2012. 2012.
641. Probabilistic Relational Reasoning for Differential Privacy
     Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin.
     Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ‘12). 2012.
642. Automatic Quantification of Cache Side-Channels
     Boris Köpf, Laurent Mauborgne, Martín Ochoa.
     24th International Conference on Computer Aided Verification (CAV ‘12). 2012.
643. Visibly Rational Expressions
     Laura Bozzelli, César Sánchez.
     Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2012.
644. A Perfect Model for Bounded Verification
     Javier Esparza, Pierre Ganty, Rupak Majumdar.
     IEEE Symposium on Logic in Computer Science (LICS). 2012.
645. Non-Monotonic Self-Adjusting Computation
     Ruy Ley-Wild, Umut A. Acar, Guy Blelloch.
     European Symposium on Programming (ESOP). 2012.
646. Linearizability with ownership transfer
     Alexey Gotsman, Hongseok Yang.
     International Conference on Concurrency Theory (CONCUR). 2012.
647. Concurrent library correctness on the TSO memory model
     Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang.
     European Symposium on Programming (ESOP). 2012.
648. Foundations for Approximation Based Analysis of Stability Properties of Hybrid Systems
     Pavithra Prabhakar.
     Allerton Conference on Communication, Control, and Computing (Allerton). 2012.
649. 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.
650. Pre-orders for reasoning about stability
     Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan.
     International Conference on Hybrid Systems: Computation and Control (HSCC). 2012.
651. 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.
652. 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.
653. 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.
654. Show no weakness: sequentially consistent specifications of TSO libraries
     Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang.
     International Symposium on Distributed Computing (DISC). 2012.
655. Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations
     D. Ivanović, M. Carro, M.V. Hermenegildo.
     International Conference on Service Oriented Computing (ICSOC). diciembre 2011.
656. A Machine-Checked Framework for Relational Separation Logic
     Juan Manuel Crespo, César Kunz.
     Software Engineering and Formal Methods - 9th International Conference, SEFM 2011. noviembre 2011.
657. Verifiable Security of Boneh-Franklin Identity-Based Encryption
     Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin.
     5th International Conference on Provable Security – ProvSec 2011. octubre 2011.
658. Computer-Aided Security Proofs for the Working Cryptographer
     Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin.
     Advances in Cryptology – CRYPTO 2011. agosto 2011.
659. Measuring Pay-per-Install: The Commoditization of Malware Distribution
     Juan Caballero, Chris Grier, Christian Kreibich, Vern Paxson.
     Usenix Security Symposium (USENIX-Security). agosto 2011.
660. CLP Projection for Constraint Handling Rules
     R. Haemmerlé, P. Lopez-Garcia, M.V. Hermenegildo.
     International Conference on Principles and Practice of Declarative Programming (PPDP). julio 2011.
661. Modular Extensions for Modular (Logic) Languages
     J. F. Morales, M.V. Hermenegildo, R. Haemmerlé.
     International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). julio 2011.
662. 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). julio 2011.
663. Formally Verifying Isolation and Availability in an Idealized Model of Virtualization
     Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna.
     FM 2011: 17th International Symposium on Formal Methods. junio 2011.
664. Relational Verification Using Product Programs
     Gilles Barthe, Juan Manuel Crespo, César Kunz.
     FM 2011: 17th International Symposium on Formal Methods. junio 2011.
665. A decade of model-driven security
     David A. Basin, Manuel Clavel, Marina Egea.
     ACM Symposium on Access Control Models and Technologies (SACMAT). junio 2011.
666. Applicative Shortcut Fusion
     Germán Andrés Delbianco, Mauro Jaskelioff, Alberto Pardo.
     12th International Symposium on Trends in Functional Programming, TFP'11. mayo 2011.
667. 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). mayo 2011.
668. Beyond Provable Security Verifiable IND-CCA Security of OAEP
     Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin.
     Topics in Cryptology — CT-RSA 2011. febrero 2011.
669. Approximating Petri Net Reachability Along Context-free Traces
     Mohamed Faouzi Atig, Pierre Ganty.
     Foundations of Software Technology and Theoretical Computer Science (FST&TCS). 2011.
670. Complexity Analysis of the Backward Coverability Algorithm for VASS
     Laura Bozzelli, Pierre Ganty.
     Reachability Problems (RP). 2011.
671. Non-Uniform Distributions in Quantitative Information-Flow
     Michael Backes, Matthias Berg, Boris Köpf.
     Proc. 6th ACM Conference on Information, Computer and Communications Security (ASIACCS ‘11). 2011.
672. Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language
     Gilles Barthe, Exequiel Rivas.
     Sixth Trusted Global Computing Conference 2011 (TGC'11). 2011.
673. Information-theoretic Bounds for Differentially Private Mechanisms
     Gilles Barthe, Boris Köpf.
     Proc. 24rd IEEE Computer Security Foundations Symposium (CSF ‘11). 2011.
674. 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 VI (FOSAD 2010). 2011.
675. Third International Workshop on Principles of Engineering Service-Oriented Systems (PESOS 2011)
     M. Carro, D. Karastoyanova, G. A. Lewis, A. Liu.
     ICSE. 2011.
676. Precision and the conjunction rule in concurrent separation logic
     Alexey Gotsman, Josh Berdine, Byron Cook.
     Proceedings of the 27th Conference on the Mathematical Foundations of Programming Semantics (MFPS'11), Pittsburgh, PA, USA. 2011.
677. Complexity of Pattern-based Verification for Multithreaded Programs
     Javier Esparza, Pierre Ganty.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2011.
678. 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.
679. 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.
680. Liveness-Preserving Atomicity Abstraction
     Alexey Gotsman, Hongseok Yang.
     International Colloquium on Automata Languages and Programming (ICALP). 2011.
681. On the Strength of Owicki-Gries for Resources
     Alexander Malkis, Laurent Mauborgne.
     9th Asian Symposium on Programming Languages and Systems (APLAS 2011). 2011.
682. Verification of Information Flow and Access Control Policies with Dependent Types
     Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
     IEEE Symposium on Security and Privacy (S&P). 2011.
683. Profiling for Run-Time Checking of Computational Properties and Performance Debugging in Logic Programs
     E. Mera, T. Trigo, P. Lopez-Garcia, M.V. Hermenegildo.
     PADL. 2011.
684. A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes
     Alejandro Sánchez, César Sánchez.
     NASA Formal Methods (NFM). 2011.
685. Modular verification of preemptive OS kernels
     Alexey Gotsman, Hongseok Yang.
     International Conference on Functional Programming (ICFP). 2011.
686. Partiality, State and Dependent Types
     Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski.
     Typed Lambda Calculi and Applications (TLCA). 2011.
687. Towards Fuzzy Granularity Control in Parallel/Distributed Computing
     T. Trigo, P. Lopez-Garcia, S. Muñoz-Hernandez.
     International Conference on Fuzzy Computation (ICFC 2010). octubre 2010.
688. A Framework for Verification and Debugging of Resource Usage Properties: Resource Usage Verification
     P. Lopez-Garcia, L. Darmawan, F. Bueno.
     Technical Communications of ICLP. julio 2010.
689. Automatic Generation of Smart, Security-Aware GUI Models
     D. Basin, M. Clavel, M. Egea, M. Schläpfer.
     Engineering Secure Software and Systems, 2nd International Symposium, ESSoS 2010, Pisa, Italy, February 3-4, 2010. Proceedings. 2010.
690. 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.
691. A Machine-Checked Formalization of Sigma-Protocols
     Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Gregoire, Sylvain Heraud.
     23rd IEEE Computer Security Foundations Symposium, CSF 2010. 2010.
692. Programming Language Techniques for Cryptographic Proofs
     Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin.
     1st International Conference on Interactive Theorem Proving, ITP 2010. 2010.
693. A Functional Framework for Result Checking
     Gilles Barthe, Pablo Buiras, César Kunz.
     Functional and Logic Programming, 10th International Symposium, FLOPS 2010. 2010.
694. Perspectives in Certificate Translation
     Gilles Barthe, César Kunz.
     Trustworthly Global Computing - 5th International Symposium, TGC 2010. 2010.
695. Computational Indistinguishability Logic
     Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech.
     ACM Conference on Computer and Communications Security (CCS). 2010.
696. Robustness Guarantees for Anonymity
     Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi.
     IEEE Computer Security Foundations Symposium (CSF). 2010.
697. Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions
     David A. Naumann, Anindya Banerjee.
     European Symposium on Programming (ESOP). 2010.
698. A Practical Generic Privacy Language
     Moritz Y. Becker, Alexander Malkis, Laurent Bussard.
     International Conference on Information Systems Security (ICISS). 2010.
699. On the Equality of Probabilistic Terms
     Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte.
     Logic Programming and Automated Reasoning (LPAR). 2010.
700. Thread-Modular Counterexample-Guided Abstraction Refinement
     Alexander Malkis, Andreas Podelski, Andrey Rybalchenko.
     Static Analysis Symposium (SAS). 2010.
701. Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients
     Stan Rosenberg, Anindya Banerjee, David A. Naumann.
     Verified Software: Theories (VSTTE). 2010.
702. 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.
     Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, ICSE 2010, Cape Town, South Africa, 1-8 May 2010. 2010.
703. Certificate Translation for the Verification of Concurrent Programs
     César Kunz.
     Trustworthly Global Computing - 5th International Symposium, TGC 2010. 2010.
704. Speaker Recognition in Encrypted Voice Streams
     Michael Backes, Goran Doychev, Markus Dürmuth, Boris Köpf.
     Proc. 15th European Symposium on Research in Computer Security (ESORICS ‘10). 2010.
705. 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.
706. Bounded Underapproximations
     Pierre Ganty, Benjamin Monmege, Rupak Majumdar.
     Computer Aided Verification (CAV). 2010.
707. Towards Data-Aware QoS-Driven Adaptation for Service Orchestrations
     D. Ivanović, M. Carro, M.V. Hermenegildo.
     IEEE International Conference on Web Services (ICWS). 2010.
708. Automatic Fragment Identification in Workflows Based on Sharing Analysis
     D. Ivanović, M. Carro, M.V. Hermenegildo.
     International Conference on Service Oriented Computing (ICSOC). 2010.
709. Approximation and Randomization for Quantitative Information-Flow Analysis
     Boris Köpf, Andrey Rybalchenko.
     Proc. 23rd IEEE Computer Security Foundations Symposium (CSF ‘10). 2010.
710. Vulnerability Bounds and Leakage Resilience of Blinded Cryptography under Timing Attacks
     Boris Köpf, Geoffrey Smith.
     Proc 23rd. IEEE Computer Security Foundations Symposium (CSF ‘10). 2010.
711. Regular Linear-Time Temporal Logic
     Martin Leucker, César Sánchez.
     International Symposium on Temporal Representation and Reasoning (TIME). 2010.
712. 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.
713. Structuring the verification of heap-manipulating programs
     Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
     Principles of Programming Languages (POPL). 2010.
714. 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.
715. Traceable data types for self-adjusting computation
     Umut A. Acar, Guy E. Blelloch, Ruy Ley-Wild, Kanat Tangwongsan, Duru Türkoglu.
     PLDI. 2010.
716. Decision Procedures for the Temporal Verification of Concurrent Lists
     Alejandro Sánchez, César Sánchez.
     International Conference on Formal Engineering Methods (ICFEM). 2010.
717. Regular Linear Temporal Logic with Past
     César Sánchez, Martin Leucker.
     International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI). 2010.
718. 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). agosto 2009.
719. Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework
     E. Mera, P. Lopez-Garcia, M.V. Hermenegildo.
     ICLP'09. julio 2009.
720. 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). junio 2009.
721. Identification of Logically Related Heap Regions
     Mark Marron, Deepak Kapur, Manuel Hermenegildo.
     International Symposium on Memory Management (ISMM). junio 2009.
722. Towards a Complete Scheme for Tabled Execution Based on Program Transformation
     P. Chico de Guzmán, M. Carro, M.V. Hermenegildo.
     Int’l. Symp. on Practical Aspects of Declarative Languages (PADL'09). enero 2009.
723. Constraint-Based Abstraction of a Model Checker for Infinite State Systems
     Gourinath Banda, John P. Gallagher.
     (Constraint) Logic Programming (WLP). 2009.
724. Formal Certification of Code-Based Cryptographic Proofs
     G. Barthe, B. Grégoire, S. Zanella Béguelin.
     36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009. 2009.
725. Implementing a Direct Method for Certificate Translation
     Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet.
     Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009. 2009.
726. 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.
     Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings. 2009.
727. Non-discriminating Arguments and Their Uses
     Henning Christiansen, John P. Gallagher.
     International Conference on Logic Programming (ICLP). 2009.
728. 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.
729. Vérification d'invariants pour des systèmes spécifiés en logique de réécriture
     Vlad Rusu, Manuel Clavel.
     Vingtièmes Journées Francophones des Langages Applicatifs (JFLA 2009). 2009.
730. Formally Certifying the Security of Digital Signature Schemes
     S. Zanella Béguelin, B. Grégoire, G. Barthe, F. Olmedo.
     30th IEEE Symposium on Security and Privacy, S&P 2009. 2009.
731. Analyzing Real-time Event-driven Programs
     Pierre Ganty, Rupak Majumdar.
     International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). 2009.
732. Verifying Liveness for Asynchronous Programs
     Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko.
     ACM SIGACT Symposium on Principles of Programming Languages (POPL). 2009.
733. 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.
734. A Tabling Implementation Based on Variables with Multiple Bindings
     P. Chico de Guzmán, M. Carro, M.V. Hermenegildo.
     ICLP'09. 2009.
735. A Sketch of a Complete Scheme for Tabled Execution Based on Program Transformation
     P. Chico de Guzmán, M. Carro, M.V. Hermenegildo.
     Int’l. Conference on Logic Programming. diciembre 2008.
736. A High-Level Implementation of Non-Deterministic, Unrestricted, Independent And-Parallelism
     A. Casas, M. Carro, M.V. Hermenegildo.
     International Conference on Logic Programming (ICLP). diciembre 2008.
737. Negative Ternary Set-Sharing
     E. Trias, J. Navas, E. S. Ackley, S. Forrest, M.V. Hermenegildo.
     International Conference on Logic Programming (ICLP). diciembre 2008.
738. Sharing Analysis of Arrays, Collections, and Recursive Structures
     Mark Marron, Mario Méndez-Lojo, Manuel Hermenegildo, Darko Stefanovic, Deepak Kapur.
     ACM WS on Program Analysis for Software Tools and Engineering (PASTE'08). noviembre 2008.
739. Modelling Mash-Up Resources
     Iván Pérez, Ángel Herranz, Susana Muñoz, Juan José Moreno-Navarro.
     13th Conference on Software Engineering and Databases, JISBD'08. octubre 2008.
740. Identification of Heap-Carried Data Dependence Via Explicit Store Heap Models
     Mark Marron, Darko Stefanovic, Deepak Kapur, Manuel Hermenegildo.
     21st Int’l. WS on Languages and Compilers for Parallel Computing (LCPC'08). agosto 2008.
741. Towards Execution Time Estimation in Abstract Machine-Based Languages
     E. Mera, P. Lopez-Garcia, M. Carro, M.V. Hermenegildo.
     PPDP'08. julio 2008.
742. Comparing Tag Scheme Variations Using an Abstract Machine Generator
     J. Morales, M. Carro, M.V. Hermenegildo.
     PPDP'08. julio 2008.
743. Safe Upper-bounds Inference of Energy Consumption for Java Bytecode Applications
     J. Navas, M. Méndez-Lojo, M.V. Hermenegildo.
     NASA LFM'08. abril 2008.
744. Efficient Context-Sensitive Shape Analysis with Graph-Based Heap Models
     Mark Marron, Manuel Hermenegildo, Darko Stefanovic, Deepak Kapur.
     International Conference on Compiler Construction (CC). abril 2008.
745. Towards a High-Level Implementation of Execution Primitives for Unrestricted, Independent And-parallelism
     A. Casas, M. Carro, M.V. Hermenegildo.
     PADL'08. enero 2008.
746. An Improved Continuation Call-Based Implementation of Tabling
     P. Chico de Guzmán, M. Carro, M.V. Hermenegildo, Claudio Silva, Ricardo Rocha.
     PADL'08. enero 2008.
747. 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). enero 2008.
748. A Practical Type Analysis for Verification of Modular Prolog Programs
     P. Pietrzak, J. Correas, G. Puebla, M.V. Hermenegildo.
     PEPM'08. enero 2008.
749. Precise Set Sharing Analysis for Java-style Programs
     M. Méndez-Lojo, M.V. Hermenegildo.
     9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'08). enero 2008.
750. Certificate Translation in Abstract Interpretation
     Gilles Barthe, César Kunz.
     17th European Symposium on Programming, ESOP 2008. 2008.
751. Certified Reasoning in Memory Hierarchies
     Gilles Barthe, César Kunz, Jorge Luis Sacchini.
     Programming Languages and Systems, 6th Asian Symposium, APLAS 2008. 2008.
752. Model-Driven Security in Practice: An Industrial Experience
     M. Clavel, V. Silva, C. Braga, M. Egea.
     Proceedings of Model Driven Architecture - Industrial Track ECMDA-FA ‘08. 2008.
753. 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.
754. Tractable Enforcement of Declassification Policies
     Gilles Barthe, Salvador Cavadini, Tamara Rezk.
     IEEE Computer Security Foundations Symposium (CSF). 2008.
755. Type-Based Termination with Sized Products
     Gilles Barthe, Benjamin Grégoire, Colin Riba.
     Annual Conference on Computer Science Logic (CSL). 2008.
756. Preservation of Proof Pbligations for Hybrid Verification Methods
     Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese.
     SEFM. 2008.

Publicaciones en Workshops con Revisión (150)

1. Demonstrating the Top-Down Solver in a Box (Extended Abstract)
   Marco Ciccalè, José F. Morales, Pedro López-García, Manuel V. Hermenegildo.
   octubre 2026.
2. Towards an Automated Reasoning Tool for Complexity Analysis of Automated Reasoners
   L. Rustenholz, M.V. Hermenegildo, P. Lopez-Garcia, A. Mansutti, F. Ridoux, N. Vazou.
   21st International Workshop on Termination (at FLoC 2026). julio 2026.
3. Dealing with the Elephant in the KV Cache: Video Frame Sampling for Multimodal LLM Inference
   Konstantinos Papaioannou, Thaleia Dimitra Doudali.
   Proceedings of the Sixth European Workshop on Machine Learning and Systems. 2026.
4. Bounding Byzantine Impact in Open CRDT Systems
   Carlos Baquero, Francisco Maia, Abel Dantas, Antonio Fernández Anta, Davide Frey, César Sánchez, Timothé Albouy.
   Proceedings of the 13th International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2026, Edinburgh, Scotland, UK, April 27-30, 2026. 2026.
5. Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
   Marco Ciccalè, Daniel Jurjo, José F. Morales, Pedro López-García, Manuel V. Hermenegildo.
   Actas de las XXV Jornadas de Programación y Lenguajes (PROLE 2026). 2026.
6. Demonstrating the Ciao Prolog Playground
   Marco Ciccalè, Daniela Ferreiro, Daniel Jurjo, José F. Morales, Pedro López-García, Manuel V. Hermenegildo.
   Actas de las XXV Jornadas de Programación y Lenguajes (PROLE 2026). 2026.
7. Multi-Configurable Search Rules in Prolog and Application to Testing
   Daniela Ferreiro, José F. Morales, Pedro López-García, Manuel V. Hermenegildo.
   Actas de las XXV Jornadas de Programación y Lenguajes (PROLE 2026). 2026.
8. Search-Guided Generation of Properties for Program Analyzers
   Daniela Ferreiro.
   Technical Communications of the 41st ICLP. septiembre 2025.
9. Some Enhancements to the Prolog Playground and ALD Notebooks for the Modern Prolog Classroom
   José F. Morales, Daniela Ferreiro, Manuel V. Hermenegildo.
   Proceedings of the 41st ICLP Workshops. septiembre 2025.
10. Measuring Data Pollution in Cryptocurrency Abuse Reporting Services
    Gibran Gomez, Kevin van Liebergen, Davide Sanvito, Giuseppe Siracusano, Roberto Gónzalez, Juan Caballero.
    Jornadas Nacionales de Investigación en Ciberseguridad (JNIC). junio 2025.
11. rustc++: Facilitating Advanced Analysis of Rust Code
    Antonis Louka, Georgios Portokalidis, Elias Athanasopoulos.
    Proceedings of the European Workshop on Systems Security (EUROSEC). abril 2025.
12. Fuzzing Space Communication Protocols
    Stephan Havermans, Lars Baumgaertner, Jussi Roberts, Marcus Wallum, Juan Caballero.
    Workshop on Security of Space and Satellite Systems. febrero 2025.
13. Advancing Workload Management with Foundational Models: Challenges in Time Series Similarity and Interpretability
    Tiemo Bang, Ioannis Roumpos, Sergiy Matusevych, Georgia Christofidi, Yuanyuan Tian, Thaleia Dimitra Doudali.
    Proceedings of the 1st Workshop Connecting Academia and Industry on Modern Integrated Database and AI Systems. 2025.
14. Auditable Shared Objects: From Registers to Synchronization Primitives
    Hagit Attiya, Antonio Fernández Anta, Alessia Milani, Alexandre Rapetti, Corentin Travers.
    Workshop on Distributed Algorithms (WDAG). 2025.
15. Offchain Runtime Verification (for The Tezos Blockchain)
    Margarita Capretto, Martín Ceresa, Felipe Gorostiaga, Fernando Macías, Paloma Pedregal, César Sánchez.
    Computer Security. ESORICS 2024 International Workshops. 2025.
16. Towards a Mechanization of Fraud Proof Games in Lean
    Martín Ceresa, César Sánchez.
    Proc. of the 6th Int’l Workshop on Formal Methods for Blockchains (FMBC 2025). 2025.
17. Setchain Algorithms for Blockchain Scalability (Extended Abstract)
    Arivarasan Karmegam, Gabina Luz Bianchi, Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, César Sánchez.
    Proc. of the 2025 IEEE Int’l Parallel and Distributed Processing Symp. (IPDPS'25 Workshops). 2025.
18. Evaluating the Effect of Improved Indirect Call Resolution on System Call Debloating
    Vidya Lakshmi Rajagopalan, Georgios Portokalidis.
    Proceedings of the Workshop on Forming an Ecosystem Around Software Transformation (FEAST). octubre 2024.
19. Teaching Pure LP with Prolog and a Fair Search Rule
    Manuel V. Hermenegildo, José F. Morales, Pedro Lopez-Garcia.
    Proceedings of the 40th ICLP Workshops. octubre 2024.
20. Clustering-Based Characterization of Database Server Ransom Scams
    Kevin van Liebergen, Gibran Gomez, Srdjan Matic, Juan Caballero.
    Jornadas Nacionales de Investigación en Ciberseguridad (JNIC). junio 2024.
21. Data Redaction in Smart-Contract-Enabled Permissioned Blockchains
    Gennaro Avitabile, Vincenzo Botta, Daniele Friolo, Ivan Visconti.
    Proceedings of the Sixth Distributed Ledger Technology Workshop (DLT 2024), Turin, Italy, May 14-15, 2024. 2024.
22. Toward Using Representation Learning for Cloud Resource Usage Forecasting
    Razine Moundir Ghorab, Thaleia Dimitra Doudali.
    Proceedings of the 2024 Workshop on AI For Systems. 2024.
23. The Importance of Workload Choice in Evaluating LLM Inference Systems
    Konstantinos Papaioannou, Thaleia Dimitra Doudali.
    Proceedings of the 4th Workshop on Machine Learning and Systems. 2024.
24. Do Predictors for Resource Overcommitment Even Predict?
    Georgia Christofidi, Thaleia Dimitra Doudali.
    Proceedings of the 4th Workshop on Machine Learning and Systems. 2024.
25. Towards a rule-based approach for deriving abstract domains
    D. Jurjo, J. F. Morales, P. Lopez-Garcia, M.V. Hermenegildo.
    Technical Communications of the 39th International Conference on Logic Programming (ICLP 2023). julio 2023.
26. Demonstrating (Hybrid) Active Logic Documents and the Ciao Prolog Playground, and an Application to Verification Tutorials
    D. Ferreiro, J.F. Morales, S. Abreu, M.V. Hermenegildo.
    Technical Communications of the 39th International Conference on Logic Programming (ICLP 2023). julio 2023.
27. Solving Recurrence Relations using Machine Learning, with Application to Cost Analysis
    M. Klemen, M.Á. Carreira-Perpiñán, P. Lopez-Garcia.
    Technical Communications of the 39th International Conference on Logic Programming (ICLP 2023). julio 2023.
28. Toward Pattern-Based Model Selection for Cloud Resource Forecasting
    Georgia Christofidi, Konstantinos Papaioannou, Thaleia Dimitra Doudali.
    Proceedings of the 3rd Workshop on Machine Learning and Systems. 2023.
29. 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). diciembre 2022.
30. 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. septiembre 2022.
31. Reactive Synthesis of LTL specifications with Rich Theories
    Andoni Rodríguez, César Sánchez.
    11th Workshop in Synthesis. agosto 2022.
32. An s(CASP) In-Browser Playground based on Ciao Prolog
    G. Garcia-Pradales, J.F. Morales, M.V. Hermenegildo, J. Arias, M. Carro.
    Proceedings of the 38th ICLP Workshops - Goal-directed Execution of Answer Set Programs. agosto 2022.
33. 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). junio 2022.
34. Multi: A Formal Playground for Multi-Smart Contract Interaction
    Martín Ceresa, César Sánchez.
    4th International Workshop on Formal Methods for Blockchains (FMBC 2022). 2022.
35. LightSwap: An Atomic Swap Does Not Require Timeouts at both Blockchains
    Philipp Hoenisch, Subhra Mazumdar, Pedro Moreno-Sanchez, Sushmita Ruj.
    Data Privacy Management, Cryptocurrencies and Blockchain Technology - ESORICS 2022 International Workshops, DPM 2022 and CBT 2022, Copenhagen, Denmark, September 26-30, 2022, Revised Selected Papers. 2022.
36. 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.
37. 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, part of NASA NFM'21). mayo 2021.
38. 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). marzo 2021.
39. 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.
40. s(CASP) for SWI-Prolog
    Jan Wielemaker, Joaquín Arias, Gopal Gupta.
    International Conference on Logic Programming (ICLP). 2021.
41. 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.
    Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2021, Virtual, 28th March 2021. 2021.
42. An application of KLEE to aerospace industrial software
    Juan Francisco García, Daniel Jurjo, Fernando Macías, Jose F. Morales, Alessandra Gorla.
    XX Jornadas de Programación y Lenguajes (PROLE 2021). 2021.
43. 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.
    Proc. 8th Workshop on Horn Clause Verification and Synthesis. 2021.
44. Synchronous and asynchronous stream runtime verification
    César Sánchez.
    Proc. of the 5th ACM Int’l Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21). 2021.
45. 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). septiembre 2020.
46. An Experiment Combining Specialization with Abstract Interpretation
    John P. Gallagher, Robert Glück.
    Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT/HCVS@ETAPS 2020 2020, and 7th Workshop on Horn Clauses for Verification and Synthesis, Dublin, Ireland, 25-26th April 2020. 2020.
47. 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.
    Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT/HCVS@ETAPS 2020 2020, and 7th Workshop on Horn Clauses for Verification and Synthesis, Dublin, Ireland, 25-26th April 2020. 2020.
48. Justifications for Goal-Directed Constraint Answer Set Programming
    Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
    Proceedings 36th International Conference on Logic Programming (Technical Communications). 2020.
49. 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). noviembre 2019.
50. 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). noviembre 2019.
51. 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). noviembre 2019.
52. 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). octubre 2019.
53. 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). octubre 2019.
54. 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). septiembre 2019.
55. 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). septiembre 2019.
56. 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). septiembre 2019.
57. Constraint Answer Set Programming without Grounding and its Applications
    Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
    3rd Int’l. Workshop on the Resurgence of Datalog in Academia and Industry (Datalog 2.0). junio 2019.
58. Transferable Anonymous Payments via TumbleBit in Permissioned Blockchains
    Claudio Ferretti, Alberto Leporati, Luca Mariot, Luca Nizzardo.
    Italian Conference on Cybersecurity (ITASEC). 2019.
59. 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.
60. Release practices for iOS and Android apps
    Daniel Domínguez-Álvarez, Alessandra Gorla.
    International Workshop on App Market Analytics (WAMA). 2019.
61. Specialize in Moderation - Building Application-aware Storage Services using FPGAs in the Datacenter
    Lucas Kuhring, Eva Garcia, Zsolt István.
    11th USENIX Workshop on Hot Topics in Storage and File Systems (HotStorage 19). 2019.
62. 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). septiembre 2018.
63. 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). septiembre 2018.
64. Knowledge Problems in Equational Extensions of Subterm Convergent Theories
    Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen.
    32nd International Workshop on Unification. julio 2018.
65. 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). julio 2018.
66. Towards Incremental and Modular Context-sensitive Analysis
    I. Garcia-Contreras, J. F. Morales, M.V. Hermenegildo.
    Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). julio 2018.
67. Towards Static Performance Guarantees for Programs with Run-time Checks
    M. Klemen, N. Stulova, P. Lopez-Garcia, J. F. Morales, M. V. Hermenegildo.
    Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). julio 2018.
68. StreamChain: Do Blockchains Need Blocks?
    Zsolt István, Alessandro Sorniotti, Marko Vukolić.
    Proceedings of the 2nd Workshop on Scalable and Resilient Infrastructures for Distributed Ledgers. 2018.
69. A Deep Learning Approach to Program Similarity
    Niccolò Marastoni, Roberto Giacobazzi, Mila Dalla Preda.
    Proceedings of the 1st International Workshop on Machine Learning and Software Engineering in Symbiosis. 2018.
70. A certified reference validation mechanism for the permission model of Android
    Gustavo Betarte, Juan Diego Campo, Felipe Gorostiaga, Carlos Luna.
    Pre-proceedings of the 27th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'17). octubre 2017.
71. 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). octubre 2017.
72. Towards a Semantics-Aware Code Transformation Toolchain for Heterogeneous Systems
    Salvador Tamarit, Julio Mariño, Guillermo Vigueras, Manuel Carro.
    Proceedings of XIV Jornadas sobre Programación y Lenguajes (PROLE 2016). septiembre 2017.
73. An Analysis of Pay-per-Install Economics Using Entity Graphs
    Platon Kotzias, Juan Caballero.
    Workshop on the Economics of Information Security (WEIS). junio 2017.
74. Which Broadcast Abstraction Captures k-Set Agreement?
    Damien Imbs, Achour Mostéfaoui, Matthieu Perrin, Michel Raynal.
    Workshop on Distributed Algorithms (WDAG). 2017.
75. 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.
76. On Improving Run-time Checking in Dynamic Languages
    Nataliia Stulova.
    Logic Programming Doctoral Consortium (DC-ICLP). 2017.
77. Towards Run-time Checks Simplification via Term Hiding
    N. Stulova, J. F. Morales, M.V. Hermenegildo.
    Technical Communications of the 33rd International Conference on Logic Programming (ICLP 2017). 2017.
78. 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). noviembre 2016.
79. Checking App User Interfaces Against App Descriptions
    Konstantin Kuznetsov, Vitalii Avdiienko, Alessandra Gorla, Andreas Zeller.
    International Workshop on App Market Analytics (WAMA). noviembre 2016.
80. Tabled CLP for Reasoning over Stream Data
    J. Arias.
    Logic Programming Doctoral Consortium (DC-ICLP). octubre 2016.
81. Program Transformations in the POLCA Project
    Jan Kuper, Lutz Schubert, Kilian Kempf, Colin Glas, Daniel Rubio Bonilla, Manuel Carro.
    Design, Automation, and Testing in Europe. marzo 2016.
82. 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). marzo 2016.
83. Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural Code
    Guillermo Vigueras, Manuel Carro, Salvador Tamarit, Julio Mariño.
    Proceedings of the First International Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016). marzo 2016.
84. Interpolant tree automata and their application in Horn clause verification
    Bishoksan Kafle, John P. Gallagher.
    Computing Research Repository (CoRR). 2016.
85. 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.
86. TASP: Towards Anonymity Sets that Persist
    J. Hayes, C. Troncoso, G. Danezis.
    Workshop on Privacy in the Electronic Society (WPES). 2016.
87. 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.
88. The CISE tool: proving weakly-consistent applications correct
    Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira, Marc Shapiro.
    PAPOC'16: Workshop on the Principles and Practice of Consistency for Distributed Data. 2016.
89. Ayudante: Identifying Undesired Variable Interactions
    Irfan Ul Haq, Juan Caballero, Michael D. Ernst.
    International Workshop on Dynamic Analysis (WODA). octubre 2015.
90. 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). julio 2015.
91. Towards a Generic Interface to Integrate CLP and Tabled Execution (Extended Abstract)
    J. Arias, M. Carro.
    Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, August 31 - September 4, 2015.. 2015.
92. Decomposition by tree dimension in Horn clause verification
    Bishoksan Kafle, John P. Gallagher, Pierre Ganty.
    International Workshop on Verification and Program Transformation (VPT). 2015.
93. Constraint Specialisation in Horn Clause Verification
    Bishoksan Kafle, John P. Gallagher.
    Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015. 2015.
94. An Algorithmic Approach to Stability Verification of Hybrid Systems: A Summary
    Pavithra Prabhakar, Miriam García Soto.
    Symbolic and Numerical Methods for Reachability Analysis, 1st International Workshop, SNR 2015. 2015.
95. 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.
96. A standard theory for the pure lambda-value calculus
    Álvaro García-Pérez, Pablo Nogueira.
    septiembre 2014.
97. Pre-Indexed Terms for Prolog
    J.F. Morales, M.V. Hermenegildo.
    International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR). septiembre 2014.
98. 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). julio 2014.
99. Towards Pre-Indexed Terms
    J.F. Morales, M.V. Hermenegildo.
    14th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS-WLPE 2014). julio 2014.
100. Validation of a Security Metamodel for the Development of Cloud Applications
     Marcos Arjona, Carolina Dania, Marina Egea, Antonio Maña.
     Proceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014.. 2014.
101. 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.
     Proceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014.. 2014.
102. 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.
103. 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.
104. Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
     Bishoksan Kafle, John P. Gallagher.
     Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014. 2014.
105. 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). noviembre 2013.
106. Derivación de intérpretes del cálculo lambda con tipos graduales
     Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey.
     septiembre 2013.
107. 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). septiembre 2013.
108. 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). agosto 2013.
109. 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). agosto 2013.
110. Towards QoS Prediction Based on Composition Structure Analysis and Probabilistic Environment Models
     D. Ivanovic, P. Kaowichakorn, M. Carro.
     5th International Workshop on Principles of Engineering Service-Oriented Systems. mayo 2013.
111. 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.
112. OCL2FOL+: Coping with Undefinedness
     Carolina Dania, Manuel Clavel.
     Proceedings of the MODELS 2013 OCL Workshop co-located with the 16th International ACM/IEEE Conference on Model Driven Engineering Languages and Systems (MODELS 2013), Miami, USA, September 30, 2013. 2013.
113. Fixing idioms: a recursion primitive for applicative DSLs
     Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens.
     Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013. 2013.
114. Acceleration of Communication-Aware Task Mapping Techniques through GPU Computing
     Javier Reyes, Juan M. Orduña, Guillermo Vigueras, Rafael Tornero.
     AINA Workshops. 2013.
115. 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). octubre 2012.
116. Enfoque normal y enfoque spine para reducción en el cálculo lambda puro
     Álvaro García-Pérez, Pablo Nogueira.
     septiembre 2012.
117. 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). septiembre 2012.
118. Reversible Language Extensions and their Application in Debugging
     Z. Drey, J.F. Morales, M.V. Hermenegildo.
     12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS 2012). septiembre 2012.
119. 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). julio 2012.
120. Analyzing Service-Oriented Systems Using Their Data and Structure
     D. Ivanovic, M. Carro, M.V. Hermenegildo.
     European Software Services and Systems Research – Results and Challenges (ICSE Workshop). julio 2012.
121. Research Challenges on Service Technology Foundations
     D. Karastoyanova, Z. Nemeth, M. Carro, D. Ivanovic, C. Pautasso, C. Di Napoli, M. Giordano.
     European Software Services and Systems Research – Results and Challenges (ICSE Workshop). julio 2012.
122. 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.
     Proceedings of the 4th International Workshop on Principles of Engineering Service-Oriented Systems, PESOS 2012. junio 2012.
123. Modeling Social Networking Privacy
     Carolina Dania.
     ESSoS-DS 2012. Doctoral Symposium. 2012.
124. A General Implementation Framework for Tabled CLP
     M. Carro, M.V. Hermenegildo, P. Stuckey.
     Jornadas sobre Programación y Lenguajes (PROLE). 2012.
125. 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.
126. 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.
127. Behavior Based Service Composition
     Fangzhe Chang, Pavithra Prabhakar, Ramesh Viswanathan.
     Web Services and Formal Methods - 8th International Workshop, WS-FM 2011, Clermont-Ferrand, France, September 1-2, 2011, Revised Selected Papers. 2012.
128. Estrategias del cálculo lambda e interderivación de artefactos semánticos
     Álvaro García-Pérez, Pablo Nogueira.
     septiembre 2011.
129. 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). septiembre 2011.
130. 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). mayo 2011.
131. 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.
132. El Cubo Beta
     Álvaro García-Pérez.
     septiembre 2010.
133. An Initial Proposal for Data-Aware Resource Analysis of Orchestrations with Applications to Predictive Monitoring
     D. Ivanović, M. Carro, M.V. Hermenegildo.
     International Workshops, ICSOC/ServiceWave 2009, Revised Selected Papers. septiembre 2010.
134. 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). julio 2010.
135. 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.
136. Modeling Concurrent Systems with Shared Resources
     A. Herranz, J. Mariño, M. Carro, J.J. Moreno-Navarro.
     14th International Workshop on Formal Methods for Industrial Critical Systems. noviembre 2009.
137. 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+). noviembre 2009.
138. Program Parallelization using Synchronized Pipelining
     L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo.
     Pre-proceedings of the 19th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'09). septiembre 2009.
139. Towards Structured State Threading in Prolog
     D. Ivanović, J.F. Morales, M. Carro, M.V. Hermenegildo.
     CICLOPS 2009. julio 2009.
140. User-Definable Resource Usage Bounds Analysis for Java Bytecode
     J. Navas, M. Méndez-Lojo, M.V. Hermenegildo.
     Electronic Notes in Theoretical Computer Science – Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09). marzo 2009.
141. 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.
142. 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). diciembre 2008.
143. 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.
     VIII Jornadas sobre Programación y Lenguajes, PROLE 2008. octubre 2008.
144. 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). septiembre 2008.
145. Efficient Set Sharing using ZBDDs
     M. Méndez-Lojo, O. Lhoták, M.V. Hermenegildo.
     21st Int’l. WS on Languages and Compilers for Parallel Computing (LCPC'08). agosto 2008.
146. 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. julio 2008.
147. Safe Upper-bounds Inference of Energy Consumption for Java Bytecode Applications
     J. Navas, M. Méndez-Lojo, M.V. Hermenegildo.
     The Sixth NASA Langley Formal Methods Workshop (LFM 08). abril 2008.
148. 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). enero 2008.
149. Certificate Translation for Specification-Preserving Advices
     Gilles Barthe, César Kunz.
     Proceedings of the 7th Workshop on Foundations of Aspect-Oriented Languages, FOAL 2008. 2008.
150. 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.

Tesis Doctorales (56)

1. A Uniform Approach to Language Containment Problems
   Kyveli Doveri.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pierre Ganty. abril 2024.
2. Succinct Cryptographic Commitments with Fine-Grained Openings for Decentralized Environments
   Dimitris Kolonelos.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Dario Fiore. diciembre 2023.
3. Visibility and Separability for Declarative Proofs of Linearizability
   Jesús Héctor Domínguez Sánchez.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Aleksandar Nanevski. diciembre 2023.
4. Compositional Reasoning of Concurrency with the Visibility Method
   Joakim Öhman.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Aleksandar Nanevski. diciembre 2023.
5. An Automated Framework for Cybersecurity Attribution and Artifact Relationship Identification
   Silvia Sebastián.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero. septiembre 2023.
6. 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. septiembre 2022.
7. 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. mayo 2022.
8. 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. julio 2021.
9. Relational logics for higher-order effectful programs
   Alejandro Aguirre Galindo.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Gilles Barthe. noviembre 2020.
10. 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. noviembre 2020.
11. On the Interaction Between Linear Codes, Secret Sharing, and Multiparty Computation
    Jaron Skovsted Gundersen.
    PhD Thesis. Aalborg University (Denmark). Supervisors: Ignacio Cascudo, Diego Ruano, Horia Cornean, Olav Geil. octubre 2020.
12. On the Use of Quasiorders in Formal Language Theory
    Pedro Valero Mejía.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pierre Ganty. julio 2020.
13. New Perspectives on Classical Automata Constructions
    Elena Gutiérrez Viedma.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pierre Ganty. junio 2020.
14. Learning secrets and models from execution time
    José Vila Bausili.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Boris Koepf. junio 2020.
15. 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. diciembre 2019.
16. 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. noviembre 2019.
17. Lineage Inference of Packed Malware using Binary Code Similarity
    Irfan Ul Haq.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero. septiembre 2019.
18. Understanding the Evolution of Android Applications
    Paolo Calciati.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla. septiembre 2019.
19. 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. mayo 2019.
20. A tale of SNARKs: quantum resilience, knowledge extractability and data privacy
    Anca Nitulescu.
    PhD Thesis. Ecole Normale Superieure (France). Supervisors: David Pointcheval, Dario Fiore, Michel Abdalla. abril 2019.
21. On the Security of Cache Algorithms
    Pablo Cañones Martín.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Boris Koepf. marzo 2019.
22. Tools for the Detection and Analysis of Potentially Unwanted Programs
    Richard Rivera Guevara.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero. noviembre 2018.
23. Be More and Be Merry: Enhancing Data and User Authentication in Collaborative Settings
    Elena Pagnin.
    PhD Thesis. Chalmers University of Technology (Sweden). Supervisors: Andrei Sabelfeld, Dario Fiore. septiembre 2018.
24. Automated Analysis of Cryptographic Constructions
    Miguel Ambrona.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Gilles Barthe. septiembre 2018.
25. Proving Consistency of Concurrent Data Structures and Transactional Memory Systems
    Artem Khyzha.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alexey Gotsman. julio 2018.
26. 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. julio 2018.
27. Improving Run-time Checking in Dynamic Programming Languages
    Nataliia Stulova.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Jose Francisco Morales, Manuel Hermenegildo. abril 2018.
28. Cryptographic Techniques for the Security of Cloud and Blockchain Systems
    Luca Nizzardo.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Dario Fiore. marzo 2018.
29. An Algorithmic Approach for Stability Verification of Hybrid Systems
    Miriam García Soto.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pravithra Prabhakar. agosto 2017.
30. 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. julio 2017.
31. 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. junio 2017.
32. Detecting, Diagnosing and Fixing Energy Issues for Mobile Applications
    Xueliang Li.
    PhD Thesis. Roskilde University (Roskilde U.). Supervisors: John Gallagher. junio 2017.
33. 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. febrero 2017.
34. Components for Automatic Horn Clause Verification
    Bishoksan Kafle.
    PhD Thesis. Roskilde University (Roskilde U.). Supervisors: John Gallagher. junio 2016.
35. 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. mayo 2016.
36. Automation and Modularity of Cryptographic Proofs in the Computational Model
    Juan Manuel Crespo.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Gilles Barthe. mayo 2016.
37. 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. febrero 2016.
38. Formally Verified Countermeasures Against Cache Based Attacks in Virtualization Platforms
    Juan Campo.
    PhD Thesis. Universidad de la República (UDELAR). Supervisors: Gilles Barthe, Gustavo Betarte. octubre 2015.
39. 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. septiembre 2015.
40. Model-driven Development of Secure Data-Management Applications
    Miguel Ángel García de Dios.
    PhD Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Manuel Clavel. abril 2015.
41. A Formalization of Elliptic Curves for Cryptography
    Evmorfia-Iro Bartzia.
    PhD Thesis. Université Paris-Saclay (Universite Paris-Saclay). Supervisors: M. Karthikeyan Bhargavan, Pierre-Yves Strub. febrero 2015.
42. 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. septiembre 2014.
43. Approximate Relational Reasoning for Probabilistic Programs
    Federico Olmedo.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Gilles Barthe. enero 2014.
44. Tableau-Based Decision Procedures for Epistemic and Temporal Epistemic Logics
    Mai Ajspur.
    PhD Thesis. Roskilde University (Roskilde U.). Supervisors: John Gallagher. octubre 2013.
45. Analysis of Service-Oriented Computing Systems
    Dragan Ivanovic.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro. enero 2013.
46. 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. noviembre 2012.
47. Formal Certification of Game-Based Cryptographic Proofs
    Santiago Zanella.
    PhD Thesis. École Nationale Supérieure des Mines de Paris (Mines ParisTech). Supervisors: Gilles Barthe. diciembre 2010.
48. A Unified Framework for Resource and Execution Time Analysis, Run-Time Checking and Unit-Testing
    Edison Fernando Mera Menéndez.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Pedro Lopez. noviembre 2010.
49. Modelling and Analysis of Real Time Systems with Logic Programming and Constraints
    Gourinath Banda.
    PhD Thesis. Roskilde University (Roskilde U.). Supervisors: John Gallagher. agosto 2010.
50. Advanced Compilation Techniques for Logic Programming
    José Francisco Morales Caballero.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro, Manuel Hermenegildo. julio 2010.
51. Técnicas Avanzadas de Compilación para Programación Lógica
    J.F. Morales.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). julio 2010.
52. 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. febrero 2009.
53. Automatic Unrestricted Independent And-Parallelism in Declarative Multiparadigm Languages
    Amadeo Casas.
    PhD Thesis. The University of New Mexico (UNM). Supervisors: Manuel Hermenegildo, Manuel Carro. diciembre 2008.
54. Analysis and Inference of Resource Usage Information
    Jorge A. Navas Laserna.
    PhD Thesis. The University of New Mexico (UNM). Supervisors: Manuel Hermenegildo. diciembre 2008.
55. A Generic Approach to Bytecode Analysis
    Mario Méndez-Lojo.
    PhD Thesis. The University of New Mexico (UNM). Supervisors: Manuel Hermenegildo. diciembre 2008.
56. Una Semántica Formal Ejecutable para OCL con Aplicaciones al Análisis y a la Validación de Modelos
    Marina Egea González.
    PhD Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Manuel Clavel. junio 2008.

Tesis de Master (67)

1. Towards Verification of Higher-Order (Constraint) Logic Programs via Abstract Interpretation
   Marco Ciccalè.
   MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. julio 2025.
2. Alternating finite automata through the lens of quasiorders: canonical representation and Angluin-style learning
   Elia Scandaletti.
   MSc Thesis. Università degli Studi di Padova (U. Padua). Supervisors: Francesco Ranzato, Pierre Ganty, Francesco Ranzato. septiembre 2024.
3. Enhancing System Security Through Static Analysis by Detecting Dormant Vulnerabilities
   Fatih Durmaz.
   MSc Thesis. Université Bretagne Sud (UBS). Supervisors: Georgios Portokalidis. septiembre 2024.
4. Efficient polynomial evaluations with preprocessing and applications to cryptography
   Mario Carrillo Redondo.
   MSc Thesis. Universidad Complutense Madrid (UCM). Supervisors: Dario Fiore, Ignacio Cascudo, Albert Rubio. junio 2024.
5. Learning Memory Access Patterns Using Machine Learning and Computer Vision
   Aristotelis Sympetheros.
   MSc Thesis. National Technical University of Athens (NTUA). Supervisors: Thaleia Dimitra Doudali, Panayiotis Tsanakas. marzo 2024.
6. A Framework for the Analysis of File Infection Malware
   Lorenzo Ippolito.
   MSc Thesis. EURECOM (EURECOM). Supervisors: Juan Caballero, Davide Balzarotti. marzo 2024.
7. Algebraic Contingent Payment and Applications
   Javier Gomez Martinez.
   MSc Thesis. Universidad Complutense Madrid (UCM). Supervisors: Pedro Moreno-Sanchez, Dario Fiore, Albert Rubio. enero 2024.
8. In-depth analysis of the Android supply chain:Vendor customizations on critical networking components
   Rathnayaka Mudiyanselage Vinuri Gayanthika Bandara.
   MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Srdjan Matic, Narseo Vallina-Rodriguez. julio 2023.
9. Covre: Implementation of Code Coverage in a Black-Box CPU Fuzzer for Speculative Leakage Study
   Elvira Moreno Sánchez.
   MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Marco Guarnieri, Jorge Blasco Arias. junio 2023.
10. 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. julio 2022.
11. 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. julio 2022.
12. Forecasting Cloud Resource Utilization Using Machine Learning and Computer Vision
    Javier Galindos.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Thaleia Dimitra Doudali. junio 2022.
13. Hadesius: Una soluzione per il controllo e il monitoraggio del perimetro cibernetico nazionale
    Andrea Colato.
    MSc Thesis. Universita degli Studi di Milano (UNIMI). Supervisors: Stelvio Cimato, Dario Fiore. octubre 2021.
14. Empirical Analysis of Trace-ability in the Lightning Network
    Meresa Gebrewahd.
    MSc Thesis. Sapienza University of Rome (Sapienza). Supervisors: Pedro Moreno-Sanchez, Angelo Spognardi. octubre 2021.
15. The Temporal Booleanization Theorem: realizability checking over numerical-LTL industrial requirements
    Andoni Rodriguez.
    MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Cesar Sanchez. septiembre 2021.
16. 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. septiembre 2021.
17. Abstract Domain for Floating-point Programs
    Daniel Jurjo Rivas.
    MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. julio 2021.
18. An Integrated Approach to Assertion-Based Random Testing in Logic Languages
    Ignacio Casso.
    MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. julio 2021.
19. Improvements to Parametric Cost Analysis and its Application to Smart Contracts
    Víctor Pérez Carrasco.
    MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. julio 2021.
20. Adaptor Signature Based Atomic Swaps Between Bitcoin and a Mimblewimble Based Cryptocurrency
    Jakob Abfalter.
    MSc Thesis. Technical University of Vienna (TUW). Supervisors: Pedro Moreno-Sanchez, Matteo Maffei. junio 2021.
21. 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. septiembre 2020.
22. Simulation-based Inclusion Checking Algorithms for ω-Languages
    Francesco Parolini.
    MSc Thesis. Università degli Studi di Padova (U. Padua). Supervisors: Francesco Ranzato, Pierre Ganty, Francesco Ranzato. julio 2020.
23. 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. septiembre 2019.
24. Homomorphic Signatures over Lattices
    Stefano Ottolenghi.
    MSc Thesis. Universita degli Studi di Genova (UNIGE). Supervisors: Dario Fiore, Giovanni Lagorio. septiembre 2019.
25. 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. julio 2019.
26. 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. julio 2019.
27. 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. junio 2019.
28. 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. junio 2019.
29. 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. enero 2019.
30. 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. septiembre 2018.
31. 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. julio 2018.
32. 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. julio 2018.
33. Decentralised Stream Runtime Verification
    Luis Miguel Danielsson.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Cesar Sanchez, Clara Benac Earle. julio 2018.
34. Microarchitecture Simulation for Security
    Paloma Pedregal Helft.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Boris Koepf, Clara Benac. julio 2018.
35. Security of Cache Replacement Policies under Side-Channel Attacks
    Felix Schroeder.
    MSc Thesis. Technical University Berlin (TU Berlin). Supervisors: Boris Koepf, Martin Skutella. marzo 2018.
36. 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. octubre 2017.
37. Study on Privacy of Parental Control Mobile Applications
    Álvaro Feal Fajardo.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Carmela Troncoso, Manuel Carro. julio 2017.
38. ClaimChain: Decentralized Public Key Infrastructure
    Bogdan Kulynych.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Carmela Troncoso, Manuel Carro. julio 2017.
39. 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. julio 2017.
40. 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. abril 2017.
41. 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. marzo 2017.
42. An Asynchronous Evaluation Engine for Stream Based Specifications
    Alexander Schramm.
    MSc Thesis. Universität zu Lübeck (Luebeck University). Supervisors: Cesar Sanchez, Martin Leucker. noviembre 2016.
43. Code Search: A Semantic, Abstract Interpretation-Based Approach
    Isabel Garcia-Contreras.
    MSc Thesis. Technical University of Madrid, School of Computer Science. julio 2016.
44. Privacy Implications of Open Data
    Hasser Veramendi Salazar.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Carmela Troncoso. julio 2016.
45. 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. julio 2015.
46. 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. julio 2015.
47. 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. julio 2015.
48. A Framework for Implementing Outsourcing Schemes
    Rosario Sebastiano Russo.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Dario Fiore, Manuel Carro. julio 2015.
49. Testing of Android Testing Tools: Development of a Benchmark for the Evaluation
    Tahir Javaid.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alessandra Gorla, Ricardo Imbert. julio 2015.
50. Concurrent Library Abstraction Without Information Hiding
    Artem Khyzha.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Alexey Gotsman, Manuel Carro. julio 2014.
51. An Empirical Study of Techniques to Detect Reverse Proxies and Load Balancers in HTTP Traffic
    Irfan Khan Tanoli.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero, Ricardo Imbert. junio 2014.
52. Análisis de Características Estáticas de Ficheros Ejecutables para la Clasificación de Malware
    Richard Rivera Guevara.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Juan Caballero. junio 2014.
53. Relational Domains for the Quantification of Cache Side Channels
    Dominik Feld.
    MSc Thesis. Saarland University (Saarland University). Supervisors: Boris Koepf, Jan Reineke. septiembre 2013.
54. 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. julio 2013.
55. Integrated Versioning and Collaboration Process Management of Automotive Production Lines Based on an Artifact-Centric Collaboration Environment
    Olena Kutsenko.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Michael Unterkalmsteiner, Manuel Carro. octubre 2012.
56. Probabilistic Analysis of Quality of Service
    Peerachai Kaowichakorn.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Stefanie Betz, Manuel Carro. octubre 2012.
57. Developing Secure Business Applications From Secure BPMN Models
    Javier Valdazo Parnisari.
    MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Manuel Clavel. septiembre 2012.
58. Sistema de Soporte a la Decisión de Programas de Intercambio
    Manuel José Llamas Rodríguez.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro. septiembre 2012.
59. Typegrapher: Inferring the Type Graph of a Binary Program
    Gustavo Grieco.
    MSc Thesis. Universidad Nacional de Rosario (UNR). Supervisors: Juan Caballero. agosto 2012.
60. Diseño de un Configurador de Productos
    Santiago Alfaro Tornero.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Carro. julio 2012.
61. 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. julio 2012.
62. Analysis and Mitigation of Information Leaks in Web Browsing Traffic
    Goran Doychev.
    MSc Thesis. Saarland University (Saarland University). Supervisors: Boris Koepf, Michael Backes. junio 2012.
63. MySQL4OCL:un compilador de OCL a MySQL
    Carolina Inés Dania Flores.
    MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Marina Egea, Manuel Clavel. noviembre 2011.
64. 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. septiembre 2011.
65. 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. julio 2011.
66. 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. septiembre 2010.
67. Exploring the beta-hypercube
    Álvaro García-Pérez.
    MSc Thesis. Facultad de Informática, Universidad Politécnica de Madrid. septiembre 2009.