Articles in Refereed Journals (23)

1. Replicomment: identifying clones in code comments
   Arianna Blasi, Nataliia Stulova, Alessandra Gorla, Oscar Nierstrasz.
   Journal of Systems and Software 182. December 2021.
2. MeMo: Automatically identifying metamorphic relations in Javadoc comments for test automation
   Arianna Blasi, Alessandra Gorla, Michael D. Ernst, Mauro Pezzè, Antonio Carzaniga.
   Journal of Systems and Software 181. November 2021.
3. Complete Abstractions for Checking Language Inclusion
   Pierre Ganty, Francesco Ranzato, Pedro Valero.
   ACM Transactions on Computational Logic 22 (4). Association for Computing Machinery, September 2021.
4. VeriFly: On-the-fly Assertion Checking via Incrementality
   M.A. Sanchez-Ordaz, I. Garcia-Contreras, V. Perez-Carrasco, J. F. Morales, P. Lopez-Garcia, M.V. Hermenegildo.
   Theory and Practice of Logic Programming 21 (6), 768–784. Cambridge U. Press, September 2021.
5. Contextual Modal Types for Algebraic Effects and Handlers
   Nikita Zyuzin, Aleksandar Nanevski.
   International Conference on Functional Programming 5 (ICFP). Association for Computing Machinery, August 2021.
6. A Survey of Binary Code Similarity
   Irfan Ul Haq, Juan Caballero.
   ACM Computing Surveys 54 (3). April 2021.
7. Incremental and Modular Context-sensitive Analysis
   I. Garcia-Contreras, J. F. Morales, M.V. Hermenegildo.
   Theory and Practice of Logic Programming 21 (2), 196–243. January 2021.
8. Hardware security without secure hardware: How to decrypt with a password and a server
   Olivier Blazy, Laura Brouilhet, Celine Chevalier, Patrick Towa, Ida Tucker, Damien Vergnaud.
   Electronic Notes in Theoretical Computer Science 895, 178-211. 2021.
9. A note on secure multiparty computation via higher residue symbols
   Ignacio Cascudo, Reto Schnyder.
   Journal of Mathematical Cryptology 15 (1), 284–297. 2021.
10. A pre-expectation calculus for probabilistic sensitivity
    Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.
    ACM SIGACT Symposium on Principles of Programming Languages 5 ({POPL}), 1–28. 2021.
11. 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.
12. On algebraic abstractions for concurrent separation logics
    Františsek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas.
    ACM SIGACT Symposium on Principles of Programming Languages 5 ({POPL}), 1–32. 2021.
13. 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.
14. 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.
15. Preface
    John P. Gallagher, Martin Sulzmann.
    Science of Computer Programming 202, 102577. 2021.
16. 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.
17. Refinement Types: A Tutorial
    Ranjit Jhala, Niki Vazou.
    Foundations and Trends® in Programming Languages 6 (3–4), 159-317. 2021.
18. A compiler for multi-key homomorphic signatures for Turing machines
    Somayeh Dolatnezhad Samarin, Dario Fiore, Daniele Venturi, Morteza Amini.
    Electronic Notes in Theoretical Computer Science 889, 145-170. 2021.
19. 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.
20. Multi-Shot Distributed Transaction Commit
    Gregory Chockler, Alexey Gotsman.
    Distributed Computing 34 (4), 301–318. Springer, 2021.
21. Specification and Space Complexity of Collaborative Text Editing
    Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, Marek Zawirski.
    Electronic Notes in Theoretical Computer Science 855, 141–160. Elsevier, 2021.
22. 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.
23. 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.

Articles in Refereed Conferences (43)

1. Lunar: a Toolbox for More Efficient Universal and Updatable zkSNARKs and Commit-and-Prove Extensions
   Matteo Campanelli, Antonio Faonio, Dario Fiore, Anaïs Querol, Hadrián Rodriguez.
   International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). December 2021.
2. Generalized Bitcoin-Compatible Channels
   Lukas Aumayr, Oguzhan Ersoy, Andreas Erwig, Sebastian Faust, Kristina Hostáková, Matteo Maffei, Pedro Moreno-Sanchez, Siavash Riahi.
   International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT). December 2021.
3. Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
   Lukas Aumayr, Pedro Moreno-Sanchez, Aniket Kate, Matteo Maffei.
   Usenix Security Symposium (USENIX-Security). August 2021.
4. STORM: Refinement Types for Secure Web Applications
   Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala.
   Usenix Symposium on Operating Systems Design and Implementation (OSDI). July 2021.
5. A2L: Anonymous Atomic Locks for Scalability and Interoperability in Payment Channel Hubs
   Erkan Tairi, Pedro Moreno-Sanchez, Matteo Maffei.
   IEEE Symposium on Security and Privacy (SP). May 2021.
6. How Did That Get In My Phone? Unwanted App Distribution on Android Devices
   Platon Kotzias, Juan Caballero, Leyla Bilge.
   IEEE Symposium on Security and Privacy (SP). May 2021.
7. Bitcoin-Compatible Virtual Channels
   Lukas Aumayr, Oguzhan Ersoy, Andreas Erwig, Sebastian Faust, Kristina Hostáková, Matteo Maffei, Pedro Moreno-Sanchez, Siavash Riahi.
   IEEE Symposium on Security and Privacy (SP). May 2021.
8. 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.
9. 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.
10. 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.
11. Secure Compilation of Constant-Resource Programs
    Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie.
    IEEE Computer Security Foundations Symposium (CSF). 2021.
12. 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.
13. 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.
14. 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.
15. 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.
16. Selectively Linkable Group Signatures - Stronger Security and Preserved Verifiability
    Ashley Fraser, Lydia Garms, Anja Lehmann.
    International Conference on Cryptology and Network Security (CANS). 2021.
17. Decomposing Permutation Automata
    Ismaël Jecker, Nicolas Mazzocchi, Petra Wolf.
    International Conference on Concurrency Theory (CONCUR). 2021.
18. Regular Path Clauses and Their Application in Solving Loops
    Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro López-García, José F. Morales.
    Computing Research Repository (CoRR). 2021.
19. 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.
20. 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.
21. I Told You Tomorrow: Practical Time-Locked Secrets Using Smart Contracts
    Enrico Bacis, Dario Facchinetti, Marco Guarnieri, Marco Rosa, Matthew Rossi, Stefano Paraboschi.
    International Conference on Availability, Reliability and Security (ARES). 2021.
22. Knowledge-driven Natural Language Understanding of English Text and its Applications
    Kinjal Basu, Sarat Varanasi, Farhad Shakerin, Joaquin Arias, Gopal Gupta.
    National Conference of the American Association for Artificial Intelligence (AAAI). 2021.
23. A Temporal Logic for Asynchronous Hyperproperties
    Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez.
    Computer Aided Verification (CAV). 2021.
24. Asynchronous Extensions of HyperLTL
    Laura Bozzelli, Adriano Peron, César Sánchez.
    IEEE Symposium on Logic in Computer Science (LICS). 2021.
25. UniStore: A fault-tolerant marriage of causal and strong consistency
    Manuel Bravo, Alexey Gotsman, Borja de Régil, Hengfeng Wei.
    Usenix Annual Technical Conference (USENIX). 2021.
26. 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.
27. Reachability in Distributed Memory Automata
    Benedikt Bollig, Fedor Ryabinin, Arnaud Sangnier.
    29th EACSL Annual Conference on Computer Science Logic (CSL 2021). 2021.
28. 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.
29. 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.
30. 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.
31. 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.
32. HLola: a Very Functional Tool for Extensible Stream Runtime Verification
    Felipe Gorostiaga, César Sánchez.
    International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2021.
33. HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams
    Felipe Gorostiaga, César Sánchez.
    International Symposium on Formal Methods (FM). 2021.
34. Nested Monitors: Monitors as Expressions to Build Monitors
    Felipe Gorostiaga, César Sánchez.
    International Conference on Runtime Verification (RV). 2021.
35. Hardware-Software Contracts for Secure Speculation
    Marco Guarnieri, Boris Köpf, Jan Reineke, Pepe Vila.
    IEEE Symposium on Security and Privacy (SP). 2021.
36. Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming
    Brendan Hall, Sarat Chandra Varanasi, Jan Fiedor, Joaquín Arias, Kinjal Basu, Fang Li, Devesh Bhatt, Kevin Driscoll, Elmer Salazar, Gopal Gupta.
    Computing Research Repository (CoRR). 2021.
37. Bounded Model Checking for Hyperproperties
    Tzu-Han Hsu, César Sánchez, Borzoo Bonakdarpour.
    International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). 2021.
38. 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.
39. Exorcising Spectres with Secure Compilers
    Marco Patrignani, Marco Guarnieri.
    ACM Conference on Computer and Communications Security (CCS). 2021.
40. Synchronous and asynchronous stream runtime verification
    César Sánchez.
    International Symposium on Software Testing and Analysis (ISSTA). 2021.
41. Efficient replication via timestamp stability
    Vitor Enes, Carlos Baquero, Alexey Gotsman, Pierre Sutra.
    Eurosys Conference (EuroSys). 2021.
42. 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.
43. Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions
    Sebastián Zudaire, Felipe Gorostiaga, César Sánchez, Gerardo Schneider, Sebastián Uchitel.
    IEEE International Conference on Robotics and Automation (ICRA). 2021.

Publications in Refereed Workshops (5)

1. 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). May 2021.
2. Incremental and Modular Context-sensitive Analysis
   I. Garcia-Contreras, J. F. Morales, M.V. Hermenegildo.
   Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021). March 2021.
3. 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.
4. s(CASP) for SWI-Prolog
   Jan Wielemaker, Joaquín Arias, Gopal Gupta.
   International Conference on Logic Programming (ICLP). 2021.
5. 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.

Ph.D. Theses (1)

1. A Scalable Static Analysis Framework for Reliable Program Development Exploiting Incrementality and Modularity
   Isabel García Contreras.
   PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Manuel Hermenegildo, Jose Francisco Morales. July 2021.

Master's Theses (8)

1. 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. October 2021.
2. Empirical Analysis of Trace-ability in the Lightning Network
   Meresa Gebrewahd.
   MSc Thesis. Sapienza University of Rome (Sapienza). Supervisors: Pedro Moreno-Sanchez, Angelo Spognardi. October 2021.
3. The Temporal Booleanization Theorem: realizability checking over numerical-LTL industrial requirements
   Andoni Rodriguez.
   MSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Cesar Sanchez. September 2021.
4. Analysis of Proof of Assets for Different Cryptocurrencies
   Marta Centellas Nadal.
   MSc Thesis. Universidad Complutense Madrid (UCM). Supervisors: Ignacio Cascudo, Pedro Moreno-Sanchez, Ignacio Luengo Velasco. September 2021.
5. Abstract Domain for Floating-point Programs
   Daniel Jurjo Rivas.
   MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. July 2021.
6. An Integrated Approach to Assertion-Based Random Testing in Logic Languages
   Ignacio Casso.
   MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. July 2021.
7. Improvements to Parametric Cost Analysis and its Application to Smart Contracts
   Víctor Pérez Carrasco.
   MSc Thesis. Universidad Politécnica de Madrid, ETSIInf. July 2021.
8. 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. June 2021.

Bachelor's Theses (1)

1. A Platform for Automating the Preparation of iOS Apps for Binary Analysis
   Alejandro de la Cruz Alvarado.
   BSc Thesis. Universidad Carlos III de Madrid (UC3M). Supervisors: Juan Caballero, Ana Isabel González-Tablas Ferreres. June 2021.

Proceedings (1)

1. Practical Aspects of Declarative Languages - 23rd International Symposium, PADL 2021, Copenhagen, Denmark, January 18-19, 2021, Proceedings
   José F. Morales, Dominic A. Orchard.
   2021.

Technical Reports and Manuals (6)

1. Resource Consumption Analysis, Verification, and Optimization for the Tezos Blockchain Technologies - TR1
   Manuel V. Hermenegildo, Pedro Lopez-Garcia, José F. Morales.
   IMDEA Software Institute. December 2021.
2. A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
   Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu.
   Computing Research Repository. 2021.
3. SoK: Practical Foundations for Spectre Defenses
   Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan.
   Computing Research Repository. 2021.
4. âœTheyâ™re not that hard to mitigateâ157: What Cryptographic Library Developers Think About Timing Attacks
   Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar.
   IACR Cryptology ePrint Archive. 2021.
5. UniStore: A fault-tolerant marriage of causal and strong consistency (extended version)
   Manuel Bravo, Alexey Gotsman, Borja de Régil, Hengfeng Wei.
   Computing Research Repository. 2021.
6. The Ciao Prolog Playground
   G. Garcia-Pradales, J.F. Morales, M.V. Hermenegildo.
   Technical University of Madrid (UPM) and IMDEA Software Institute. 2021.