Publicaciones del Instituto IMDEA Software
Artículos en Revistas
- 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.
Fifty Years of Prolog and Beyond.
Theory and Practice of Logic Programming, 20th Anniversary Special Issue,
En Prensa, Cambridge U. Press,
Mayo
2022.
- Agostino Dovier, Andrea Formisano, Gopal Gupta, Manuel V. Hermenegildo, Enrico Pontelli, Ricardo Rocha.
Parallel Logic Programming: A Sequel.
Theory and Practice of Logic Programming, 20th Anniversary Special Issue,
En Prensa, Cambridge U. Press,
Marzo
2022.
- Roberto Rodriguez-Echeverria, Fernando Macías, Adrian Rutle, José M. Conejero.
Suggesting model transformation repairs for rule-based languages using a contract-based
testing approach.
Vol. 21,
Núm. 1,
páginas 81--112,
2022.
- Joakim Öhman, Aleksandar Nanevski.
Visibility Reasoning for Concurrent Snapshot Algorithms.
PACMPL,
Vol. 6,
Núm. POPL,
2022.
- Arias, Joaquín, Carro, Manuel, Chen, Zhuo, Gupta, Gopal.
Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming.
Theory and Practice of Logic Programming,
Vol. 22,
Núm. 1,
páginas 51--80,
Cambridge University Press,
2022.
- Lydia Garms, Siaw-Lynn Ng, Elizabeth A. Quaglia, Giulia Traverso.
Anonymity and rewards in peer rating systems.
Journal of Computer Security,
Vol. 30,
Núm. 1,
páginas 109--165,
IOS Press,
2022.
- Xueliang Li, Junyang Chen, Yepang Liu, Kaishun Wu, Gallagher, John P..
Combatting Energy Issues for Mobile Applications.
ACM Transactions on Software Engineering and Methodology,
En Prensa, 2022.
- Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, Maurizio Proietti.
Analysis and Transformation of Constrained Horn Clauses for Program Verification.
Theory and Practice of Logic Programming,
En Prensa, Cambridge U. Press,
Noviembre
2021.
- Pierre Ganty, Francesco Ranzato, Pedro Valero.
Complete Abstractions for Checking Language Inclusion.
ACM Trans. Comput. Logic,
Vol. 22,
Núm. 4,
páginas 1--40,
Association for Computing Machinery,
Septiembre
2021.
- M.A. Sanchez-Ordaz, I. Garcia-Contreras, V. Perez-Carrasco, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
VeriFly: On-the-fly Assertion Checking via Incrementality.
Theory and Practice of Logic Programming,
Vol. 21,
Núm. 6,
páginas 768--784,
Cambridge U. Press,
Septiembre
2021.
Special Issue on ICLP'21.
- I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
Incremental and Modular Context-sensitive Analysis.
Theory and Practice of Logic Programming,
Vol. 21,
Núm. 2,
páginas 196--243,
Cambridge U. Press,
Enero
2021.
- Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato.
Higher-order probabilistic adversarial computations: categorical semantics
and program logics.
Proc. ACM Program. Lang.,
Vol. 5,
Núm. ICFP,
páginas 1--30,
2021.
- Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.
A pre-expectation calculus for probabilistic sensitivity.
Proc. ACM Program. Lang.,
Vol. 5,
Núm. POPL,
páginas 1--28,
2021.
- Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth.
Masking in Fine-Grained Leakage Models: Construction, Implementation
and Verification.
IACR Trans. Cryptogr. Hardw. Embed. Syst.,
Vol. 2021,
Núm. 2,
páginas 189--228,
2021.
- Ranjit Jhala, Niki Vazou.
Refinement Types: A Tutorial.
Found. Trends Program. Lang.,
Vol. 6,
Núm. 3-4,
páginas 159--317,
2021.
- Arianna Blasi, Alessandra Gorla, Michael D.
Ernst, Mauro Pezz`e, Antonio Carzaniga.
MeMo: Automatically identifying metamorphic
relations in Javadoc comments for test automation.
Journal of Systems and Software,
Vol. 181,
11
2021.
- Arianna Blasi, Nataliia Stulova, Alessandra Gorla, Oscar Nierstrasz.
Replicomment: identifying clones in code comments.
Journal of Systems and Software,
Vol. 182,
12
2021.
- Gregory Chockler, Alexey Gotsman.
Multi-Shot Distributed Transaction Commit.
Distributed Computing,
Vol. 34,
Núm. 4,
páginas 301--318,
Springer,
2021.
- Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, Marek Zawirski.
Specification and Space Complexity of Collaborative Text Editing.
Theoretical Computer Science,
Vol. 855,
páginas 141--160,
Elsevier,
2021.
- Somayeh Dolatnezhad Samarin, Dario Fiore, Daniele Venturi, Morteza Amini.
A compiler for multi-key homomorphic signatures for Turing machines.
Theoretical Computer Science,
Vol. 889,
páginas 145--170,
2021.
- Miguel Ambrona, Dario Fiore, Claudio Soriente.
Controlled Functional Encryption Revisited: Multi-Authority Extensions
and Efficient Schemes for Quadratic Functions.
Proceedings on Privacy Enhancing Technologies,
Vol. 2021,
Núm. 1,
páginas 21--42,
Sciendo,
2021.
- Ignacio Cascudo, Reto Schnyder.
A note on secure multiparty computation via higher residue symbols.
Journal of Mathematical Cryptology,
Vol. 15,
Núm. 1,
páginas 284--297,
2021.
- Nikita Zyuzin, Aleksandar Nanevski.
Contextual Modal Types for Algebraic Effects and Handlers.
PACMPL,
Vol. 5,
Núm. ICFP,
páginas 1--29,
2021.
- Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas.
On Algebraic Abstractions for Concurrent Separation Logics.
PACMPL,
Vol. 5,
Núm. POPL,
páginas 1--32,
2021.
- Pierre Ganty, Elena Gutiérrez, Pedro Valero.
A Congruence-Based Perspective on Finite Tree Automata.
Fundam. Informaticae,
Vol. 184,
Núm. 1,
páginas 1--47,
2021.
- Felipe Gorostiaga, César Sánchez.
Stream runtime verification of real-time event streams with the Striver language.
International Journal on Software Tools for Technology Transfer,
Vol. 23,
Núm. 2,
páginas 157--183,
2021.
- Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonarkdarpour.
Gray-Box Monitoring of Hyperproperties with an Application to Privacy.
Formal Methods in Systems Desing,
Vol. 58,
Núm. 1-2,
páginas 126--159,
2021.
- Alfonso Ortega, Julian Fiérrez, Aythami Morales, Zilong Wang, Marina de la Cruz, César Luis Alonso, Tony Ribeiro.
Symbolic AI for XAI: Evaluating LFIT Inductive Programming for
Explaining Biases in Machine Learning.
Computers,
Vol. 10,
Núm. 11,
Multidisciplinary Digital Publishing Institute,
2021.
- Irfan Ul Haq, Juan Caballero.
A Survey of Binary Code Similarity.
ACM Comput. Surv.,
Vol. 54,
Núm. 3,
páginas 1--51,
2021.
- John P. Gallagher, Martin Sulzmann.
Preface, Special Issue on FLOPS 2018.
Science of Computer Programming,
Vol. 202,
2021.
- Olivier Blazy, Laura Brouilhet, Céline Chevalier, Patrick Towa, Ida Tucker, Damien Vergnaud.
Hardware security without secure hardware: How to decrypt with a password
and a server.
Theoretical Computer Science,
Vol. 895,
páginas 178--211,
2021.
- Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie.
System-Level Non-interference of Constant-Time Cryptography. Part
II: Verified Static Analysis and Stealth Memory.
J. Autom. Reason.,
Vol. 64,
Núm. 8,
páginas 1685--1729,
2020.
- Gilles Barthe, Sonia Belaïd, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Francois-Xavier Standaert, Pierre-Yves Strub.
Improved parallel mask refreshing algorithms: generic solutions with
parametrized non-interference and automated optimizations.
J. Cryptographic Engineering,
Vol. 10,
Núm. 1,
páginas 17--26,
2020.
- Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu.
Formal verification of a constant-time preserving C compiler.
Proc. ACM Program. Lang.,
Vol. 4,
Núm. POPL,
páginas 1--30,
2020.
- Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou.
Relational proofs for quantum programs.
Proc. ACM Program. Lang.,
Vol. 4,
Núm. POPL,
páginas 1--29,
2020.
- Gilles Barthe, Justin Hsu, Kevin Liao.
A probabilistic separation logic.
Proc. ACM Program. Lang.,
Vol. 4,
Núm. POPL,
páginas 1--30,
2020.
- Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou.
Verifying replicated data types with typeclass refinements in Liquid
Haskell.
Proc. ACM Program. Lang.,
Vol. 4,
Núm. OOPSLA,
páginas 1--30,
ACM,
2020.
- Martin A. T. Handley, Niki Vazou, Graham Hutton.
Liquidate your assets: reasoning about resource usage in liquid Haskell.
Proc. ACM Program. Lang.,
Vol. 4,
Núm. POPL,
páginas 1--27,
2020.
- Ray Neiheiser, Luciana Rech, Manuel Bravo, Luís E. T. Rodrigues, Miguel Correia.
Fireplug: Efficient and Robust Geo-Replication of Graph Databases.
IEEE Trans. Parallel Distributed Syst.,
Vol. 31,
Núm. 8,
páginas 1942--1953,
2020.
- 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.
Decentralized Privacy-Preserving Proximity Tracing.
IEEE Data Eng. Bull.,
Vol. 43,
Núm. 2,
páginas 36--66,
2020.
- Dario Fiore, Christian Thiel, Matthias Baldauf.
Potenziale von Chatbots für den innerbetrieblichen IT-Support.
HMD Prax. Wirtsch.,
Vol. 57,
Núm. 1,
páginas 77--88,
2020.
- Ignacio Cascudo, Jaron Skovsted Gundersen, Diego Ruano.
Squares of matrix-product codes.
Finite Fields and Their Applications,
Vol. 62,
2020.
- Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham.
Proving highly-concurrent traversals correct.
Proc. ACM Program. Lang.,
Vol. 4,
Núm. OOPSLA,
páginas 1--29,
2020.
- Alejandro Aguirre, Shin-ya Katsumata.
Weakest Preconditions in Fibrations.
Electronic Notes in Theoretical Computer Science,
Vol. 352,
páginas 5--27,
2020.
The 36th Mathematical Foundations of Programming Semantics Conference, 2020.
- Fabio Fioravanti, John P. Gallagher, Maurizio Proietti.
Preface, Special Issue on LOPSTR 2017.
Fundam. Inform.,
Vol. 173,
Núm. 4,
2020.
- Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub.
Relational *-Liftings for
Differential Privacy.
Logical Methods in Computer Science,
Vol. 15,
Núm. 4,
Diciembre
2019.
- Patrick Baillot, Gilles Barthe, Ugo Dal Lago.
Implicit Computational Complexity of Subrecursive Definitions and
Applications to Cryptographic Proofs.
Journal of Automated Reasoning,
Vol. 63,
Núm. 4,
páginas 813--855,
Diciembre
2019.
- Alejandro Calleja, Juan Tapiador, Juan Caballero.
The MalSource Dataset: Quantifying Complexity and Code Reuse in Malware Development.
IEEE Transactions on Information Forensics and Security,
Vol. 14,
Núm. 12,
páginas 3175--3190,
IEEE,
Diciembre
2019.
- César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Yli`es Falcone, Adrian Francalanza, Srdan Krstic, João M. Lourenco, Dejan Nickovic, Gordon J. Pace, José Rufino, Julien Signoles, Dmitriy Traytel, Alexander Weiss.
A survey of challenges for runtime verification from advanced application
domains (beyond software).
Formal Methods in System Design,
Vol. 54,
Núm. 3,
páginas 279--335,
Noviembre
2019.
- Aleksandar Nanevski, Anindya Banerjee, Germán
Andrés Delbianco, Ignacio Fábregas.
Specifying concurrent programs in separation logic: morphisms and
simulations.
PACMPL,
Vol. 3,
Núm. OOPSLA,
páginas 1--30,
ACM,
Octubre
2019.
- Joaquín Arias, Manuel Carro.
Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP.
Theory and Practice of Logic Programming,
Vol. 19,
Núm. 5-6,
páginas 1107--1123,
Septiembre
2019.
Special Issue on ICLP'19.
- Jesús J. Doménech, John P. Gallagher, Samir Genaim.
Control-Flow Refinement by Partial Evaluation, and its Application
to Termination and Cost Analysis.
TPLP,
Vol. 19,
Núm. 5-6,
páginas 990--1005,
Cambridge University Press,
Septiembre
2019.
- Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna.
System-Level Non-interference of Constant-Time Cryptography. Part
I: Model.
Journal of Automated Reasoning,
Vol. 63,
Núm. 1,
páginas 1--51,
Junio
2019.
- Joaquín Arias, Manuel Carro.
Description, Implementation, and Evaluation of a Generic Design for Tabled CLP.
Theory and Practice of Logic Programming,
Vol. 19,
Núm. 3,
páginas 412--448,
Cambridge U. Press,
Mayo
2019.
- Dario Fiore, Aikaterini Mitrokotsa, Luca Nizzardo, Elena Pagnin.
Multi-key homomorphic authenticators.
IET Information Security,
Vol. 13,
Núm. 6,
páginas 618--638,
Institution of Engineering and Technology,
Abril
2019.
- Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt.
Automated Analysis of Cryptographic Assumptions in Generic Group Models.
Journal of Cryptology,
Vol. 32,
Núm. 2,
páginas 324--360,
Abril
2019.
- Gilles Barthe, Christos Dimitrakakis, Marco Gaboardi, Andreas Haeberlen, Aaron Roth, Aleksandra B. Slavkovic.
Program for TPDP 2016.
Journal of Privacy and Confidentiality,
Vol. 9,
Núm. 1,
Marzo
2019.
- Pablo Cañones, Boris Köpf, Jan Reineke.
On the Incomparability of Cache Algorithms in Terms of Timing Leakage.
Logical Methods in Computer Science,
Vol. 15,
Núm. 1,
Marzo
2019.
- Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato.
A^2I: abstract^2 interpretation.
PACMPL,
Vol. 3,
Núm. POPL,
páginas 1--31,
ACM,
Enero
2019.
- Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.
Formal Verification of Higher-order Probabilistic Programs: Reasoning About Approximation,
Convergence, Bayesian Inference, and Optimization.
Proc. ACM Program. Lang.,
Vol. 3,
Núm. POPL,
páginas 1--30,
ACM,
Enero
2019.
- Richard Rivera, Platon Kotzias, Avinash Sudhodanan, Juan Caballero.
Costly Freeware: A Systematic Analysis of Abuse in Download Portals.
IET Information Security,
Vol. 13,
Núm. 1,
páginas 27--35,
IET,
Enero
2019.
- James Parker, Niki Vazou, Michael Hicks.
LWeb: information flow security for multi-tier web applications.
PACMPL,
Vol. 3,
Núm. POPL,
páginas 1--30,
2019.
- Antonio Faonio, Jesper Buus Nielsen, Mark Simkin, Daniele Venturi.
Continuously non-malleable codes with split-state refresh.
Theoretical Computer Science,
Vol. 759,
páginas 98--132,
2019.
- Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, Yolanda Ortega-Mallén.
Rule Formats for Nominal Process Calculi.
Logical Methods in Computer Science,
Vol. 15,
Núm. 4,
2019.
- Luca Aceto, Ignacio Fábregas, Carlos Gregorio-Rodríguez, Anna Ingólfsdóttir.
Logical characterisations, rule formats and compositionality for input-output
conformance simulation.
J. Log. Algebr. Meth. Program.,
Vol. 106,
páginas 78--106,
2019.
- Luca Aceto, Dario Della Monica, Ignacio Fábregas, Anna Ingólfsdóttir.
When Are Prime Formulae Characteristic?.
Theor. Comput. Sci.,
Vol. 777,
páginas 3--31,
2019.
- Antonio Faonio, Jesper Buus Nielsen, Mark Simkin, Daniele Venturi.
Continuously non-malleable codes with split-state refresh.
Theoretical Computer Science,
Vol. 759,
páginas 98--132,
2019.
- Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
A relational logic for higher-order programs.
Journal of Functional Programming,
Vol. 29,
Cambridge University Press,
2019.
- Julio Mariño, Raúl N. N. Alborodo, Lars-Åke Fredlund, Ángel Herranz-Nieva.
Synthesis of verifiable concurrent Java components from formal models.
Software and Systems Modeling,
Vol. 18,
Núm. 1,
páginas 71--105,
2019.
- Zorana Banković, Umer Liqat, Pedro Lopez-Garcia.
A General Methodology for Energy-efficient
Scheduling in Multicore Environments based on
Evolutionary Algorithms.
Journal of Multiple-Valued Logic and Soft Computing (JMVLSC), SOCO'15 Special Issue,
Vol. 32,
Núm. 3-4,
páginas 313--341,
Old City Publishing,
2019.
- Álvaro García-Pérez, Pablo Nogueira.
The full-reducing Krivine abstract machine KN simulates pure
normal-order reduction in lockstep: A proof via corresponding calculus.
Journal of Functional Programming,
Vol. 29,
Núm. E7,
páginas 1--38,
Cambridge University Press,
2019.
- Kuhring, Lucas, István, Zsolt.
I Can't Believe It's Not (Only) Software! Bionic Distributed Storage for Parquet Files.
Proc. VLDB Endow.,
Vol. 12,
Núm. 12,
páginas 1838--1841,
VLDB Endowment,
2019.
- István, Zsolt.
The Glass Half Full: Using Programmable Hardware Accelerators in Analytics.
IEEE Data Eng. Bull.,
Vol. 42,
Núm. 1,
páginas 49--60,
2019.
- Alonso, Gustavo, Istvan, Zsolt, Kara, Kaan, Owaida, Muhsen, Sidler, David.
doppioDB 1.0: Machine Learning inside a Relational Engine.
IEEE Data Engineering,
Vol. 42,
Núm. 2,
páginas 19--31,
2019.
- Roberto Bruni, Roberto Giacobazzi, Roberta Gori.
Code obfuscation against abstraction refinement attacks.
Formal Aspects of Computing,
Vol. 30,
Núm. 6,
páginas 685--711,
Noviembre
2018.
- Catalano, Dario, Fiore, Dario, Nizzardo Luca.
Homomorphic signatures with sublinear public keys via asymmetric programmable hash functions.
Design, Codes and Cryptography,
Vol. 86,
Núm. 10,
páginas 2197--2246,
Octubre
2018.
- Irfan Ul Haq, Sergio Chica, Juan Caballero, Somesh Jha.
Malware lineage in the wild.
Computers & Security,
Vol. 78,
páginas 347--363,
Elsevier,
Septiembre
2018.
- Irfan Ul Haq, Sergio Chica, Juan Caballero, Somesh Jha.
Malware Lineage in the Wild.
Computers & Security,
Vol. 78,
páginas 347--363,
Elsevier,
Agosto
2018.
- István, Zsolt, Sidler, David, Alonso, Gustavo.
Active Pages 20 Years Later: Active Storage for the Cloud.
IEEE Internet Computing,
Vol. 22,
Núm. 4,
páginas 6--14,
Julio
2018.
- Anindya Banerjee, David A. Naumann, Mohammad Nikouei.
A Logical Analysis of Framing for Specifications with Pure Method Calls.
ACM Trans. Program. Lang. Syst.,
Vol. 40,
Núm. 2,
páginas 1--90,
ACM,
Mayo
2018.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
Some Trade-offs in Reducing the Overhead of Assertion
Run-time Checks via Static Analysis.
Science of Computer Programming,
Vol. 155,
páginas 3--26,
Elsevier North-Holland,
Abril
2018.
Selected and Extended papers from the 2016 International
Symposium on Principles and Practice of Declarative
Programming.
- Andrea Cerone, Alexey Gotsman.
Analysing snapshot isolation.
Journal of the ACM,
Vol. 65,
Núm. 2,
páginas 1--41,
ACM Press,
Marzo
2018.
- P. Lopez-Garcia, L. Darmawan, M. Klemen, U. Liqat, F. Bueno, M. V. Hermenegildo.
Interval-based Resource Usage Verification by Translation into Horn Clauses and an
Application to Energy Consumption.
Theory and Practice of Logic Programming, Special Issue on Computational Logic for Verification,
Vol. 18,
Núm. 2,
páginas 167--223,
Cambridge U. Press,
Marzo
2018.
arXiv:1803.04451.
- Bishoksan Kafle, John P. Gallagher, Pierre Ganty.
Tree dimension in verification of constrained Horn clauses.
TPLP,
Vol. 18,
Núm. 2,
páginas 224--251,
Marzo
2018.
- Roberto Giacobazzi, Isabella Mastroeni.
Abstract Non-Interference: A Unifying Framework for Weakening Information-flow.
ACM Trans. Priv. Secur.,
Vol. 21,
Núm. 2,
páginas 1--31,
ACM,
Febrero
2018.
- John P. Gallagher, Mai Ajspur, Bishoksan Kafle.
Optimised determinisation and completion of finite tree automata.
Journal of Logical and Algebraic Methods in Programming,
Vol. 95,
páginas 1--16,
Febrero
2018.
- Andreas Abel, Joakim Öhman, Andrea Vezzosi.
Decidability of conversion for type theory in type theory.
Proceedings of the ACM on Programming Languages (PACMPL),
Vol. 2,
Núm. POPL,
páginas 1--29,
ACM,
Enero
2018.
- Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky.
Characterizing transactional memory consistency conditions using observational refinement.
Journal of the ACM,
Vol. 65,
Núm. 1,
páginas 1--44,
ACM Press,
Enero
2018.
- Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
Monadic refinements for relational cost analysis.
PACMPL,
Vol. 2,
Núm. POPL,
páginas 1--32,
2018.
- Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
Proving expected sensitivity of probabilistic programs.
PACMPL,
Vol. 2,
Núm. POPL,
páginas 1--29,
2018.
- Dario Catalano, Dario Fiore.
Practical Homomorphic Message Authenticators for Arithmetic Circuits.
Journal of Cryptology,
Vol. 31,
Núm. 1,
páginas 23--59,
Springer,
2018.
- Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
On reducing linearizability to state reachability.
Inf. Comput.,
Vol. 261,
Núm. Part 2,
páginas 383--400,
2018.
- Joaquín Arias, Manuel Carro, Elmer Salazar, Kyle Marple, Gopal Gupta.
Constraint Answer Set Programming without Grounding.
Theory and Practice of Logic Programming,
Vol. 18,
Núm. 3-4,
páginas 337--354,
Cambridge U. Press,
2018.
- Yli`es Falcone, César Sánchez.
Introduction to the special issue on runtime verification.
Formal Methods in Systems Design,
Vol. 53,
Núm. 1,
páginas 1--5,
2018.
- Laura Bozzelli, César Sánchez.
Visibly Linear Temporal Logic.
Journal of Automated Reasoning,
Vol. 60,
Núm. 2,
páginas 177--220,
2018.
- Bishoksan Kafle, John P. Gallagher, Graeme Gange, Peter Schachte, Harald Sndergaard, Peter J. Stuckey.
An iterative approach to precondition inference using constrained
Horn clauses.
TPLP,
Vol. 18,
Núm. 3-4,
páginas 553--570,
2018.
- U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
An Evolutionary Scheduling Approach for Trading-off
Accuracy vs. Verifiable Energy in Multicore Processors.
Logic Journal of the IGPL,
Vol. 25,
Núm. 6,
páginas 1006--1019,
Oxford Academic Press,
Diciembre
2017.
- Pierre Ganty, Radu Iosif, Filip Konecný.
Underapproximation of procedure summaries for integer programs.
International Journal on Software Tools for Technology Transfer (STTT),
Vol. 19,
Núm. 5,
páginas 565--584,
Octubre
2017.
- Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
A relational logic for higher-order programs.
PACMPL (ICFP),
Vol. 1,
páginas 1--29,
ACM,
Agosto
2017.
- Alejandro Sánchez, César Sánchez.
Parametrized Verification Diagrams: Temporal Verification of
Symmetric Parametrized Concurrent Systems.
Annals of Mathematics and Artificial Intelligence,
Vol. 80,
Núm. 3--4,
páginas 249--282,
Agosto
2017.
- Dario Catalano, Dario Fiore, Rosario Gennaro.
A Certificateless Approach to Onion Routing.
International Journal of Information Security,
Vol. 16,
Núm. 3,
páginas 327--343,
Springer,
Junio
2017.
- Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
Model checking parameterized asynchronous shared-memory systems.
Formal Methods in System Design,
Vol. 50,
Núm. 2-3,
páginas 140--167,
Junio
2017.
- Javier Esparza, Pierre Ganty, Jér^ome Leroux, Rupak Majumdar.
Verification of population protocols.
Acta Informatica,
Vol. 54,
Núm. 2,
páginas 191--215,
Marzo
2017.
- Roberto Giacobazzi, Isabella Mastroeni, Mila Dalla Preda.
Maximal incompleteness as obfuscation potency.
Formal Aspects of Computing,
Vol. 29,
Núm. 1,
páginas 3--31,
Enero
2017.
- Reza Shokri, George Theodorakopoulos, Carmela Troncoso.
Privacy Games Along Location Traces: A Game-Theoretic Framework
for Optimizing Location Privacy.
ACM Trans. Priv. Secur.,
Vol. 19,
Núm. 4,
páginas 1--31,
2017.
- Apostolos Pyrgelis, Carmela Troncoso, Emiliano De Cristofaro.
What Does The Crowd Say About You? Evaluating Aggregation-based Location Privacy.
PoPETs,
Vol. 2017,
Núm. 4,
páginas 156--176,
2017.
- Carmela Troncoso, George Danezis, Marios Isaakidis, Harry Halpin.
Systematizing Decentralization and Privacy: Lessons from 15 years of research and deployments.
PoPETs,
Vol. 2017,
Núm. 4,
páginas 404--426,
2017.
- Fiore, Dario, Vasco, María Isabel González, Soriente, Claudio.
Partitioned Group Password-Based Authenticated Key Exchange.
The Computer Journal,
Vol. 60,
Núm. 12,
páginas 1912--1922,
2017.
- Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue.
A messy state of the union: taming the composite state machines of
TLS.
Commun. ACM,
Vol. 60,
Núm. 2,
páginas 99--107,
2017.
- Bishoksan Kafle, John P. Gallagher.
Horn clause verification with convex polyhedral abstraction and tree
automata-based refinement.
Computer Languages, Systems & Structures,
Vol. 47,
páginas 2--18,
2017.
- Bishoksan Kafle, John P. Gallagher.
Constraint specialisation in Horn clause verification.
Science of Computer Programming,
Vol. 137,
páginas 125--140,
2017.
- K. Eder, J.P. Gallagher, P. Lopez-Garcia, H. Muller, Z. Banković, K. Georgiou, R. Haemmerlé, M. V. Hermenegildo, B. Kafle, S. Kerrison, M. Kirkeby, M. Klemen, X. Li, U. Liqat, J. Morse, M. Rhiger, M. Rosendahl.
ENTRA: Whole-Systems Energy Transparency.
Microprocessors and Microsystems,
Vol. 47, Part B,
páginas 278--286,
Elsevier,
Noviembre
2016.
- Manuel Carro, Andy King.
Introduction to the 32nd International Conference on Logic Programming Special Issue.
Theory and Practice of Logic Programming,
Vol. 16,
Núm. 5-6,
páginas 509--514,
Cambridge University Press,
Septiembre
2016.
- I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
Semantic Code Browsing.
Theory and Practice of Logic Programming,
32nd Int'l. Conference on Logic Programming (ICLP'16) Special Issue,
Vol. 16,
Núm. 5-6,
páginas 721--737,
Cambridge U. Press,
Septiembre
2016.
- P. Lopez-Garcia, M. Klemen, U. Liqat, M. V. Hermenegildo.
A General Framework for Static Profiling of Parametric Resource Usage.
Theory and Practice of Logic Programming, 32nd Int'l. Conference on Logic Programming (ICLP'16) Special Issue,
Vol. 16,
Núm. 5-6,
páginas 849--865,
Cambridge U. Press,
Septiembre
2016.
- Fredlund, Lars-Åke, Mariño, Julio, Alborodo, Raúl N.N., Herranz, Angel.
A testing-based approach to ensure the safety of shared resource concurrent systems.
Journal of Risk and Reliability, Proceedings of the Institution of Mechanical Engineers, Part O,
Vol. 230,
Núm. 5,
páginas 457--472,
Sage Publications,
Julio
2016.
- Juan Caballero, Zhiqiang Lin.
Type Inference on Executables.
ACM Computing Surveys,
Vol. 48,
Núm. 4,
páginas 1--35,
ACM,
Mayo
2016.
- Javier Esparza, Pierre Ganty, Rupak Majumdar.
Parameterized Verification of Asynchronous Shared-Memory Systems.
J. ACM,
Vol. 63,
Núm. 1,
páginas 1--48,
ACM,
Marzo
2016.
- J.F. Morales, M. Carro, M. V. Hermenegildo.
Description and Optimization of Abstract Machines
in a Dialect of Prolog.
Theory and Practice of Logic Programming,
Vol. 16,
Núm. 1,
páginas 1--58,
Cambridge University Press,
Enero
2016.
- J. Hughes, C. Sparks, A. Stoughton, R. Parikh, A. Reuther, S. Jagannathan.
Building Resource Adaptive Software Systems (BRASS): Objectives and System Evaluation.
SIGSOFT Softw. Eng. Notes,
Vol. 41,
Núm. 1,
páginas 1--2,
ACM,
Enero
2016.
- Isabella Mastroeni, Roberto Giacobazzi.
Weakening Additivity in Adjoining Closures.
Order,
Vol. 33,
Núm. 3,
páginas 503--516,
2016.
- Gilles Barthe, Juan Manuel Crespo, César Kunz.
Product programs and relational program logics.
J. Log. Algebr. Meth. Program.,
Vol. 85,
Núm. 5,
páginas 847--859,
2016.
- Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce.
Programming language techniques for differential privacy.
SIGLOG News,
Vol. 3,
Núm. 1,
páginas 34--53,
2016.
- Sandrine Blazy, Vincent Laporte, David Pichardie.
Verified Abstract Interpretation Techniques for Disassembling Low-level
Self-modifying Code.
Journal of Automated Reasoning,
Vol. 56,
Núm. 3,
páginas 283--308,
2016.
- Guillermo Vigueras, Juan M. Orduña.
On the Use of GPU for Accelerating Communication-Aware Mapping Techniques.
The Computer Journal,
Vol. 59,
Núm. 6,
páginas 836--847,
2016.
- Giovanni Bernardi, Matthew Hennessy.
Using higher-order contracts to model session types.
Logical Methods in Computer Science,
Vol. 12,
Núm. 2,
2016.
- S. Oya, F. Pérez-González, C. Troncoso.
Design of Pool Mixes Against Profiling Attacks in Real Conditions.
IEEE/ACM Trans. Netw.,
Vol. 24,
Núm. 6,
páginas 3662--3675,
2016.
- Laura Bozzelli, César Sánchez.
Foundations of Boolean Stream Runtime Verification.
Theoretical Computer Science,
Vol. 631,
páginas 118--138,
2016.
- Bernd Finkbeiner, César Sánchez.
Special issue on Rich Models, EU-COST Action IC0901 Rich-Model Toolkit.
Acta Informatica,
Vol. 53,
Núm. 4,
páginas 325--326,
2016.
- César Sánchez, Kristen Brent Venable, Esteban Zimányi.
Special issue on temporal representation and reasoning (TIME'13).
Acta Informatica,
Vol. 53,
Núm. 2,
páginas 87--88,
2016.
- Álvaro García-Pérez, Pablo Nogueira.
No solvable lambda-value term left behind.
Logical Methods in Computer Science,
Vol. 12,
Núm. 12,
páginas 1--43,
2016.
- Axel Schulz, Loza Mencía, Eneldo, Benedikt Schmidt.
A rapid-prototyping framework for extracting small-scale incident-related
information in microblogs: Application of multi-label classification
on tweets.
Information Systems,
Vol. 57,
páginas 88--110,
2016.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
Practical Run-time Checking via Unobtrusive Property Caching.
Theory and Practice of Logic Programming,
31st Int'l. Conference on Logic Programming (ICLP'15)
Special Issue,
Vol. 15,
Núm. 04-05,
páginas 726--741,
Cambridge U. Press,
Septiembre
2015.
http://arxiv.org/abs/1507.05986.
- Goran Doychev, Boris Köpf, Laurent Mauborgne, Jan Reineke.
CacheAudit: A Tool for the Static Analysis of Cache Side Channels.
ACM Transactions on Information and System Security (TISSEC),
Vol. 18,
Núm. 1,
páginas 1--32,
ACM,
Junio
2015.
- Vigueras, Guillermo, Orduña, Juan M..
On the Use of GPU for Accelerating Communication-Aware Mapping Techniques.
The Computer Journal,
En Prensa, Mayo
2015.
- Giovanni Bernardi, Matthew Hennessy.
Mutually Testing Processes.
Logical Methods in Computer Science,
Vol. 11,
Núm. 2,
Abril
2015.
- Zorana Banković, Pedro Lopez-Garcia.
Stochastic vs. Deterministic Evolutionary
Algorithm-based Allocation and Scheduling for
XMOS Chips.
Neurocomputing,
Vol. 150,
páginas 82--89,
Elsevier,
Febrero
2015.
- Andreas Metzger, Philip Leitner, Dragan
Ivanovic, Eric Schmieders, Roslin Franklin, Manuel Carro, Schahram Dustdar, Klaus Pohl.
Comparing and Combining Predictive Business Process
Monitoring Techniques.
System, Man, and Cybernetics: Systems, IEEE
Transactions on,
Vol. 45,
Núm. 2,
páginas 276--290,
Febrero
2015.
- Antonio Nappa, M. Zubair Rafique, Juan Caballero.
The MALICIA Dataset: Identification and Analysis of Drive-by Download Operations.
International Journal of Information Security,
Vol. 14,
Núm. 1,
páginas 15--33,
Springer Berlin Heidelberg,
Febrero
2015.
- Gilles Barthe.
High-Assurance Cryptography: Cryptographic Software We can Trust.
IEEE Security & Privacy,
Vol. 13,
Núm. 5,
páginas 86--89,
2015.
- Gilles Barthe, Alberto Pardo, Gerardo Schneider.
SEFM: Software Engineering and Formal Methods.
Software and System Modeling,
Vol. 14,
Núm. 1,
páginas 3--4,
2015.
- Guillermo Vigueras, Federico Sket, Cristóbal Samaniego, Ling Wu, Ludovic Noels, Denny Tjahjanto, Eva Casoni, Guillaume Houzeaux, Ahmed Makradi, Jon M. Molina-Aldareguia, Mariano Vázquez, Antoine Jérusalem.
An XFEM/CZM implementation for massively parallel simulations of composites fracture.
Composite Structures,
Vol. 125,
Núm. 0,
páginas 542--557,
2015.
- Antonio Carzaniga, Alessandra Gorla, Nicol`o, Mauro Pezz`e.
Automatic Workarounds: Exploiting the Intrinsic Redundancy
of Web Applications.
ACM Transactions on Software Engineering and
Methodologies,
Vol. 24,
Núm. 3,
páginas 1--42,
2015.
- Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan.
Stability Preserving Simulations and Bisimulations for Hybrid Systems.
IEEE Trans. Automat. Contr.,
Vol. 60,
Núm. 12,
páginas 3210--3225,
2015.
- Pavithra Prabhakar, Miriam Garcia Soto.
AVERIST: An Algorithmic Verifier for Stability.
Electr. Notes Theor. Comput. Sci.,
Vol. 317,
páginas 133--139,
2015.
- Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan.
Hybrid automata-based CEGAR for rectangular hybrid systems.
Formal Methods in System Design,
Vol. 46,
Núm. 2,
páginas 105--134,
2015.
- Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, Geir E. Dullerud.
A decidable class of planar linear hybrid systems.
Theoretical Computer Science,
Vol. 574,
páginas 1--17,
2015.
- Dario Catalano, Dario Fiore, Rosario Gennaro, Konstantinos Vamvourellis.
Algebraic (trapdoor) one-way functions: Constructions and applications.
Theoretical Computer Science,
Vol. 592,
páginas 143--165,
Springer,
2015.
- Andrea Cerone, Matthew Hennessy, Massimo Merro.
Modelling MAC-Layer Communications in Wireless Systems.
Logical Methods in Computer Science,
Vol. 11,
Núm. 1,
2015.
- Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
Mtac: A Monad for Typed Tactic Programming in Coq.
Journal of Functional Programming (JFP),
Vol. 25,
2015.
- Backes, Michael, Köpf, Boris.
Quantifying information flow in cryptographic systems.
Mathematical Structures in Computer Science,
Vol. 25,
Núm. 2,
páginas 457--479,
2
2015.
- Alejandro Sánchez, César Sánchez.
Parametrized Invariance for Infinite State Processes.
Acta Informatica,
Vol. 52,
Núm. 6,
páginas 525--557,
2015.
- A. Serrano, P. Lopez-Garcia, M. V. Hermenegildo.
Resource Usage Analysis of Logic Programs via Abstract
Interpretation Using Sized Types.
Theory and Practice of Logic Programming, 30th Int'l. Conference on Logic Programming (ICLP'14) Special Issue,
Vol. 14,
Núm. 4-5,
páginas 739--754,
Cambridge U. Press,
Julio
2014.
- Gilles Barthe, Delphine Demange, David Pichardie.
Formal Verification of an SSA-Based Middle-End for CompCert.
ACM Trans. Program. Lang. Syst.,
Vol. 36,
Núm. 1,
páginas 1--35,
ACM,
Marzo
2014.
- J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn.
Pushdown flow analysis with abstract garbage collection.
J. Funct. Program.,
Vol. 24,
Núm. 2-3,
páginas 218--283,
2014.
- Vigueras, Guillermo, Roy, Ishani, Cookson, Andrew, Lee, Jack, Smith, Nicolas, Nordsletten, David.
Toward GPGPU accelerated human electromechanical cardiac simulations.
International Journal for Numerical Methods in Biomedical Engineering,
Vol. 30,
Núm. 1,
páginas 117--134,
2014.
- Guillermo Vigueras, Juan M. Orduña, Miguel Lozano, Jose M. Cecilia, Jose M. Garcia.
Accelerating collision detection for large-scale crowd simulation on multi-core and many-core architectures.
International Journal of High Performance Computing and Applications,
Vol. 28,
Núm. 1,
2014.
- Alexander Malkis, Anindya Banerjee.
On Automation in the Verification of Software Barriers: Experience
Report.
J. Autom. Reasoning,
Vol. 52,
Núm. 3,
páginas 275--329,
2014.
- Michel Abdalla, Dario Catalano, Dario Fiore.
Verifiable Random Functions: Relations to Identity-Based Key-Encapsulation and New Constructions.
Journal of Cryptology,
Vol. 27,
Núm. 3,
páginas 544--593,
Springer,
2014.
- Ahmed Bouajjani, Michael Emmi.
Bounded phase analysis of message-passing programs.
STTT,
Vol. 16,
Núm. 2,
páginas 127--146,
2014.
- Javier Esparza, Pierre Ganty, Tomás Poch.
Pattern-based Verification for Multithreaded Programs.
ACM Transactions on Programming Languages and Systems,
Vol. 36,
Núm. 3,
páginas 1--29,
2014.
- G.J. Duck, R. Haemmerlé, M. Sulzmann.
On Termination, Confluence and Consistent CHR-based
Type Inference.
Theory and Practice of Logic Programming, 30th
Int'l. Conference on Logic Programming (ICLP'14)
Special Issue,
Vol. 14,
Núm. 4-5,
páginas 619--632,
Cambridge U. Press,
2014.
- Laura Bozzelli, César Sánchez.
Visibly Rational Expressions.
Acta Informatica,
Vol. 51,
Núm. 1,
páginas 25--49,
2014.
- Álvaro García-Pérez, Pablo Nogueira.
On the syntactic and functional correspondence between hybrid (or
layered) normalisers and abstract machines.
Science of Computer Programming,
Vol. 95,
páginas 176--199,
Elsevier,
2014.
- Dupressoir, Francois, Gordon, Andrew D., Jürjens, Jan, Naumann, David A..
Guiding a General-Purpose C Verifier to Prove
Cryptographic Protocols.
Journal of Computer Security (JCS),
Vol. 22,
Núm. 5,
páginas 823--866,
IOS Press,
2014.
Also appears as tech. rep. MSR-TR-2011-50.
- John P. Gallagher, Bishoksan Kafle.
Analysis and Transformation Tools for Constrained Horn Clause Verification.
Theory and Practice of Logic Programming,
Vol. 14,
Núm. 4-5 (supplementary materials),
páginas 90--101,
Cambridge University Press,
2014.
- David A. Basin, Manuel Clavel, Marina Egea, Miguel Ángel García de Dios, Carolina Dania.
A Model-Driven Methodology for Developing Secure Data-Management Applications.
IEEE Trans. Software Eng.,
Vol. 40,
Núm. 4,
páginas 324--337,
2014.
- Gilles Barthe, David Pichardie, Tamara Rezk.
A Certified Lightweight Non-interference Java Bytecode Verifier.
Mathematical Structures in Computer Science,
Vol. 23,
Núm. 5,
páginas 1032--1081,
Cambridge University Press,
Octubre
2013.
- Alexey Gotsman, Hongseok Yang.
Linearizability with ownership transfer.
Logical Methods in Computer Science,
Vol. 9,
Núm. 3,
Septiembre
2013.
- Alexey Gotsman, Hongseok Yang.
Modular verification of preemptive OS kernels.
Journal of Functional Programming,
Vol. 23,
Núm. 4,
páginas 452--514,
Cambridge University Press,
Julio
2013.
- Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
How to make ad hoc proof automation less ad hoc.
Journal of Functional Programming (JFP),
Vol. 23,
Núm. 4,
páginas 357--401,
Julio
2013.
- Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
Dependent Type Theory for Verification of Information Flow and Access Control Policies.
ACM Transactions on Programming Languages and Systems (TOPLAS),
Vol. 35,
Núm. 2(6),
páginas 1--6,
Julio
2013.
- Vigueras, Guillermo, Orduña, Juan M., Lozano, Miguel, Jégou, Yvon.
A Scalable Multiagent System Architecture for Interactive Applications.
Sci. Comput. Program.,
Vol. 78,
Núm. 6,
páginas 715--724,
Elsevier North-Holland, Inc.,
Junio
2013.
- D. Ivanovic, M. Carro, M. V. Hermenegildo.
A Sharing-Based Approach to Supporting Adaptation
in Service Compositions.
Computing,
Vol. 95,
Núm. 6,
páginas 453--492,
Springer Wien,
Junio
2013.
- Murdoch J. Gabbay, Aleksandar Nanevski.
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT).
Journal of Applied Logic (JAPPL),
Vol. 11,
Núm. 1,
páginas 1--29,
Marzo
2013.
- Juan Caballero, Dawn Song.
Automatic Protocol Reverse-Engineering: Message Format Extraction and Field Semantics.
Computer Networks,
Vol. 57,
Núm. 2,
páginas 451--474,
Elsevier,
Febrero
2013.
- Vigueras, Guillermo, Orduña, Juan M., Lozano, Miguel.
A Read-Copy Update based parallel server for distributed crowd simulations.
The Journal of Supercomputing,
Vol. 64,
Núm. 1,
páginas 156--166,
Springer US,
2013.
- C. Michler, A. N. Cookson, R. Chabiniok, E. Hyde, J. Lee, M. Sinclair, T. Sochi, A. Goyal, G. Vigueras, D. A. Nordsletten, N.P. Smith.
A computationally efficient framework for the simulation of cardiac perfusion using a multi-compartment Darcy porous-media flow model.
International Journal of Numerical Methods in Biomedical Engineering,
Vol. 29,
Núm. 2,
2013.
- Anindya Banerjee, David A. Naumann, Stan Rosenberg.
Local Reasoning for Global Invariants, Part I: Region Logic.
Journal of the ACM,
Vol. 60,
Núm. 3,
páginas 1--56,
ACM,
2013.
- Anindya Banerjee, David A. Naumann.
Local Reasoning for Global Invariants, Part II: Dynamic Boundaries.
Journal of the ACM,
Vol. 60,
Núm. 3,
páginas 1--73,
ACM,
2013.
- Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
Dependent Type Theory for Verification of Information Flow and Access Control Policies.
ACM Trans. Program. Lang. Syst.,
Vol. 35,
Núm. 2,
páginas 1--41,
ACM,
2013.
- Ahmed Bouajjani, Michael Emmi.
Analysis of Recursively Parallel Programs.
ACM Trans. Program. Lang. Syst.,
Vol. 35,
Núm. 3,
páginas 1--49,
2013.
- Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin.
Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks.
ACM Transactions on Programming Languages and Systems (TOPLAS), accepted for publication,
En Prensa, ACM,
2013.
- M. Carro, Ángel Herranz, Julio Mariño.
A Model-Driven Approach to Teaching Concurrency.
ACM Transactions on Computer Education,
Vol. 13,
Núm. 1,
2013.
- Kyriakos Kritikos, Barbara Pernici, Pierluigi Plebani, Cinzia Cappiello, Marco Comuzzi, Salima Benbernou, Ivona Brandic, Attila Kertesz, Michael Parkin, M. Carro.
A Survey on Service Quality Description.
ACM Computing Surveys,
Vol. 46,
Núm. 1,
2013.
- Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang.
Secure distributed programming with value-dependent types.
J. Funct. Program.,
Vol. 23,
Núm. 4,
páginas 402--451,
2013.
- Maria-Cristina Marinescu, César Sánchez.
Fusing Statecharts and Java.
ACM Transactions on Embedded Computing Systems,
Vol. 12,
páginas 1--21,
2013.
- Mark Marron, César Sánchez, Zhendong Su, Manuel Fähndrich.
Abstracting Runtime Heaps for Program Understanding.
IEEE Transactions on Software Engineering,
Vol. 39,
Núm. 6,
páginas 774--786,
IEEE Computer Society,
2013.
- Marina Zapater, César Sánchez, José L. Ayala, José M. Moya, José L. Risco-Martín.
Ubiquitous Green Computing Techniques for High Demand Applications in Smart Environments.
Sensors,
Vol. 12,
Núm. 8,
páginas 10659--10677,
Agosto
2012.
- Juan Caballero.
Understanding the Role of Malware in Cybercrime.
ERCIM News,
Vol. 2012,
Núm. 90,
páginas 15--16,
Julio
2012.
- M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, E. Mera, J.F. Morales, G. Puebla.
An Overview of Ciao and its Design Philosophy.
Theory and Practice of Logic Programming,
Vol. 12,
Núm. 1--2,
páginas 219--252,
Cambridge University Press,
Enero
2012.
- Gilles Barthe, Jorge Cuéllar, Javier Lopez, Alexander Pretschner.
Preface.
Journal of Computer Security,
Vol. 20,
Núm. 4,
páginas 307--308,
2012.
- Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir E. Dullerud.
Verification of Bounded Discrete Horizon Hybrid Automata.
IEEE Transactions on Automatic Control,
Vol. 57,
Núm. 6,
páginas 1445--1455,
2012.
- Patrick Cousot, Radhia Cousot, Laurent Mauborgne.
Theories, Solvers and Static Analysis by Abstract Interpretation.
Journal of the ACM,
En Prensa, ACM,
2012.
- Ganty, Pierre, Majumdar, Rupak.
Algorithmic verification of asynchronous programs.
ACM Trans. Program. Lang. Syst.,
Vol. 34,
Núm. 1,
páginas 1--48,
ACM,
2012.
- Pierre Ganty, Rupak Majumdar, Benjamin Monmege.
Bounded Underapproximations.
Formal Methods in System Design,
Vol. 40,
Núm. 2,
páginas 206--231,
2012.
- Boris Köpf, Pasquale Malacaria, Catuscia Palamidessi.
Quantitative Security Analysis (Dagstuhl Seminar 12481).
Dagstuhl Reports,
Vol. 2,
Núm. 11,
páginas 135--154,
2012.
- J. F. Morales, R. Haemmerlé, M. Carro, M. V. Hermenegildo.
Lightweight compilation of (C)LP to JavaScript.
Theory and Practice of Logic Programming, 28th Int'l. Conference on Logic Programming (ICLP'12) Special Issue,
Vol. 12,
Núm. 4-5,
páginas 755--773,
Cambridge U. Press,
2012.
- E. Albert, P. Arenas, G. Puebla, M. Hermenegildo.
Certificate Size Reduction in Abstraction-Carrying Code.
Theory and Practice of Logic Programming,
Vol. 12,
Núm. 3,
páginas 283--318,
2012.
- Isabella Mastroeni, Anindya Banerjee.
Modelling Declassification Policies using Abstract Domain Completeness.
Mathematical Structures in Computer Science,
Vol. 21,
Núm. 6,
páginas 1253--1299,
Diciembre
2011.
- Gilles Barthe, Pedro D'Argenio, Tamara Rezk.
Secure Information Flow by Self-Composition.
Mathematical Structures in Computer Science,
Vol. 21,
Núm. 6,
páginas 1207--1252,
Cambridge University Press,
Octubre
2011.
- Gilles Barthe, César Kunz.
An Abstract Model of Certificate Translation.
ACM Trans. Program. Lang. Syst.,
Vol. 33,
Núm. 4,
páginas 1--13,
ACM,
Julio
2011.
- P. Chico de Guzmán, A. Casas, M. Carro, M. V. Hermenegildo.
Parallel Backtracking with Answer Memoing for
Independent And-Parallelism.
Theory and Practice of Logic Programming, 27th
Int'l. Conference on Logic Programming (ICLP'11)
Special Issue,
Vol. 11,
Núm. 4--5,
páginas 555--574,
Cambridge U. Press,
Julio
2011.
- Julien Bertrane, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, X. Rival.
Static Analysis by Abstract Interpretation of Embedded Critical
Software.
Software Engineering Notes,
Vol. 36,
Núm. 1,
páginas 1--8,
ACM,
Enero
2011.
- G. Puebla, E. Albert, M. V. Hermenegildo.
Efficient Local Unfolding with Ancestor Stacks.
Theory and Practice of Logic Programming,
Vol. 11,
Núm. 1,
páginas 1--32,
Cambridge U. Press,
Enero
2011.
- Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger.
Parikh's Theorem: A simple and direct automaton construction.
Information Processing Letters,
Vol. 111,
páginas 614--619,
2011.
- Boris Köpf, David Basin.
Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks.
Journal of Computer Security,
Vol. 1,
páginas 1--31,
2011.
- Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld.
Security of Multithreaded Programs by Compilation.
ACM Trans. Inf. Syst. Secur.,
Vol. 13,
Núm. 3,
2010.
- M. Egea, V. Rusu.
Formal Executable Semantics for Conformance in the MDE Framework.
Innovations in Systems and Software Engineering,
Vol. 6,
páginas 73--81,
Springer London,
2010.
- Pierre Ganty, Nicolas Maquet, Jean-Francois Raskin.
Fixed Point Guided Abstraction Refinement for Alternating Automata.
Theor. Comput. Sci.,
Vol. 411,
Núm. 38-39,
páginas 3444--3459,
2010.
- A. Stivala, P. J. Stuckey, M. García de la Banda, M. V. Hermenegildo, A. Wirth.
Lock-free Parallel Dynamic Programming.
Journal of Parallel and Distributed Computing,
Vol. 70,
Núm. 8,
páginas 839--848,
Elsevier,
2010.
- P. Lopez-Garcia, F. Bueno, M. V. Hermenegildo.
Automatic Inference of Determinacy and Mutual Exclusion for
Logic Programs Using Mode and Type Analyses.
New Generation Computing,
Vol. 28,
Núm. 2,
páginas 117--206,
Ohmsha, Ltd. and Springer,
2010.
- D. Cabeza, M. Hermenegildo.
Non-Strict Independence-Based Program
Parallelization Using Sharing and Freeness
Information.
Theoretical Computer Science,
Vol. 410,
Núm. 46,
páginas 4704--4723,
Elsevier Science,
Octubre
2009.
- Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk.
Certificate Translation for Optimizing Compilers.
ACM Trans. Program. Lang. Syst.,
Vol. 31,
Núm. 5,
ACM,
Julio
2009.
- Elvira Albert, John P. Gallagher, Miguel Gómez-Zamalloa, Germán Puebla.
Type-based homeomorphic embedding for online termination.
Inf. Process. Lett.,
Vol. 109,
Núm. 15,
páginas 879--886,
Elsevier,
Julio
2009.
- Toufik Taibi, Ángel Herranz, Juan José
Moreno-Navarro.
Stepwise Refinement Validation of Design Patterns Formalized
in TLA+ Using the TLC Model Checker.
Journal of Object Technology (JOT, (available online)),
Vol. 8,
Núm. 2,
páginas 137--161,
Marzo
2009.
- Julio Mariño, Juan José Moreno-Navarro, Susana Muñoz
Hernández.
Implementing Constructive Intensional Negation.
New Generation Computing,
Vol. 27,
Núm. 1,
páginas 25--56,
Enero
2009.
- D. Basin, M. Clavel, J. Doser, M. Egea.
Automated Analysis of Security-Design Models.
Information & Software Technology,
Vol. 51,
Núm. 5,
páginas 815--831,
2009.
- E. Albert, G. Puebla, M. V. Hermenegildo.
Abstraction-Carrying Code: A Model for Mobile
Code Safety.
New Generation Computing,
Vol. 26,
Núm. 2,
páginas 171--204,
Marzo
2008.
- Julio Mariño, Ángel Herranz, Juan José
Moreno-Navarro.
Demandedness Analysis with Partial Predicates.
Theory and Practice of Logic Programming,
Vol. 7,
Núm. 1-2,
páginas 153--182,
Enero
2007.
- M. Clavel, J. Meseguer, M. Palomino.
Reflection in Membership Equational Logic, Many-Sorted Equational
Logic, Horn Logic with Equality, and Rewriting Logic.
Theoretical Computer Science,
Vol. 373,
Núm. 1-2,
páginas 70--91,
2007.
Artículos en Congresos con Revisión Estricta
- Matthias Götze, Srdjan Matic, Costas Iordanou, Georgios Smaragdakis, Nikolaos Laoutaris.
Measuring Web Cookies in Governmental Websites.
14th ACM Web Science Conference,
páginas 44--54,
ACM,
Junio
2022.
- Daniel Domínguez-Álvarez, Daniel Tomic, Alessandra Gorla.
ReChan: An Automated Analysis of Android App Release
Notes to Report Inconsistencies.
MobileSoft 2019: Proceedings of the 9th IEEE/ACM
International Conference on Mobile Software
Engineering and Systems,
Mayo
2022.
To appear.
- Mattia Fazzini, Chase Choi, Juan Manuel Copia, Gabriel Lee, Yoshiki Kakehi, Alessandra Gorla, Alessandro Orso.
Use of Test Doubles in Android Testing: An In-Depth Investigation.
ICSE 2022: Proceedings of the 44th International
Conference on Software Engineering,
Mayo
2022.
To appear.
- Sri Aravinda Krishnan Thyagarajan, Giulio Malavolta, Pedro Moreno-Sanchez.
Universal Atomic Swaps: Secure Exchange of Coins Across All Blockchains.
Proceedings of the 43nd IEEE Symposium on Security and Privacy,
Mayo
2022.
- Guria, Sankha Narayan, Vazou, Niki, Guarnieri, Marco, Parker, James.
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification.
Proceedings of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation,
PLDI 2022,
ACM,
2022.
- Veronica Dahl, Juan José Moreno-Navarro.
Doughnut Computing in City Planning for Achieving Human and Planetary
Rights.
Bio-inspired Systems and Applications: from Robotics to Ambient Intelligence
- 9th International Work-Conference on the Interplay Between Natural
and Artificial Computation, IWINAC 2022, Proceedings, Part II,
Lecture Notes in Computer Science,
Vol. 13259,
páginas 562--572,
Springer,
2022.
- Joaquín Arias, Manuel Carro, Gopal Gupta.
Towards Dynamic Consistency Checking in Goal-Directed Predicate Answer
Set Programming.
24th International Symposium Practical Aspects of Declarative Languages,
PADL 2022,
LNCS,
Vol. 13165,
páginas 117--134,
Springer,
2022.
- Matteo Campanelli, Antonio Faonio, Dario Fiore, Anaïs Querol, Hadrián Rodriguez.
Lunar: a Toolbox for More Efficient Universal and Updatable zkSNARKs and Commit-and-Prove Extensions.
ASIACRYPT 2021: 27th Annual International Conference on the Theory and Applications of Cryptology and Information Security,
Lecture Notes in Computer Science,
Vol. 13092,
páginas 3--33,
Springer,
Diciembre
2021.
- Lukas Aumayr, Oguzhan Ersoy, Andreas Erwig, Sebastian Faust, Kristina Hostáková, Matteo Maffei, Pedro Moreno-Sanchez, Siavash Riahi.
Generalized Channels from Limited Blockchain Scripts and Adaptor Signatures.
ASIACRYPT 2021: 27th Annual International Conference on the Theory and Applications of Cryptology and Information Security,
LNCS,
Vol. 13091,
páginas 635--664,
Springer,
Diciembre
2021.
- Lukas Aumayr, Pedro Moreno-Sanchez, Aniket Kate, Matteo Maffei.
Blitz: Secure Multi-Hop Payments Without Two-Phase Commits.
30th USENIX Security Symposium,
páginas 4043--4060,
USENIX Association,
Agosto
2021.
- Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala.
STORM: Refinement Types for Secure Web Applications.
15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21),
páginas 441--459,
USENIX Association,
Julio
2021.
- Eduardo Blázquez, Sergio Pastrana, Álvaro Feal, Julien Gamba, Platon Kotzias, Narseo Vallina-Rodriguez, Juan Tapiador.
Trouble Over-The-Air: An Analysis of FOTA Apps in the Android Ecosystem.
42nd IEEE Symposium on Security and Privacy, SP 2021,
páginas 1606--1622,
IEEE,
Mayo
2021.
- Lukas Aumayr, Matteo Maffei, Oguzhan Ersoy, Andreas Erwig, Sebastian Faust, Siavash Riahi, Kristina Hostáková, Pedro Moreno-Sanchez.
Bitcoin-Compatible Virtual Channels.
Proceedings of the 42nd IEEE Symposium on Security and Privacy,
páginas 901--918,
IEEE,
Mayo
2021.
- Erkan Tairi, Pedro Moreno-Sanchez, Matteo Maffei.
A2L: Anonymous Atomic Locks for Scalability and Interoperability
in Payment Channel Hubs.
Proceedings of the 42nd IEEE Symposium on Security and Privacy,
páginas 1834--1851,
IEEE,
Mayo
2021.
- Platon Kotzias, Juan Caballero, Leyla Bilge.
How Did That Get In My Phone? Unwanted App Distribution on Android Devices.
Proceedings of the 42nd IEEE Symposium on Security and Privacy,
páginas 53--69,
IEEE,
Mayo
2021.
- Marco Guarnieri, Boris Köpf, Jan Reineke, Pepe Vila.
Hardware-Software Contracts for Secure Speculation.
Proceedings of the 42nd IEEE Symposium on Security and Privacy,
S&P 2021,
IEEE,
2021.
- Marco Patrignani, Marco Guarnieri.
Exorcising Spectres with Secure Compilers.
Proceedings of the 28th ACM Conference on Computer and Communications Security,
CCS 2021,
páginas 445--461,
ACM,
2021.
- Enrico Bacis, Dario Facchinetti, Marco Guarnieri, Marco Rosa, Matthew Rossi, Stefano Paraboschi.
I Told You Tomorrow: Practical Time-Locked Secrets Using Smart Contracts.
Proceedings of the 16th International Conference on Availability, Reliability and Security,
ARES 2021,
ACM,
2021.
- Marco Guarnieri, Boris Köpf, Jan Reineke, Pepe Vila.
Hardware-Software Contracts for Secure Speculation.
42nd IEEE Symposium on Security and Privacy, SP 2021,
páginas 1868--1883,
IEEE,
2021.
- Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya.
Structured Leakage and Applications to Cryptographic Constant-Time
and Cost.
CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications
Security,
páginas 462--476,
ACM,
2021.
- Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub.
Mechanized Proofs of Adversarial Complexity and Application to Universal
Composability.
CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications
Security,
páginas 2541--2563,
ACM,
2021.
- Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou.
EasyPQC: Verifying Post-Quantum Cryptography.
CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications
Security,
páginas 2564--2586,
ACM,
2021.
- Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie.
Secure Compilation of Constant-Resource Programs.
34th IEEE Computer Security Foundations Symposium, CSF 2021,
páginas 1--12,
IEEE,
2021.
- Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu.
A Quantum Interpretation of Bunched Logic & Quantum Separation
Logic.
36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS
2021,
páginas 1--14,
IEEE,
2021.
- Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno.
SoK: Computer-Aided Cryptography.
42nd IEEE Symposium on Security and Privacy, SP 2021,
páginas 777--795,
IEEE,
2021.
- Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe.
High-Assurance Cryptography in the Spectre Era.
42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco,
CA, USA, 24-27 May 2021,
páginas 1884--1901,
IEEE,
2021.
- Man-Kit Sit, Manuel Bravo, Zsolt István.
An experimental framework for improving the performance of BFT consensus
for future permissioned blockchains.
DEBS '21: The 15th ACM International Conference on Distributed
and Event-based Systems,
páginas 55--65,
ACM,
2021.
- Manuel Bravo, Alexey Gotsman, Borja de Régil, Hengfeng Wei.
UniStore: A fault-tolerant marriage of causal and strong consistency.
USENIX ATC'21: USENIX Annual Technical Conference,
páginas 923--937,
USENIX,
2021.
- Vitor Enes, Carlos Baquero, Alexey Gotsman, Pierre Sutra.
Efficient replication via timestamp stability.
EuroSys'21: European Conference on Computer Systems,
páginas 178--193,
ACM,
2021.
- Alexandre Bois, Ignacio Cascudo, Dario Fiore, Dongwoo Kim.
Flexible and Efficient Verifiable Computation on Encrypted Data.
Public-Key Cryptography - PKC 2021 - 24th IACR International Conference
on Practice and Theory of Public-Key Cryptography, Proceedings, Part II,
Lecture Notes in Computer Science,
Vol. 12711,
páginas 528--558,
Springer,
2021.
- Daniel Benarroch, Matteo Campanelli, Dario Fiore, Kobi Gurkan, Dimitris Kolonelos.
Zero-Knowledge Proofs for Set Membership: Efficient, Succinct, Modular.
Financial Cryptography and Data Security: 25th International Conference, FC 2021, Virtual Event, March 1–5, 2021, Revised Selected Papers, Part I ,
Lecture Notes in Computer Science,
Springer,
2021.
- Ismaël Jecker, Nicolas Mazzocchi, Petra Wolf.
Decomposing Permutation Automata.
32nd International Conference on Concurrency Theory (CONCUR 2021),
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 203,
páginas 1--19,
Schloss Dagstuhl -- Leibniz-Zentrum für Informatik,
2021.
- Erkan Tairi, Pedro Moreno-Sanchez, Matteo Maffei.
Post-Quantum Adaptor Signature for Privacy-Preserving Off-Chain Payments.
Proceedings of the 25th International Conference on Financial Cryptography and Data Security,
Lecture Notes in Computer Science,
Vol. 12675,
páginas 131--150,
Springer,
2021.
- Matteo Romiti, Friedhelm Victor, Pedro Moreno-Sanchez, Peter Sebastian Nordholt, Bernhard Haslhofer, Matteo Maffei.
Cross-Layer Deanonymization Methods in the Lightning Protocol.
25th International Conference on Financial Cryptography and Data Security,
Lecture Notes in Computer Science,
Vol. 12674,
páginas 187--204,
Springer,
2021.
- Alexei Zamyatin, Mustafa Al-Bassam, Dionysis Zindros, Elefterios Kokoris-Kogias, Pedro Moreno-Sanchez, Aggelos Kiayias, William Knottenbelt.
SoK: Communication Across Distributed Ledgers.
25th International Conference on Financial Cryptography and Data Security,
Lecture Notes in Computer Science,
Vol. 12675,
páginas 3--36,
Springer,
2021.
- Kyveli Doveri, Pierre Ganty, Francesco Parolini, Francesco Ranzato.
Inclusion Testing of Büchi Automata Based on Well-Quasiorders.
32nd International Conference on Concurrency Theory (CONCUR 2021),
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 203,
páginas 1--22,
Schloss Dagstuhl -- Leibniz-Zentrum für Informatik,
2021.
- Ignacio Casso, José F. Morales, Pedro López-García, Manuel V. Hermenegildo.
Testing Your (Static Analysis) Truths.
Logic-Based Program Synthesis and Transformation - 30th International
Symposium, Post-Proceedings,
Lecture Notes in Computer Science,
Vol. 12561,
páginas 271--292,
Springer,
2021.
- Ashley Fraser, Lydia Garms, Anja Lehmann.
Selectively Linkable Group Signatures - Stronger Security and Preserved
Verifiability.
Cryptology and Network Security - 20th International Conference, CANS
2021,
Lecture Notes in Computer Science,
Vol. 13099,
páginas 200--221,
Springer,
2021.
- Felipe Gorostiaga, César Sánchez.
Nested Monitors: Monitors as Expressions to Build Monitors.
Proc. of the 21st Int'l Conference on Runtime Verification (RV'21),
LNCS,
Vol. 12974,
páginas 164--183,
Springer,
2021.
- César Sánchez.
Synchronous and asynchronous stream runtime verification.
Proc. of the 5th ACM Int'l Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21),
páginas 5--7,
ACM,
2021.
- Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez.
A Temporal Logic for Asynchronous Hyperproperties.
Proc. of the 33rd Int'l Conf. on Computer Aided Verification (CAV'21), Part I,
LNCS,
Vol. 12759,
páginas 694--717,
Springer,
2021.
- Felipe Gorostiaga, César Sánchez.
HStriver: A Very Functional Extensible Tool for the
Runtime Verification of Real-Time Event Streams.
Proc. of the 24th Int'l Symp. on Formal Methods (FM'21),
LNCS,
Vol. 13047,
páginas 563--580,
Springer,
2021.
- Sebastián Zudaire, Felipe Gorostiaga, César Sánchez, Gerardo Schneider, Sebastián Uchitel.
Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions.
Proc. of the IEEE Int'l Conf. on Robotics and Automation, (ICRA'21),
páginas 6824--6830,
IEEE,
2021.
- Laura Bozzelli, Adriano Peron, César Sánchez.
Asynchronous Extensions of HyperLTL.
Proc. of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'21),
páginas 1--13,
IEEE,
2021.
- Felipe Gorostiaga, César Sánchez.
HLola: a Very Functional Tool for Extensible Stream Runtime Verification.
Proc. of the 27th Int'l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21). Part II,
LNCS,
Vol. 12652,
páginas 349--356,
Springer,
2021.
- Tzu-Han Hsu, César Sánchez, Borzoo Bonakdarpour.
Bounded Model Checking for Hyperproperties.
Proc. of the 27th Int'l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21). Part I,
LNCS,
Vol. 12651,
páginas 94--112,
Springer,
2021.
- Daniel Wilms, Carsten Stöcker, Juan Caballero.
Data Provenance in Vehicle Data Chains.
93rd IEEE Vehicular Technology Conference, VTC Spring 2021,
páginas 1--5,
IEEE,
2021.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira.
Certified Compilation for Cryptography: Extended x86 Instructions
and Constant-Time Verification.
21st International Conference on Cryptology in India, INDOCRYPT 2020,
Lecture Notes in Computer Science,
Vol. 12578,
páginas 107--127,
Springer,
Diciembre
2020.
- Matteo Campanelli, Dario Fiore, Nicola Grego, Dimitris Kolonelos, Luca Nizzardo.
Incrementally Aggregatable Vector Commitments and Applications to Verifiable Decentralized Storage.
ASIACRYPT 2020: 26th Annual International Conference on the Theory and Applications of Cryptology and Information Security,
LNCS,
Vol. 12492,
páginas 3--35,
Springer,
Diciembre
2020.
- Ignacio Cascudo, Bernardo David.
ALBATROSS: Publicly AttestabLe BATched Randomness Based On Secret Sharing.
Advances in Cryptology - ASIACRYPT 2020 -26th International Conference
on the Theory and Application of Cryptology and Information Security, Part III,
Lecture Notes in Computer Science,
Vol. 12493,
páginas 311--341,
Springer,
Diciembre
2020.
- Ignacio Cascudo, Jaron Skovsted Gundersen.
A Secret-Sharing Based MPC Protocol for Boolean Circuits with Good Amortized Complexity.
Theory of Cryptography- 18th International Conference, TCC 2020, Part II,
Lecture Notes in Computer Science,
Vol. 12551,
páginas 652--682,
Springer,
Diciembre
2020.
- Silvia Sebastián, Juan Caballero.
AVClass2: Massive Malware Tag Extraction from AV Labels.
Proceedings of the 2020 Annual Computer Security Applications Conference,
Diciembre
2020.
- Fabio Gadducci, Hernán C. Melgratti, Christian Roldán, Matteo Sammartino.
Implementation Correctness for Replicated Data Types, Categorically.
International Colloquium on Theoretical Aspects of Computing, ICTAC 2020,
LNCS,
Vol. 12545,
páginas 283--303,
Springer,
Noviembre
2020.
- Silvia Sebastián, Juan Caballero.
Towards Attribution in Mobile Markets: Identifying Developer Account Polymorphism.
Proceedings of the 27th ACM Conference on Computer and Communication Security,
Noviembre
2020.
- Nataliia Stulova, Arianna Blasi, Alessandra Gorla, Oscar Nierstrasz.
Towards Detecting Inconsistent Comments in Java Source Code Automatically.
20th IEEE International Working Conference on Source Code Analysis
and Manipulation, SCAM 2020,
páginas 65--69,
IEEE,
Octubre
2020.
- Antonio Faonio, Dario Fiore.
Improving the Efficiency of Re-randomizable and Replayable CCA Secure
Public Key Encryption.
Applied Cryptography and Network Security - 18th International Conference, ACNS 2020,
LNCS,
Vol. 12146,
páginas 271--291,
Springer,
Octubre
2020.
- Mattia Fazzini, Alessandra Gorla, Alessandro Orso.
A Framework for Automated Test Mocking of Mobile Apps.
35th IEEE/ACM International Conference on Automated Software Engineering,
ASE 2020,
páginas 1204--1208,
IEEE,
Septiembre
2020.
- Frantisek Farka.
slepice: Towards a Verified Implementation of Type Theory in Type
Theory.
30th International Symposium on Logic-Based Program
Synthesis and Transformation, LOPSTR 2020,
LNCS,
Vol. 12561,
páginas 133--150,
Springer,
Septiembre
2020.
- Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera.
Model-Agnostic Counterfactual Explanations for Consequential Decisions.
The 23rd International Conference on Artificial Intelligence and Statistics,
AISTATS 2020,
Proceedings of Machine Learning Research,
Vol. 108,
páginas 895--905,
PMLR,
Agosto
2020.
- Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato.
Hypothesis Testing Interpretations and Renyi Differential Privacy.
The 23rd International Conference on Artificial Intelligence and Statistics,
AISTATS 2020,
Proceedings of Machine Learning Research,
Vol. 108,
páginas 2496--2506,
PMLR,
Agosto
2020.
- Gianluca Brian, Antonio Faonio, Maciej Obremski, Mark Simkin, Daniele Venturi.
Non-malleable Secret Sharing Against Bounded Joint-Tampering Attacks
in the Plain Model.
40th Annual International Cryptology Conference, CRYPTO 2020,
LNCS,
Vol. 12172,
páginas 127--155,
Springer,
Agosto
2020.
- Nuno Afonso, Manuel Bravo, Luís Rodrigues.
Combining High Throughput and Low Migration Latency for Consistent
Data Storage on the Edge.
29th International Conference on Computer Communications and Networks,
ICCCN 2020,
páginas 1--11,
IEEE,
Agosto
2020.
- Gianluca Brian, Antonio Faonio, Maciej Obremski, Mark Simkin, Daniele Venturi.
Non-malleable Secret Sharing Against Bounded Joint-Tampering Attacks
in the Plain Model.
40th Annual International Cryptology Conference, CRYPTO 2020,
LNCS,
Vol. 12172,
páginas 127--155,
Springer,
Agosto
2020.
- Pierre Ganty, Elena Gutiérrez, Pedro Valero.
A Quasiorder-Based Perspective on Residual Automata.
45th International Symposium on Mathematical Foundations of Computer
Science, MFCS 2020,
LIPIcs,
Vol. 170,
páginas 1--14,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
Agosto
2020.
- Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan.
Deciding Differential Privacy for Programs with Finite Inputs and
Outputs.
35th Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS '20,
páginas 141--154,
ACM,
Julio
2020.
- Gilles Barthe, Charlie Jacomme, Steve Kremer.
Universal equivalence and majority of probabilistic programs over
finite fields.
35th Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS '20,
páginas 155--166,
ACM,
Julio
2020.
- Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe.
Constant-time foundations for the new spectre era.
Proceedings of the 41st ACM SIGPLAN International Conference on
Programming Language Design and Implementation, PLDI 2020,
páginas 913--926,
ACM,
Junio
2020.
- Paolo Calciati, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller.
Automatically Granted Permissions in Android apps: An Empirical Study
on their Prevalence and on the Potential Threats for Privacy.
MSR 2020: 17th International Conference on Mining Software Repositories,
páginas 114--124,
ACM,
Junio
2020.
- Uwe Wolter, Fernando Macías, Adrian Rutle.
Multilevel Typed Graph Transformations.
Graph Transformation - 13th International Conference, ICGT 2020,
LNCS,
Vol. 12150,
páginas 163--182,
Springer,
Junio
2020.
- Pepe Vila, Pierre Ganty, Marco Guarnieri, Boris Köpf.
CacheQuery: Learning Replacement Policies from Hardware Caches.
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation,
PLDI 2020,
páginas 519--532,
ACM,
Junio
2020.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub.
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
2020 IEEE Symposium on Security and Privacy, SP 2020,
páginas 965--982,
IEEE,
Mayo
2020.
- Dario Fiore, Anca Nitulescu, David Pointcheval.
Boosting Verifiable Computation on Encrypted Data.
23rd IACR International Conference
on Practice and Theory of Public-Key Cryptography, PKC 2020,
LNCS,
Vol. 12111,
páginas 124--154,
Springer,
Mayo
2020.
- Dario Catalano, Mario Di Raimondo, Dario Fiore, Irene Giacomelli.
MonZa:
Fast Maliciously Secure Two Party Computation on Z2k.
23rd IACR International Conference
on Practice and Theory of Public-Key Cryptography, PKC 2020,
LNCS,
Vol. 12111,
páginas 357--386,
Springer,
Mayo
2020.
- Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo.
On the Versatility of Open Logical Relations - Continuity, Automatic
Differentiation, and a Containment Theorem.
29th European Symposium on Programming,
ESOP 2020, Held as Part of ETAPS 2020,
Lecture Notes in Computer Science,
Vol. 12075,
páginas 56--83,
Springer,
Abril
2020.
- I. Casso, J. F. Morales, P. Lopez-Garcia, R. Giacobazzi, M. V. Hermenegildo.
Computing Abstract Distances in Logic Programs.
Post-Proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation
(LOPSTR'19),
LNCS,
Vol. 12042,
Springer-Verlag,
Abril
2020.
- I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
An Integrated Approach to Assertion-Based Random Testing in Prolog.
Post-Proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation
(LOPSTR'19),
LNCS,
Vol. 12042,
páginas 159--176,
Springer-Verlag,
Abril
2020.
- M. Klemen, P. Lopez-Garcia, J. Gallagher, J.F. Morales, M. V. Hermenegildo.
A General Framework for Static Cost Analysis of Parallel Logic Programs.
Post-Proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation (LOPSTR'19),
LNCS,
Vol. 12042,
páginas 19--35,
Springer-Verlag,
Abril
2020.
- Avinash Sudhodanan, Soheil Khodayari, Juan Caballero.
Cross-Origin State Inference (COSI) Attacks: Leaking Web Site States through XS-Leaks.
Network and Distributed Systems Security Symposium,
Febrero
2020.
- R. Bruni, R. Giacobazzi, R. Gori, I. Garcia-Contreras, D. Pavlovic.
Abstract Extensionality -- On the Properties of Incomplete Abstract Interpretations.
Proc. ACM Symposium on Principles of Programming Languages 2020,
Enero
2020.
- Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, Andrés Sánchez
.
Spectector: Principled detection of speculative information flows.
Proceedings of the 41st IEEE Symposium on Security and Privacy,
S&P 2020,
IEEE,
2020.
- Martín Ceresa, Felipe Gorostiaga, César Sánchez.
Declarative Stream Runtime Verification (hLola).
LNCS,
Vol. 12470,
páginas 25--43,
Springer,
2020.
- Alvaro Feal, Paolo Calciati, Narseo Vallina-Rodriguez, Carmela Troncoso, Alessandra Gorla.
Angel or Devil? A Privacy Study of Mobile Parental
Control Apps.
The 20th Privacy Enhancing Technologies Symposium (PoPETs 2020.2),
páginas 314--335,
2020.
- Manuel Bravo, Gregory Chockler, Alexey Gotsman.
Making Byzantine consensus live.
DISC'20: International Symposium on Distributed Computing,
LIPICS,
Vol. 179,
Dagstuhl,
2020.
- Vitor Enes, Carlos Baquero, Tuanir França Rezende, Alexey Gotsman, Matthieu Perrin, Pierre Sutra.
State-machine replication for planet-scale systems.
EuroSys'20: European Conference on Computer Systems,
ACM,
2020.
- I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
Incremental Analysis of Logic Programs with Assertions and Open Predicates.
Proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation (LOPSTR'19),
LNCS,
Vol. 12042,
páginas 36--56,
Springer,
2020.
- Joaquín Arias, Zhuo Chen, Manuel Carro, Gopal Gupta.
Modeling and Reasoning in Event Calculus Using Goal-Directed Constraint
Answer Set Programming.
Post-Proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation (LOPSTR'19),
LNCS,
Vol. 12042,
páginas 139--155,
Springer-Verlag,
2020.
- Martín Ceresa, Felipe Gorostiaga, César Sánchez.
Declarative Stream Runtime Verification (hLola).
Proc. of the 18th Asian Symposium on Programming Languages and Systems (APLAS'20),
LNCS,
Vol. 12470,
páginas 25--43,
Springer,
2020.
- Gordon J. Pace, César Sánchez, Gerardo Schneider.
Reliable Smart Contracts.
Proc. of the 9th Int'l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2020). Verification. Part III,
LNCS,
Vol. 12478,
páginas 3--8,
Springer,
2020.
- Borzoo Bonakdarpour, Pavithra Prabhakar, César Sánchez.
Model Checking Timed Hyperproperties in Discrete-Time Systems.
Proc. of the 12th NASA Formal Methods Symposium (NFM'2020),
LNCS,
Vol. 12229,
páginas 311--328,
Springer,
2020.
- Felipe Gorostiaga, Luis Miguel Danielsson, César Sánchez.
Unifying the Time-Event Spectrum for Stream Runtime Verification.
Proc. of the 20th Int'l Conf on Runtime Verification (RV'20),
LNCS,
Vol. 12399,
páginas 462--481,
Springer,
2020.
- Xueliang Li, Yuming Yang, Yepang Liu, John P. Gallagher, Kaishun Wu.
Detecting and Diagnosing Energy Issues for Mobile Applications.
Proc. of the ACM SIGSOFT International Symposium on Software Testing and Analysis,
ACM Press,
2020.
- John P. Gallagher, Robert Glück.
An Experiment Combining Specialization with Abstract Interpretation.
Proceedings 8th International Workshop on Verification and Program
Transformation and 7th Workshop on Horn Clauses for Verification and
Synthesis, VPT/HCV (ETAPS) 2020, and 7th Workshop on Horn Clauses
for Verification and Synthesis,
EPTCS,
Vol. 320,
páginas 155--158,
2020.
- Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek.
Privacy Amplification by Mixing and Diffusion Mechanisms.
Advances in Neural Information Processing Systems 32: Annual Conference
on Neural Information Processing Systems (NeurIPS 2019),
páginas 13277--13287,
Diciembre
2019.
- Gianluca Brian, Antonio Faonio, Daniele Venturi.
Continuously Non-malleable Secret Sharing for General Access Structures.
Theory of Cryptography - 17th International Conference, TCC 2019,
Proceedings, Part II,
Lecture Notes in Computer Science,
Vol. 11892,
páginas 211--232,
Springer,
Diciembre
2019.
- Gianluca Brian, Antonio Faonio, Daniele Venturi.
Continuously Non-malleable Secret Sharing for General Access Structures.
Theory of Cryptography - 17th International Conference, TCC 2019,
Proceedings, Part II,
Lecture Notes in Computer Science,
Vol. 11892,
páginas 211--232,
Springer,
Diciembre
2019.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran.
A Machine-Checked Proof of Security for AWS Key Management Service.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2019,
páginas 63--78,
ACM,
Noviembre
2019.
- José Bacelar Almeida, Cecile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub.
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability
of Sponge and Secure High-Assurance Implementations of SHA-3.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2019,
páginas 1607--1622,
ACM,
Noviembre
2019.
- Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Mélissa Rossi, Mehdi Tibouchi.
GALACTICS: Gaussian Sampling for Lattice-Based Constant- Time Implementation
of Cryptographic Signatures, Revisited.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2019,
páginas 2147--2164,
ACM,
Noviembre
2019.
- Piotr Mardziel, Niki Vazou.
PLAS 2019: ACM SIGSAC Workshop on Programming Languages and
Analysis for Security.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2019,
Noviembre
2019.
- Antonio Faonio, Dario Fiore, Javier Herranz, Carla R`afols.
Structure-Preserving and Re-randomizable RCCA-secure Public Key Encryption and its Applications.
ASIACRYPT 2019: 25th Annual International Conference on the Theory and Applications of Cryptology and Information Security,
LNCS,
Springer,
Noviembre
2019.
- Matteo Campanelli, Dario Fiore, Anaïs Querol.
LegoSNARK: Modular Design and Composition of Succinct Zero-Knowledge Proofs.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security,
CCS '19,
páginas 2075--2092,
ACM,
Noviembre
2019.
- Ignacio Cascudo, Ivan Damgrd, Bernardo David, Nico Döttling, Rafael Dowsley, Irene Giacomelli.
Efficient UC Commitment Extension with Homomorphism for Free (and
Applications).
Advances in Cryptology - ASIACRYPT 2019 -25th International Conference
on the Theory and Application of Cryptology and Information Security,
páginas 606--635,
Noviembre
2019.
- Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei.
Verifying Relational Properties using Trace Logic.
Formal Methods in Computer Aided Design, FMCAD 2019,
páginas 170--178,
IEEE,
Octubre
2019.
- Artem Khyzha, Hagit Attiya, Alexey Gotsman.
Privatization-safe transactional memories.
DISC'19: International Symposium on Distributed Computing,
LIPICS,
Vol. 146,
páginas 1--17,
Dagstuhl,
Octubre
2019.
- Luis Miguel Danielsson, César Sánchez.
Decentralized Stream Runtime Verification.
Proc. of the 19th Int'l Conf. on Runtime Verification (RV'19),
Lecture Notes in Computer Science,
Vol. 11757,
páginas 185--201,
Springer,
Octubre
2019.
- Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, Daniel Thoma.
Runtime Verification for Timed Event Streams with Partial Information.
Proc. of the 19th Int'l Conf. on Runtime Verification (RV'19),
Lecture Notes in Computer Science,
Vol. 11757,
páginas 273--291,
Springer,
Octubre
2019.
- Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, Francois-Xavier Standaert.
maskVerif: Automated Verification of Higher-Order Masking in Presence
of Physical Defaults.
Computer Security - ESORICS 2019 - 24th European Symposium on Research
in Computer Security, Proceedings, Part I,
Lecture Notes in Computer Science,
Vol. 11735,
páginas 300--318,
Springer,
Septiembre
2019.
- Manuel Bravo, Alexey Gotsman.
Reconfigurable atomic transaction commit.
PODC'19: Symposium on Principles of Distributed Computing,
páginas 399--408,
ACM Press,
Agosto
2019.
- Iskander Sánchez-Rola, Matteo Dell'Amico, Platon Kotzias, Davide Balzarotti, Leyla Bilge, Pierre-Antoine Vervier, Igor Santos.
Can I Opt Out Yet?: GDPR and the Global Illusion of Cookie Control.
Proceedings of the 2019 ACM Asia Conference on Computer and Communications
Security, AsiaCCS 2019,
páginas 340--351,
ACM,
Julio
2019.
- Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub.
Symbolic Methods in Computational Cryptography Proofs.
32nd IEEE Computer Security Foundations Symposium, CSF 2019,
páginas 136--151,
IEEE,
Junio
2019.
- Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata.
Approximate Span Liftings: Compositional Semantics for Relaxations
of Differential Privacy.
34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS
2019, Vancouver, BC, Canada,
páginas 1--14,
IEEE,
Junio
2019.
- Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan.
FaCT: a DSL for timing-sensitive computation.
Proceedings of the 40th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI 2019,
páginas 174--189,
ACM,
Junio
2019.
- Ezgi Cicek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg.
Bidirectional type checking for relational properties.
Proceedings of the 40th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI 2019,
páginas 533--547,
ACM,
Junio
2019.
- Alexey Gotsman, Anatole Lefort, Gregory Chockler.
White-box atomic multicast.
DSN'19: International Conference on Dependable Systems and Networks,
páginas 176--187,
IEEE Press,
Junio
2019.
- Pepe Vila, Boris Köpf, Jose Morales.
Theory and Practice of Finding Eviction Sets.
Proc. 40th IEEE Symposium on Security and Privacy (S& P '19),
páginas 39--54,
IEEE,
Mayo
2019.
- John P. Gallagher.
Polyvariant Program Specialisation with Property-based Abstraction.
Proceedings Seventh International Workshop on Verification and Program
Transformation (VPT),
EPTCS,
Vol. 299,
páginas 34--48,
Abril
2019.
- Platon Kotzias, Leyla Bilge, Pierre-Antoine Vervier, Juan Caballero.
Mind your Own Business: A Longitudinal Study of Threats and Vulnerabilities in Enterprises.
Network and Distributed Systems Security Symposium,
Febrero
2019.
- Joaquín Arias, Manuel Carro.
Incremental Evaluation of Lattice-Based Aggregates in Logic Programming
Using Modular TCLP.
21st Int'l. Symposium on Practical Aspects of
Declarative Languages,
LNCS,
Vol. 11372,
páginas 98--114,
Springer,
Enero
2019.
- I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
Multivariant Assertion-based Guidance in Abstract
Interpretation.
Post-Proceedings of the 28th International Symposium on
Logic-based Program Synthesis and Transformation
(LOPSTR'18),
LNCS,
Núm. 11408,
páginas 184--201,
Springer-Verlag,
Enero
2019.
- Marco Guarnieri, Musard Balliu, Daniel Schoepe, David Basin, Andrei Sabelfeld.
Information-flow Control for Database-backed Applications.
Proceedings of the 4th IEEE European Symposium on Security and Privacy,
EuroS&P 2019,
IEEE,
2019.
- Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn.
Type-level computations for Ruby libraries.
Proceedings of the 40th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI,
páginas 966--979,
ACM,
2019.
- Antonio Faonio, Daniele Venturi.
Non-malleable Secret Sharing in the Computational Setting: Adaptive
Tampering, Noisy-Leakage Resilience, and Improved Rate.
Advances in Cryptology - CRYPTO 2019 - 39th Annual International
Cryptology Conference,
Lecture Notes in Computer Science,
Vol. 11693,
páginas 448--479,
Springer,
2019.
- Sandro Coretti, Antonio Faonio, Daniele Venturi.
Rate-Optimizing Compilers for Continuously Non-malleable Codes.
Applied Cryptography and Network Security - 17th International Conference,
ACNS 2019,
Lecture Notes in Computer Science,
Vol. 11464,
páginas 3--23,
Springer,
2019.
- Antonio Faonio.
Efficient Fully-Leakage Resilient One-More Signature Schemes.
Topics in Cryptology - CT-RSA 2019 - The Cryptographers' Track at
the RSA Conference,
Lecture Notes in Computer Science,
Vol. 11405,
páginas 350--371,
Springer,
2019.
- Antonio Faonio, Daniele Venturi.
Non-malleable Secret Sharing in the Computational Setting: Adaptive
Tampering, Noisy-Leakage Resilience, and Improved Rate.
Advances in Cryptology - CRYPTO 2019 - 39th Annual International
Cryptology Conference,
Lecture Notes in Computer Science,
Vol. 11693,
páginas 448--479,
Springer,
2019.
- Sandro Coretti, Antonio Faonio, Daniele Venturi.
Rate-Optimizing Compilers for Continuously Non-malleable Codes.
Applied Cryptography and Network Security - 17th International Conference,
ACNS 2019,
Lecture Notes in Computer Science,
Vol. 11464,
páginas 3--23,
Springer,
2019.
- Antonio Faonio.
Efficient Fully-Leakage Resilient One-More Signature Schemes.
Topics in Cryptology - CT-RSA 2019 - The Cryptographers' Track at
the RSA Conference,
Lecture Notes in Computer Science,
Vol. 11405,
páginas 350--371,
Springer,
2019.
- Pierre Ganty, Francesco Ranzato, Pedro Valero.
Language Inclusion Algorithms as Complete Abstract Interpretations.
Static Analysis - 26th International Symposium, SAS 2019,
Lecture Notes in Computer Science,
Vol. 11822,
páginas 140--161,
Springer,
2019.
- Pierre Ganty, Elena Gutiérrez, Pedro Valero.
A Congruence-based Perspective on Automata Minimization Algorithms.
44th International Symposium on Mathematical Foundations of Computer
Science, MFCS 2019,
LIPIcs,
Vol. 138,
páginas 1--14,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2019.
- Pierre Ganty, Pedro Valero.
Regular Expression Search on Compressed Text.
2019 Data Compression Conference (DCC),
páginas 528--537,
IEEE,
2019.
- Norine Coenen, Bernd Finkbeiner, César Sánchez, Leander Tentrup.
Verifying Hyperliveness.
Proc. of the 31st Int'l Conf. on Computer Aided Verification (CAV'19),
Lecture Notes in Computer Science,
Vol. 11561,
páginas 121--139,
Springer,
2019.
- Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonakdarpour.
Gray-Box Monitoring of Hyperproperties.
Formal Methods - The Next 30 Years - Third World Congress, FM 2019,
Lecture Notes in Computer Science,
Vol. 11800,
páginas 406--424,
Springer,
2019.
- Álvaro García-Pérez, Maria A. Schett.
Deconstructing Stellar Consensus.
23rd International Conference on Principles of Distributed Systems
(OPODIS 2019),
LIPIcs,
Vol. 153,
páginas 1--16,
Schloss Daghstul - Leibniz-Zentrum fuer Informatik,
2019.
- Kuhring, Lucas, István, Zsolt.
Storing Parquet Tile by Tile: Application-Aware Storage with Deduplication.
2019 29th International Conference on Field Programmable Logic and Applications (FPL),
páginas 415--416,
2019.
- Eran, Haggai, Zeno, Lior, István, Zsolt, Silberstein, Mark.
Design Patterns for Code Reuse in HLS Packet Processing Pipelines.
2019 IEEE 27th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM),
páginas 208--217,
IEEE,
2019.
- Platon Kotzias, Abbas Razaghpanah, Johanna Amann, Kenneth G. Paterson, Narseo Vallina-Rodriguez, Juan Caballero.
Coming of Age: A Longitudinal Study of TLS Deployment.
Proceedings of ACM Internet Measurement Conference,
Octubre
2018.
- Juanru Li, Zhiqiang Lin, Juan Caballero, Yuanyuan Zhang, Dawu Gu.
K-Hunt: Pinpointing Insecure Cryptographic Keys from Execution Traces.
Proceedings of the 25th ACM Conference on Computer and Communication Security,
Octubre
2018.
- Dario Fiore, Elena Pagnin.
Matrioska: A Compiler for Multi-Key Homomorphic Signatures.
Security and Cryptography for Networks - 11th International Conference,
SCN 2018,
LNCS,
Vol. 11035,
páginas 43--62,
Springer,
Septiembre
2018.
- M. Klemen, N. Stulova, P. Lopez-Garcia, J. F. Morales, M. V. Hermenegildo.
Static Performance
Guarantees for Programs with Run-time
Checks.
20th Int'l. ACM SIGPLAN Symposium on Principles and
Practice of Declarative Programming (PPDP'18),
13 páginas,
ACM Press,
Septiembre
2018.
- Michel Abdalla, Dario Catalano, Dario Fiore, Romain Gay, Bogdan Ursu.
Multi-Input Functional Encryption for Inner Products: Function-Hiding Realizations and Constructions without Pairings.
Advances in Cryptology: Proc. of the 38th Annual Cryptology Conference (CRYPTO 2018),
LNCS,
Vol. 10991,
páginas 597--627,
Springer,
Agosto
2018.
- He, Zhenhao, Sidler, David, István, Zsolt, Alonso, Gustavo.
A Flexible K-Means Operator for Hybrid Databases.
Proceedings of the International Conference on Field-Programmable Logic and Applications,
FPL'18,
páginas 368--371,
Agosto
2018.
- István, Zsolt, Alonso, Gustavo, Singla, Ankit.
Providing Multi-tenant Services with FPGAs: Case Study on a Key-Value Store.
Proceedings of the International Conference on Field-Programmable Logic and Applications,
FPL'18,
páginas 119--124,
Agosto
2018.
- Blasi, Arianna, Goffi, Alberto, Kuznetsov,
Konstantin, Gorla, Alessandra, Ernst, Michael
D., Pezz`e, Mauro, Delgado Castellanos,
Sergio.
Translating Code Comments to Procedure
Specifications.
Proceedings of the 27th International Symposium on
Software Testing and Analysis,
páginas 242--253,
Julio
2018.
- Catalano, Dario, Fiore, Dario, Nizzardo Luca.
On the Security Notions for Homomorphic Signatures.
Applied Cryptography and Network Security, ACNS 2018,
LNCS,
Vol. 10892,
páginas 183--201,
Springer,
Junio
2018.
- Vishal Karande, Swarup Chandra, Zhiqiang Lin, Juan Caballero, Latifur Khan, Kevin Hamlen.
BCD: Decomposing Binary Code Into Components Using Graph-Based Clustering.
13th ACM ASIA Conference on Information, Computer and Communications Security,
Junio
2018.
- Konstantin Kuznetsov, Vitalii Avdiienko, Alessandra Gorla, Andreas Zeller.
Analyzing the User Interface of Android Apps.
5th IEEE/ACM International Conference on Mobile
Software Engineering and Systems, MOBILESoft,
páginas 84--87,
Mayo
2018.
- Arianna Blasi, Alessandra Gorla.
RepliComment: Identifying Clones in Code Comments.
2018 IEEE/ACM 26th International Conference on
Program Comprehension (ICPC),
páginas 320--323,
Mayo
2018.
- Paolo Calciati, Konstantin Kuznetsov, Alessandra Gorla.
What did Really Change with the new Release of the
App?.
Proceedings of the 15th International Conference on
Mining Software Repositories (MSR),
páginas 142--152,
IEEE Computer Society,
Mayo
2018.
- Chen Chen, Daniele E. Asoni, Adrian Perrig, David Barrera, George Danezis, Carmela Troncoso.
TARANET: Traffic-Analysis Resistant Anonymity at the NETwork layer.
2018 IEEE European Symposium on Security and Privacy, EuroS&P
2017, London, United Kindgdom, April 24-26, 2018,
páginas 137--152,
Abril
2018.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
Exploiting Term Hiding to Reduce Run-time
Checking Overhead.
20th International Symposium on Practical Aspects of
Declarative Languages (PADL 2018),
LNCS,
Núm. 10702,
páginas 99--115,
Springer-Verlag,
Enero
2018.
- Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato.
Program Analysis Is Harder Than Verification: A Computability Perspective.
Computer Aided Verification - 30th International Conference, CAV '18,
LNCS,
Vol. 10982,
páginas 75--95,
Springer,
2018.
- Roberto Bruni, Roberto Giacobazzi, Roberta Gori.
Code Obfuscation Against Abstract Model Checking Attacks.
Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI '18,
LNCS,
Vol. 10747,
páginas 94--115,
Springer,
2018.
- Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi.
Symbolic Proofs for Lattice-Based Cryptography.
Proceedings of the 2018 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2018, Toronto, ON, Canada, October
15-19, 2018,
páginas 538--555,
ACM,
2018.
- Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva.
Almost Sure Productivity.
45th International Colloquium on Automata, Languages, and Programming,
ICALP 2018, July 9-13, 2018, Prague, Czech Republic,
LIPIcs,
Vol. 107,
páginas 1--15,
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
2018.
- Gilles Barthe, Benjamin Grégoire, Vincent Laporte.
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic
"Constant-Time".
31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford,
United Kingdom, July 9-12, 2018,
páginas 328--343,
IEEE Computer Society,
2018.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela.
Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing
MPC Frameworks.
31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford,
United Kingdom, July 9-12, 2018,
páginas 132--146,
IEEE Computer Society,
2018.
- Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi.
Masking the GLP Lattice-Based Signature Scheme at Any Order.
Advances in Cryptology - EUROCRYPT 2018 - 37th Annual International
Conference on the Theory and Applications of Cryptographic Techniques,
Tel Aviv, Israel, April 29 - May 3, 2018 Proceedings, Part II,
Lecture Notes in Computer Science,
Vol. 10821,
páginas 354--384,
Springer,
2018.
- Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg.
Relational Reasoning for Markov Chains in a Probabilistic Guarded
Lambda Calculus.
Programming Languages and Systems - 27th European Symposium on Programming,
ESOP 2018, Held as Part of the European Joint Conferences on Theory
and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April
14-20, 2018, Proceedings,
Lecture Notes in Computer Science,
Vol. 10801,
páginas 214--241,
Springer,
2018.
- Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
An Assertion-Based Program Logic for Probabilistic Programs.
Programming Languages and Systems - 27th European Symposium on Programming,
ESOP 2018, Held as Part of the European Joint Conferences on Theory
and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April
14-20, 2018, Proceedings,
Lecture Notes in Computer Science,
Vol. 10801,
páginas 117--144,
Springer,
2018.
- Borja Balle, Gilles Barthe, Marco Gaboardi.
Privacy Amplification by Subsampling: Tight Analyses via Couplings
and Divergences.
Advances in Neural Information Processing Systems 31: Annual Conference
on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December
2018, Montréal, Canada.,
páginas 6280--6290,
2018.
- Antonio Faonio, Jesper Buus Nielsen, Mark Simkin, Daniele Venturi.
Continuously Non-malleable Codes with Split-State Refresh.
Applied Cryptography and Network Security - 16th International Conference,
ACNS 2018,
Lecture Notes in Computer Science,
Vol. 10892,
páginas 121--139,
Springer,
2018.
- Cedric Baumann, Andrei Marian Dan, Yuri Meshman, Torsten Hoefler, Martin T. Vechev.
Automatic Verification of RMA Programs via Abstraction Extrapolation.
Verification, Model Checking, and Abstract Interpretation - 19th International
Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018,
Proceedings,
páginas 47--70,
2018.
- Antonio Faonio, Jesper Buus Nielsen, Mark Simkin, Daniele Venturi.
Continuously Non-malleable Codes with Split-State Refresh.
Applied Cryptography and Network Security - 16th International Conference,
ACNS 2018,
Lecture Notes in Computer Science,
Vol. 10892,
páginas 121--139,
Springer,
2018.
- Álvaro García-Pérez, Alexey Gotsman.
Federated Byzantine quorum systems.
OPODIS'18: International Conference on Principles of Distributed Systems,
LIPICS,
Vol. 125,
páginas 1--16,
Dagstuhl,
2018.
- Gregory Chockler, Alexey Gotsman.
Multi-Shot Distributed Transaction Commit.
DISC'18: International Symposium on Distributed Computing,
LIPICS,
Vol. 121,
páginas 1--18,
Dagstuhl,
2018.
- Artem Khyzha, Hagit Attiya, Alexey Gotsman, Noam Rinetzky.
Safe privatization in transactional memory.
PPoPP'18: Symposium on Principles and Practice of Parallel Programming,
páginas 233--245,
ACM Press,
2018.
- Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey.
Paxos consensus, deconstructed and abstracted.
ESOP'18: European Symposium on Programming, Thessaloniki, Greece,
LNCS,
Vol. 10801,
páginas 912--939,
Springer,
2018.
- Mike Dodds, Mark Batty, Alexey Gotsman.
Compositional verification of compiler optimisations on relaxed memory.
ESOP'18: European Symposium on Programming, Thessaloniki, Greece,
LNCS,
Vol. 10801,
páginas 1027--1055,
Springer,
2018.
- Apostolos Pyrgelis, Carmela Troncoso, Emiliano De Cristofaro.
Knock Knock, Who's There? Membership Inference on Aggregate Location
Data.
25th Annual Network and Distributed System Security Symposium, NDSS
2018, San Diego, California,
The Internet Society,
2018.
- Masayuki Abe, Miguel Ambrona, Miyako Ohkubo, Mehdi Tibouchi.
Lower Bounds on Structure-Preserving Signatures for Bilateral Messages.
Security and Cryptography for Networks - 11th International Conference,
SCN 2018, Amalfi, Italy, September 5-7, 2018, Proceedings,
páginas 3--22,
2018.
- Pierre Ganty, Elena Gutiérrez.
The Parikh Property for Weighted Context-Free Grammars.
38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018),
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 122,
páginas 1--20,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
2018.
- Javier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy.
Verification of Immediate Observation Population Protocols.
29th International Conference on Concurrency Theory (CONCUR 2018),
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 118,
páginas 1--16,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
2018.
- Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic.
Sound up-to techniques and Complete abstract domains.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18,
páginas 175--184,
ACM Press,
2018.
- Miriam García Soto, Pavithra Prabhakar.
Averist: Algorithmic Verifier for Stability of Linear Hybrid Systems.
Proceedings of the 21st International Conference on Hybrid Systems:
Computation and Control (Part of CPS Week),
HSCC '18,
páginas 259--264,
ACM,
2018.
- U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
Inferring Energy Bounds via Static Program Analysis
and Evolutionary Modeling of Basic Blocks.
Logic-Based Program Synthesis and
Transformation - 27th International Symposium,
LOPSTR 2017, Namur, Belgium, October 10-12, 2017,
Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 10855,
Springer,
2018.
- Borzoo Bonakdarpour, César Sánchez, Gerardo Schneider.
Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification.
Proc. of the 8th Int'l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2018). Verification. Part II,
LNCS,
Vol. 11245,
páginas 8--27,
Springer,
2018.
- César Sánchez, Gerardo Schneider, Martin Leucker.
Reliable Smart Contracts: State-of-the-Art, Applications, Challenges and Future Directions.
Proc. of the 8th Int'l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2018). Verification. Part IV,
LNCS,
Vol. 11247,
páginas 275--279,
Springer,
2018.
- Christian Colombo, Yliés Falcone, Martin Leucker, Giles Reger, César Sánchez, Gerardo Schneider, Volker Stolz.
COST Action IC1402 Runtime Verification Beyond Monitoring.
Proc. of the 18th Int'l Conf. on Runtime Verification (RV'18),
LNCS,
Vol. 11237,
páginas 18--26,
Springer,
2018.
- César Sánchez.
Online and Offline Stream Runtime Verification of Synchronous Systems.
Proc. of the 18th Int'l Conf. on Runtime Verification (RV'18),
LNCS,
Vol. 11237,
páginas 138--163,
Springer,
2018.
- Felipe Gorostiaga, César Sánchez.
Striver: Stream Runtime Verification for Real-Time Event-Streams.
Proc. of the 18th Int'l Conf. on Runtime Verification (RV'18),
LNCS,
Vol. 11237,
páginas 282--298,
Springer,
2018.
- Pablo Chico de Guzman, Felipe Gorostiaga, César Sánchez.
Pipekit: A Deployment Tool with Advanced Scheduling and Inter-Service Communication for Multi-Tier Applications.
Proc. of the IEEE Int'l Conf. on Web Services (ICWS'18),
páginas 379--382,
IEEE CS Press,
2018.
- Pablo Chico de Guzman, Felipe Gorostiaga, César Sánchez.
i2kit: A Deployment Tool with the Simplicity of Containers and the Security of Virtual Machines.
Proc. of the 19th Int'l Conf. on Web Information Systems Engineering (WISE 2018), Part I,
LNCS,
Vol. 11233,
páginas 81--95,
Springer,
2018.
- Raúl Pardo, César Sánchez, Gerardo Schneider.
Timed Epistemic Knowledge Bases for Social Networks.
Proc. of 22nd Int'l Symposium on Formal Methods (FM'18),
LNCS,
Vol. 10951,
páginas 185--202,
Springer,
2018.
- Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, Alexander Schramm.
TeSSLa: Runtime Verification of Non-synchronized Real-Time Streams.
Proc. of the 33rd ACM/SIGAPP Symposium on Applied Computing (SAC'17),
páginas 1925--1933,
ACM Press,
2018.
Track on Software Verification and Testing Track (SVT).
- Pierre Ganty, Boris Köpf, Pedro Valero.
A Language-Theoretic View on Network Protocols.
Proc. of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017),
LNCS,
Vol. 10482,
páginas 363--379,
Springer,
Octubre
2017.
- Graeme Gange, Pierre Ganty, Peter J. Stuckey.
Fixing the State Budget: Approximation of Regular Languages with Small DFAs.
Proc. of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017),
LNCS,
Vol. 10482,
páginas 67--83,
Springer,
Octubre
2017.
- Manuel Barbosa, Dario Catalano, Dario Fiore.
Labeled Homomorphic Encryption: Scalable and Privacy-Preserving Processing of Outsourced Data.
Proc. of the 22nd European Symposium on Research in Computer Security (ESORICS 2017),
LNCS,
Vol. 10492,
páginas 146--166,
Springer,
Septiembre
2017.
- Pierre Ganty, Elena Gutiérrez.
Parikh Image of Pushdown Automata.
Proc. of the 21st International Symposium on Fundamentals of Computation Theory (FCT 2017),
LNCS,
Vol. 10472,
páginas 271--283,
Springer,
Septiembre
2017.
- Carmen Elisabetta Zaira Baltico, Dario Catalano, Dario Fiore, Romain Gay.
Practical Functional Encryption for Quadratic Functions
with Applications to Predicate Encryption.
Advances in Cryptology: Proc. of the 37th Annual Cryptology Conference (CRYPTO 2017),
LNCS,
Vol. 10401,
páginas 67--98,
Springer,
Agosto
2017.
- Vitalii Avdiienko, Konstantin Kuznetsov, Isabelle Rommelfanger, Andreas Rau, Alessandra
Gorla, Andreas Zeller.
Detecting behavior anomalies in graphical user
interfaces.
Proceedings of the 39th International Conference on
Software Engineering (ICSE 2017),
páginas 201--203,
IEEE Computer Society,
Mayo
2017.
- Paolo Calciati, Alessandra Gorla.
How Do Apps Evolve in Their Permission Requests?: A
Preliminary Study.
Proceedings of the 14th International Conference on
Mining Software Repositories (MSR),
páginas 37--41,
IEEE Computer Society,
Mayo
2017.
- Chaz Lever, Platon Kotzias, Davide Balzarotti, Juan Caballero, Manos Antonakakis.
A Lustrum of Malware Network Communication: Evolution and Insights.
Proceedings of the 38th IEEE Symposium on Security and Privacy,
Mayo
2017.
- Oliver Kennedy, D. Richard Hipp, Stratos Idreos, Amélie Marian, Arnab Nandi, Carmela Troncoso, Eugene Wu.
Small Data.
Proc. of the 33rd IEEE International Conference on Data Engineering (ICDE 2017),
páginas 1475--1476,
IEEE Computer Society,
Abril
2017.
- Alessio Gambi, Alessandra Gorla, Andreas
Zeller.
O!Snap: Cost-Efficient Testing in the Cloud.
Proceedings of the 10th IEEE International
Conference on Software Testing, Verification and
Validation (ICST),
páginas 454--459,
IEEE Computer Society,
Marzo
2017.
- Simon Oya, Fernando Pérez-González, Carmela Troncoso.
Filter design for delay-based anonymous communications.
Proc. of the 42nd IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP 2017),
páginas 2107--2111,
IEEE,
Marzo
2017.
- Vitalii Avdiienko, Konstantin Kuznetsov, Alessandra Gorla, Andreas Zeller, Steven Arzt, Siegfried Rasthofer, Eric Bodden.
App Mining.
Software Engineering 2017,
LNI,
Vol. P-267,
páginas 113--114,
GI,
Febrero
2017.
- Andreas Metzger, Philipp Leitner, Dragan Ivanovic, Eric Schmieders, Rod Franklin, Manuel Carro, Schahram Dustdar, Klaus Pohl.
Vergleich und Kombination von Techniken des Predictive Business Process Monitoring.
Software Engineering 2017, Fachtagung des GI-Fachbereichs Softwaretechnik,
Lecture Notes in Informatics (LNI),
Vol. P-267,
páginas 79--80,
GI,
Febrero
2017.
- Srdjan Matic, Carmela Troncoso, Juan Caballero.
Dissecting Tor Bridges: a Security Evaluation of their Private and
Public Infrastructures.
Proceedings of the Network and Distributed System Security Symposium,
Febrero
2017.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub.
Jasmin: High-Assurance and High-Speed Cryptography.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2017, Dallas, TX, USA, October 30-November 3, 2017,
páginas 1807--1823,
ACM,
2017.
- Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee.
Attribute-Based Encryption in the Generic Group Model:
Automated Proofs and New Constructions.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2017, Dallas, TX, USA, October 30-November 3, 2017,
páginas 647--664,
ACM,
2017.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira.
A Fast and Verified Software Stack for Secure Function Evaluation.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2017, Dallas, TX, USA, October 30-November 3, 2017,
páginas 1989--2006,
ACM,
2017.
- Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu.
Verified Translation Validation of Static Analyses.
30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa
Barbara, CA, USA, August 21-25, 2017,
páginas 405--419,
IEEE Computer Society,
2017.
- Miguel Ambrona, Gilles Barthe, Benedikt Schmidt.
Generic Transformations of Predicate Encodings: Constructions and
Applications.
Advances in Cryptology - CRYPTO 2017 - 37th Annual International
Cryptology Conference, Santa Barbara, CA, USA, August 20-24, 2017,
Proceedings, Part I,
Lecture Notes in Computer Science,
Vol. 10401,
páginas 36--66,
Springer,
2017.
- Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
Proving uniformity and independence by self-composition and coupling.
LPAR-21, 21st International Conference on Logic for Programming, Artificial
Intelligence and Reasoning, Maun, Botswana, 7-12th May 2017,
EPiC Series,
Vol. 46,
páginas 385--403,
EasyChair,
2017.
- Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub.
*-Liftings for Differential Privacy.
44th International Colloquium on Automata, Languages, and Programming,
ICALP 2017, July 10-14, 2017, Warsaw, Poland,
LIPIcs,
Vol. 80,
páginas 1--12,
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
2017.
- Martín Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, Vijay Ganesh.
Reasoning about Probabilistic Defense Mechanisms against Remote Attacks.
2017 IEEE European Symposium on Security and Privacy, EuroS&P
2017, Paris, France, April 26-28, 2017,
páginas 499--513,
IEEE,
2017.
- Gilles Barthe, Francois Dupressoir, Sebastian Faust, Benjamin Grégoire, Francois-Xavier Standaert, Pierre-Yves Strub.
Parallel Implementations of Masking Schemes and the
Bounded Moment Leakage Model.
Advances in Cryptology - EUROCRYPT 2017 - 36th Annual
International Conference on the Theory and
Applications of Cryptographic Techniques, Paris,
France, April 30 - May 4, 2017, Proceedings, Part
I,
Lecture Notes in Computer Science,
Vol. 10210,
páginas 535--566,
2017.
- Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns.
Is Your Software on Dope? - Formal Analysis of
Surreptitiously "enhanced" Programs.
Programming Languages and Systems - 26th European
Symposium on Programming, ESOP 2017, Held as Part
of the European Joint Conferences on Theory and
Practice of Software, ETAPS 2017, Uppsala, Sweden,
April 22-29, 2017, Proceedings,
Lecture Notes in Computer Science,
Vol. 10201,
páginas 83--110,
2017.
- Ezgi Cicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann.
Relational cost analysis.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of
Programming Languages, POPL 2017, Paris, France, January 18-20, 2017,
páginas 316--329,
ACM,
2017.
- Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
Coupling proofs are probabilistic product programs.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of
Programming Languages, POPL 2017, Paris, France, January 18-20, 2017,
páginas 161--174,
ACM,
2017.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira.
A Fast and Verified Software Stack for Secure Function Evaluation.
Proceedings of the 24th ACM Conference on Computer and Communications Security, (CCS),
2017.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub.
Jasmin: High-Assurance and High-Speed Cryptography.
Proceedings of the 24th ACM Conference on Computer and Communications Security, (CCS),
2017.
- Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu.
Verified Translation Validation of Static Analyses.
IEEE 30th Computer Security Foundations Symposium, (CSF),
2017.
- Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, Yolanda Ortega-Mallén.
Rule Formats for Nominal Process Calculi.
28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany,
LIPIcs,
Vol. 85,
páginas 1--16,
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
2017.
- Alexey Gotsman, Sebastian Burckhardt.
Consistency models with global operation sequencing and their composition.
DISC'17: International Symposium on Distributed Computing,
LIPICS,
Vol. 91,
páginas 1--16,
Dagstuhl,
2017.
- Andrea Cerone, Alexey Gotsman, Hongseok Yang.
Algebraic laws for weak consistency.
CONCUR'17: International Conference on Concurrency Theory,
LIPICS,
Vol. 85,
páginas 1--18,
Dagstuhl,
2017.
- Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson.
Proving linearizability using partial orders.
ESOP'17: European Symposium on Programming, Uppsala, Sweden,
LNCS,
Vol. 10201,
páginas 639--667,
Springer,
2017.
- Simon Oya, Carmela Troncoso, Fernando Pérez-González.
Back to the Drawing Board: Revisiting the Design of Optimal Location Privacy-preserving Mechanisms.
Proc. of the ACM Conference on Computer and Communications Security (CCS 2017),
páginas 1959--1972,
ACM,
2017.
- Yevgeniy Dodis, Dario Fiore.
Unilaterally-Authenticated Key Exchange.
Financial Cryptography and Data Security 2017, Proceedings,
LNCS,
Springer,
2017.
- Miguel Ambrona, Gilles Barthe, Benedikt Schmidt.
Generic Transformations of Predicate Encodings: Constructions and
Applications.
Advances in Cryptology - CRYPTO 2017 - 37th Annual International
Cryptology Conference, Santa Barbara, CA, USA, August 20-24, 2017,
Proceedings, Part I,
páginas 36--66,
2017.
- Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee.
Attribute-Based Encryption in the Generic Group Model: Automated Proofs
and New Constructions.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and
Communications Security, CCS 2017, Dallas, TX, USA, October 30 -
November 03, 2017,
páginas 647--664,
2017.
- Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
Concurrent Data Structures Linked in Time.
European Conference on Object-Oriented Programming (ECOOP),
páginas 1--30,
2017.
- Pepe Vila, Boris Köpf.
Loophole: Timing Attacks on Shared Event Loops in Chrome.
26th USENIX Security Symposium,
USENIX Association,
2017.
- Goran Doychev, Boris Köpf.
Rigorous Analysis of Software Countermeasures against Cache Attacks.
38th ACM SIGPLAN Conference on Programming Language Design and Implementations (PLDI),
ACM,
2017.
- Heiko Mantel, Alexandra Weber, Boris Köpf.
A Systematic Study of Cache Side Channels across AES Implementations.
Proc. 9th International Symposium on Engineering Secure Software and Systems (ESSoS '17),
Springer,
2017.
- Pablo Cañones, Boris Köpf, Jan Reineke.
Security Analysis of Cache Replacement Policies.
Proc. 6th Conference on Principles of Security and Trust (POST '17),
Springer,
2017.
- Pavithra Prabhakar, Miriam García Soto.
Formal Synthesis of Stabilizing Controllers for Switched Systems.
Proceedings of the 20th International Conference on Hybrid Systems:
Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18-20,
páginas 111--120,
2017.
- Véronique Cortier, Constantin Catalin Dragan, Francois Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi.
Machine-Checked Proofs of Privacy for Electronic Voting Protocols.
2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose,
CA, USA, May 22-26, 2017,
páginas 993--1008,
2017.
- Damien Imbs, Achour Mostéfaoui, Matthieu Perrin, Michel Raynal.
Which Broadcast Abstraction Captures k-Set Agreement?.
31st International Symposium on Distributed Computing, DISC 2017,
LIPIcs,
Vol. 91,
páginas 1--16,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2017.
- Matteo Campanelli, Rosario Gennaro, Steven Goldfeder, Luca Nizzardo.
Zero-knowledge contingent payments revisited: Attacks and payments for services.
ACM CCS 2017 -- 24rd ACM Conference on Computer and Communication Security,
páginas 229--243,
2017.
- Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub.
Computer-aided verification in mechanism design.
Proceedings of the 12th Conference on Web and Internet Economics (WINE 2016),
Lecture Notes in Computer Science,
Vol. 10123,
páginas 279--293,
Springer,
Diciembre
2016.
- Antonio Nappa, Rana Faisal Munir, Irfan Khan Tanoli, Christian Kreibich, Juan Caballero.
RevProbe: Detecting Silent Reverse Proxies in Malicious Server Infrastructures.
Proceedings of the 2016 Annual Computer Security Applications Conference,
Diciembre
2016.
- Joaquín Arias, Manuel Carro.
Description and Evaluation of a Generic Design to Integrate CLP and Tabled Execution.
18th Int'l. ACM Symposium on Principles and
Practice of Declarative Programming,
páginas 10--23,
ACM Press,
Septiembre
2016.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
Reducing the Overhead of Assertion Run-time
Checks via Static Analysis.
18th Int'l. ACM SIGPLAN Symposium on Principles and
Practice of Declarative Programming (PPDP'16),
páginas 90--103,
ACM Press,
Septiembre
2016.
- Marcos Sebastián, Richard Rivera, Platon Kotzias, Juan Caballero.
AVClass: A Tool for Massive Malware Labeling.
Proceedings of the 19th International Symposium on Research in Attacks, Intrusions and Defenses,
Septiembre
2016.
- Alejandro Calleja, Juan Tapiador, Juan Caballero.
A Look into 30 Years of Malware Development from a Software Metrics Perspective.
Proceedings of the 19th International Symposium on Research in Attacks, Intrusions and Defenses,
Septiembre
2016.
- Platon Kotzias, Leyla Bilge, Juan Caballero.
Measuring PUP Prevalence and PUP Distribution through Pay-Per-Install Services.
Proceedings of the 25th USENIX Security Symposium,
Agosto
2016.
- Goffi, Alberto, Gorla, Alessandra, Ernst, Michael D., Pezz`e, Mauro.
Automatic Generation of Oracles for Exceptional Behaviors.
Proceedings of the 25th International Symposium on Software Testing and Analysis,
ISSTA 2016,
páginas 213--224,
ACM,
Julio
2016.
- R. Haemmerlé, P. Lopez-Garcia, U. Liqat, M. Klemen, J. P. Gallagher, M. V. Hermenegildo.
A Transformational Approach to Parametric
Accumulated-cost Static Profiling.
13th International Symposium on Functional and Logic Programming (FLOPS 2016),
LNCS,
Vol. 9613,
páginas 163--180,
Springer,
Marzo
2016.
- Mila Dalla Preda, Roberto Giacobazzi, Isabella Mastroeni.
Completeness in Approximate Transduction.
Proceedings of the 23rd International Symposium on Static Analysis (SAS),
Lecture Notes in Computer Science,
Vol. 9837,
páginas 126--146,
Springer,
2016.
- Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
Proving Differential Privacy via Probabilistic Couplings.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2016, New York, NY, USA, July 5-8, 2016,
páginas 749--758,
ACM,
2016.
- Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
Advanced Probabilistic Couplings for Differential Privacy.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and
Communications Security, Vienna, Austria, October 24-28, 2016,
páginas 55--67,
ACM,
2016.
- Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub.
Differentially Private Bayesian Programming.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and
Communications Security, Vienna, Austria, October 24-28, 2016,
páginas 68--79,
ACM,
2016.
- Gilles Barthe, Sonia Belaïd, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini.
Strong Non-Interference and Type-Directed Higher-Order Masking.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and
Communications Security, Vienna, Austria, October 24-28, 2016,
páginas 116--129,
ACM,
2016.
- Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns.
Facets of Software Doping.
Leveraging Applications of Formal Methods, Verification and Validation:
Discussion, Dissemination, Applications - 7th International Symposium,
ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings,
Part II,
Lecture Notes in Computer Science,
Vol. 9953,
páginas 601--608,
Springer,
2016.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Michael Emmi.
Verifying Constant-Time Implementations.
25th USENIX Security Symposium, USENIX Security 16, Austin, TX,
USA, August 10-12, 2016,
páginas 53--70,
USENIX Association,
2016.
- Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub.
A Program Logic for Union Bounds.
43rd International Colloquium on Automata, Languages, and Programming,
ICALP 2016, July 11-15, 2016, Rome, Italy,
LIPIcs,
Vol. 55,
páginas 1--15,
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
2016.
- Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu.
Synthesizing Probabilistic Invariants via Doob's Decomposition.
Computer Aided Verification - 28th International Conference, CAV
2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I,
Lecture Notes in Computer Science,
Vol. 9779,
páginas 43--61,
Springer,
2016.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir.
Verifiable Side-Channel Security of Cryptographic Implementations:
Constant-Time MEE-CBC.
Fast Software Encryption - 23rd International Conference, FSE 2016,
Bochum, Germany, March 20-23, 2016, Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 9783,
páginas 163--184,
Springer,
2016.
- Sandrine Blazy, Vincent Laporte, David Pichardie.
An abstract memory functor for verified C static analyzers.
Proceedings of the 21st ACM SIGPLAN International Conference on
Functional Programming, ICFP 2016, Nara, Japan, September 18-22,
2016,
páginas 325--337,
2016.
- Cédric Fournet, Chantal Keller, Vincent Laporte.
A Certified Compiler for Verifiable Computing.
IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon,
Portugal, June 27 - July 1, 2016,
páginas 268--280,
2016.
- Torben Amtoft, Anindya Banerjee.
A Theory of Slicing for Probabilistic Control Flow Graphs.
Foundations of Software Science and Computation Structures - 19th
International Conference, FOSSACS 2016, Held as Part of the European
Joint Conferences on Theory and Practice of Software, ETAPS 2016,
Eindhoven, The Netherlands, April 2-8, 2016, Proceedings,
páginas 180--196,
2016.
- Anindya Banerjee, David A. Schmidt, Mohammad Nikouei.
Relational Logic with Framing and Hypotheses.
Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS),
2016.
- Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, Marek Zawirski.
Specification and Complexity of Collaborative Text Editing.
PODC'16: Symposium on Principles of Distributed Computing,
páginas 259--268,
ACM Press,
2016.
- Andrea Cerone, Alexey Gotsman.
Analysing Snapshot Isolation.
PODC'16: Symposium on Principles of Distributed Computing,
páginas 55--64,
ACM Press,
2016.
- Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson.
A Generic Logic for Proving Linearizability.
FM'16: International Symposium on Formal Methods,
LNCS,
Vol. 9995,
páginas 426--443,
Springer,
2016.
- Giovanni Bernardi, Alexey Gotsman.
Robustness against Consistency Models with Atomic Visibility.
CONCUR'16: International Conference on Concurrency Theory,
LIPICS,
Vol. 59,
páginas 1--15,
Dagstuhl,
2016.
- Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro.
'Cause I'm strong enough: reasoning about consistency choices in distributed systems.
POPL'16: Symposium on Principles of Programming Languages, St. Petersburg, FL, USA,
páginas 371--384,
ACM Press,
2016.
- Dario Fiore, Cédric Fournet, Esha Gosh, Markulf Kohlweiss, Olga Ohrimenko, Bryan Parno.
Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data.
ACM CCS 2016 -- 23rd ACM Conference on Computer and Communication Security,
páginas 1304--1316,
2016.
- Dario Fiore, Aikaterini Mitrokotsa, Luca Nizzardo, Elena Pagnin.
Multi-Key Homomorphic Authenticators.
ASIACRYPT 2016: 22nd Annual International Conference on the Theory and Applications of Cryptology and Information Security,
LNCS,
Springer,
2016.
- Dario Fiore, Anca Nitulescu.
On the (In)security of SNARKs in the Presence of Oracles.
TCC 2016-B: 14th Theory of Cryptography Conference,
LNCS,
Springer,
2016.
- Johannes Krupp, Dominique Schroeder, Mark Simkin, Dario Fiore, Giuseppe Ateniese, Stefan Nuernberger.
Nearly Optimal Verifiable Data Streaming.
PKC 2016: 19th International Workshop on Theory and Practice in Public Key Cryptography,
LNCS,
Springer,
2016.
- Miguel Ambrona, Gilles Barthe, Benedikt Schmidt.
Automated Unbounded Analysis of Cryptographic Constructions in the
Generic Group Model.
Advances in Cryptology - EUROCRYPT 2016 - 35th Annual International
Conference on the Theory and Applications of Cryptographic Techniques,
Lecture Notes in Computer Science,
Vol. 9666,
páginas 822--851,
Springer,
2016.
- Michael Emmi, Constantin Enea.
Symbolic Abstract Data Type Inference.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2016,
St. Petersburg, Florida, United States,
January 20-22, 2016,
páginas 513--525,
ACM,
2016.
- Sergey, Ilya, Nanevski, Aleksandar, Banerjee, Anindya, Delbianco, Germán Andrés.
Hoare-style Specifications As Correctness Conditions for Non-linearizable Concurrent Objects.
International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA),
páginas 92--110,
2016.
- Javier Esparza, Pierre Ganty, Jér^ome Leroux, Rupak Majumdar.
Model Checking Population Protocols.
36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016),
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 65,
páginas 1--14,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
2016.
- Pierre Ganty, Damir Valput.
Bounded-oscillation Pushdown Automata.
Proceedings of the Seventh International Symposium on Games, Automata,
Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16
September 2016,
EPTCS,
Vol. 226,
páginas 178--197,
2016.
- Pavithra Prabhakar, Miriam García Soto, Ratan Lal.
Verification Techniques for Hybrid Systems.
Leveraging Applications of Formal Methods, Verification and Validation:
Discussion, Dissemination, Applications - 7th International Symposium,
ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings,
Part II,
páginas 833--842,
2016.
- Pavithra Prabhakar, Miriam García Soto.
An Algorithmic Approach to Global Asymptotic Stability Verification of Hybrid Systems.
Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016,
páginas 1--10,
ACM,
2016.
- Pavithra Prabhakar, Miriam García Soto.
Counterexample Guided Abstraction Refinement for Stability Analysis.
Computer Aided Verification - 28th International Conference, CAV 2016,
Lecture Notes in Computer Science,
Vol. 9779,
páginas 495--512,
Springer,
2016.
- Pavithra Prabhakar, Miriam García Soto.
Hybridization for Stability Analysis of Switched Linear Systems.
Proc. of the 19th International Conference on Hybrid Systems:
Computation and Control, HSCC 2016,
páginas 71--80,
ACM,
2016.
- Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub.
Formal proofs of transcendence for e and pi as an application of multivariate
and symmetric polynomials.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016,
páginas 76--87,
ACM,
2016.
- Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin.
Dependent types and multi-monadic effects in F.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2016, St. Petersburg,
FL, USA, January 20 - 22, 2016,
páginas 256--270,
ACM,
2016.
- Raúl Pardo, Ivana Kellyerova, César Sánchez, Gerardo Schneider.
Specification of Evolving Privacy Policies for Online Social Networks.
Proc. of the 23rd Int'l Symp. on Temporal Representation and Reasoning (TIME'16),
páginas 70--79,
IEEE Computer Society Press,
2016.
- Bishoksan Kafle, John P. Gallagher, José F. Morales.
Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation
and Finite Tree Automata.
Computer Aided Verification - 28th International Conference, CAV
2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I,
Lecture Notes in Computer Science,
Vol. 9779,
páginas 261--268,
Springer,
2016.
- Xueliang Li, John P. Gallagher.
Fine-Grained Energy Modeling for the Source Code of a Mobile Application.
Proceedings of the 13th International Conference on Mobile and Ubiquitous
Systems: Computing, Networking and Services, MobiQuitous 2016, Hiroshima,
Japan, November 28 - December 1, 2016,
páginas 180--189,
ACM,
2016.
- Xueliang Li, John P. Gallagher.
A Source-level Energy Optimization Framework for Mobile Applications.
16th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2016),
2016.
- Christian Meurisch, Usman Naeem, Muhammad Awais Azam, Frederik Janssen, Benedikt Schmidt, Max Mühlhäuser.
Smarticipation: intelligent personal guidance of human behavior utilizing
anticipatory models.
Proceedings of the 2016 ACM International Joint Conference on Pervasive
and Ubiquitous Computing, UbiComp Adjunct 2016, Heidelberg, Germany,
September 12-16, 2016,
páginas 1227--1230,
ACM,
2016.
- Alexander Seeliger, Timo Nolle, Benedikt Schmidt, Max Mühlhäuser.
Process Compliance Checking using Taint Flow Analysis.
Proceedings of the International Conference on Information Systems
- Digital Innovation at the Crossroads, ICIS 2016, Dublin, Ireland,
December 11-14, 2016,
Association for Information Systems,
2016.
- Alexander Seeliger, Benedikt Schmidt, Immanuel Schweizer, Max Mühlhäuser.
What Belongs Together Comes Together: Activity-centric Document Clustering
for Information Work.
Proceedings of the 21st International Conference on Intelligent User
Interfaces, IUI 2016, Sonoma, CA, USA, March 07 - 10, 2016,
páginas 60--70,
ACM,
2016.
- Marc Fischlin, Felix Günther, Benedikt Schmidt, Bogdan Warinschi.
Key Confirmation in Key Exchange: A Formal Treatment and Implications
for TLS 1.3.
IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA,
USA, May 22-26, 2016,
páginas 452--469,
IEEE Computer Society,
2016.
- Shauvik Roy Choudhary, Alessandra Gorla, Alessandro Orso.
Automated Test Input Generation for Android: Are We There Yet?.
Proceedings of the 30th IEEE/ACM International Conference on
Automated Software Engineering,
ASE 2015,
páginas 429--440,
Noviembre
2015.
- Irfan Ul Haq, Juan Caballero, Michael D. Ernst.
Ayudante: Identifying Undesired Variable Interactions.
Proceedings of the 13th International Workshop on Dynamic Analysis,
Octubre
2015.
- Platon Kotzias, Srdjan Matic, Richard Rivera, Juan Caballero.
Certified PUP: Abuse in Authenticode Code Signing.
Proceedings of the 22nd ACM Conference on Computer and Communication Security,
Octubre
2015.
- Srdjan Matic, Platon Kotzias, Juan Caballero.
CARONTE: Detecting Location Leaks for Deanonymizing Tor Hidden Services.
Proceedings of the 22nd ACM Conference on Computer and Communication Security,
Octubre
2015.
- Salvador Tamarit, Guillermo Vigueras, Manuel Carro, Julio Mariño.
A Haskell Implementation of a Rule-Based
Program Transformation for C Programs.
International Symposium on Practical Aspects of Declarative Languages,
LNCS,
Núm. 9131,
páginas 105--114,
Springer-Verlag,
Junio
2015.
- Vitalii Avdiienko, Konstantin Kuznetsov, Alessandra
Gorla, Andreas Zeller, Steven Arzt, Siegfried Rasthofer, Eric Bodden.
Mining Apps for Abnormal Usage of Sensitive Data.
Proceedings of the 37th International Conference on
Software Engineering,
ICSE 2015,
páginas 426--436,
ACM,
Mayo
2015.
- Antonio Nappa, Richard Johnson, Leyla Bilge, Juan Caballero, Tudor Dimitras.
The Attack of the Clones: A Study of the Impact of Shared Code on Vulnerability Patching.
Proceedings of the 36th IEEE Symposium on Security and Privacy,
Mayo
2015.
- Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt.
Automated Proofs of Pairing-based Cryptography.
Proceedings of the 22nd ACM SIGSAC Conference on Computer and
Communications Security,
páginas 1156--1168,
ACM,
2015.
- Gilles Barthe, Sonia Belaïd, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub.
Verified Proofs of Higher-Order Masking.
Advances in Cryptology - EUROCRYPT 2015 - 34th Annual International
Conference on the Theory and Applications of Cryptographic Techniques,
Sofia, Bulgaria, April 26-30, 2015, Proceedings, Part I,
Lecture Notes in Computer Science,
Vol. 9056,
páginas 457--485,
Springer,
2015.
- Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt.
Mind the Gap: Modular Machine-checked Proofs of One-round Key Exchange
Protocols.
Advances in Cryptology - EUROCRYPT 2015 - 34th Annual International
Conference on the Theory and Applications of Cryptographic Techniques,
Lecture Notes in Computer Science,
Vol. 9057,
páginas 689--718,
Springer,
2015.
- Patrick Baillot, Gilles Barthe, Ugo Dal Lago.
Implicit Computational Complexity of Subrecursive Definitions and
Applications to Cryptographic Proofs.
Logic for Programming, Artificial Intelligence, and Reasoning - 20th
International Conference, LPAR-20 2015, Suva, Fiji, November 24-28,
2015, Proceedings,
Lecture Notes in Computer Science,
Vol. 9450,
páginas 203--218,
Springer,
2015.
- Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub.
Relational Reasoning via Probabilistic Coupling.
Logic for Programming, Artificial Intelligence, and Reasoning - 20th
International Conference, LPAR-20 2015, Suva, Fiji, November 24-28,
2015, Proceedings,
Lecture Notes in Computer Science,
Vol. 9450,
páginas 387--401,
Springer,
2015.
- Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub.
Higher-Order Approximate Relational Refinement Types for Mechanism
Design and Differential Privacy.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2015, Mumbai, India, January
15-17, 2015,
páginas 55--68,
ACM,
2015.
- Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi.
Strongly-Optimal Structure Preserving Signatures from Type II Pairings:
Synthesis and Lower Bounds.
PKC 2015: 18th International Workshop on Theory and Practice in
Public Key Cryptography,
Lecture Notes in Computer Science,
Vol. 9020,
páginas 355--376,
Springer,
2015.
- Jerusalem, Antoine, Vigueras, Guillermo, Sket, Federico, Samaniego, Cristobal, Wu, Ling, Noels, Ludovic, Tjahjanto, Denny, Casoni, Eva, Houzeaux, Guillaume, Makradi, Ahmed, Molina-Aldareguia, Jon M., Vazquez, Mariano.
An XFEM/CZM implementation for massively parallel simulations of composites fracture.
European Solid Mechanics Conference, ESMC 2015,
2015.
- Andrea Mattavelli, Alberto Goffi, Alessandra Gorla.
Synthesis of Equivalent Method Calls in Guava.
Proceedings of the 7th International Symposium on
Search-Based Software Engineering,
SSBSE 2015,
páginas 248--254,
Springer,
2015.
- Pavithra Prabhakar, Nima Roohi, Mahesh Viswanathan.
Deciding Concurrent Planar Monotonic Linear Hybrid Systems.
Formal Modeling and Analysis of Timed Systems - 13th International
Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings,
páginas 256--269,
2015.
- Pavithra Prabhakar, Miriam Garcia Soto.
Foundations of Quantitative Predicate Abstraction for Stability Analysis
of Hybrid Systems.
Verification, Model Checking, and Abstract Interpretation - 16th International
Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings,
Lecture Notes in Computer Science,
Vol. 8931,
páginas 318--335,
Springer,
2015.
- Andrea Cerone, Alexey Gotsman, Hongseok Yang.
Transaction chopping for parallel snapshot isolation.
DISC'15: International Symposium on Distributed Computing, Tokyo, Japan,
LNCS,
Vol. 9363,
páginas 388--404,
Springer,
2015.
- Andrea Cerone, Giovanni Bernardi, Alexey Gotsman.
A framework for transactional consistency models with atomic visibility.
CONCUR'15: International Conference on Concurrency Theory, Madrid, Spain,
LIPICS,
Vol. 42,
páginas 58--71,
Dagstuhl,
2015.
- Alexey Gotsman, Hongseok Yang.
Composite replicated data types.
ESOP'15: European Symposium on Programming, London, UK,
LNCS,
Vol. 9032,
páginas 585--609,
Springer,
2015.
- Dario Catalano, Dario Fiore.
Using Linearly-Homomorphic Encryption to Evaluate Degree-2 Functions on Encrypted Data.
ACM CCS 2015 -- 22nd ACM Conference on Computer and Communication Security,
páginas 1518--1529,
2015.
- Dario Catalano, Dario Fiore, Luca Nizzardo.
Programmable Hash Functions go Private: Constructions and Application to (Homomorphic) Signatures with Shorter Public Keys.
Advances in Cryptology -- CRYPTO 2015 -- 35th Annual Cryptology Conference,
Santa Barbara, CA, USA, August 16-20, 2015, Proceedings, Part II,
LNCS,
Vol. 9216,
páginas 254--274,
Springer,
2015.
- Michael Backes, Manuel Barbosa, Dario Fiore, Raphael M. Reischuk.
ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data.
36th IEEE Symposium on Security and Privacy (Oakland) 2015,
IEEE Computer Society,
2015.
- Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
On Reducing Linearizability to State Reachability.
Automata, Languages, and Programming - 42nd International Colloquium,
ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II,
páginas 95--107,
2015.
- Michael Emmi, Constantin Enea, Jad Hamza.
Monitoring Refinement via Symbolic Reasoning.
Proceedings of the 36th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI 2015, Portland, OR, USA, June
15-17, 2015,
páginas 260--269,
ACM,
2015.
- Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric.
SMACK+Corral: A Modular Verifier - (Competition Contribution).
Tools and Algorithms for the Construction and Analysis of Systems
- 21st International Conference, TACAS 2015, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS
2015, London, UK, April 11-18, 2015. Proceedings,
páginas 451--454,
2015.
- Michael Emmi, Pierre Ganty, Rupak Majumdar, Fernando Rosa-Velardo.
Analysis of Asynchronous Programs with Event-Based Synchronization.
Programming Languages and Systems - 24th European Symposium on Programming,
ESOP 2015, Held as Part of the European Joint Conferences on Theory
and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015.
Proceedings,
páginas 535--559,
2015.
- Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
Tractable Refinement Checking for Concurrent Objects.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2015, Mumbai, India, January
15-17, 2015,
páginas 651--662,
ACM,
2015.
- Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
Mechanized Verification of Fine-grained Concurrent Programs.
Conference on Programming Language Design and Implementation (PLDI),
páginas 77--87,
2015.
- Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee.
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.
European Symposium on Programming (ESOP),
páginas 333--358,
2015.
- Ganty, Pierre, Genaim, Samir, Lal, Ratan, Prabhakar, Pavithra.
From Non-Zenoness Verification to Termination.
MEMOCODE '15: 13th ACM-IEEE Int. Conf. on Formal Methods and Models for System Design,
IEEE Computer Society,
2015.
- Esparza, Javier, Ganty, Pierre, Leroux, Jér^ome, Majumdar, Rupak.
Verification of Population Protocols.
CONCUR '15: Proc. 26th Int. Conf. on Concurrency Theory,
2015.
- Durand-Gasselin, Antoine, Esparza, Javier, Ganty, Pierre, Majumdar, Rupak.
Model Checking Parameterized Asynchronous Shared-Memory Systems.
CAV '15: Proc. 25th Int. Conf. on Computer Aided Verification,
LNCS,
Vol. 9206,
Springer,
2015.
- Ganty, Pierre, Iosif, Radu.
Interprocedural Reachability for Flat Integer Programs.
FCT '15: Proc. 20th Int. Symp. on Fundamentals of Computation Theory,
LNCS,
Springer,
2015.
- Boris Köpf.
Reasoning about the Trade-off between Security and Performance.
Proc. 12th International Conference on Quantitative Evaluation of Systems (QEST '15),
Springer,
2015.
- Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko.
Symbolic Polytopes for Quantitative Interpolation and Verification.
Proc. 27th International Conference on Computer Aided Verification (CAV '15),
Springer,
2015.
- Goran Doychev, Boris Köpf.
Rational Protection Against Timing Attacks.
Proc. 28th IEEE Computer Security Foundations Symposium (CSF'15),
IEEE,
2015.
- Julio Mariño, Raúl N.N. Alborodo.
A Model-driven Methodology for Generating and
Verifying CSP-based Java Code.
Communicating Process Architectures 2015, Proceedings of the 37th WoTUG Conference on Concurrent and Parallel Systems,
páginas 85--108,
Open Channel Publishing Ltd.,
2015.
- Ratan Lal, Pavithra Prabhakar.
Bounded error flowpipe computation of parameterized linear systems.
Proceedings of the International Conference on Embedded Software (EMSOFT),
ACM, IEEE,
2015.
- Z. Banković, U. Liqat, P. Lopez-Garcia.
A Practical Approach for Energy Efficient Scheduling in
Multicore Environments by combining Evolutionary and YDS Algorithms
with Faster Energy Estimation.
The 11th International Conference on Artificial Intelligence Applications and Innovations (AIAI'15),
IFIP Advances in Information and Communication Technology,
Vol. 458,
páginas 478--493,
Springer,
2015.
- Z. Banković, U. Liqat, P. Lopez-Garcia.
Trading-off Accuracy vs. Energy in Multicore
Processors via Evolutionary Algorithms
Combining Loop Perforation and
Static Analysis-based Scheduling.
Hybrid Artificial Intelligent Systems (HAIS 2015),
Lecture Notes in Computer Science,
Vol. 9121,
páginas 690--701,
Springer International Publishing,
2015.
- Z. Banković, P. Lopez-Garcia.
Improved Energy-aware Stochastic Scheduling based on
Evolutionary Algorithms via Copula-based
Modeling of Task Dependences.
International Conference on Soft Computing Models in
Industrial and Environmental Applications (SOCO 2015),
Advances in Intelligent Systems and Computing,
Vol. 368,
páginas 153--163,
Springer International Publishing,
2015.
- Z. Banković, P. Lopez-Garcia.
Energy Efficient Allocation and Scheduling for
DVFS-enabled Multicore Environments using a
Multiobjective Evolutionary Algorithm.
Genetic and Evolutionary Computation Conference (GECCO 2015),
páginas 1353--1354,
ACM,
2015.
- J.F. Morales, M. V. Hermenegildo.
Pre-Indexed Terms for Prolog.
Post-Proceedings of the 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'14),
LNCS,
Vol. 8981,
páginas 317--331,
Springer,
2015.
- Bernd Finkbeiner, Markus N. Rabe, César Sánchez.
Algorithms for Model Checking HyperLTL and HyperCTL*.
Proc. of the 27th Int'l Conf. on Computer Aided Verification (CAV'15),
LNCS,
Vol. 9206,
Springer,
2015.
- Bishoksan Kafle, John P. Gallagher.
Tree automata-based refinement with application to Horn clause verification.
Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings,
Lecture Notes in Computer Science,
Vol. 8931,
páginas 209--226,
Springer,
2015.
- Bishoksan Kafle, John P. Gallagher.
Constraint Specialisation in Horn Clause Verification.
Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015,
páginas 85--90,
Association for Computing Machinery,
2015.
- Carolina Dania, Manuel Clavel.
Model-Based Formal Reasoning about Data-Management Applications.
Fundamental Approaches to Software Engineering - 18th International
Conference, FASE 2015, Held as Part of the European Joint Conferences
on Theory and Practice of Software, ETAPS 2015, London, UK, April
11-18, 2015. Proceedings,
Lecture Notes in Computer Science,
Vol. 9033,
páginas 218--232,
Springer,
2015.
- Miguel Ángel García de Dios, Carolina Dania, Manuel Clavel.
Formal Reasoning about Fine-Grained Access Control Policies.
11th Asia-Pacific Conference on Conceptual Modelling, APCCM 2015,
Sydney, Australia, January 2015,
CRPIT,
Vol. 165,
páginas 91--100,
Australian Computer Society,
2015.
- M. Zubair Rafique, Juan Caballero, Christophe Huygens, Wouter Joosen.
Network Dialog Minimization and Network Dialog Diffing: Two Novel Primitives for Network Security Applications.
Proceedings of the 2014 Annual Computer Security Applications Conference,
Diciembre
2014.
- Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie.
System-level Non-interference for Constant-time Cryptography.
21st ACM Conference on Computer and Communications Security (CCS 2014),
páginas 1267--1279,
ACM,
Noviembre
2014.
- Gilles Barthe, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz.
Synthesis of Fault Attacks on Cryptographic Implementations.
21st ACM Conference on Computer and Communications Security (CCS 2014),
páginas 1016--1027,
ACM,
Noviembre
2014.
- Dragan Ivanovic, Manuel Carro.
Transforming Service Compositions into Cloud-Friendly Actor Networks.
Service-Oriented Computing - 12th International Conference, ICSOC
2014, Paris, France, November 3-6, 2014. Proceedings,
LNCS,
Vol. 8831,
páginas 291--305,
Springer Verlag,
Noviembre
2014.
- Dragan Ivanović, Manuel Carro, Peerachai Kaowichakorn.
Towards QoS Prediction Based on Composition Structure Analysis and Probabilistic Models.
Service-Oriented Computing - 12th International Conference, ICSOC,
LNCS,
Vol. 8831,
páginas 394--402,
Springer Verlag,
Noviembre
2014.
- Zhaoyan Xu, Antonio Nappa, Robert Baykov, Guangliang Yang, Juan Caballero, Guofei Gu.
AutoProbe: Towards Automatic Active Malicious Server Probing Using Dynamic Binary Analysis.
Proceedings of the 21st ACM Conference on Computer and Communication Security,
Noviembre
2014.
- Liang Wang, Antonio Nappa, Juan Caballero, Thomas Ristenpart, Aditya Akella.
WhoWas: A Platform for Measuring Web Deployments on IaaS Clouds.
Proceedings of the 2014 ACM Internet Measurement Conference,
Noviembre
2014.
- R. Haemmerlé.
On Combining Backward and Forward Chaining
in Constraint Logic Programming.
16th Int'l. ACM SIGPLAN Symposium on Principles and
Practice of Declarative Programming (PPDP'14),
12 páginas,
ACM Press,
Septiembre
2014.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
Assertion-based Debugging of
Higher-Order (C)LP Programs.
16th Int'l. ACM SIGPLAN Symposium on Principles and
Practice of Declarative Programming (PPDP'14),
páginas 225--235,
ACM Press,
Septiembre
2014.
- David Urbina, Yufei Gu, Juan Caballero, Zhiqiang Lin.
SigPath: A Memory Graph Based Approach for Program Data Introspection and Modification.
Proceedings of the 19th European Symposium on Research in Computer Security,
Septiembre
2014.
- Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub.
Certified Synthesis of Efficient Batch Verifiers.
Computer Security Foundations Symposium (CSF 2014),
Julio
2014.
- Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub.
Proving differential privacy in Hoare logic.
Computer Security Foundations Symposium (CSF 2014),
Julio
2014.
CoRR abs/1407.2988 [cs.LO].
- Antonio Nappa, Zhaoyan Xu, Juan Caballero, Guofei Gu.
CyberProbe: Towards Internet-Scale Active Detection of Malicious Servers.
Proceedings of the Network and Distributed System Security Symposium,
Febrero
2014.
- Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones.
Modular, higher-order cardinality analysis in theory and
practice.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL '14,
páginas 335--348,
ACM,
2014.
- Gilles Barthe, Francois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz.
Making RSA-PSS Provably Secure against Non-random Faults.
Cryptographic Hardware and Embedded Systems - CHES 2014 - 16th International
Workshop, Busan, South Korea, September 23-26, 2014. Proceedings,
Lecture Notes in Computer Science,
Vol. 8731,
páginas 206--222,
Springer,
2014.
- Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt.
Automated Analysis of Cryptographic Assumptions in Generic Group Models.
Advances in Cryptology - CRYPTO 2014 - 34th Annual Cryptology Conference,
Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part I,
Lecture Notes in Computer Science,
Vol. 8616,
páginas 95--112,
Springer,
2014.
- Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin.
Probabilistic relational verification for cryptographic implementations.
The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, POPL '14, San Diego, CA, USA, January 20-21,
2014,
páginas 193--206,
ACM,
2014.
- Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa.
Leakage Resilience against Concurrent Cache Attacks.
Principles of Security and Trust - Third International Conference,
POST 2014, Held as Part of the European Joint Conferences on Theory
and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13,
2014, Proceedings,
Lecture Notes in Computer Science,
Vol. 8414,
páginas 140--158,
Springer,
2014.
- Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub.
Higher-Order Approximate Relational Refinement Types for Mechanism
Design and Differential Privacy.
Computer Security Foundations Symposium (CSF 2014),
2014.
CoRR abs/1407.6845 [cs.PL].
- Giovanni Bernardi, Ornela Dardha, Simon J. Gay, Dimitrios Kouzapas.
On Duality Relations for Session Types.
Trustworthy Global Computing, TGC 2014 Revised Selected Papers,
Lecture Notes in Computer Science,
páginas 51--66,
Springer Berlin Heidelberg,
2014.
- Giovanni Bernardi, Matthew Hennessy.
Using Higher-Order Contracts to Model Session Types (Extended Abstract).
CONCUR 2014 - Concurrency Theory - 25th International Conference,
CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings,
Lecture Notes in Computer Science,
Vol. 8704,
páginas 387--401,
Springer,
2014.
- Anindya Banerjee, David A. Naumann.
A Logical Analysis of Framing for Specifications with Pure Method
Calls.
Verified Software: Theories, Tools and Experiments - 6th International
Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised
Selected Papers,
páginas 3--20,
2014.
- Pavithra Prabhakar, Miriam Garcia Soto.
An algorithmic approach to stability verification of polyhedral switched
systems.
American Control Conference, ACC 2014, Portland, OR, USA, June 4-6,
2014,
páginas 2318--2323,
IEEE,
2014.
- Jun Liu, Pavithra Prabhakar.
Switching control of dynamical systems from metric temporal logic
specifications.
2014 IEEE International Conference on Robotics and Automation, ICRA
2014, Hong Kong, China, May 31 - June 7, 2014,
páginas 5333--5338,
IEEE,
2014.
- Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky.
Safety of live transactions in transactional memory: TMS is necessary and sufficient.
DISC'14: International Symposium on Distributed Computing, Austin, TX, USA,
LNCS,
Vol. 8784,
páginas 376--390,
Springer,
2014.
- Andrea Cerone, Alexey Gotsman, Hongseok Yang.
Parameterised linearisability.
ICALP'14: International Colloquium on Automata, Languages, and Programming, Copenhagen, Denmark,
LNCS,
Vol. 8573,
páginas 98--109,
Springer,
2014.
- Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski.
Replicated data types: specification, verification, optimality.
Proceedings of the 41st ACM Symposium on Principles of Programming Languages (POPL'14), San Diego, CA, USA,
páginas 271--284,
ACM Press,
2014.
- Dario Fiore, Rosario Gennaro, Valerio Pastro.
Efficiently Verifiable Computation on Encrypted Data.
ACM CCS 2014 -- 21th ACM Conference on Computer and Communication Security,
páginas 844--855,
2014.
- Dario Catalano, Dario Fiore, Bogdan Warinschi.
Homomorphic Signatures with Efficient Verification for Polynomial Functions.
Advances in Cryptology -- CRYPTO 2014 -- 34th Annual Cryptology Conference,
Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part I,
LNCS,
Vol. 8616,
páginas 371--389,
Springer,
2014.
- Dario Catalano, Dario Fiore, Rosario Gennaro, Luca Nizzardo.
Generalizing Homomorphic MACs for Arithmetic Circuits.
PKC 2014: 17th International Workshop on Theory and Practice in Public Key Cryptography,
LNCS,
Vol. 8383,
páginas 538--555,
Springer,
2014.
- Yevgeniy Dodis, Dario Fiore.
Interactive Encryption and Message Authentication.
Security and Cryptography for Networks - 9th International Conference,
SCN 2014,
LNCS,
Vol. 8642,
páginas 494--513,
Springer,
2014.
- Cerone, Andrea, Hennessy, Matthew.
Characterising Testing Preorders for Broadcasting Distributed Systems.
Trustworthy Global Computing,
páginas 67--81,
Springer,
2014.
- Zvonimir Rakamaric, Michael Emmi.
SMACK: Decoupling Source Language Details from Verifier Implementations.
Computer Aided Verification - 26th International Conference, CAV
2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna,
Austria, July 18-22, 2014. Proceedings,
Vol. 8559,
páginas 106--113,
Springer,
2014.
- Michael Emmi, Burcu Kulahcioglu Ozkan, Serdar Tasiran.
Exploiting synchronization in the analysis of shared-memory asynchronous
programs.
2014 International Symposium on Model Checking of Software, SPIN
2014, Proceedings, San Jose, CA, USA, July 21-23, 2014,
páginas 20--29,
ACM,
2014.
- Zhoulai Fu.
Targeted Update - Aggressive Memory Abstraction Beyond Common Sense
and Its Application on Static Numeric Analysis.
Programming Languages and Systems - 23rd European Symposium on Programming,
ESOP 2014, Held as Part of the European Joint Conferences on Theory
and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13,
2014, Proceedings,
páginas 534--553,
2014.
- Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, German Andres Delbianco.
Communicating State Transition Systems for Fine-Grained Concurrent Resources.
European Symposium on Programming (ESOP),
páginas 290--310,
2014.
- Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv.
Modular Reasoning about Heap Paths via Effectively Propositional Formulas.
Principles of Programming Languages (POPL),
páginas 385--396,
2014.
- Ganty, Pierre, Rezine, Ahmed.
Ordered Counter Abstraction (Refinable Subword Relations for Parameterized Verification).
LATA'14, 8th Int. Conf. on Language and Automata Theory and Applications,
LNCS,
Vol. 8370,
páginas 396--407,
Springer,
2014.
- Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa.
Leakage Resilience against Concurrent Cache Attacks.
Proc. 3rd Conference on Principles of Security and Trust (POST '14),
Springer,
2014.
- U. Liqat, S. Kerrison, A. Serrano, K. Georgiou, P. Lopez-Garcia, N. Grech, M. V. Hermenegildo, K. Eder.
Energy Consumption Analysis of Programs based on XMOS ISA-Level Models.
Logic-Based Program Synthesis and Transformation, 23rd International
Symposium, LOPSTR 2013, Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 8901,
páginas 72--90,
Springer,
2014.
- Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin.
Proving the TLS Handshake Secure (As It Is).
Advances in Cryptology - CRYPTO 2014 - 34th Annual Cryptology Conference,
Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part II,
páginas 235--255,
2014.
- Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub.
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS.
Proceedings of the 2014 IEEE Symposium on Security and Privacy,
SP '14,
páginas 98--113,
IEEE Computer Society,
2014.
- Evmorfia-Iro Bartzia, Pierre-Yves Strub.
A Formal Library for Elliptic Curves in the Coq Proof Assistant.
Interactive Theorem Proving - 5th International Conference, ITP
2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna,
Austria, July 14-17, 2014. Proceedings,
Lecture Notes in Computer Science,
Vol. 8558,
páginas 77--92,
Springer,
2014.
- Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman.
Gradual typing embedded securely in JavaScript.
The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, POPL '14, San Diego, CA, USA, January 20-21,
2014,
páginas 425--438,
ACM,
2014.
- Alejandro Sánchez, César Sánchez.
Formal Verification of Skiplists with Arbitrarily Many Levels.
Proc. of the 12th Int'l Symp. on Automated Technology for Verification and Analysis (ATVA),
LNCS,
Vol. 8837,
páginas 314--329,
Springer,
2014.
- Alejandro Sánchez, César Sánchez.
Parametrized Verification Diagrams.
Proc. of the 21st Int'l Symp. on Temporal Representation and Reasoning (TIME'14),
páginas 132--141,
IEEE Computer Society Press,
2014.
- Laura Bozzelli, César Sánchez.
Foundations of Boolean Stream Runtime Verification.
Proc. of the 14th Int'l Conf. on Runtime Verification (RV'14),
LNCS,
Vol. 8734,
páginas 64--79,
Springer,
2014.
- Alejandro Sánchez, César Sánchez.
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes.
Proc. of the 26th Int'l Conf. on Computer Aided Verification (CAV'14),
LNCS,
Vol. 8559,
páginas 620--627,
Springer,
2014.
- Laura Bozzelli, César Sánchez.
Visibly Linear Temporal Logic.
Proc. of the 7th Int'l Joint Conf. on Automated Reasoning (IJCAR'14),
LNCS,
Vol. 8562,
páginas 418--433,
Springer,
2014.
- Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez.
Temporal Logics for Hyperproperties.
Proc. of the 3rd Conference on Principles of Security and Trust (POST 2014),
LNCS,
Vol. 8414,
páginas 265--284,
Springer,
2014.
- Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey.
Deriving interpretations of the gradually-typed lambda calculus.
Proceedings of the ACM SIGPLAN 2014 Workshop on Partial
Evaluation and Program Manipulation,
páginas 157--168,
ACM,
2014.
- Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin.
Automated Verification of Group Key Agreement Protocols.
Proceedings of the 2014 IEEE Symposium on Security and Privacy,
SP '14,
páginas 179--194,
IEEE Computer Society,
2014.
- Marcos Arjona, Carolina Dania, Marina Egea, Antonio Maña.
Validation of a Security Metamodel for the Development of Cloud Applications.
Proceedings of the 14th International Workshop on OCL and Textual
Modelling co-located with 17th International Conference on Model Driven
Engineering Languages and Systems (MODELS 2014), Valencia, Spain,
September 30, 2014.,
páginas 33--42,
2014.
- Achim D. Brucker, Tony Clark, Carolina Dania, Geri Georg, Martin Gogolla, Frédéric Jouault, Ernest Teniente, Burkhart Wolff.
Panel Discussion: Proposals for Improving OCL.
Proceedings of the 14th International Workshop on OCL and Textual
Modelling co-located with 17th International Conference on Model Driven
Engineering Languages and Systems (MODELS 2014), Valencia, Spain,
September 30, 2014.,
páginas 83--99,
2014.
- Carolina Dania, Manuel Clavel.
Modeling Social Networking Privacy.
2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, September 1-3, 2014,
páginas 50--57,
2014.
- Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella Béguelin.
Fully automated analysis of padding-based encryption in
the computational model.
2013 ACM SIGSAC Conference on Computer and Communications Security (CCS'13),
páginas 1247--1260,
ACM,
Noviembre
2013.
- Martina Lindorfer, Matthias Neumayr, Juan Caballero, Christian Platzer.
POSTER: Cross-Platform Malware: Write Once, Infect Everywhere.
Proceedings of the 20th ACM Conference on Computer and Communications Security,
Noviembre
2013.
- M. Zubair Rafique, Juan Caballero.
FIRMA: Malware Clustering and Network Signature Generation with Mixed Network Behaviors.
Proceedings of the 16th International Symposium on Research in Attacks, Intrusions and Defenses,
Octubre
2013.
- A. Serrano, P. Lopez-Garcia, F. Bueno, M. V. Hermenegildo.
Sized Type Analysis for Logic Programs.
Theory and Practice of Logic Programming,
29th Int'l. Conference on Logic Programming (ICLP'13) Special Issue,
On-line Supplement (technical communication),
Vol. 13,
Núm. 4-5,
páginas 1--14,
Cambridge U. Press,
Agosto
2013.
- Antonio Nappa, M. Zubair Rafique, Juan Caballero.
Driving in the Cloud: An Analysis of Drive-by Download Operations and Abuse Reporting.
Proceedings of the 10th Conference on Detection of Intrusions and Malware & Vulnerability Assessment,
Julio
2013.
- Z. Drey, J. F. Morales, M. V. Hermenegildo, M. Carro.
Reversible Language Extensions and their Application in Debugging.
Practical Aspects of Declarative Languages (PADL'13),
LNCS,
Vol. 7752,
Springer,
Enero
2013.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
Supporting Pruning in Tabled LP.
Practical Aspects of Declarative Languages (PADL'13),
LNCS,
Springer Verlag,
Enero
2013.
- Dominique Devriese, Ilya Sergey, Dave Clarke, Frank Piessens.
Fixing idioms: a recursion primitive for applicative DSLs.
Proceedings of the ACM SIGPLAN 2013 Workshop on Partial
Evaluation and Program Manipulation, PEPM 2013,
páginas 97--106,
ACM,
2013.
- Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, Frank Piessens.
Monadic abstract interpreters.
Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and
Implementation, PLDI '13,
páginas 399--410,
ACM,
2013.
- Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin.
Verified Computational Differential Privacy with Applications
to Smart Metering.
2013 IEEE 26th Computer Security Foundations Symposium,
New Orleans, LA, USA, June 26-28, 2013,
páginas 287--301,
IEEE,
2013.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir.
Certified computer-aided cryptography: efficient provably
secure machine code from high-level implementations.
2013 ACM SIGSAC Conference on Computer and Communications Security (CCS'13),
páginas 1217--1230,
2013.
- Gilles Barthe, Juan Manuel Crespo, César Kunz.
Beyond 2-Safety: Asymmetric Product Programs for Relational
Program Verification.
Logical Foundations of Computer Science, International Symposium,
LFCS 2013,
Lecture Notes in Computer Science,
Vol. 7734,
páginas 29--43,
Springer,
2013.
- Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron.
From Relational Verification to SIMD Loop Synthesis.
ACM SIGPLAN Symposium on Principles and Practice of Parallel
Programming, PPoPP '13,
páginas 123--134,
ACM,
2013.
- Guillermo Vigueras, Cristobal Samaniego, Guillaume Houzeau, Mariano Vazquez, Antoine Jerusalem.
An XFEM Implementation for Fracture Simulations of Composites.
International Conference on Computational Plasticity.
Fundamentals and Applications. COMPLAS 2013,
2013.
- Guillermo Vigueras, Cristobal Samaniego, Eva Casoni, Guillaume Houzeau, Federico Sket, Jon Molina-Aldareguia, Ahmed Makradi, Mariano Vazquez, Antoine Jerusalem.
An XFEM-CZM Implementation for Large-Scale Fracture Simulations of
Composites Laminates.
European Congress and Exhibition on Advanced Materials and Processes. EUROMAT 2013,
2013.
- Pavithra Prabhakar, Miriam Garcia Soto.
Abstraction Based Model-Checking of Stability of Hybrid
Systems.
CAV,
páginas 280--295,
2013.
- Pavithra Prabhakar, Jun Liu, Richard M. Murray.
Pre-orders for reasoning about stability properties with
respect to input of hybrid systems.
EMSOFT,
páginas 1--10,
2013.
- Pavithra Prabhakar, Mahesh Viswanathan.
On the decidability of stability of hybrid systems.
HSCC,
2013.
- Scott C. Livingston, Pavithra Prabhakar, Alex B. Jose, Richard M. Murray.
Patching task-level robot controllers based on a local -calculus
formula.
ICRA,
2013.
- Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan.
Hybrid Automata based CEGAR for Rectangular Hybrid Automata.
VMCAI,
2013.
- Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky.
A programming language perspective on transactional memory consistency.
Proceedings of the 32nd ACM Symposium on Principles of Distributed Computing (PODC'13), Montreal, Canada,
páginas 309--318,
ACM Press,
2013.
- Alexey Gotsman, Noam Rinetzky, Hongseok Yang.
Verifying concurrent memory reclamation algorithms with grace.
Proceedings of the 22nd European Symposium on Programming (ESOP'13), Rome, Italy,
LNCS,
Vol. 7792,
páginas 249--269,
Springer,
2013.
- Mark Batty, Mike Dodds, Alexey Gotsman.
Library abstraction for C/C++ concurrency.
Proceedings of the 40th ACM Symposium on Principles of Programming Languages (POPL'13), Rome, Italy,
páginas 235--248,
ACM Press,
2013.
- Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza.
Verifying Concurrent Programs Against Sequential Specifications.
ESOP '13: Proc. 22nd European Symposium on Programming,
LNCS,
Springer,
2013.
- Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski.
Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures.
Principles and Practice of Declarative Programming (PPDP),
páginas 145--156,
2013.
- Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
Mtac: A Monad for Typed Tactic Programming in Coq.
International Conference on Functional Programming (ICFP),
páginas 87--100,
2013.
- Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv.
Effectively-Propositional Reasoning about Reachability in Linked Data Structures.
Computer Aided Verification (CAV),
páginas 756--772,
2013.
- Ruy Ley-Wild, Aleksandar Nanevski.
Subjective Auxiliary State for Coarse-Grained Concurrency.
Principles of Programming Languages (POPL),
páginas 561--574,
2013.
- Javier Esparza, Pierre Ganty, Rupak Majumdar.
Parameterized Verification of Asynchronous Shared-Memory Systems.
CAV'13: Proc. 23rd Int. Conf. on Computer Aided Verification,
LNCS,
Vol. 8044,
páginas 124--140,
Springer,
2013.
- Pierre Ganty, Samir Genaim.
Proving Termination Starting from the End.
CAV'13: Proc. 23rd Int. Conf. on Computer Aided Verification,
LNCS,
Vol. 8044,
páginas 397--412,
Springer,
2013.
- Pierre Ganty, Radu Iosif, Filip Konecný.
Underapproximation of Procedure Summaries for Integer Programs.
TACAS'13: Proc. 19th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems,
LNCS,
Vol. 7795,
páginas 247--261,
Springer,
2013.
- Boris Köpf, Andrey Rybalchenko.
Automation of Quantitative Information-Flow Analysis.
13th International
School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM),
LNCS 7938,
Springer,
2013.
- Goran Doychev, Dominik Feld, Boris Köpf, Laurent Mauborgne, Jan Reineke.
CacheAudit: A Tool for the Static Analysis of Cache Side Channels.
22nd USENIX Security Symposium,
USENIX,
2013.
- Pavithra Prabhakar, Boris Köpf.
Verifying Information Flow Properties of Hybrid Systems.
Proc. 2nd ACM International Conference on High Confidence Networked Systems (HiCoNS),
ACM,
2013.
- Michael Backes, Goran Doychev, Boris Köpf.
Preventing Side-Channel Leaks in Web Traffic: A Formal Approach.
Proc. 20th Network and Distributed Systems Security Symposium (NDSS),
Internet Society,
2013.
- Z. Banković, P. Lopez-Garcia.
Genetic Algorithm-based Allocation and Scheduling for Voltage and Frequency Scalable XMOS Chips.
Hybrid Artificial Intelligent Systems (HAIS 2013),
Lecture Notes in Computer Science,
Vol. 8073,
páginas 401--410,
Springer,
2013.
- Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits.
Fully abstract compilation to JavaScript.
The 40th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '13,
páginas 371--384,
ACM,
2013.
- Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub.
Implementing TLS with Verified Cryptographic Security.
IEEE Symposium on Security and Privacy,
páginas 445--459,
IEEE Computer Society,
2013.
- Álvaro García-Pérez, Pablo Nogueira, Juan José
Moreno-Navarro.
Deriving the Full-reducing Krivine Machine from the Small-step
Operational Semantics of Normal Order.
Proceedings of the 15th Symposium on Principles and Practice of
Declarative Programming,
PPDP '13,
páginas 85--96,
ACM,
2013.
- Álvaro García-Pérez, Pablo Nogueira.
A syntactic and functional correspondence between reduction semantics
and reduction-free full normalisers.
Proceedings of the ACM SIGPLAN 2013 Workshop on Partial
Evaluation and Program Manipulation,
PEPM '13,
páginas 107--116,
ACM,
2013.
- Germán Andrés Delbianco, Aleksandar Nanevski.
Hoare-style reasoning with (algebraic) continuations.
Proceedings of the 18th ACM SIGPLAN international
conference on Functional programming,
ICFP '13,
páginas 363--376,
ACM,
2013.
- Simon Meier, Benedikt Schmidt, Cas Cremers, David A. Basin.
The TAMARIN Prover for the Symbolic Analysis of Security Protocols.
Computer Aided Verification - 25th International Conference, CAV
2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings,
Lecture Notes in Computer Science,
Vol. 8044,
páginas 696--701,
Springer,
2013.
- Carolina Dania, Manuel Clavel.
OCL2FOL+: Coping with Undefinedness.
Proceedings of the MODELS 2013 OCL Workshop co-located with
the 16th International ACM/IEEE Conference on Model Driven
Engineering Languages and Systems (MODELS 2013), Miami,
USA, September 30, 2013,
CEUR Workshop Proceedings,
Vol. 1092,
páginas 53--62,
CEUR-WS.org,
2013.
- D. Ivanovic, M. Carro, M. V. Hermenegildo.
A Constraint-Based Approach to Quality Assurance in
Service Choreographies.
10th International Conference on Service Oriented
Computing, ICSOC'12,
LNCS,
Vol. 7637,
Springer Verlag,
Noviembre
2012.
- Chris Grier, Lucas Ballard, Juan Caballero, Neha
Chachra, Christian J. Dietrich, Kirill Levchenko, Panayiotis Mavrommatis, Damon McCoy, Antonio Nappa, Andreas Pitsillidis, Niels Provos, M. Zubair Rafique, Moheeb Abu Rajab, Christian Rossow, Kurt Thomas, Vern Paxson, Stefan Savage, Geoffrey M. Voelker.
Manufacturing Compromise: The Emergence of Exploit-as-a-Service.
Proceedings of the 19th ACM Conference on Computer and
Communication Security,
Octubre
2012.
- George Bariannys, M. Carro, Dimitris Plexousakis.
Deriving Specifications for Composite Web Services.
IEEE Signature Conference on Computers, Software, and Applications,
IEEE Computer Society,
IEEE,
Julio
2012.
- Juan Caballero, Gustavo Grieco, Mark Marron, Antonio Nappa.
Early Detection of Dangling Pointers in Use-After-Free and Double-Free Vulnerabilities.
Proceedings of the 2012 International Symposium on Software Testing and Analysis,
Julio
2012.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, P. Stuckey.
A General Implementation Framework for
Tabled CLP.
FLOPS'12,
LNCS,
Núm. 7294,
páginas 104--119,
Springer Verlag,
Mayo
2012.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, P. Stuckey.
A General Implementation Framework for
Tabled CLP.
15th Int'l. Symposium on Functional and Logic Programming,
LNCS,
Vol. 7294,
páginas 104--119,
Springer Verlag,
Mayo
2012.
- P. Chico de Guzmán, A. Casas, M. Carro, M. V. Hermenegildo.
A Segment-Swapping Approach for Executing Trapped Computations.
PADL'12,
LNCS,
Vol. 7149,
páginas 138--152,
Springer Verlag,
Enero
2012.
- José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin.
Full Proof Cryptography: Verifiable Compilation of Efficient
Zero-Knowledge Protocols.
ACM Conference on Computer and Communications Security,
páginas 488--500,
2012.
- Gilles Barthe, David Pointcheval, Santiago Zanella Béguelin.
Verified Security of Redundancy-Free Encryption from Rabin
and RSA.
ACM Conference on Computer and Communications Security,
páginas 724--735,
2012.
- Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin.
Automation in Computer-Aided Cryptography: Proofs, Attacks
and Designs.
Certified Programs and Proofs - Second International Conference, CPP 2012,
Lecture Notes in Computer Science,
Vol. 7679,
páginas 7--8,
Springer,
2012.
- Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna.
Cache-Leakage Resilient OS Isolation in an Idealized Model
of Virtualization.
25th IEEE Computer Security Foundations Symposium, CSF 2012,
páginas 186--197,
IEEE,
2012.
- Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin.
Verified Security of Merkle-Damgrd.
25th IEEE Computer Security Foundations Symposium, CSF 2012,
páginas 354--368,
IEEE,
2012.
- Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin.
Computer-Aided Cryptographic Proofs.
Interactive Theorem Proving - Third International Conference, ITP 2012,
Lecture Notes in Computer Science,
Vol. 7406,
páginas 11--27,
Springer,
2012.
- Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas.
Secure Multi-Execution through Static Program Transformation.
Formal Techniques for Distributed Systems - Joint 14th IFIP
WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP
WG 6.1 International Conference, FORTE 2012,
Lecture Notes in Computer Science,
Vol. 7273,
páginas 186--202,
Springer,
2012.
- Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin.
Probabilistic Relational Hoare Logics for Computer-Aided
Security Proofs.
Mathematics of Program Construction - 11th International Conference, MPC 2012,
Lecture Notes in Computer Science,
Vol. 7342,
páginas 1--6,
Springer,
2012.
- Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin.
Computer-Aided Cryptographic Proofs.
Static Analysis - 19th International Symposium, SAS 2012,
Lecture Notes in Computer Science,
Vol. 7460,
páginas 1--2,
Springer,
2012.
- Gilles Barthe, Delphine Demange, David Pichardie.
A Formally Verified SSA-Based Middle-End - Static Single
Assignment Meets CompCert.
21st European Symposium on Programming, ESOP 2012,
Lecture Notes in Computer Science,
Vol. 7211,
páginas 47--66,
Springer,
2012.
- Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin.
Probabilistic relational reasoning for differential privacy.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2012,
páginas 97--110,
ACM,
2012.
- Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin.
Verified Indifferentiable Hashing into Elliptic Curves.
1st Conference on Principles of Security and Trust, POST 2012,
Lecture Notes in Computer Science,
Vol. 7215,
Springer,
2012.
- Mark Marron, Ondrej Lhoták, Anindya Banerjee.
Programming Paradigm Driven Heap Analysis.
21st International Conference on Compiler Construction (CC 2012),
Lecture Notes in Computer Science,
Vol. 7210,
páginas 41--60,
Springer Berlin Heidelberg,
2012.
- Stan Rosenberg, Anindya Banerjee, David A. Naumann.
Decision Procedures for Region Logic.
13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012),
Lecture Notes in Computer Science,
Vol. 7148,
páginas 379--395,
Springer Berlin Heidelberg,
2012.
- Alexander Malkis, Anindya Banerjee.
Verification of Software Barriers.
Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel Programming (PPoPP 2012),
páginas 313--314,
ACM,
2012.
- Pavithra Prabhakar.
Foundations for Approximation Based Analysis of Stability Properties of Hybrid Systems.
50th Annual Allerton Conference on Communication, Control and Computing,
2012.
- Pavithra Prabhakar, Mahesh Viswanathan.
Conformance Testing of Boolean Programs with Multiple Faults.
Formal Techniques for Distributed Systems - Joint 14th IFIP
WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP
WG 6.1 International Conference, FORTE 2012, Stockholm,
Sweden, June 13-16, 2012. Proceedings,
Lecture Notes in Computer Science,
Vol. 7273,
páginas 101--117,
Springer,
2012.
- Pavithra Prabhakar, Geir E. Dullerud, Mahesh Viswanathan.
Pre-orders for reasoning about stability.
Hybrid Systems: Computation and Control (part of CPS Week
2012), HSCC'12, Beijing, China, April 17-19, 2012,
páginas 197--206,
ACM,
2012.
- Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang.
Show no weakness: sequentially consistent specifications of TSO libraries.
Proceedings of the International Symposium on Distributed Computing (DISC'12), Salvador, Bahia, Brazil,
LNCS,
Vol. 7611,
páginas 31--45,
Springer,
2012.
- Alexey Gotsman, Hongseok Yang.
Linearizability with ownership transfer.
Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), Newcastle upon Tyne, UK,
LNCS,
Vol. 7454,
páginas 256--271,
Springer,
2012.
- Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang.
Concurrent library correctness on the TSO memory model.
Proceedings of the 21st European Symposium on Programming (ESOP'12), Tallinn, Estonia,
LNCS,
Vol. 7211,
páginas 87--107,
Springer,
2012.
- Ruy Ley-Wild, Umut A. Acar, Guy Blelloch.
Non-Monotonic Self-Adjusting Computation.
European Symposium on Programming, ESOP 2012,
Lecture Notes in Computer Science,
Vol. 7211,
páginas 476--496,
Springer,
2012.
- César Sánchez, Julián Samborski-Forlese.
Efficient Regular Linear Temporal Logic Using Dualization and Stratification.
Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME'12),
páginas 13--20,
IEEE Computer Society,
2012.
- César Sánchez, Julián Samborski-Forlese.
How to Translate Efficiently Extensions of Temporal Logics into Alternating Automata.
Proceedings of The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC'12),
LNCS,
Vol. 7521,
páginas 30--45,
Springer,
2012.
- Javier Esparza, Pierre Ganty, Rupak Majumdar.
A Perfect Model for Bounded Verification.
LICS'12: Proc. 27th Annual ACM/IEEE Symp. on Logic in Computer Science,
páginas 285--294,
IEEE Computer Society Press,
2012.
- Boris Köpf, Laurent Mauborgne, Martín Ochoa.
Automatic Quantification of Cache Side-Channels.
24th International Conference on Computer Aided Verification (CAV '12),
Lecture Notes in Computer Science,
Vol. 7358,
páginas 564--580,
Springer-Verlag,
2012.
- Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin.
Probabilistic Relational Reasoning for Differential Privacy.
Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12),
páginas 97--109,
ACM,
2012.
- Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, Bor-Yuh Evan Chang.
Invariant Generation for Parametrized Systems Using Self-reflection.
Proc. of the 19th International Symposium on Static Analysis (SAS'12),
LNCS,
Vol. 7460,
páginas 146--163,
Springer,
2012.
- César Sánchez, Julián Samborski-Forlese.
Efficient Regular Linear Temporal Logic Using Dualization and Stratification.
Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME'12),
páginas 13--20,
IEEE Computer Society,
2012.
- César Sánchez, Julián Samborski-Forlese.
How to Translate Efficiently Extensions of Temporal Logics into Alternating Automata.
Proceedings of The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC'12),
LNCS,
Vol. 7521,
páginas 30--45,
Springer,
2012.
- Laura Bozzelli, César Sánchez.
Visibly Rational Expressions.
Proc. of the 32nd Int'l Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12),
Leibniz International Proceedings in Informatics (LIPIcs),
páginas 211--223,
Leibniz-Zentrum fuer Informatik,
2012.
- Mai Ajspur, John P. Gallagher.
Towards Abstract Interpretation of Epistemic Logic.
8th Scandinavian Logic Symposium, 20-21 August 2012, Roskilde University, Denmark,
Roskilde University,
2012.
Extended Abstract.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Constraint-Based Runtime Prediction of SLA
Violations in Service Orchestrations.
Service-Oriented Computing -- ICSOC 2011,
LNCS,
Vol. 7084,
páginas 62--76,
Springer Verlag,
Diciembre
2011.
Best paper award.
- Juan Manuel Crespo, César Kunz.
A Machine-Checked Framework for Relational Separation Logic.
Software Engineering and Formal Methods - 9th International
Conference, SEFM 2011,
LNCS,
Vol. 7041,
páginas 122--137,
Springer,
Noviembre
2011.
- Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin.
Verifiable Security of Boneh-Franklin Identity-Based Encryption.
5th International Conference on Provable Security -- ProvSec 2011,
Lecture Notes in Computer Science,
Vol. 6980,
páginas 68--83,
Springer,
Octubre
2011.
- Barthe, Gilles, Grégoire, Benjamin, Heraud, Sylvain, Zanella Béguelin, Santiago.
Computer-Aided Security Proofs for the Working Cryptographer.
Advances in Cryptology -- CRYPTO 2011,
Lecture Notes in Computer Science,
Vol. 6841,
páginas 71--90,
Springer,
Agosto
2011.
- Juan Caballero, Chris Grier, Christian Kreibich, Vern Paxson.
Measuring Pay-per-Install: The Commoditization of Malware Distribution.
Proceedings of the 20th USENIX Security Symposium,
Agosto
2011.
- J. F. Morales, M. V. Hermenegildo, R. Haemmerlé.
Modular Extensions for Modular (Logic) Languages.
Proceedings of the 21th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'11),
LNCS,
Vol. 7225,
páginas 139--154,
Springer,
Julio
2011.
- R. Haemmerlé, P. Lopez-Garcia, M. V. Hermenegildo.
CLP Projection for Constraint Handling Rules.
Proceedings of the 13th International ACM SIGPLAN Conference
on Principles and Practice of Declarative Programming,
páginas 137--148,
ACM Press,
Julio
2011.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Automated Attribute Inference in Complex Service
Workflows Based on Sharing Analysis.
Proceedings of the 8th IEEE Conference on Services
Computing SCC 2011,
páginas 120--127,
IEEE Press,
Julio
2011.
- Gilles Barthe, Juan Manuel Crespo, César Kunz.
Relational Verification Using Product Programs.
FM 2011: 17th International Symposium on Formal Methods,
LNCS,
Vol. 6664,
páginas 200--214,
Springer,
Junio
2011.
- Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna.
Formally Verifying Isolation and Availability in an Idealized
Model of Virtualization.
FM 2011: 17th International Symposium on Formal Methods,
LNCS,
Vol. 6664,
páginas 231--245,
Springer,
Junio
2011.
- David A. Basin, Manuel Clavel, Marina Egea.
A decade of model-driven security.
SACMAT 2011, 16th ACM Symposium on Access Control Models
and Technologies,
páginas 1--10,
ACM,
Junio
2011.
- Germán Andrés Delbianco, Mauro Jaskelioff, Alberto Pardo.
Applicative Shortcut Fusion.
12th International Symposium on Trends in Functional
Programming, TFP'11,
Mayo
2011.
- Noah M. Johnson, Juan Caballero, Kevin Chen, Stephen McCamant, Pongsin Poosankam, Daniel
Reynaud, Dawn Song.
Differential Slicing: Identifying Causal Execution Differences for Security Applications.
Proceedings of the IEEE Symposium on Security and Privacy,
Mayo
2011.
- Barthe, Gilles, Grégoire, Benjamin, Lakhnech, Yassine, Zanella Béguelin, Santiago.
Beyond Provable Security Verifiable IND-CCA Security of OAEP.
Topics in Cryptology --- CT-RSA 2011,
Lecture Notes in Computer Science,
Vol. 6558,
páginas 180--196,
Springer,
Febrero
2011.
- E. Mera, T. Trigo, P. Lopez-Garcia, M. V. Hermenegildo.
Profiling for Run-Time Checking of
Computational Properties and Performance Debugging in Logic Programs.
Practical Aspects of Declarative Languages (PADL'11),
Lecture Notes in Computer Science,
Vol. 6539,
páginas 38--53,
Springer-Verlag,
Enero
2011.
- Gilles Barthe, Exequiel Rivas.
Static Enforcement of Information Flow Policies for a Concurrent Object-Oriented Language.
Sixth Trusted Global Computing Conference 2011 (TGC'11),
LNCS,
Springer,
2011.
- Alexey Gotsman, Hongseok Yang.
Modular verification of preemptive OS kernels.
Proceedings of the 16th ACM International Conference on Functional Programming (ICFP'11), Tokyo, Japan,
páginas 404--417,
ACM Press,
2011.
- Alexey Gotsman, Hongseok Yang.
Liveness-Preserving Atomicity Abstraction.
Proceedings of the 38th International Colloquium on Automata, Languages and Programming, (ICALP'11), Zurich, Switzerland,
LNCS,
Vol. 6756,
páginas 453--465,
Springer,
2011.
- Alexey Gotsman, Josh Berdine, Byron Cook.
Precision and the conjunction rule in concurrent separation logic.
Proceedings of the 27th Conference on the Mathematical Foundations of Programming Semantics (MFPS'11), Pittsburgh, PA, USA,
Elsevier,
2011.
- Patrick Cousot, Radhia Cousot, Laurent Mauborgne.
The Reduced Product of Abstract Domains and the Combination of Decision Procedures.
14th International Conference on Fondations of Software Science and Computation Structures (FoSSaCS 2011),
Lecture Notes in Computer Science,
Vol. 6604,
páginas 456--472,
Springer-Verlag,
2011.
- Alexander Malkis, Laurent Mauborgne.
On the Strength of Owicki-Gries for Resources.
9th Asian Symposium on Programming Languages and Systems (APLAS 2011),
Lecture Notes in Computer Science,
Vol. 7078,
páginas 172--187,
Springer,
2011.
- Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival.
Proving the Absence of Runtime Errors with the Static Analyzer Astrée.
Society of Automotive Engineering World Congress (SAE 2011),
2011.
- David A. Basin, Manuel Clavel, Marina Egea, Miguel Angel García de Dios, Carolina Dania, Gonzalo Ortiz, Javier Valdazo.
Model-Driven Development of Security-Aware GUIs for
Data-Centric Applications.
Foundations of Security Analysis and Design VI (FOSAD 2010),
LNCS,
Vol. 6858,
páginas 101--124,
Springer,
2011.
- Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
How to make ad hoc proof automation less ad hoc.
International Conference on Functional Programming (ICFP),
páginas 163--175,
2011.
- Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
Verification of Information Flow and Access Control Policies with Dependent Types.
IEEE Symposium on Security and Privacy (S&P),
páginas 165--179,
2011.
- Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski.
Partiality, State and Dependent Types.
Typed Lambda Calculi and Applications (TLCA),
páginas 198--212,
2011.
- Mohamed Faouzi Atig, Pierre Ganty.
Approximating Petri Net Reachability Along Context-free Traces.
FSTTCS '11: Proc. 31st Int. Conf. on Fondation of Software Technology and Theoretical Computer Science,
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 13,
Leibniz-Zentrum fuer Informatik,
2011.
- Laura Bozzelli, Pierre Ganty.
Complexity Analysis of the Backward Coverability Algorithm for VASS.
RP '11: Proc. 5th Workshop on Reachability Problems,
LNCS,
Vol. 6945,
Springer,
2011.
- Javier Esparza, Pierre Ganty.
Complexity of Pattern-based Verification for Multithreaded Programs.
POPL '11: Proc. 38th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages,
páginas 499--510,
ACM Press,
2011.
- Gilles Barthe, Boris Köpf.
Information-theoretic Bounds for Differentially Private Mechanisms.
Proc. 24rd IEEE Computer Security Foundations Symposium (CSF '11),
páginas 191--204,
IEEE,
2011.
- Michael Backes, Matthias Berg, Boris Köpf.
Non-Uniform Distributions in Quantitative Information-Flow.
Proc. 6th ACM Conference on Information, Computer and Communications Security (ASIACCS '11),
páginas 367--375,
ACM,
2011.
- M. Carro, D. Karastoyanova, G. A. Lewis, A. Liu.
Third International Workshop on Principles of Engineering
Service-Oriented Systems (PESOS 2011).
ICSE,
páginas 1218--1219,
2011.
- Alejandro Sánchez, César Sánchez.
A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes.
Proc. of the 3rd NASA Formal Methods Symposium (NFM'11),
LNCS,
Vol. 6447,
páginas 343--358,
Springer,
2011.
- Dupressoir, Francois, Gordon, Andrew D., Jürjens, Jan, Naumann, David A..
Guiding a General-Purpose C Verifier to Prove
Cryptographic Protocols.
Proceedings of the 2011 IEEE 24th Computer Security
Foundations Symposium (CSF),
páginas 3--17,
IEEE Computer Society,
2011.
- T. Trigo, P. Lopez-Garcia, S. Muñoz-Hernandez.
Towards Fuzzy Granularity Control in Parallel/Distributed Computing.
International Conference on Fuzzy Computation (ICFC 2010),
páginas 43--55,
SciTePress,
Octubre
2010.
- P. Lopez-Garcia, L. Darmawan, F. Bueno.
A Framework for Verification and Debugging of Resource Usage Properties: Resource Usage Verification.
Technical Communications of the 26th Int'l.
Conference on Logic Programming (ICLP'10),
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 7,
páginas 104--113,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
Julio
2010.
- Julien Bertrane, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, X. Rival.
Static Analysis and Verification of Aerospace Software by Abstract Interpretation.
AIAA InfotechAerospace 2010,
páginas 1--38,
American Institue of Aeronautics and Astronautics,
Abril
2010.
AIAA-2010-3385.
- Gilles Barthe, Pablo Buiras, César Kunz.
A Functional Framework for Result Checking.
Functional and Logic Programming, 10th International Symposium,
FLOPS 2010,
Lecture Notes in Computer Science,
Vol. 6009,
páginas 72--86,
Springer,
2010.
- Gilles Barthe, César Kunz.
Perspectives in Certificate Translation.
Trustworthly Global Computing - 5th International Symposium,
TGC 2010,
Lecture Notes in Computer Science,
Vol. 6084,
páginas 23--34,
Springer,
2010.
- Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech.
Computational Indistinguishability Logic.
Proceedings of the 17th ACM Conference on Computer and Communications
Security, CCS 2010,
páginas 375--386,
ACM,
2010.
- Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi.
Robustness Guarantees for Anonymity.
Proceedings of the 23rd IEEE Computer Security Foundations
Symposium, CSF 2010,
páginas 91--106,
IEEE Computer Society,
2010.
- Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte.
On the Equality of Probabilistic Terms.
Logic for Programming, Artificial Intelligence, and Reasoning
- 16th International Conference, LPAR-16,
Lecture Notes in Computer Science,
Vol. 6355,
Springer,
2010.
- Barthe, Gilles, Hedin, Daniel, Zanella Béguelin, Santiago, Gregoire, Benjamin, Heraud, Sylvain.
A Machine-Checked Formalization of Sigma-Protocols.
23rd IEEE Computer Security Foundations Symposium, CSF 2010,
páginas 246--260,
IEEE Computer Society,
2010.
- Barthe, Gilles, Grégoire, Benjamin, Zanella Béguelin, Santiago.
Programming Language Techniques for Cryptographic Proofs.
1st International Conference on Interactive Theorem Proving, ITP 2010,
Lecture Notes in Computer Science,
Vol. 6172,
páginas 115--130,
Springer,
2010.
- César Kunz.
Certificate Translation for the Verification of Concurrent
Programs.
Trustworthly Global Computing - 5th International Symposium,
TGC 2010,
Lecture Notes in Computer Science,
Vol. 6084,
páginas 237--252,
Springer,
2010.
- L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo.
Program Parallelization using Synchronized Pipelining.
Proceedings of the 19th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'09),
LNCS,
Núm. 6037,
páginas 173--187,
Springer,
2010.
- David A. Naumann, Anindya Banerjee.
Dynamic Boundaries: Information Hiding by Second Order
Framing with First Order Assertions.
ESOP,
páginas 2--22,
2010.
- Stan Rosenberg, Anindya Banerjee, David A. Naumann.
Local Reasoning and Dynamic Framing for the
Composite Pattern and Its Clients.
VSTTE,
páginas 183--198,
2010.
- Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jér^ome Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival.
Astrée: Proving the Absence of Runtime Errors.
Embedded Real Time Software and Systems - ERTSS 2010,
páginas 1--9,
2010.
- Patrick Cousot, Radhia Cousot, Laurent Mauborgne.
A Scalable Segmented Decision Tree Abstract Domain.
Pnueli Festschrift,
Lecture Notes in Computer Science,
Vol. 6200,
páginas 72--95,
Springer-Verlag,
2010.
- Umut A. Acar, Guy E. Blelloch, Ruy Ley-Wild, Kanat Tangwongsan, Duru Türkoglu.
Traceable data types for self-adjusting computation.
PLDI,
páginas 483--496,
2010.
- M. A. García de Dios, C. Dania, M. Schläpfer, D. Basin, M. Clavel, M. Egea.
SSG: a Model-Based Development Environment for Smart, Security-Aware
GUIs.
Proceedings of the 32nd ACM/IEEE International Conference
on Software Engineering - Volume 2, ICSE 2010, Cape Town,
South Africa, 1-8 May 2010,
páginas 311--312,
ACM,
2010.
- D. Basin, M. Clavel, M. Egea, M. Schläpfer.
Automatic Generation of Smart, Security-Aware GUI Models.
Engineering Secure Software and Systems, 2nd International
Symposium, ESSoS 2010, Pisa, Italy, February 3-4, 2010.
Proceedings,
Lecture Notes in Computer Science,
Vol. 5965,
páginas 201--217,
Springer,
2010.
- M. Egea, C. Dania, M. Clavel.
MySQL4OCL: A Stored Procedure-Based MySQL Code Generator for OCL.
Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010),
Electronic Communications of the EASST,
Vol. 36,
2010.
- Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
Structuring the verification of heap-manipulating programs.
Principles of Programming Languages (POPL),
páginas 261--274,
2010.
- Alexander Malkis, Andreas Podelski, Andrey Rybalchenko.
Thread-Modular Counterexample-Guided Abstraction Refinement.
Static Analysis - 17th International Symposium, SAS 2010,
Lecture Notes in Computer Science,
Vol. 6337,
páginas 356--372,
Springer,
2010.
- Moritz Y. Becker, Alexander Malkis, Laurent Bussard.
A Practical Generic Privacy Language.
Information Systems Security - 6th International Conference,
ICISS 2010,
Lecture Notes in Computer Science,
Vol. 6503,
páginas 125--139,
Springer,
2010.
- Pierre Ganty, Benjamin Monmege, Rupak Majumdar.
Bounded Underapproximations.
CAV'10: Proc. 20th Int. Conf. on Computer Aided Verification,
LNCS,
Vol. 6174,
páginas 600--614,
Springer,
2010.
- Boris Köpf, Geoffrey Smith.
Vulnerability Bounds and Leakage Resilience of Blinded Cryptography
under Timing Attacks.
Proc 23rd. IEEE Computer Security Foundations Symposium (CSF '10),
páginas 44--56,
IEEE,
2010.
- Boris Köpf, Andrey Rybalchenko.
Approximation and Randomization for Quantitative Information-Flow
Analysis.
Proc. 23rd IEEE Computer Security Foundations Symposium (CSF '10),
páginas 3--14,
IEEE,
2010.
- Michael Backes, Goran Doychev, Markus Dürmuth, Boris Köpf.
Speaker Recognition in Encrypted Voice Streams.
Proc. 15th European Symposium on Research in Computer Security (ESORICS '10),
LNCS 6345,
páginas 508--523,
Springer,
2010.
- Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur.
Shape Analysis with Reference Set Relations.
VMCAI,
2010.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Automatic Fragment Identification in Workflows
Based on Sharing Analysis.
Service-Oriented Computing -- ICSOC 2010,
LNCS,
Vol. 6470,
páginas 350--364,
Springer Verlag,
2010.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Towards Data-Aware QoS-Driven Adaptation for
Service Orchestrations.
Proceedings of the 2010 IEEE International
Conference on Web Services (ICWS 2010), Miami, FL,
USA, 5-10 July 2010,
páginas 107--114,
IEEE,
2010.
- Martin Leucker, César Sánchez.
Regular Linear-Time Temporal Logic.
Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10),
páginas 3--5,
IEEE Computer Society,
2010.
- César Sánchez, Martin Leucker.
Regular Linear Temporal Logic with Past.
Proc. of the 11th Int'l Conf. on Verification, Model
Checking, and Abstract Interpretation, (VMCAI'10),
LNCS,
Vol. 5944,
páginas 295--311,
Springer,
2010.
- Krishnendu Chatterjee, Luca de Alfaro, Vishwanath Raman, César Sánchez.
Analyzing the Impact of Change in Multi-threaded Programs.
Proc. of the 13th Int'l Conf. on Fundamental Approaches to Software Engineering (FASE'10),
LNCS,
Vol. 6013,
páginas 293--307,
Springer,
2010.
- Alejandro Sánchez, César Sánchez.
Decision Procedures for the Temporal Verification of Concurrent Lists.
Proc. of the 12th Int'l Conf. on Formal Engineering Methods (ICFEM'10),
LNCS,
Vol. 6447,
páginas 74--89,
Springer,
2010.
- Gourinath Banda, John P. Gallagher.
Constraint-Based Abstract Semantics for Temporal Logic:
A Direct Approach to Design and Implementation.
Logic for Programming, Artificial Intelligence, and Reasoning
- 16th International Conference, LPAR-16, Dakar, Senegal,
April 25-May 1, 2010, Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 6355,
páginas 27--45,
Springer,
2010.
- A. Herranz, J. Mariño, M. Carro, J.J. Moreno-Navarro.
Modeling Concurrent Systems with Shared Resources.
14th International Workshop on Formal Methods for Industrial
Critical Systems,
Lecture Notes in Computer Science,
Vol. 5825,
páginas 102--116,
Noviembre
2009.
- G. Marpons, J. Mariño, M. Carro, A. Herranz, L.Å. Fredlund, J.J. Moreno-Navarro, A. Polo.
A Coding Rule Conformance Checker Integrated into GCC.
Spanish Conference on Programming and Computer Languages (PROLE'09),
ENTCS,
Vol. 258,
páginas 149--159,
Elsevier,
Agosto
2009.
- E. Mera, P. Lopez-Garcia, M. V. Hermenegildo.
Integrating Software Testing and Run-Time
Checking in an Assertion Verification Framework.
25th Int'l. Conference on Logic Programming (ICLP'09),
LNCS,
Vol. 5649,
páginas 281--295,
Springer-Verlag,
Julio
2009.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
A Tabling Implementation Based on
Variables with Multiple Bindings.
International Conference on Logic Programming (ICLP 2009),
LNCS,
Núm. 5649,
páginas 190--204,
Springer-Verlag,
Julio
2009.
- V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee.
Merlin: specification inference for explicit information
flow problems.
PLDI,
páginas 75--86,
Junio
2009.
- Mark Marron, Deepak Kapur, Manuel Hermenegildo.
Identification of Logically Related Heap
Regions.
ISMM'09: Proceedings of the 8th international symposium
on Memory management,
ACM Press,
Junio
2009.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
Towards a Complete Scheme for Tabled Execution
Based on Program Transformation.
11th International Symposium on Practical Aspects of
Declarative Languages (PADL'09),
LNCS,
Núm. 5418,
páginas 224--238,
Springer-Verlag,
Enero
2009.
- Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet.
Implementing a Direct Method for Certificate Translation.
Formal Methods and Software Engineering, 11th International
Conference on Formal Engineering Methods, ICFEM 2009,
Lecture Notes in Computer Science,
Vol. 5885,
páginas 541--560,
Springer,
2009.
- Barthe, G., Grégoire, B., Zanella Béguelin, S..
Formal Certification of Code-Based Cryptographic Proofs.
36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009,
páginas 90--101,
ACM,
2009.
- Zanella Béguelin, S., Grégoire, B., Barthe, G., Olmedo, F..
Formally Certifying the Security of Digital Signature Schemes.
30th IEEE Symposium on Security and Privacy, S&P 2009,
páginas 237--250,
IEEE Computer Society,
2009.
- Avraham Shinnar, Marco Pistoia, Anindya Banerjee.
A language for information flow: dynamic tracking in multiple
interdependent dimensions.
PLAS,
páginas 125--131,
2009.
- M. Clavel, M. Egea, M. A. García de Dios.
Checking Unsatisfiability for OCL Constraints.
Proceedings of the Workshop "The Pragmatics of OCL and
Other Textual Specification Languages" at MoDELS 2009,
Electronic Communications of the EASST,
Vol. 24,
2009.
- M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. L. Talcott.
Unification and Narrowing in Maude 2.4.
Rewriting Techniques and Applications, 20th International
Conference, RTA 2009, Brasília, Brazil, June 29 -
July 1, 2009, Proceedings,
Lecture Notes in Computer Science,
Vol. 5595,
páginas 380--390,
Springer,
2009.
- Vlad Rusu, Manuel Clavel.
Vérification d'invariants pour des syst`emes
spécifiés en logique de réécriture.
Vingti`emes Journées Francophones
des Langages Applicatifs (JFLA 2009),
Studia Informatica Universalis,
Vol. 7.2,
páginas 317--350,
2009.
- Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko.
Verifying Liveness for Asynchronous Programs.
POPL '09: Proc. 36th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages,
páginas 102--113,
ACM Press,
2009.
- Pierre Ganty, Nicolas Maquet, Jean-Francois Raskin.
Fixpoint Guided Abstraction Refinement for Alternating Automata.
CIAA '09: Proc. 14th Int. Conf. on Implementation and Application of Automata,
LNCS,
Vol. 5642,
Springer,
2009.
- Pierre Ganty, Rupak Majumdar.
Analyzing Real-time Event-driven Programs.
FORMATS '09: Proc. 7th Int. Conf. on Formal Modelling and Analysis of Timed Systems,
LNCS,
Vol. 5813,
páginas 164--178,
Springer,
2009.
- Gourinath Banda, John P. Gallagher.
Constraint-Based Abstraction of a Model Checker for Infinite State Systems.
Proceedings of the 23rd Workshop on (Constraint) Logic Programming,
University of Potsdam (Publikationsserver der Universität Potsdam),
2009.
- Henning Christiansen, John P. Gallagher.
Non-discriminating Arguments and Their Uses.
Logic Programming, 25th International Conference, ICLP 2009,
Pasadena, CA, USA, July 14-17, 2009. Proceedings,
Lecture Notes in Computer Science,
Vol. 5649,
páginas 55--69,
Springer,
2009.
- E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo.
Negative Ternary Set-Sharing.
International Conference on Logic Programming, ICLP,
LNCS,
Núm. 5366,
páginas 301--316,
Springer-Verlag,
Diciembre
2008.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
A Sketch of a Complete Scheme for Tabled
Execution Based on Program Transformation.
Int'l. Conference on Logic Programming,
LNCS,
Vol. 5366,
páginas 795--800,
Springer Verlag,
Diciembre
2008.
Short paper.
- A. Casas, M. Carro, M. V. Hermenegildo.
A High-Level Implementation of
Non-Deterministic, Unrestricted, Independent
And-Parallelism.
24th International Conference on Logic Programming
(ICLP'08),
LNCS,
Vol. 5366,
páginas 651--666,
Springer-Verlag,
Diciembre
2008.
- Mark Marron, Mario Méndez-Lojo, Manuel Hermenegildo
and Darko Stefanovic, Deepak Kapur.
Sharing Analysis of Arrays, Collections, and
Recursive Structures.
ACM WS on Program Analysis for Software Tools and
Engineering (PASTE'08),
ACM,
Noviembre
2008.
- Iván Pérez, Ángel Herranz, Susana Muñoz, Juan José
Moreno-Navarro.
Modelling Mash-Up Resources.
13th Conference on Software Engineering and
Databases, JISBD'08,
páginas 135--146,
Octubre
2008.
- Mark Marron, Darko Stefanovic, Deepak Kapur, Manuel
Hermenegildo.
Identification of Heap-Carried Data Dependence
Via Explicit Store Heap Models.
21st Int'l. WS on Languages and Compilers for
Parallel Computing (LCPC'08),
LNCS,
Springer-Verlag,
Agosto
2008.
- J. Morales, M. Carro, M. V. Hermenegildo.
Comparing Tag Scheme Variations Using an
Abstract Machine Generator.
10th Int'l. ACM SIGPLAN Symposium on Principles and
Practice of Declarative Programming (PPDP'08),
páginas 32--43,
ACM Press,
Julio
2008.
- E. Mera, P. Lopez-Garcia, M. Carro, M. V. Hermenegildo.
Towards Execution Time Estimation in
Abstract Machine-Based Languages.
10th Int'l. ACM SIGPLAN Symposium on Principles and
Practice of Declarative Programming (PPDP'08),
páginas 174--184,
ACM Press,
Julio
2008.
- Mark Marron, Manuel Hermenegildo, Darko Stefanovic, Deepak Kapur.
Efficient Context-Sensitive Shape Analysis with Graph-Based
Heap Models.
International Conference on Compiler Construction (CC
2008),
Lecture Notes in Computer Science,
15 páginas,
Springer,
Abril
2008.
- M. Méndez-Lojo, M. Hermenegildo.
Precise Set Sharing Analysis
for Java-style Programs.
9th International Conference on Verification, Model
Checking and Abstract Interpretation (VMCAI'08),
LNCS,
Núm. 4905,
páginas 172--187,
Springer-Verlag,
Enero
2008.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, Claudio Silva, Ricardo Rocha.
An Improved Continuation Call-Based
Implementation of Tabling.
10th International Symposium on Practical Aspects of
Declarative Languages (PADL'08),
LNCS,
Vol. 4902,
páginas 198--213,
Springer-Verlag,
Enero
2008.
- G. Marpons, J. Mariño, M. Carro, A. Herranz, J.J. Moreno-Navarro, L.Å. Fredlund.
Automatic Coding Rule Conformance Checking Using Logic
Programming.
10th International Symposium on Practical Aspects of
Declarative Languages (PADL'08),
LNCS,
Vol. 4902,
páginas 18--34,
Springer Verlag,
Enero
2008.
- A. Casas, M. Carro, M. V. Hermenegildo.
Towards a High-Level Implementation of Execution
Primitives for Unrestricted, Independent
And-parallelism.
10th International Symposium on Practical Aspects of
Declarative Languages (PADL'08),
LNCS,
Vol. 4902,
páginas 230--247,
Springer-Verlag,
Enero
2008.
- P. Pietrzak, J. Correas, G. Puebla, M. V. Hermenegildo.
A Practical Type Analysis for Verification of
Modular Prolog Programs.
ACM SIGPLAN 2008 Workshop on Partial Evaluation and
Program Manipulation (PEPM'08),
páginas 61--70,
ACM Press,
Enero
2008.
- Gilles Barthe, César Kunz, Jorge Luis Sacchini.
Certified Reasoning in Memory Hierarchies.
Programming Languages and Systems, 6th Asian Symposium,
APLAS 2008,
Lecture Notes in Computer Science,
Vol. 5356,
páginas 75--90,
Springer,
2008.
- Gilles Barthe, César Kunz.
Certificate Translation in Abstract Interpretation.
17th European Symposium
on Programming, ESOP 2008,
Lecture Notes in Computer Science,
Vol. 4960,
páginas 368--382,
Springer,
2008.
- Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese.
Preservation of Proof Obligations for Hybrid Verification
Methods.
Sixth IEEE International Conference on Software Engineering
and Formal Methods, SEFM 2008,
páginas 127--136,
IEEE Computer Society,
2008.
- Gilles Barthe, Salvador Cavadini, Tamara Rezk.
Tractable Enforcement of Declassification Policies.
Proceedings of the 21st IEEE Computer Security Foundations
Symposium, CSF 2008,
páginas 83--97,
IEEE Computer Society,
2008.
- Gilles Barthe, Benjamin Grégoire, Colin Riba.
Type-Based Termination with Sized Products.
Computer Science Logic, 22nd International Workshop, CSL 2008,
Lecture Notes in Computer Science,
Vol. 5213,
páginas 493--507,
Springer,
2008.
- Gilles Barthe, Benjamin Grégoire, Mariela Pavlova.
Preservation of Proof Obligations from Java to the Java
Virtual Machine.
Automated Reasoning, 4th International Joint Conference,
IJCAR 2008,
Lecture Notes in Computer Science,
Vol. 5195,
páginas 83--99,
Springer,
2008.
- M. Clavel, V. Silva, C. Braga, M. Egea.
Model-Driven Security in Practice: An Industrial Experience.
Proceedings of Model Driven Architecture - Industrial Track ECMDA-FA '08,
Lecture Notes in Computer Science,
Vol. 5095,
páginas 327--338,
Springer-Verlag,
2008.
- M. Clavel, M. Egea, M. A. García de Dios.
ECEASST Building an Efficient Component for OCL Evaluation.
Proceedings of the 8th International Workshop on OCL Concepts and Tools (OCL 2008)
at MoDELS 2008,
Electronic Communications of the EASST,
Vol. 15,
2008.
- Tom Schrijvers, Maurice Bruynooghe, John P. Gallagher.
From Monomorphic to Polymorphic Well-Typings and Beyond.
Logic-Based Program Synthesis and Transformation, 18th International
Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008,
Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 5438,
páginas 152--167,
Springer,
2008.
- Gourinath Banda, John P. Gallagher.
Analysis of Linear Hybrid Systems in CLP.
Logic-Based Program Synthesis and Transformation, 18th International
Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008,
Revised Selected Papers,
Lecture Notes in Computer Science,
páginas 55--70,
Springer,
2008.
- John P. Gallagher, Mads Rosendahl.
Approximating Term Rewriting Systems: A Horn Clause Specification
and Its Implementation.
Logic for Programming, Artificial Intelligence, and Reasoning,
15th International Conference, LPAR 2008, Doha, Qatar, November
22-27, 2008. Proceedings,
Lecture Notes in Computer Science,
Vol. 5330,
páginas 682--696,
Springer,
2008.
- J. Navas, E. Mera, P. Lopez-Garcia, M. Hermenegildo.
User-Definable Resource Bounds Analysis
for Logic Programs.
23rd International Conference on Logic Programming
(ICLP'07),
Lecture Notes in Computer Science,
Vol. 4670,
páginas 348--363,
Springer,
Septiembre
2007.
10-year Test of Time Award.
- P. Pietrzak, M. V. Hermenegildo.
Automatic Binding-related Error Diagnosis in Logic
Programs.
International Conference on Logic Programming
(ICLP'07),
LNCS,
Núm. 4670,
páginas 333--347,
Springer-Verlag,
Septiembre
2007.
- M. Méndez-Lojo, J. Navas, M. Hermenegildo.
A Flexible (C)LP-Based Approach to the
Analysis of Object-Oriented Programs.
17th International Symposium on Logic-based Program Synthesis
and Transformation (LOPSTR 2007),
Lecture Notes in Computer Science,
Núm. 4915,
páginas 154--168,
Springer-Verlag,
Agosto
2007.
- A. Casas, M. Carro, M. V. Hermenegildo.
Annotation Algorithms for Unrestricted Independent
And-Parallelism in Logic Programs.
17th International Symposium on Logic-based Program
Synthesis and Transformation (LOPSTR'07),
LNCS,
Núm. 4915,
páginas 138--153,
Springer-Verlag,
Agosto
2007.
- J.F. Morales, M. Carro, M. V. Hermenegildo.
Towards Description and Optimization of Abstract
Machines in an Extension of Prolog.
Logic-Based Program Synthesis and
Transformation (LOPSTR'06),
LNCS,
Núm. 4407,
páginas 77--93,
Julio
2007.
- Mark Marron, Darko Stefanovic, Manuel Hermenegildo, Deepak Kapur.
Heap Analysis in the Presence of Collection
Libraries.
ACM WS on Program Analysis for Software Tools and
Engineering (PASTE'07),
ACM,
Junio
2007.
- M. Marron, D. Stefanovic, M. Hermenegildo, D. Kapur.
Heap Analysis in the Presence of Collection
Libraries.
ACM WS on Program Analysis for Software Tools and
Engineering (PASTE'07),
ACM,
Junio
2007.
- E. Mera, P. Lopez-Garcia, G. Puebla, M. Carro, M. Hermenegildo.
Combining Static Analysis and Profiling for
Estimating Execution Times.
Ninth International Symposium on Practical Aspects of
Declarative Languages (PADL'07),
LNCS,
Núm. 4354,
páginas 140--154,
Springer-Verlag,
Enero
2007.
- D. Basin, M. Clavel, J. Doser, M. Egea.
A Metamodel-Based Approach for Analyzing Security-Design
Models.
Proceedings of the Tenth International Conference on
Model Driven Engineering Languages and Systems, MODELS '07,
Lecture Notes in Computer Science,
Vol. 4735,
páginas 420--435,
Springer-Verlag,
2007.
- M. Clavel, F. Durán, J. Hendrix, S. Lucas, J. Meseguer, P. C. Ölveczky.
The Maude Formal Tool Environment.
Algebra and Coalgebra in Computer Science, 2nd International
Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007,
Proceedings,
Lecture Notes in Computer Science,
Vol. 4624,
páginas 173--178,
Springer,
2007.
Libros y Monografías
- Manuel V. Hermenegildo, Pedro Lopez-Garcia, Alberto Pettorossi, Maurizio Proietti (Eds.).
Fundamenta Informaticae, Special Issue on the 26th International
Symposium on Logic-Based Program Synthesis
and Transformation: LOPSTR 2016.
Vol. 177,
Núm. 3--4,
IOS Press,
Diciembre
2020.
- Alexey Gotsman, Ana Sokolova (Eds.).
Proc. of Formal Techniques for Distributed Objects, Components, and Systems
- 40th IFIP WG 6.1 International Conference, FORTE 2020, Held
as Part of the 15th International Federated Conference on Distributed
Computing Techniques, DisCoTec 2020.
Lecture Notes in Computer Science,
Vol. 12136,
Springer,
Junio
2020.
- Pierre Ganty, Mohamed Ka^aniche (Eds.).
Verification and Evaluation of Computer and Communication Systems
- 13th International Conference, VECoS 2019, Proceedings.
Lecture Notes in Computer Science,
Vol. 11847,
Springer,
Octubre
2019.
- Alessandra Gorla, José Miguel Rojas (Eds.).
Proceedings of the 12th International Workshop on
Search-Based Software Testing, SBST-ICSE 2019.
IEEE / ACM,
2019.
- Umer Liqat.
A Multi-Language and Multi-Platform Framework for Resource
Consumption Analysis and its Application to
Energy-Efficient Software Development.
Tesis Doctoral, Escuela Técnica Superior de Ingenieros Informáticos, UPM,
Julio
2018.
- Nataliia Stulova.
Improving Run-time Checking in Dynamic Programming Languages.
Tesis Doctoral, Escuela Técnica Superior de Ingenieros Informáticos, UPM,
Mayo
2018.
- Gilles Barthe, Geoff Sutcliffe, Margus Veanes (Eds.).
LPAR-22. 22nd International Conference on Logic for Programming,
Artificial Intelligence and Reasoning.
EPiC Series in Computing,
Vol. 57,
EasyChair,
2018.
- Alessandra Gorla, Juan Pablo Galeotti (Eds.).
Proceedings of the 11th International Workshop on Search-Based Software
Testing, ICSE 2018.
ACM,
2018.
- John P. Gallagher, Martin Sulzmann (Eds.).
Functional and Logic Programming - 14th International Symposium, FLOPS
2018, Nagoya, Japan, May 9-11, 2018, Proceedings.
Lecture Notes in Computer Science,
Vol. 10818,
Springer,
2018.
- John P. Gallagher, Fabio Fioravanti (Eds.).
Logic-Based Program Synthesis and Transformation - 27th International
Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised
Selected Papers.
Lecture Notes in Computer Science,
Vol. 10855,
Springer,
2018.
- John P. Gallagher, Rob van Glabbeek, Wendelin Serwe (Eds.).
Proceedings Third Workshop on Models for Formal Analysis of Real Systems
and Sixth International Workshop on Verification and Program Transformation,
MARS/VPT-ETAPS 2018, and Sixth International Workshop on Verification
and Program Transformation Thessaloniki, Greece, 20th April 2018.
EPTCS,
Vol. 268,
2018.
- M. V. Hermenegildo, P. Lopez-Garcia (Eds.).
Logic-Based Program Synthesis and Transformation - 26th International
Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8,
2016, Revised Selected Papers.
Lecture Notes in Computer Science,
Núm. 10184,
330 páginas,
Springer,
Julio
2017.
- Giorgos Fagas, Luca Gammaitoni, John P. Gallagher, Douglas J. Paul (Eds.).
ICT: Energy Concepts for Energy Efficiency and Sustainability.
248 páginas,
InTech Open Access Publishers,
Marzo
2017.
- Srdjan Matic.
Active Techniques for Revealing and Analyzing the Security of Hidden Servers.
Tesis Doctoral, Universita degli Studi di Milano,
Milano, Italy,
Febrero
2017.
(available online).
- Miriam García Soto.
An Algorithmic Approach for Stability Verification of Hybrid Systems.
Tesis Doctoral, School of Computer Science, UPM,
Núm. 10.20868/UPM.thesis.47805,
2017.
- Manuel Carro, Andy King (Eds.).
32nd International Conference on Logic Programming.
Vol. 16,
Núm. 5-6,
Cambridge University Press,
Septiembre
2016.
- Manuel Carro, Salvador Tamarit, Guillermo Vigueras, Julio Mariño (Eds.).
Proceedings of the First Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016).
Marzo
2016.
- A. Zaks, M. V. Hermenegildo.
Proceedings of the 25th International Conference on Compiler Construction (CC 2016).
ACM,
Marzo
2016.
- Gilles Barthe, Evangelos P. Markatos, Pierangela Samarati (Eds.).
Security and Trust Management - 12th International Workshop, STM
2016, Heraklion, Crete, Greece, September 26-27, 2016, Proceedings.
Lecture Notes in Computer Science,
Vol. 9871,
Springer,
2016.
- Pierre Ganty, Michele Loreti (Eds.).
Trustworthy Global Computing - 10th International Symposium, TGC
2015, Madrid, Spain, August 31 - September 1, 2015,
Revised Selected Papers.
Lecture Notes in Computer Science,
Vol. 9533,
Springer,
2016.
- Manuel Carro, Andy King, Neda Saeedloei, Marina De Vos (Eds.).
Technical Communications of the 32nd International Conference on Logic
Programming.
OASICS,
Vol. 52,
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
2016.
- Juan Caballero, Eric Bodden, Elias Athanasopoulos.
Engineering Secure Software and Systems - 8th International
Symposium, ESSoS 2016. Proceedings.
Lecture Notes in Computer Science,
Vol. 9639,
Springer,
2016.
- John P. Gallagher, Philipp Rümmer (Eds.).
Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis,
HCVS (satellite event of ETAPS), Eindhoven, The Netherlands, 3rd April 2016.
EPTCS,
Vol. 219,
2016.
- Alejandro Sánchez.
Formal Verification of Temporal Properties for Parametrized
Concurrent Programs and Concurrent Data Structures.
Tesis Doctoral, ETS de Ingenieros Informáticos, Technical University of
Madrid,
Septiembre
2015.
- Joaquín Arias.
Design and implementation of a modular interface to
integrate CLP and tabled execution.
Tesis de Licenciatura, ETSI Ing. Informatica,
Julio
2015.
- Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, Annabelle McIver.
Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar
15181).
Dagstuhl Reports,
Vol. 5,
Núm. 4,
páginas 123--141,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
2015.
- Frank Piessens, Juan Caballero, Nataliia Bielova.
Engineering Secure Software and Systems - 7th International
Symposium, ESSoS 2015, Milan, Italy, March, 4-6, 2015. Proceedings.
Lecture Notes in Computer Science,
Vol. 8978,
Springer,
2015.
- Álvaro García-Pérez.
Operational aspects of full-reduction in lambda calculi.
Tesis Doctoral, Facultad de Informática, Universidad Politécnica de Madrid,
Septiembre
2014.
Advisors: Juan José Moreno Navarro and Pablo Nogueira.
- R. Haemmerlé, J. Sneyers.
Proceedings of the Eleventh Workshop on Constraint
Handling Rules (CHR 2014).
CoRR abs/1406.1510,
2014.
- Juan Caballero, Simson Garfinkel.
Fourteenth Annual DFRWS Conference.
Vol. 11, Supplement 2,
Núm. 0,
páginas 1--2,
2014.
The Proceedings of the 14th Annual Digital Forensics Research Conference.
- Nataliia Stulova.
Dynamic Checking of Assertions for Higher-order
Predicates.
Tesis de Licenciatura, Technical University of Madrid, School of Computer
Science,
E-28660, Boadilla del Monte, Madrid, Spain,
73 páginas,
Julio
2013.
- Dragan Ivanovic.
Analysis of Service-Oriented Computing Systems.
Tesis Doctoral, School of Computer Science, UPM,
Enero
2013.
- R. Haemmerlé, J.F. Morales.
Proceedings of the 23rd Workshop on Logic-based methods
in Programming Environments (WLPE 2013).
CoRR abs/1308.2055,
2013.
- Clay Shields, Juan Caballero.
Thirteenth Annual DFRWS Conference.
Vol. 10, Supplement,
Núm. 0,
páginas 1--2,
2013.
The Proceedings of the 13th Annual Digital Forensics Research Conference.
- Javier Valdazo.
Developing Secure Business Applications from Secure BPMN Models.
Tesis de Licenciatura, Universidad Complutense de Madrid, Spain,
Septiembre
2012.
- Gilles Barthe, Benjamin Livshits, Riccardo Scandariato.
Engineering Secure Software and Systems - 4th International
Symposium, ESSoS 2012, Eindhoven, The Netherlands, February,
16-17, 2012. Proceedings.
Lecture Notes in Computer Science,
Vol. 7159,
Springer,
2012.
- Gilles Barthe, Anupam Datta, Sandro Etalle.
Formal Aspects of Security and Trust - 8th International
Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011.
Revised Selected Papers.
Lecture Notes in Computer Science,
Vol. 7140,
Springer,
2012.
- Gilles Barthe, Alberto Pardo, Gerardo Schneider.
Software Engineering and Formal Methods - 9th International
Conference, SEFM 2011.
Lecture Notes in Computer Science,
Vol. 7041,
Springer,
Noviembre
2011.
- Julián Samborski-Forlese.
Two Algorithms for Model Checking of Regular Linear Temporal Logic.
Tesis de Licenciatura, Dpto. Sistemas Informáticos y Computación, Universidad Complutense de Madrid,
Septiembre
2011.
- Alejandro Sánchez.
Decision Procedures for the Temporal Verification
of Concurrent Data Structures.
Tesis de Licenciatura, Dpto. Sistemas Informáticos y Computación, Universidad
Complutense de Madrid,
Julio
2011.
- John P. Gallagher, Michael Gelfond.
Theory and Practice of Logic Programming.
27th Int'l. Conference on Logic Programming
(ICLP'11) Special Issue.
Vol. 11 (4--5),
páginas 429--839,
Cambridge University Press,
Julio
2011.
- John P. Gallagher, Michael Gelfond.
Technical Communications of the 27th International Conference
on Logic Programming (ICLP'11).
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 11,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
Julio
2011.
- M. Carro, D. Karastoyanova, G. A. Lewis, A. Liu.
Third International Workshop on Principles of Enginering Service-Oriented Systems (PESOS 2011).
ACM,
Mayo
2011.
- Gilles Barthe.
Programming Languages and Systems - 20th European Symposium
on Programming, ESOP 2011, held as part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2011.
Lecture Notes in Computer Science,
Vol. 6602,
Springer,
Marzo
2011.
- M. Carro, J.H. Reppy.
ACM SIGPLAN Proceedings of the Workshop on Declarative Aspects of Multicore Programming.
ACM,
Enero
2011.
- Jorge Cuéllar, Javier Lopez, Gilles Barthe, Alexander Pretschner.
Security and Trust Management - 6th International Workshop,
STM 2010, Athens, Greece, September 23-24, 2010, Revised
Selected Papers.
Lecture Notes in Computer Science,
Vol. 6710,
Springer,
2011.
- M. V. Hermenegildo, T. Schaub.
Theory and Practice of Logic Programming.
26th Int'l. Conference on Logic Programming
(ICLP'10) Special Issue.
Vol. 10 (4--6),
páginas 361--778,
Cambridge University Press,
Julio
2010.
- M. V. Hermenegildo, T. Schaub.
Technical Communications of the 26th Int'l.
Conference on Logic Programming (ICLP'10).
Leibniz International Proceedings in
Informatics (LIPIcs),
Vol. 7,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
Julio
2010.
- J.F. Morales.
Advanced Compilation Techniques for Logic Programming.
Tesis Doctoral, Universidad Politécnica de Madrid (UPM),
Facultad Informática UPM, 28660-Boadilla del Monte,
Madrid-Spain,
Julio
2010.
- G. Barthe, M. Hermenegildo.
Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010.
LNCS,
Núm. 5944,
Springer,
Enero
2010.
- M. V. Hermenegildo, J. Palsberg.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages (POPL 2010).
ACM,
Enero
2010.
- Rafael Caballero, John P. Gallagher.
Proceedings of the 19th Workshop on Logic-based methods
in Programming Environments (WLPE 2009).
CoRR, abs/1002.4535,
2010.
- John P. Gallagher, Janis Voigtländer.
Proceedings of the 2010 ACM SIGPLAN Workshop on Partial
Evaluation and Program Manipulation, PEPM 2010, Madrid,
Spain, January 18-19, 2010.
ACM,
2010.
- Álvaro García-Pérez.
Exploring the beta-hypercube.
Tesis de Licenciatura, Facultad de Informática, Universidad Politécnica de Madrid,
Septiembre
2009.
Advisor: Pablo Nogueira.
- Alessandro Aldini, Gilles Barthe, Roberto Gorrieri.
Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009
Tutorial Lectures.
Lecture Notes in Computer Science,
Vol. 5705,
Springer,
2009.
- Anindya Banerjee.
FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs.
ACM,
2009.
- Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary Leavens, Peter Müller, Tobias Wrigstad.
Formal Techniques for Java-Like Programs.
Lecture Notes in Computer Science,
Vol. 5475,
páginas 70--76,
Springer Berlin / Heidelberg,
2009.
- J. Garrigue, M. V. Hermenegildo.
Functional and Logic Programming, 9th International
Symposium, FLOPS'08.
LNCS,
Núm. 4989,
Springer,
Abril
2008.
- M. V. Hermenegildo.
ACM SIGPLAN-Intel Workshop on Declarative Aspects of
Multicore Programming, DAMP'08, Informal Proceedings.
Enero
2008.
- Gilles Barthe, Frank S. de Boer.
Formal Methods for Open Object-Based Distributed Systems,
10th IFIP WG 6.1 International Conference, FMOODS 2008,
Oslo, Norway, June 4-6, 2008, Proceedings.
Lecture Notes in Computer Science,
Vol. 5051,
Springer,
2008.
- Gilles Barthe, Cédric Fournet.
Trustworthy Global Computing, Third Symposium, TGC 2007,
Sophia-Antipolis, France, November 5-6, 2007, Revised Selected
Papers.
Lecture Notes in Computer Science,
Vol. 4912,
Springer,
2008.
- M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C. L. Talcott.
All About Maude - A High-Performance Logical Framework,
How to Specify, Program and Verify Systems in Rewriting
Logic.
Lecture Notes in Computer Science,
Vol. 4350,
Springer,
2007.
Artíulos Invitados y Tutoriales
- Manuel V. Hermenegildo, Pedro Lopez-Garcia, Alberto Pettorossi, Maurizio Proietti.
Preface, Fundamenta Informaticae, Special Issue on the 26th International
Symposium on Logic-Based Program Synthesis
and Transformation: LOPSTR 2016.
Vol. 177,
Núm. 3--4,
páginas 1--3,
IOS Press,
Diciembre
2020.
- V. Perez-Carrasco, M. Klemen, P. Lopez-Garcia, J.F. Morales, M. V. Hermenegildo.
Cost Analysis of Smart Contracts via Parametric Resource Analysis.
Proceedings of the 27th Static Analysis Symposium (SAS 2020),
LNCS,
Vol. 12389,
páginas 7--31,
Springer,
Noviembre
2020.
- J. Gallagher, M. V. Hermenegildo, B. Kafle, M. Klemen, P. Lopez-Garcia, J.F. Morales.
From big-step to small-step semantics and back with interpreter specialization (invited paper).
Proceedings of the Eighth International Workshop on Verification and Program Transformation
(VPT 2020),
Electronic Proceedings in Theoretical Computer Science (EPTCS),
páginas 50--65,
Open Publishing Association (OPA),
2020.
Co-located with ETAPS 2020.
- M. V. Hermenegildo, I. Garcia-Contreras, J. Morales, P. Lopez-Garcia, M. Klemen, I. Casso.
Multivariant Assertion-based Guidance of Top-down Horn Clause-based
Analysis in CiaoPP.
Workshop on Declarative Program Analysis (DPA 2019),
1 páginas,
Julio
2019.
(Abstract of invited talk). Associated to FCRC 2019.
- M. V. Hermenegildo, M. Carro, P. Lopez-Garcia, J.F. Morales, J. Arias, I. Garcia-Contreras, M. Klemen, N. Stulova.
25 Years of Ciao (abstract of invited tutorial).
Pre-proceedings of the 28th International Symposium on
Logic-based Program Synthesis and Transformation
(LOPSTR'18),
Septiembre
2018.
- M. V. Hermenegildo, P. Lopez-Garcia, J. Morales, I. Garcia-Contreras, M. Klemen, N. Stulova.
Horn Clause-based Program Analysis and Verification with CiaoPP.
1st International Workshop on Declarative Program Analysis (DPA 2018),
1 páginas,
Julio
2018.
(Abstract of invited talk). Associated to ECOOP/ISSTA 2018.
- Floriana Esposito, Carlo Ghezzi, Manuel V. Hermenegildo, Helene Kirchner, Luke Ong.
Informatics Research Evaluation.
12 páginas,
Informatics Europe,
Marzo
2018.
http://www.informatics-europe.org/news/436-research_evaluation.html.
- Alexey Gotsman.
Tutorial: Consistency Choices in Modern Distributed Systems.
Proc. of the 2018 ACM Symposium on Principles of Distributed Computing, PODC'18,
páginas 491--491,
ACM,
2018.
- M. V. Hermenegildo, P. Lopez-Garcia, U. Liqat, M. Klemen.
Energy Consumption Analysis and Verification by Transformantion into Horn Clauses and Abstract Interpretation.
5th International Workshop on Verification and Program Transformation (VPT 2017),
Vol. 253,
páginas 4--6,
EPTCS,
Abril
2017.
(Abstract of invited talk).
- Gilles Barthe, Francois Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub.
EasyCrypt: A Tutorial.
Foundations of Security Analysis and Design VII - FOSAD 2012/2013
Tutorial Lectures,
Lecture Notes in Computer Science,
Vol. 8604,
páginas 146--166,
Springer,
2013.
- M. V. Hermenegildo.
Conferences vs. Journals in CS, what to do?
Evolutionary ways forward and the ICLP/TPLP model.
Dagstuhl 12452: Publication Culture in Computing Research -- Position Papers,
Núm. 12452,
12 páginas,
IBFI -- Dagstuhl,
Noviembre
2012.
Slides: (available online).
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Constraint-Based Runtime Prediction of SLA
Violations in Service Orchestrations.
22nd Workshop on Logic-based Methods in Programming Environments,
1 páginas,
Septiembre
2012.
(abstract of invited talk).
- Aizatulin, Mihhail, Dupressoir, Francois, Gordon, Andrew D., Jürjens, Jan.
Verifying Cryptographic Code in C: Some Experience and
the Csec Challenge.
Formal Aspects of Security and Trust (FAST),
Lecture Notes in Computer Science,
Vol. 7140,
páginas 1--20,
Springer Berlin Heidelberg,
2012.
Invited Paper, also appears as tech. rep. MSR-TR-2011-118.
- John P. Gallagher.
Program Analysis With Regular Tree Languages.
Logic-Based Program Synthesis and Transformation - 21st
International Symposium, LOPSTR 2011, Odense, Denmark, July
18-20, 2011. Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 7225,
Springer,
2012.
Extended Abstract.
- M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, R. Haemmerlé, E. Mera, J. F. Morales, G. Puebla.
An Overview of the Ciao System.
Proc. of RuleML-Europe 2011,
LNCS,
Vol. 6826,
páginas 2--3,
Springer-Verlag,
Julio
2011.
(abstract of invited talk).
- John P. Gallagher, Michael Gelfond.
Introduction to the 27th International Conference on Logic
Programming (ICLP'11) Special Issue.
Vol. 11,
Núm. 4-5,
páginas 429--432,
Cambridge University Press,
Julio
2011.
- John P. Gallagher, Michael Gelfond.
Introduction to Technical Communications of the 27th
Int'l. Conference on Logic Programming (ICLP'11).
Technical Communications of the 27th International Conference on Logic Programming (ICLP'11),
Leibniz International Proceedings in Informatics (LIPIcs),
Vol. 11,
páginas 1--9,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
Julio
2011.
- M. V. Hermenegildo, T. Schaub.
Introduction to the 26th Int'l. Conference on
Logic Programming (ICLP'10) Special Issue.
Vol. 10,
Núm. 4--6,
páginas 361--364,
Cambridge University Press,
Julio
2010.
- M. V. Hermenegildo, T. Schaub.
Introduction to Technical Communications of the 26th
Int'l. Conference on Logic Programming (ICLP'10).
Technical Communications of the 26th Int'l.
Conference on Logic Programming (ICLP'10),
Leibniz International Proceedings in
Informatics (LIPIcs),
Vol. 7,
páginas 8--11,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
Julio
2010.
- Anindya Banerjee.
Semantics and Enforcement of Expressive Information Flow Policies.
Formal Aspects in Security and Trust,
Lecture Notes in Computer Science,
Vol. 5983,
páginas 1--3,
Springer Berlin / Heidelberg,
2010.
- Barthe, Gilles, Grégoire, Benjamin, Heraud, Sylvain, Zanella Béguelin, Santiago.
Formal Certification of ElGamal Encryption. A Gentle Introduction to CertiCrypt.
5th International workshop on Formal Aspects in Security and Trust, FAST 2008,
Lecture Notes in Computer Science,
Vol. 5491,
páginas 1--19,
Springer,
2009.
- Gilles Barthe.
Certificate Translation.
Proceedings of the 5th International Verification Workshop, VERIFY'08
in connection with IJCAR 2008,
CEUR Workshop Proceedings,
Vol. 372,
CEUR-WS.org,
2008.
- M. V. Hermenegildo, F. Bueno, A. Casas, J. Navas, E. Mera, M. Carro, P. Lopez-Garcia.
Automatic Granularity-Aware Parallelization of
Programs with Predicates, Functions, and
Constraints.
DAMP'07, ACM SIGPLAN Workshop on Declarative Aspects of
Multicore Programming,
páginas 1--1,
ACM,
Enero
2007.
(abstract of invited talk).
Artículos en Libros y Otras Colecciones
- Adrian Francalanza, Jorge A. Perez, César Sánchez.
Runtime Verification for Decentralized and Distributed Systems.
Lectures on Runtime Verification -- Introductory and Advanced Topics,
LNCS,
Vol. 10457,
páginas 169--205,
Springer,
2018.
- P. Lopez-Garcia, M. V. Hermenegildo, M. Klemen, U. Liqat.
Energy Consumption Analysis and Verification using CiaoPP.
The ALP Newsletter,
Vol. 30,
Núm. 3,
The Association for Logic Programming,
Septiembre
2017.
- Kerstin Eder, John P. Gallagher.
Energy-Aware Software Engineering.
ICT - Energy Concepts for Energy Efficiency and Sustainability,
páginas 103--127,
InTech Open Access Publishers,
Marzo
2017.
- Giorgos Fagas, John P. Gallagher, Luca Gammaitoni, Douglas J. Paul.
Energy Challenges for ICT.
ICT - Energy Concepts for Energy Efficiency and Sustainability,
InTech Open Access Publishers,
Marzo
2017.
- Alberto Goffi, Alessandra Gorla, Andrea
Mattavelli, Mauro Pezz`e.
Intrinsic Redundancy for Reliability and Beyond.
Present and Ulterior Software Engineering,
páginas 153--171,
Springer,
2017.
- Salvador Tamarit, Guillermo Vigueras, Manuel Carro, Julio Mariño.
Machine Learning-Driven Automatic Program Transformation to Increase
Performance in Heterogeneous Architectures.
Tools for High Performance Computing 2016,
Springer International Publishing,
2017.
- U. Liqat, K. Georgiou, S. Kerrison, P. Lopez-Garcia, M. V. Hermenegildo, J. P. Gallagher, K. Eder.
Inferring Parametric Energy Consumption Functions at Different
Software Levels: ISA vs. LLVM IR.
Foundational and Practical Aspects of Resource Analysis: 4th
International Workshop, FOPARA 2015, London, UK,
April 11, 2015. Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 9964,
páginas 81--100,
Springer,
2016.
- Luca Aceto, Álvaro García-Pérez, Anna Ingólfsdóttir.
Rule formats for bounded nondeterminism in structural operational
semantics.
Semantics, Logics and Calculi---Essays Dedicated to Hanne Riis Nielson
and Flemming Nielson on the Occasion of Their 60th Birthdays,
LNCS,
Vol. 9560,
páginas 313--343,
Springer,
2016.
- Konstantin Kuznetsov, Alessandra Gorla, Ilaria
Tavecchia, Florian Gross, Andreas Zeller.
Mining Android Apps for Anomalies.
The Art and Science of Analyzing Software Data,
páginas 257--284,
Morgan Kaufmann,
2015.
- Barthe, Gilles, Dupressoir, Francois, Grégoire, Benjamin, Schmidt, Benedikt, Strub, Pierre-Yves.
Computer-Aided Proofs in Cryptography: An Overview.
All about Proofs, Proofs for All (APPA),
Mathematical Logic and Foundations,
Vol. 55,
College Publications,
jan
2015.
- K. Georgiou, U. Liqat.
Towards LLVM-Based Energy Consumption Analysis of Programs.
ICT-Energy (Nanoenergy) Letters,
Núm. 8,
páginas 16--17,
Julio
2014.
- Miguel Ángel García de Dios, Carolina Dania, David A. Basin, Manuel Clavel.
Model-Driven Development of a Secure eHealth Application.
Engineering Secure Future Internet Services and Systems - Current
Research,
páginas 97--118,
2014.
- Kerstin Eder, Steve Kerrison, John Gallagher, Pedro Lopez-Garcia.
Whole Systems Energy Transparency.
Núm. 6,
páginas 67--68,
Agosto
2013.
- Dave Clarke, Johan Östlund, Ilya Sergey, Tobias Wrigstad.
Ownership Types: A Survey.
Aliasing in Object-Oriented Programming. Types, Analysis
and Verification,
LNCS,
Vol. 7850,
páginas 15--58,
Springer,
2013.
- Anindya Banerjee, David A. Naumann.
State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings.
Aliasing in Object-Oriented Programming,
Lecture Notes in Computer Science,
Vol. 7850,
páginas 319--365,
Springer,
2013.
- Barthe, Gilles, Dupressoir, Francois, Grégoire, Benjamin, Kunz, César, Schmidt, Benedikt, Strub, Pierre-Yves.
EasyCrypt: A Tutorial.
Foundations of Security Analysis and Design VII (FOSAD),
Lecture Notes in Computer Science,
Vol. 8604,
páginas 146--166,
Springer International Publishing,
2013.
- Juan Caballero, Adam Barth, Dawn Song.
Content-Sniffing XSS Attacks: XSS with non-HTML Content.
The Death of the Internet,
Wiley,
Julio
2012.
- T. Trigo, P. Lopez-Garcia, S. Muñoz-Hernandez.
A Fuzzy Approach to Resource Aware Automatic Parallelization.
Computational Intelligence,
Studies in Computational Intelligence (SCI),
Vol. 399,
páginas 229--245,
Springer Berlin Heidelberg,
2012.
- P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo.
Interval-Based Resource Usage Verification: Formalization and Prototype.
Foundational and Practical Aspects of Resource Analysis. Second International Workshop FOPARA 2011, Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 7177,
páginas 54--71,
Springer-Verlag,
2012.
- V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee.
Merlin: specification inference for explicit information
flow problems.
Mining Software Specifications,
páginas 377--410,
Chapman & Hall/CRC,
Mayo
2011.
- Patrick Cousot, Radhia Cousot, Laurent Mauborgne.
Logical Abstract Domains and Interpretations.
The Future of Software Engineering,
páginas 48--71,
Springer-Verlag,
2011.
- Manuel Clavel, Narciso Martí-Oliet, Miguel Palomino.
Parameterized Metareasoning in Membership Equational Logic.
Formal Modeling: Actors, Open Systems, Biological Systems
- Essays Dedicated to Carolyn Talcott on the Occasion of
Her 70th Birthday,
LNCS,
Vol. 7000,
páginas 277--298,
Springer,
2011.
- M. Carro, M. V. Hermenegildo.
Logic Languages.
Encyclopedia of Parallel Computing,
páginas 1057--1068,
Springer,
2011.
- M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, J.F. Morales, G. Puebla.
An Overview of The Ciao Multiparadigm Language
and Program Development Environment
and its Design Philosophy.
Festschrift for Ugo Montanari,
LNCS,
Vol. 5065,
páginas 209--237,
Springer-Verlag,
Junio
2008.
- Gilles Barthe, César Kunz.
An Introduction to Certificate Translation.
Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009
Tutorial Lectures,
Lecture Notes in Computer Science,
Vol. 5705,
páginas 51--95,
Springer,
2008.
- Gilles Barthe, Benjamin Grégoire, Colin Riba.
A Tutorial on Type-Based Termination.
Language Engineering and Rigorous Software Development,
International LerNet ALFA Summer School 2008,
Lecture Notes in Computer Science,
Vol. 5520,
páginas 100--152,
Springer,
2008.
- César Sánchez, Matteo Slanina, Henny B. Sipma, Zohar Manna.
The Reaction Algebra: A Formal Language for Event Correlation.
Pillars of Computer Science: Essays Dedicated to Boris
(Boaz) Trakhtenbrot on the Occasion of His 85th
Birthday,
LNCS,
Vol. 4800,
páginas 586--609,
Springer-Verlag,
2008.
- Ángel Herranz, Juan José Moreno-Navarro.
Modeling and Reasoning about Design Patterns in SLAM-SL.
Design Pattern Formalization Techniques,
IGI Publishing,
Marzo
2007.
Publicaciones en Workshops con Revisión
- Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro Lopez-Garcia, José F. Morales.
Regular Path Clauses and their Application in Solving
Loops.
Proceedings of the Eighth International Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021),
Electronic Proceedings in Theoretical Computer Science (EPTCS),
Vol. 344,
páginas 22--35,
Open Publishing Association (OPA),
Agosto
2021.
Co-located with ETAPS 2021.
- M. A. Sanchez-Ordaz, I. Garcia-Contreras, V. Perez-Carrasco, J. F. Morales, P. Lopez-Garcia, M. Hermenegildo.
VeriFly: On-the-fly Assertion Checking with CiaoPP.
6th Workshop on Formal Integrated Development Environment (F-IDE 2021),
Electronic Proceedings in Theoretical Computer Science (EPTCS),
páginas 1--5,
Open Publishing Association (OPA),
Mayo
2021.
Co-located with ETAPS 2021.
- I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
Incremental and Modular Context-sensitive Analysis.
Workshop on Horn Clauses for Verification and Synthesis (HCVS 2021),
Marzo
2021.
(Talk).
- Juan Francisco García, Daniel Jurjo, Fernando
Macías, José Francisco Morales, Alessandra
Gorla.
An application of KLEE to aerospace industrial
software.
2nd International KLEE Workshop on Symbolic Execution,
2021.
- Joaquín Arias, Gopal Gupta, Manuel Carro.
A Short Tutorial on s(CASP), a Goal-directed Execution of Constraint
Answer Set Programs.
Proceedings of the 37th ICLP 2021 Workshops,
Vol. 2970,
CEUR-WS.org,
2021.
- I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
Testing Your (Static Analysis) Truths.
Pre-proceedings of the 30th International Symposium on
Logic-based Program Synthesis and Transformation
(LOPSTR'20),
Septiembre
2020.
- Juan José Moreno-Navarro.
Industrial innovation and top ranked universities.
Academic Proceedings of the 2020 University-Industry Interaction Conference Series,
Junio
2020.
- Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
Justifications for Goal-Directed Constraint Answer Set Programming.
Proceedings 36th International Conference on
Logic Programming (Technical Communications),
EPTCS,
Vol. 325,
páginas 59--72,
Open Publishing Association,
2020.
- I. Casso, J. F. Morales, P. Lopez-Garcia, R. Giacobazzi, M. V. Hermenegildo.
Computing Abstract Distances in Logic Programs.
Pre-proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation
(LOPSTR'19),
Noviembre
2019.
- I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
An Integrated Approach to Assertion-Based Random Testing in Prolog.
Pre-proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation
(LOPSTR'19),
Noviembre
2019.
- M. Klemen, P. Lopez-Garcia, J. Gallagher, J.F. Morales, M. V. Hermenegildo.
A General Framework for Static Cost Analysis of Parallel Logic Programs.
Pre-proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation (LOPSTR'19),
Noviembre
2019.
- I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
Experiments in Context-Sensitive Incremental and Modular Static Analysis in CiaoPP.
10th Workshop on Tools for Automatic Program Analysis (TAPAS'19),
Octubre
2019.
(Extended Abstract).
- I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
Incremental Analysis of Logic Programs with Assertions and Open Predicates.
Pre-proceedings of the 29th International Symposium on
Logic-based Program Synthesis and Transformation (LOPSTR'19),
Octubre
2019.
- J. Arias, Z. Chen, M. Carro, G. Gupta.
Modeling and Reasoning in Event Calculus Using Goal-Directed Constraint Answer Set Programming.
Pre-Proc. of the 29th Int'l. Symposium on
Logic-based Program Synthesis and Transformation ,
Septiembre
2019.
- M. Klemen, P. Lopez-Garcia, J. Gallagher, J.F. Morales, M. V. Hermenegildo.
Towards a General Framework for Static Cost Analysis of Parallel Logic Programs.
Technical Communications of the 35th International
Conference on Logic Programming (ICLP 2019),
Electronic Proceedings in Theoretical Computer Science (EPTCS),
páginas 238--240,
Open Publishing Association (OPA),
Septiembre
2019.
(Extended Abstract).
- I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
Towards Computing Abstract Distances in Logic Programs.
Technical Communications of the 35th International
Conference on Logic Programming (ICLP 2019),
Electronic Proceedings in Theoretical Computer Science (EPTCS),
páginas 65--66,
Open Publishing Association (OPA),
Septiembre
2019.
(Extended Abstract).
- Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
Constraint Answer Set Programming without Grounding and
its Applications.
3rd Int'l. Workshop on the Resurgence of Datalog
in Academia and Industry (Datalog 2.0),
Vol. 2368,
páginas 22--26,
CEUR-WS,
Junio
2019.
- Arianna Blasi, Mauro Pezz`e, Alessandra
Gorla, Michael D. Ernst.
Research on NLP for RE at Universit`a della
Svizzera Italiana (USI): A Report.
Joint Proceedings of REFSQ-2019 Workshops,
Doctoral Symposium, Live Studies Track, and Poster
Track co-located with the 25th International
Conference on Requirements Engineering: Foundation
for Software Quality (REFSQ 2019),
CEUR Workshop Proceedings,
Vol. 2376,
CEUR-WS.org,
2019.
- Daniel Domínguez-Álvarez, Alessandra Gorla.
Release practices for iOS and Android apps.
Proceedings of the 3rd ACM SIGSOFT International
Workshop on App Market Analytics, WAMA-ESEC/SIGSOFT
FSE 2019,
páginas 15--18,
ACM,
2019.
- Kuhring, Lucas, Garcia, Eva, István, Zsolt.
Specialize in Moderation - Building Application-aware Storage Services using FPGAs in the Datacenter.
11th USENIX Workshop on Hot Topics in Storage and File Systems (HotStorage 19),
2019.
- Claudio Ferretti, Alberto Leporati, Luca Mariot, Luca Nizzardo.
Transferable Anonymous Payments via TumbleBit in Permissioned Blockchains.
Proceedings of the Second Distributed Ledger Technology Workshop,
DLT-ITASEC 2019,
CEUR Workshop Proceedings,
Vol. 2334,
páginas 56--67,
CEUR-WS.org,
2019.
- I. Garcia-Contreras, J.F. Morales, M. V. Hermenegildo.
Multivariant Assertion-based Guidance in Abstract
Interpretation.
Pre-proceedings of the 28th International Symposium on
Logic-based Program Synthesis and Transformation
(LOPSTR'18),
Septiembre
2018.
- P. Lopez-Garcia, M. Klemen, U. Liqat, M. V. Hermenegildo.
A General Framework for Static Profiling of Parametric Resource Usage (extended abstract).
19th International Workshop on Logic and Computational Complexity (LCC 2018),
4 páginas,
Julio
2018.
Associated to FLOC 2018.
- I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
Towards Incremental and Modular Context-sensitive Analysis.
Technical Communications of the 34th International
Conference on Logic Programming (ICLP 2018),
OpenAccess Series in Informatics (OASIcs),
2 páginas,
Dagstuhl Press,
Julio
2018.
(Extended Abstract).
- M. Klemen, N. Stulova, P. Lopez-Garcia, J. F. Morales, M. V. Hermenegildo.
Towards Static Performance Guarantees for
Programs with Run-time Checks.
Technical Communications of the 34th International
Conference on Logic Programming (ICLP 2018),
OpenAccess Series in Informatics (OASIcs),
2 páginas,
Julio
2018.
(Extended Abstract).
- Serdar Erbatur, Andrew M. Marshall, Christophe
Ringeissen.
Knowledge Problems in Equational Extensions of Subterm
Convergent Theories.
32nd International Workshop on Unification,
Julio
2018.
- István, Zsolt, Sorniotti, Alessandro, Vukolić, Marko.
StreamChain: Do Blockchains Need Blocks?.
Proceedings of the 2nd Workshop on Scalable and Resilient Infrastructures for Distributed Ledgers,
SERIAL'18,
páginas 1--6,
2018.
- Gustavo Betarte, Juan Diego Campo, Felipe Gorostiaga, Carlos Luna.
A certified reference validation mechanism for the permission model of Android.
Pre-proceedings of the 27th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'17),
Octubre
2017.
arXiv:1709.03652.
- U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
Inferring Energy Bounds via Static Program Analysis
and Evolutionary Modeling of Basic Blocks.
Pre-proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'17),
Octubre
2017.
arXiv:1601.02800.
- Salvador Tamarit, Julio Mariño, Guillermo
Vigueras, Manuel Carro.
Towards a Semantics-Aware Code Transformation
Toolchain for Heterogeneous Systems.
Proceedings of XIV Jornadas sobre Programación y
Lenguajes (PROLE 2016),
EPTCS,
Septiembre
2017.
- Guillermo Vigueras, Manuel Carro, Salvador
Tamarit, Julio Mariño.
Towards Automatic Learning of Heuristics for Mechanical
Transformations of Procedural Code.
Proceedings of XIV Jornadas sobre Programación y
Lenguajes (PROLE 2016),
EPTCS,
Septiembre
2017.
- Platon Kotzias, Juan Caballero.
An Analysis of Pay-per-Install Economics Using Entity Graphs.
16th Annual Workshop on the Economics of Information Security,
Junio
2017.
- Simon Oya, Carmela Troncoso, Fernando Pérez-González.
Is Geo-Indistinguishability What You Are Looking for?.
Proc. of the 16th Workshop on Privacy in the Electronic Society (WPES 2017),
páginas 137--140,
ACM,
2017.
- Nataliia Stulova.
On Improving Run-time Checking in Dynamic Languages.
Technical Communications of the 33rd International
Conference on Logic Programming (ICLP 2017),
OpenAccess Series in Informatics (OASIcs),
Vol. 58,
páginas 1501--1510,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
2017.
CP/ICLP/SAT Doctoral Program 2017.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
Towards Run-time Checks Simplification via Term Hiding.
Technical Communications of the 33rd International
Conference on Logic Programming (ICLP 2017),
OpenAccess Series in Informatics (OASIcs),
Vol. 58,
páginas 91--93,
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik,
2017.
(Extended Abstract).
- Konstantin Kuznetsov, Vitalii Avdiienko, Alessandra Gorla, Andreas Zeller.
Checking App User Interfaces Against App
Descriptions.
Proceedings of the 1st International Workshop on App
Market Analytics,
WAMA 2016,
páginas 1--7,
ACM,
Noviembre
2016.
- Vitalii Avdiienko, Konstantin Kuznetsov, Paolo
Calciati, Juan Carlos Caiza Román, Alessandra Gorla, Andreas Zeller.
CALAPPA: a Toolchain for Mining Android
Applications.
Proceedings of the 1st International Workshop on App
Market Analytics,
WAMA 2016,
páginas 22--25,
ACM,
Noviembre
2016.
- J. Arias.
Tabled CLP for Reasoning over Stream Data.
Technical Communications of the 32nd Int'l. Conference on Logic
Programming,
Vol. 52,
páginas 1--8,
OASIcs,
Octubre
2016.
Doctoral Consortium.
- Jan Kuper, Lutz Schubert, Kilian Kempf, Colin Glas, Daniel Rubio Bonilla, Manuel Carro.
Program Transformations in the POLCA Project.
Design, Automation, and Testing in Europe,
EDAA,
Marzo
2016.
- Guillermo Vigueras, Manuel Carro, Salvador Tamarit, Julio Mariño.
Towards Automatic Learning of Heuristics for Mechanical
Transformations of Procedural Code.
Proceedings of the First International Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016),
Marzo
2016.
- Salvador Tamarit, Julio Mariño, Guillermo Vigueras, Manuel Carro.
Towards a Semantics-Aware Transformation Toolchain for
Heterogeneous Systems.
Proceedings of the First International Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016),
Marzo
2016.
- Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira, Marc Shapiro.
The CISE tool: proving weakly-consistent applications correct.
PAPOC'16: Workshop on the Principles and Practice of
Consistency for Distributed Data,
páginas 1--3,
ACM Press,
2016.
- J. Hayes, C. Troncoso, G. Danezis
.
TASP: Towards Anonymity Sets that Persist.
15th Workshop on Privacy in the Electronic Society, WPES,
ACM,
2016.
- Bishoksan Kafle, John P. Gallagher, Pierre Ganty.
Solving non-linear Horn clauses using a linear Horn clause solver.
Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis,
HCVS 2016, satellite event of ETAPS, Eindhoven, The Netherlands, 3rd April 2016,
EPTCS,
Vol. 219,
páginas 33--48,
2016.
- U. Liqat, Z. Banković, P. Lopez-Garcia, M. V. Hermenegildo.
Inferring Energy Bounds Statically by Evolutionary Analysis of Basic Blocks.
Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES 2016),
2016.
arXiv:1601.02800.
- Bishoksan Kafle, John P. Gallagher.
Interpolant tree automata and their application in Horn clause verification.
Proceedings of the Fourth International Workshop on Verification and
Program Transformation, VPT 2016, Eindhoven, The Netherlands,
2nd April 2016.,
EPTCS,
Vol. 216,
páginas 104--117,
2016.
- R. Haemmerle, M. V. Hermenegildo, M. Klemen, U. Liqat, P. Lopez-Garcia.
Energy Analysis and Verification by Translation to Horn Clauses and Abstract Interpretation.
Workshop on Horn Clauses for Verification and Synthesis (HCVS'2015),
Julio
2015.
- Kafle, Bishoksan, Gallagher, John P., Ganty, Pierre.
Decomposition by tree dimension in Horn clause verification.
VPT '15: 3rd Int. Workshop on Verification and Program Transformation,
EPTCS,
Vol. 199,
páginas 1--14,
2015.
arXiv:1512.03862.
- Pavithra Prabhakar, Miriam García Soto.
An Algorithmic Approach to Stability Verification of Hybrid Systems: A Summary.
Symbolic and Numerical Methods for Reachability Analysis, 1st International Workshop, SNR 2015,
EPiC Series in Computing,
Vol. 37,
páginas 32--39,
EasyChair,
2015.
- Joaquín Arias, Manuel Carro.
Towards a Generic Interface to Integrate CLP and
Tabled Execution (Extended Abstract).
Technical Communications of the 31st International Conference on Logic Programming,
CEUR Workshop Proceedings,
Vol. 1433,
CEUR-WS.org,
2015.
Extended Abstract.
- P. Lopez-Garcia, R. Haemmerlé, M. Klemen, U. Liqat, M. V. Hermenegildo.
Towards Energy Consumption Verification via Static Analysis.
Workshop on High Performance Energy Efficient Embedded Systems (HIP3ES), arXiv:1501.03064,
11 páginas,
2015.
arXiv:1512.09369.
- J.F. Morales, M. V. Hermenegildo.
Pre-Indexed Terms for Prolog.
Pre-proceedings of the 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'14),
15 páginas,
Septiembre
2014.
- Álvaro García-Pérez, Pablo Nogueira.
A standard theory for the pure lambda-value calculus.
Septiembre
2014.
International Workshop on Domain Theory and Applications (Domains
XI).
- J.F. Morales, M. V. Hermenegildo.
Towards Pre-Indexed Terms.
14th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS-WLPE 2014),
14 páginas,
RWTH Aachen University,
Julio
2014.
http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2014.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
Towards Assertion-based Debugging of
Higher-Order (C)LP Programs (Extended
Abstract).
Theory and Practice of Logic Programming, 30th
Int'l. Conference on Logic Programming (ICLP'14)
Special Issue, On-line Supplement,
Vol. 14,
Núm. 4-5,
páginas 209--210,
Cambridge U. Press,
Julio
2014.
- Bishoksan Kafle, John P. Gallagher.
Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification.
Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014,
Vol. 169,
páginas 53--67,
EPTCS,
2014.
- U. Liqat, S. Kerrison, A. Serrano, K. Georgiou, P. Lopez-Garcia, N. Grech, M. V. Hermenegildo, K. Eder.
Energy Consumption Analysis of Programs based on XMOS ISA-Level Models.
Pre-proceedings of the 23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'13),
Septiembre
2013.
- Álvaro García-Pérez, Pablo Nogueira, Ilya Sergey.
Derivación de intérpretes del cálculo lambda con tipos graduales.
V Taller de Programación Funcional TPF 2013,
Septiembre
2013.
Charla impartida en el V Taller de Programación Funcional TPF 2013.
- Dragan Ivanović.
Implementing Constraint Handling Rules as a
Domain-Specific Language Embedded in Java.
Proceedings of the 23rd Workshop on Logic-based
methods in Programming Environments (WLPE 2013),
Agosto
2013.
- A. Serrano, P. Lopez-Garcia, M. V. Hermenegildo.
Towards an Abstract Domain for Resource Analysis of Logic Programs Using Sized Types.
23rd Workshop on Logic-based Methods in Programming Environments (WLPE 2013),
15 páginas,
Agosto
2013.
CoRR abs/1308.3940.
- D. Ivanovic, P. Kaowichakorn, M. Carro.
Towards QoS Prediction Based on Composition Structure Analysis and Probabilistic Environment Models.
5th International Workshop on Principles of Engineering Service-Oriented Systems,
Mayo
2013.
- Javier Reyes, Juan M. Orduña, Guillermo Vigueras, Rafael Tornero.
Acceleration of Communication-Aware Task Mapping Techniques
through GPU Computing.
AINA Workshops,
páginas 843--848,
2013.
- Julián Samborski-Forlese, César Sánchez.
Bounded Model Checking for Regular Linear Temporal Logic (extended abstract).
Proceedings of the 24th Nordic Workshop on Programming Theory (NWPT'12),
Octubre
2012.
Available at (available online).
- Z. Drey, J.F. Morales, M. V. Hermenegildo.
Reversible Language Extensions and their Application in Debugging.
12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS 2012),
15 páginas,
Septiembre
2012.
- E.J. Gallego-Arias, R. Haemmerlé, M. V. Hermenegildo, J.F. Morales .
The Ciao CLP(FD) Library: A Modular CLP Extension for Prolog.
12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS 2012),
15 páginas,
Septiembre
2012.
- Álvaro García-Pérez, Pablo Nogueira.
Enfoque normal y enfoque spine para reducción en el cálculo lambda
puro.
IV Taller de Programación Funcional TPF 2012,
Septiembre
2012.
Charla impartida en el IV Taller de Programación Funcional TPF 2012.
- D. Ivanovic, M. Carro, M. V. Hermenegildo.
Analyzing Service-Oriented Systems Using Their Data and Structure.
European Software Services and Systems Research -- Results and Challenges (ICSE Workshop),
Julio
2012.
- D. Karastoyanova, Z. Nemeth, M. Carro, D. Ivanovic, C. Pautasso, C. Di Napoli, M. Giordano.
Research Challenges on Service Technology Foundations.
European Software Services and Systems Research -- Results and Challenges (ICSE Workshop),
Julio
2012.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Exploring the Impact of Inaccuracy and Imprecision
of QoS Assumptions on Proactive Constraint-Based
QoS Prediction for Service Orchestrations.
Proceedings of the 4th International Workshop on
Principles of Engineering Service-Oriented Systems,
PESOS 2012,
páginas 931--937,
IEEE Press,
Junio
2012.
- Fangzhe Chang, Pavithra Prabhakar, Ramesh Viswanathan.
Behavior Based Service Composition.
Web Services and Formal Methods - 8th International Workshop,
WS-FM 2011, Clermont-Ferrand, France, September 1-2, 2011,
Revised Selected Papers,
Lecture Notes in Computer Science,
Vol. 7176,
páginas 17--31,
Springer,
2012.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Constraint-Based Runtime Prediction of SLA
Violations in Service Orchestrations.
XII Jornadas sobre Programación y Lenguajes (PROLE),
Universidad de Almería,
2012.
- J. F. Morales, R. Haemmerlé, M. Carro, M. V. Hermenegildo.
Lightweight compilation of (C)LP to JavaScript.
XII Jornadas sobre Programación y Lenguajes (PROLE),
Universidad de Almería,
2012.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, P. Stuckey.
A General Implementation Framework for
Tabled CLP.
XII Jornadas sobre Programación y Lenguajes (PROLE),
Universidad de Almería,
2012.
- Carolina Dania.
Modeling Social Networking Privacy.
ESSoS-DS 2012. Doctoral Symposium,
Workshop Proceedings,
Vol. 834,
páginas 49--54,
CEUR,
2012.
- F. Bueno, M. García de la Banda, M. V. Hermenegildo, P. Lopez-Garcia, E. Mera, P. J. Stuckey.
Towards Resource Usage Analysis of MiniZinc Models.
MiniZinc Workshop (MZN'11),
15 páginas,
Septiembre
2011.
- Álvaro García-Pérez, Pablo Nogueira.
Estrategias del cálculo lambda e interderivación de artefactos
semánticos.
III Taller de Programación Funcional TPF 2011,
Septiembre
2011.
Charla impartida en el III Taller de Programación Funcional TPF
2011.
- P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo.
Interval-based Resource Usage Verification: Formalization and Prototype.
2nd International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'2011),
Mayo
2011.
- M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, E. Mera, J.F. Morales, G. Puebla.
The Ciao Approach to the Dynamic vs. Static Language Dilemma.
Proceedings for the International Workshop on Scripts to Programs (STOP'11),
4 páginas,
ACM,
2011.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
An Initial Proposal for Data-Aware Resource
Analysis of Orchestrations with Applications to
Predictive Monitoring.
International Workshops, ICSOC/ServiceWave 2009,
Revised Selected Papers,
LNCS,
Núm. 6275,
Springer,
Septiembre
2010.
- Álvaro García-Pérez.
El Cubo Beta.
II Taller de Programación Funcional TPF 2010,
Septiembre
2010.
Charla impartida en el II Taller de Programación Funcional TPF 2010.
- R. Haemmerlé.
(Co)inductive Semantics for Constraint Handling Rules.
Annual ERCIM Workshop on Constraint Solving and
Constraint Logic Programming,
2010.
- Álvaro García-Pérez, Pablo Nogueira, Emilio Jesús
Gallego Arias.
The Beta Cube (Extended Abstract).
Proceedings of the 1st International Workshop on Strategies in
Rewriting, Proving, and Programming (IWS'10),
páginas 3--7,
July 9
2010.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
An Initial Proposal for Data-Aware Resource
Analysis of Orchestrations with Applications to
Proactive Monitoring.
Pre-proceedings of the 2nd Workshop on Monitoring,
Adaptation and Beyond (MONA+),
Noviembre
2009.
- L. Scandolo, C. Kunz, G. Barthe, M.V. Hermenegildo.
Program Parallelization using Synchronized Pipelining.
Pre-proceedings of the 19th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'09),
Septiembre
2009.
- D. Ivanović, J.F. Morales, M. Carro, M. V. Hermenegildo.
Towards Structured State Threading in Prolog.
CICLOPS 2009,
15 páginas,
Julio
2009.
- J. Navas, M. Méndez-Lojo, M. V. Hermenegildo.
User-Definable Resource Usage Bounds
Analysis for Java Bytecode.
Proceedings of the Workshop on Bytecode Semantics,
Verification, Analysis and Transformation (BYTECODE'09),
Electronic Notes in Theoretical Computer Science,
Vol. 253,
Núm. 5,
páginas 65--82,
Elsevier - North Holland,
Marzo
2009.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
A Program Transformation for Continuation
Call-Based Tabled Execution.
Colloquium on Implementation of Constraint and LOgic
Programming Systems (ICLP associated workshop),
15 páginas,
University of Udine,
Diciembre
2008.
- G. Marpons, J. Mariño, M. Carro, A. Herranz, L.Å. Fredlund, J.J. Moreno-Navarro, A. Polo.
A Coding Rule Conformance Checker Integrated into GCC.
VIII Jornadas sobre Programación y Lenguajes, PROLE 2008,
páginas 245--249,
Octubre
2008.
- Pablo Nogueira, Juan José Moreno-Navarro.
Bialgebra Views: A Way for Polytypic Programming to
Cohabit with Data Abstraction.
Proceedings of the 2nd ACM SIGPLAN Workshop on Generic
Programming (ICFP-WGP'08),
páginas 61--73,
ACM Press,
Septiembre
2008.
- M. Méndez-Lojo, O. Lhoták, M. V. Hermenegildo.
Efficient Set Sharing using ZBDDs.
21st Int'l. WS on Languages and Compilers for
Parallel Computing (LCPC'08),
LNCS,
Vol. 5335,
páginas 94--108,
Springer-Verlag,
Agosto
2008.
- E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo.
Two Efficient Representations for Set-Sharing
Analysis in Logic Programs .
17th International Workshop on Functional and (Constraint) Logic
Programming, WFLP'08,
15 páginas,
Julio
2008.
- J. Navas, M. Méndez-Lojo, M. Hermenegildo.
Safe Upper-bounds Inference of Energy Consumption for
Java Bytecode Applications.
The Sixth NASA Langley Formal Methods Workshop (LFM 08),
páginas 29--32,
Abril
2008.
Extended Abstract.
- Gilles Barthe, César Kunz.
Certificate Translation for Specification-Preserving Advices.
Proceedings of the 7th Workshop on Foundations of Aspect-Oriented
Languages, FOAL 2008,
páginas 9--18,
ACM,
2008.
- G. Marpons-Ucero, J. Mariño, A. Herranz, L.Å. Fredlund, M. Carro, J.J. Moreno-Navarro.
Automatic Coding Rule Conformance Checking Using Logic Programs.
17th Workshop on Logic-based methods in Programming
Environments, WLPE 2007,
Septiembre
2007.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo, Claudio Silva, Ricardo Rocha.
Some Improvements over the Continuation Call
Tabling Implementation Technique.
Colloquium on Implementation of Constraint and LOgic
Programming Systems (ICLP associated workshop),
15 páginas,
Universidade do Porto,
Septiembre
2007.
- A. Casas, M. Carro, M. V. Hermenegildo.
Towards High-Level Execution Primitives for
And-Parallelism: Preliminary Results.
Colloquium on Implementation of Constraint and LOgic
Programming Systems (CICLOPS'07, ICLP associated
workshop),
15 páginas,
U. of Evora,
Septiembre
2007.
- J. Navas, M. Méndez-Lojo, M. V. Hermenegildo.
An Efficient, Context and Path Sensitive Analysis Framework
for Java Programs.
9th Workshop on Formal Techniques for Java-like Programs
FTfJP 2007,
12 páginas,
Julio
2007.
- A. Casas, M. Carro, M. V. Hermenegildo.
Towards A High-Level Implementation of Flexible
Parallelism Primitives for Symbolic
Languages.
Parallel Symbolic Computation (PASCO'07),
2 páginas,
ACM Press,
Julio
2007.
Extended Abstract.
- M. Hermenegildo, The Ciao Development Team.
An Overview of The Ciao Multiparadigm Language
and Program Development Environment and its
Design Philosophy.
ECOOP Workshop on Multiparadigm Programming with
Object-Oriented Languages MPOOL 2007,
Julio
2007.
- M. Méndez-Lojo, J. Navas, M. V. Hermenegildo.
An Efficient, Parametric Fixpoint Algorithm for
Analysis of Java Bytecode.
ETAPS Workshop on Bytecode Semantics, Verification,
Analysis and Transformation (BYTECODE 2007),
Electronic Notes in Theoretical Computer Science,
Elsevier - North Holland,
Marzo
2007.
Informes Técnicos y Manuales
- F. Bueno, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, J.F. Morales (Eds.).
The Ciao System. Reference Manual (V1.20).
Febrero
2022.
Available at http://ciao-lang.org.
- Joaquín Arias, Manuel Carro, Zhuo Chen, Gopal Gupta.
Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming.
Núm. 2106.14566 [cs.AI],
arXiv,
Junio
2021.
- M.A. Sanchez-Ordaz, I. Garcia-Contreras, V. Perez-Carrasco, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
VeriFly: On-the-fly Assertion Checking via Incrementality.
Núm. CLIP-1/2021.0,
21 páginas,
The CLIP Lab, IMDEA Software Institute and T.U. Madrid,
Mayo
2021.
- F. Bueno, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, J.F. Morales (Eds.).
The Ciao System. Reference Manual (V1.20).
Abril
2021.
Available at http://ciao-lang.org.
- Joaquín Arias, Manuel Carro.
A Theoretical Study of (Full) Tabled Constraint Logic Programming.
Núm. 2009.14430 [cs.LO],
arXiv,
Septiembre
2020.
- F. Bueno, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, J.F. Morales (Eds.).
The Ciao System. Ref. Manual (V1.19).
Marzo
2020.
Available at http://ciao-lang.org.
- Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth.
Masking in Fine-Grained Leakage Models: Construction, Implementation
and Verification.
2020.
Cryptology ePrint Archive, Report 2020/603.
- Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe.
High-Assurance Cryptography Software in the Spectre Era.
2020.
Cryptology ePrint Archive, Report 2020/1104.
- Irfan Ul Haq, Juan Caballero.
A Survey of Binary Code Similarity.
Septiembre
2019.
- M. Klemen, P. Lopez-Garcia, J. Gallagher, J.F. Morales, M. V. Hermenegildo.
Towards a General Framework for Static Cost Analysis of Parallel Logic Programs.
Núm. CLIP-1/2019.0,
19 páginas,
The CLIP Lab, IMDEA Software Institute and T.U. Madrid,
Julio
2019.
- I. Casso, J. F. Morales, P. Lopez-Garcia, M. V. Hermenegildo.
Computing Abstract Distances in Logic Programs.
Núm. CLIP-2/2019.0,
21 páginas,
The CLIP Lab, IMDEA Software Institute and T.U. Madrid,
Julio
2019.
- I. Garcia-Contreras, J. F. Morales, M. V. Hermenegildo.
An Approach to Incremental and Modular Context-sensitive Analysis of Logic Programs.
Núm. CLIP-2/2018.0,
28 páginas,
The CLIP Lab, IMDEA Software Institute and T.U. Madrid,
Abril
2018.
- M. Klemen, N. Stulova, P. Lopez-Garcia, J. F. Morales, M. V. Hermenegildo.
An Approach to Static Performance Guarantees for Programs with Run-time Checks.
Núm. CLIP-1/2018.0,
15 páginas,
The CLIP Lab, IMDEA Software Institute and T.U. Madrid,
Abril
2018.
- F. Bueno, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, J.F. Morales (Eds.).
The Ciao System. Ref. Manual (V1.16).
Julio
2017.
Available at http://ciao-lang.org.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
Term Hiding and its Impact on Run-time
Check Simplification.
Núm. CLIP-1/2017.0,
27 páginas,
The CLIP Lab,
Mayo
2017.
CoRR abs/1705.06662 (v2) [cs.PL].
- Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee.
Attribute-Based Encryption in the Generic Group Model: Automated Proofs
and New Constructions.
29 páginas,
IACR Cryptology ePrint Archive,
2017.
- Miguel Ambrona, Gilles Barthe, Benedikt Schmidt.
Automated Unbounded Analysis of Cryptographic Constructions in the
Generic Group Model.
30 páginas,
IACR Cryptology ePrint Archive,
2016.
- Miguel Ambrona, Gilles Barthe, Benedikt Schmidt.
Generic Transformations of Predicate Encodings: Constructions and
Applications.
30 páginas,
IACR Cryptology ePrint Archive,
2016.
- Pierre Ganty, Boris Köpf, Pedro Valero.
A Language-theoretic View on Network Protocols.
2016.
- P. Lopez-Garcia, R. Haemmerlé, U. Liqat, M. Klemen, M. V. Hermenegildo.
Parametric Static Profiling.
Núm. CLIP-2/2015.0,
The CLIP Lab,
Abril
2015.
- Guillermo Vigueras, Salvador Tamarit, Manuel Carro, Julio Mariño.
Towards a Rule-Based Approach to Generate High-Performance Scientific Code.
Núm. CLIP1/2015.0,
8 páginas,
The CLIP Lab,
Marzo
2015.
http://cliplab.org/papers/vigueras15-rule-based.pdf.
- Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub.
Computer-aided Verification in Mechanism Design.
2015.
CoRR abs/1502.04052 [cs.GT].
- R. Haemmerlé.
On the Confluence of the Analytical Semantics of CHR.
Núm. CLIP2/2014.0,
12 páginas,
Technical University of Madrid (UPM),
Julio
2014.
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, Francois Dupressoir, Benjamin Grégoire, Pierre-Yves Strub.
Verified Implementations for Secure and Verifiable Computation.
Junio
2014.
IACR Cryptology ePrint Archive, Report 2014/456.
- N. Stulova, J. F. Morales, M. V. Hermenegildo.
An Approach to Assertion-based Debugging of
Higher-Order (C)LP Programs.
Núm. CLIP-1/2014.0,
25 páginas,
The CLIP Lab,
Enero
2014.
CoRR abs/1404.4246 [cs.PL].
- Pierre Ganty, Radu Iosif.
Generating Bounded Languages Using Bounded Control Sets.
2014.
- Juan Caballero, Gustavo Grieco, Mark Marron, Zhiqiang Lin, David Urbina.
ARTISTE: Automatic Generation of Hybrid Data Structure Signatures from Binary Code Executions.
Núm. TR-IMDEA-SW-2012-001,
IMDEA Software Institute,
Agosto
2012.
- Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin.
Verified Security of Redundancy-Free Encryption from Rabin and RSA.
Cryptology ePrint Archive, Report 2012/308,
2012.
(available online).
- Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin.
Automated Analysis and Synthesis of Padding-Based Encryption Schemes.
Cryptology ePrint Archive, Report 2012/695,
2012.
(available online).
- José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin.
Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols.
Cryptology ePrint Archive, Report 2012/258,
2012.
(available online).
- Marianne Busch, Miguel Ángel García de Dios.
ActionUWE: Transformation of UWE to ActionGUI Models.
Ludwig-Maximilians-Universität München,
2012.
- F. Bueno, M. Carro, M. V. Hermenegildo, R. Haemmerlé, P. Lopez-Garcia, E. Mera, J.F. Morales, G. Puebla-(Eds.).
The Ciao System. Ref. Manual (V1.14).
Julio
2011.
Available at http://ciao-lang.org.
- M. V. Hermenegildo, J.F. Morales.
The LPdoc Documentation Generator. Ref. Manual (V3.0).
UPM,
Julio
2011.
Available at http://ciao-lang.org.
- P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo.
Towards Resource Usage Function Verification based on Input Data Size Intervals.
Núm. CLIP4/2011.0,
Technical University of Madrid (UPM),
Abril
2011.
Available at http://cliplab.org/papers/resource-verif-11-tr.pdf.
- P. Chico de Guzmán, A. Casas, M. Carro, M. V. Hermenegildo.
A Simulation Study on Parallel
Backtracking with Solution Memoing for
Independent And-Parallelism.
Núm. CLIP1/2011.0,
12 páginas,
Technical University of Madrid (UPM),
Enero
2011.
- J.F. Morales, M. V. Hermenegildo, R. Haemmerlé.
Towards Modular Extensions for a Modular Language.
Núm. CLIP2/2011.0,
15 páginas,
Technical University of Madrid (UPM),
Enero
2011.
- Alexander Malkis.
On the strength of Owicki-Gries for resources.
2011.
Technical report, (available online).
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Automated Attribute Inference in Complex Service
Workflows Based on Sharing Analysis.
Núm. CLIP5/2010.0,
Technical University of Madrid (UPM),
Diciembre
2010.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Automatic Fragment Identification in Workflows Based on Sharing Analysis.
Núm. CLIP4/2010.0,
15 páginas,
Technical University of Madrid (UPM),
Junio
2010.
Submitted.
- E. Mera, T. Trigo, P. Lopez-Garcia, M. V. Hermenegildo.
An Approach to Profiling for Run-Time Checking of
Computational Properties and Performance Debugging.
Núm. CLIP3/2010.0,
29 páginas,
Technical University of Madrid (UPM),
Marzo
2010.
- M. V. Hermenegildo, F. Bueno, M. Carro, P. Lopez-Garcia, E. Mera, J.F. Morales, G. Puebla.
An Overview of Ciao and its Design Philosophy.
Núm. CLIP2/2010.0,
Technical University of Madrid (UPM),
Marzo
2010.
Under consideration for publication in Theory and
Practice of Logic Programming (TPLP).
- D. Ivanović, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, E. Mera.
Towards Data-Aware Cost-Driven Adaptation for
Service Orchestrations.
Núm. CLIP5/2009.1,
Technical University of Madrid (UPM),
Marzo
2010.
- P. Lopez-Garcia, L. Darmawan, F. Bueno, M. V. Hermenegildo.
Towards a Framework for Resource Usage Verification and Debugging in the CiaoPP System.
Núm. CLIP1/2010.0,
Technical University of Madrid (UPM),
Febrero
2010.
Available at http://cliplab.org/papers/resource-verif-10-tr.pdf.
- Javier Esparza, Pierre Ganty, Stefan Kiefer, Michael Luttenberger.
Parikh's Theorem: A simple and direct construction.
2010.
- Pierre Ganty, Rupak Majumdar.
Algorithmic Verification of Asynchronous Programs.
2010.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Sharing-Based Independence-Driven Fragment
Identification for Service Orchestrations.
Núm. CLIP7/2009.0,
Technical University of Madrid (UPM),
Diciembre
2009.
- D. Ivanović, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, E. Mera.
Towards Data-Aware Cost-Driven Adaptation for
Service Orchestrations.
Núm. CLIP5/2009.0,
Technical University of Madrid (UPM),
Noviembre
2009.
Replaced by a later version.
- J.F. Morales, M. Carro, M. V. Hermenegildo.
Description and Optimization of Abstract Machines
in a Dialect of Prolog.
Núm. CLIP4/2009.0,
Technical University of Madrid (UPM),
Octubre
2009.
- D. Ivanović, M. Carro, M. V. Hermenegildo.
Towards Data-Aware Resource Analysis for
Service Orchestrations.
Núm. CLIP3/2009.0,
Technical University of Madrid (UPM),
Junio
2009.
- E. Mera, P. Lopez-Garcia, M. V. Hermenegildo.
Towards Integrating Run-Time Checking and
Software Testing in a Verification Framework.
Núm. CLIP1/2009.0,
19 páginas,
Technical University of Madrid (UPM),
Marzo
2009.
- P. Lopez-Garcia, F. Bueno, M. V. Hermenegildo.
Inferring Determinacy and Mutual Exclusion in
Logic Programs Using Mode and Type
Analysis.
Núm. CLIP2/2009.0,
Technical University of Madrid (UPM),
Febrero
2009.
- Pierre Ganty, Rupak Majumdar, Benjamin Monmege.
Bounded Underapproximations.
2009.
- F. Bueno, D. Cabeza, M. Carro, M. V. Hermenegildo, P. Lopez-Garcia, G. Puebla-(Eds.).
The Ciao System. Ref. Manual (V1.13).
2009.
Available at http://ciao-lang.org.
- E. Trias, J. Navas, E. S. Ackley, S. Forrest, M. V. Hermenegildo.
Efficient Representations for Set-Sharing Analysis.
Núm. CLIP9/2008.0,
University of New Mexico and Technical University of
Madrid,
Septiembre
2008.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
Bridge Program Transformation for the CCall
Tabling Scheme.
Núm. CLIP6/2008.0,
Technical University of Madrid (UPM),
Septiembre
2008.
- A. Casas, M. Carro, M. V. Hermenegildo.
A High-Level Implementation of
Non-Deterministic, Unrestricted, Independent
And-Parallelism.
Núm. TR-CS-2008-10,
University of New Mexico (UNM),
Septiembre
2008.
- J. Navas, E. Mera, P. Lopez-Garcia, M. Hermenegildo.
Inference of User-Definable Resource Bounds Usage for Logic Programs and its Applications.
Núm. CLIP5/2008.0,
Technical University of Madrid (UPM),
Julio
2008.
- M. Méndez-Lojo, O. Lhoták, M. V. Hermenegildo.
Fast Set Sharing using ZBDDs.
University of New Mexico,
Junio
2008.
- M. Hermenegildo, E. Albert, P. Arenas, F. Bueno, M. Carro, A. Casas, P. Chico de Guzmán, J. Correas, S. Genaim, J. Lipton, Pedro
Lopez-Garcia, M. Méndez, E. Mera, J. Morales, J. Navas, R. Padilla, P. Pietrzak, G. Puebla, M. Zamalloa, D. Zanardini.
Rigorous Methods for Mobile and Heterogeneous
Software Systems -- Second Year Report.
Núm. CLIP3/2008.0,
Technical University of Madrid (UPM),
Abril
2008.
- J. Navas, M. Méndez-Lojo, M. V. Hermenegildo.
Customizable Resource Usage Analysis for Java Bytecode.
Núm. UNM TR-CS-2008-02 - CLIP1/2008.0,
University of New Mexico,
Enero
2008.
- A. Casas, M. Carro, M. V. Hermenegildo.
Automatic Unrestricted Independent
And-Parallelism in Logic Programs.
Núm. CLIP11/2007.0,
Technical University of Madrid (UPM),
Diciembre
2007.
Under consideration for publication in Theory and
Practice of Logic Programming (TPLP).
- M. Méndez-Lojo, M. Hermenegildo.
Precise Set Sharing for Java-style Programs (and proofs).
Núm. CLIP2/2007.1,
Technical University of Madrid (UPM),
Noviembre
2007.
- A. Casas, M. Carro, M. V. Hermenegildo.
Towards a High-Level Implementation of Execution
Primitives for Non-restricted, Independent
And-parallelism.
Núm. TR-CS-2007-16,
University of New Mexico (UNM),
Octubre
2007.
- A. Casas, M. Carro, M. V. Hermenegildo.
Annotation Algorithms for Unrestricted Independent
And-Parallelism in Logic Programs.
Núm. TR-CS-2007-14,
University of New Mexico (UNM),
Septiembre
2007.
- E. Mera, P. Lopez-Garcia, M. Carro, M. V. Hermenegildo.
Towards Execution Time Estimation in
Abstract Machine-Based (Logic) Languages.
Núm. CLIP8/2007.0,
Technical University of Madrid (UPM),
Agosto
2007.
- G. Marpons, J. Mariño, M. Carro, A. Herranz, J.J. Moreno-Navarro, L.Å. Fredlund.
Automatic Coding Rule Conformance Checking Using Logic Programming.
Núm. CLIP6/2007.0,
Technical University of Madrid (UPM),
Agosto
2007.
- P. Chico de Guzmán, M. Carro, M. V. Hermenegildo.
An Improved Continuation Call-Based Implementation of Tabling.
Núm. CLIP9/2007.0,
Technical University of Madrid (UPM),
Agosto
2007.
- A. Casas, M. Carro, M. V. Hermenegildo.
Towards a High-Level Implementation of Execution
Primitives for Non-Restricted, Independent
And-Parallelism.
Núm. CLIP7/2007.0,
Technical University of Madrid (UPM),
Agosto
2007.
- A. Casas, M. Carro, M. V. Hermenegildo.
Annotation Algorithms for Unrestricted Independent
And-Parallelism in Logic Programs.
Núm. CLIP5/2007.0,
Technical University of Madrid (UPM),
Junio
2007.
- M. Hermenegildo, E. Albert, P. Arenas, A. Beascoa, F. Bueno, D. Cabeza, M. Carro, J. Correas, A. García Pañoso, J. Lipton, P. Lopez-Garcia, E. Mera, J. Morales, C. Ochoa, G. Puebla.
Rigorous Methods for Mobile and Heterogeneous
Software Systems -- First Year Report.
Núm. CLIP4/2007.0,
Technical University of Madrid (UPM),
Marzo
2007.
- M. Méndez-Lojo, M. Hermenegildo.
Precise Set Sharing and Nullity Analysis
for Java-style Programs.
Núm. CLIP2/2007.0,
Technical University of Madrid (UPM),
Febrero
2007.
- P. Lopez-Garcia, F. Bueno, M. V. Hermenegildo.
Inferring Determinacy in Logic Programs Using
Mode and Type Information.
Núm. CLIP3/2007.0,
Technical University of Madrid (UPM),
Febrero
2007.