IMDEA Software

IMDEA initiative

Home > Research > Publications > 2022
Filter

Articles in Refereed Journals (13)

  1. 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, August 2022.
  2. Fifty Years of Prolog and Beyond
    Philipp Körner, Michael Leuschel, João Barbosa, Vítor Santos-Costa, Verónica Dahl, Manuel V. Hermenegildo, Jose F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu, Giovanni Ciatto.
    Theory and Practice of Logic Programming 22 (6), 776–858. Cambridge U. Press, May 2022.
  3. 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, March 2022.
  4. 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, January 2022.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. Making Byzantine consensus live
    Manuel Bravo, Gregory Chockler, Alexey Gotsman.
    Distributed Computing 35 (6), 503–532. Springer, 2022.
  10. 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.
  11. 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.
  12. Introduction to the 38th International Conference on Logic Programming Special Issue
    Yuliya Lierler, José F. Morales.
    Theory and Practice of Logic Programming 22 (4), 499–504. 2022.
  13. Introduction to the 38th International Conference on Logic Programming Special Issue II
    Yuliya Lierler, José F. Morales.
    Theory and Practice of Logic Programming 22 (5), 640–640. 2022.

Articles in Refereed Conferences (51)

  1. Efficient Modular SMT-Based Model Checking of Pointer Programs
    I. Garcia-Contreras, A. Gurfinkel, J. A. Navas.
    Static Analysis Symposium (SAS). December 2022.
  2. Watch Your Back: Identifying Cybercrime Financial Relationships in Bitcoin through Back-and-Forth Exploration
    Gibran Gomez, Pedro Moreno-Sanchez, Juan Caballero.
    ACM Conference on Computer and Communications Security (CCS). November 2022.
  3. Call Me Maybe: Using NLP to Automatically Generate Unit Test Cases Compliant with Temporal Constraints
    Arianna Blasi, Alessandra Gorla, Michael D. Ernst, Mauro Pezzè.
    International Conference on Automated Software Engineering (ASE). October 2022.
  4. LISSA: Lazy Initialization with Specialized Solver Aid
    Juan Manuel Copia, Pablo Ponzio, Nazareno Aguirre, Alessandra Gorla, Marcelo Frias.
    International Conference on Automated Software Engineering (ASE). October 2022.
  5. On the Usage of Programming Languages in the iOS Ecosystem
    Daniel Dominguez, Alessandra Gorla, Juan Caballero.
    IEEE Working Conference on Source Code Analysis and Manipulation (SCAM). October 2022.
  6. Deep dive into the IoT backend ecosystem
    Said Jawad Saidi, Srdjan Matic, Georgios Smaragdakis, Oliver Gasser, Anja Feldmann.
    Internet Measurement Conference (IMC). October 2022.
  7. Measuring Web Cookies in Governmental Websites
    Matthias Götze, Srdjan Matic, Costas Iordanou, Georgios Smaragdakis, Nikolaos Laoutaris.
    Web Science Conference (WebSci). June 2022.
  8. ReChan: An Automated Analysis of Android App Release Notes to Report Inconsistencies
    Daniel Domínguez-Álvarez, Daniel Tomic, Alessandra Gorla.
    International Conference on Mobile Software Engineering and Systems (MOBILESoft). May 2022.
  9. Use of Test Doubles in Android Testing: An In-Depth Investigation
    Mattia Fazzini, Chase Choi, Juan Manuel Copia, Gabriel Lee, Yoshiki Kakehi, Alessandra Gorla, Alessandro Orso.
    International Conference on Software Engineering (ICSE). May 2022.
  10. Universal Atomic Swaps: Secure Exchange of Coins Across All Blockchains
    Sri Aravinda Krishnan Thyagarajan, Giulio Malavolta, Pedro Moreno-Sanchez.
    IEEE Symposium on Security and Privacy (SP). May 2022.
  11. ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
    Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker.
    ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2022.
  12. How to Safely Use Extensionality in Liquid Haskell
    Niki Vazou, Michael Greenberg.
    ACM SIGPLAN International Symposium on Haskell (Haskell). 2022.
  13. Liquid Proof Macros
    Henry Blanchette, Niki Vazou, Leonidas Lampropoulos.
    ACM SIGPLAN International Symposium on Haskell (Haskell). 2022.
  14. Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
    Lykourgos Mastorou, Nikolaos Papaspyrou, Niki Vazou.
    ACM SIGPLAN International Symposium on Haskell (Haskell). 2022.
  15. 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.
  16. 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.
  17. Progressive And Efficient Verification For Digital Signatures
    Cecilia Boschini, Dario Fiore, Elena Pagnin.
    International Conference on Applied Cryptography and Network Security (ACNS). 2022.
  18. 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.
  19. 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.
  20. Subversion-Resilient Enhanced Privacy ID
    Antonio Faonio, Dario Fiore, Luca Nizzardo, Claudio Soriente.
    The Cryptographer’s Track at RSA Conference (CT-RSA). 2022.
  21. Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers
    Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Antonio Russo, César Sánchez.
    IEEE International Conference on Blockchain (Blockchain). 2022.
  22. Transaction Monitoring of Smart Contracts
    Margarita Capretto, Martín Ceresa, César Sánchez.
    International Conference on Runtime Verification (RV). 2022.
  23. Multi: A Formal Playground for Multi-Smart Contract Interaction
    Martín Ceresa, César Sánchez.
    Computer Aided Verification (CAV). 2022.
  24. Symbolic Synthesis of Indifferentiability Attacks
    Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe.
    Asia Conference on Information, Computer and Communications Security (AsiaCCS). 2022.
  25. 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.
  26. 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.
  27. Efficient Proofs of Knowledge for Threshold Relations
    Gennaro Avitabile, Vincenzo Botta, Daniele Friolo, Ivan Visconti.
    European Symposium On Research In Computer Security (ESORICS). 2022.
  28. 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.
  29. 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.
  30. 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.
  31. 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.
  32. 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.
  33. Deciding program properties via complete abstractions on bounded domains
    Roberto Bruni, Roberta Gori, Nicolas Manini.
    Static Analysis Symposium (SAS). 2022.
  34. 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.
  35. On Interactive Oracle Proofs for Boolean R1CS Statements
    Ignacio Cascudo, Emanuele Giunta.
    Financial Cryptography and Data Security Conference (FC). 2022.
  36. Adaptively Secure Single Secret Leader Election from DDH
    Dario Catalano, Dario Fiore, Emanuele Giunta.
    ACM Symposium on Principles of Distributed Computing (PODC). 2022.
  37. 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.
  38. Vector Commitments over Rings and Compressed Σ-Protocols
    Thomas Attema, Ignacio Cascudo, Ronald Cramer, Ivan Damgård, Daniel Escudero.
    Theory of Cryptography Conference (TCC). 2022.
  39. On the impossibility of algebraic vector commitments in pairing-free groups
    Dario Catalano, Dario Fiore, Rosario Gennaro, Emanuele Giunta.
    Theory of Cryptography Conference (TCC). 2022.
  40. Acuerdo: Fast atomic broadcast over RDMA
    Joseph Izraelevitz, Gaukas Wang, Rhett Hanscom, Kayli Silvers, Tamara Silbergleit Lehman, Gregory Chockler, Alexey Gotsman.
    International Conference on Parallel Processing (ICPP). 2022.
  41. 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.
  42. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
    Laura Bozzelli, Adriano Peron, César Sánchez.
    International Conference on Concurrency Theory (CONCUR). 2022.
  43. 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.
  44. FORQ-Based Language Inclusion Formal Testing
    Kyveli Doveri, Pierre Ganty, Nicolas Mazzocchi.
    Computer Aided Verification (CAV). 2022.
  45. Automatic Detection of Speculative Execution Combinations
    Xaver Fabian, Marco Guarnieri, Marco Patrignani.
    ACM Conference on Computer and Communications Security (CCS). 2022.
  46. Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification
    Felipe Gorostiaga, Sebastián Zudaire, César Sánchez, Gerardo Schneider, Sebastián Uchitel.
    International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). 2022.
  47. Monitorability of Expressive Verdicts
    Felipe Gorostiaga, César Sánchez.
    NASA Formal Methods (NFM). 2022.
  48. Anticipatory Recurrent Monitoring with Uncertainty and Assumptions
    Hannes Kallwies, Martin Leucker, César Sánchez, Torben Scheffel.
    International Conference on Runtime Verification (RV). 2022.
  49. Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions
    Hannes Kallwies, Martin Leucker, César Sánchez.
    International Symposium on Automated Technology for Verification and Analysis (ATVA). 2022.
  50. Liveness and latency of Byzantine state-machine replication
    Manuel Bravo, Gregory Chockler, Alexey Gotsman.
    International Symposium on Distributed Computing (DISC). 2022.
  51. 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.

Publications in Refereed Workshops (7)

  1. Challenges in inferring privacy properties of smart devices: towards scalable multi-vantage point testing methods
    Aniketh Girish, Vijay Prakash, Serge Egelman, Joel Reardon, Juan Tapiador, Danny Yuxing Huang, Srdjan Matic, Narseo Vallina-Rodriguez.
    ACM International Conference on Emerging Networking Experiments and Technologies Student Workshop (CoNEXT-SW). December 2022.
  2. A SAT-based Efficient Method for the Synthesis from numerical LTL spefications
    Andoni Rodríguez, César Sánchez.
    Jornadas de PROgramación y LEnguajes (PROLE) 2022. September 2022.
  3. Reactive Synthesis of LTL specifications with Rich Theories
    Andoni Rodríguez, César Sánchez.
    11th Workshop in Synthesis. August 2022.
  4. An s(CASP) In-Browser Playground based on Ciao Prolog
    G. Garcia-Pradales, J.F. Morales, M.V. Hermenegildo, J. Arias, M. Carro.
    International Conference on Logic Programming (ICLP). August 2022.
  5. FATR: a Framework for Automated Analysis of Threat Reports
    Juan Caballero, Gibran Gomez, Srdjan Matic, Gustavo Sánchez, Silvia Sebastián, Arturo Villacañas.
    Jornadas Nacionales de Investigación en Ciberseguridad (JNIC). June 2022.
  6. 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.
  7. 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.

Ph.D. Theses (2)

  1. ARCHITECH:Advanced Research of Cryptographic Techniques to build efficient blockchains with privacy and security
    Anaïs Querol Cruz.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Dario Fiore. September 2022.
  2. Theory and Practice of Stream Runtime Verification for Sequences and Real-Time Event Based Systems
    Felipe Gorostiaga.
    PhD Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Cesar Sanchez. May 2022.

Master's Theses (3)

  1. Analysis of the Impact of the Collateral Funds in Payment Channel Networks
    Ana Marija Eres.
    MSc Thesis. University of Zagreb (UniZG). Supervisors: Pedro Moreno-Sanchez, Marina Bagic Babac. July 2022.
  2. Hunting for New Threats in a Feed of Malicious Samples
    Kevin van Liebergen Ávila.
    MSc Thesis. Universidad de Alcalá (UAH). Supervisors: Juan Caballero, Javier Junquera Sánchez. July 2022.
  3. Forecasting Cloud Resource Utilization Using Machine Learning and Computer Vision
    Javier Galindos.
    MSc Thesis. Universidad Politécnica de Madrid (UPM). Supervisors: Thaleia Dimitra Doudali. June 2022.

Bachelor's Theses (2)

  1. Browser Fingerprinting Detection and Mitigation Framework
    Karthik Ramakrishnan.
    BSc Thesis. Manipal Institute of Technology (MIT). Supervisors: Srdjan Matic, Juan Caballero, Sudheesh Puthenveettil Gopi. July 2022.
  2. Sistemas de restricciones algebraicas para pruebas criptográficas aplicado a SHA-256
    Miguel Morona Minguez.
    BSc Thesis. Universidad Complutense de Madrid (UCM). Supervisors: Ignacio Cascudo, Dario Fiore, Ignacio Luengo Velasco. June 2022.

Sections of Chapters in a Book (1)

  1. Verifiable Computation and Succinct Arguments for NP
    Dario Fiore.
    In Asymmetric Cryptography: Primitives and Protocols. Wiley. 2022.

Proceedings (2)

  1. Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming (PPDP 2022)
    Accattoli B, M.V. Hermenegildo.
    September 2022.
  2. Proceedings 38th International Conference on Logic Programming
    Yuliya Lierler, José F. Morales, Carmine Dodaro, Verónica Dahl, Martin Gebser, Tuncay Tekle.
    2022.

Technical Reports and Manuals (8)

  1. Resource Consumption Analysis, Verification, and Optimization for the Tezos Blockchain Technologies - TR2
    Manuel V. Hermenegildo, Pedro Lopez-Garcia, José F. Morales.
    IMDEA Software Institute. December 2022.
  2. A Deep Dive into VirusTotal: Characterizing and Clustering a Massive File Feed
    Kevin van Liebergen, Juan Caballero, Platon Kotzias, Chris Gates.
    Computing Research Repository. October 2022.
  3. Automated Approximate Recurrence Solving applied to Static Analysis of Energy Consumption
    L. Rustenholz.
    CLIP Lab, IMDEA Software Institute. August 2022.
  4. Flux: Liquid Types for Rust
    Nico Lehmann, Adam Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala.
    Computing Research Repository. 2022.
  5. CoqQ: Foundational Verification of Quantum Programs
    Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying.
    Computing Research Repository. 2022.
  6. Spectre Declassified: Reading from the Right Place at the Wrong Time
    Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom.
    IACR Cryptology ePrint Archive. 2022.
  7. Typing High-Speed Cryptography against Spectre v1
    Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean.
    IACR Cryptology ePrint Archive. 2022.
  8. Breaking and Fixing Speculative Load Hardening
    Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom.
    IACR Cryptology ePrint Archive. 2022.

Invited Papers and Tutorials (3)

  1. 50-Years of Prolog and Beyond (invited talk)
    M.V. Hermenegildo.
    November 2022.
  2. Some reflections on Prolog's evolution, status, and future on the 50th anniversary of the birth of Prolog (abstract of invited talk)
    M.V. Hermenegildo.
    International Conference on Logic Programming. August 2022.
  3. Analysis and Verification of the Resource Consumption of Tezos Contracts
    M.V. Hermenegildo, P. Lopez-Garcia, J.F. Morales, V. Perez-Carrasco.
    March 2022.