Working papers

• SecurePtrs: proving secure compilation with data-flow back-translation and turn-taking simulation, by Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Cătălin Hriţcu and Deepak Garg. Accepted to the 35th IEEE Computer Security Foundations Symposium (CSF 2022).

• Formalizing stack safety as a security property, by Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce and Andrew Tolmach. Submitted.

Recent publications

• SecurePtrs: proving secure compilation with data-flow back-translation and turn-taking simulation (extended abstract), by Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Cătălin Hriţcu and Deepak Garg. In 6th Workshop on Principles of Secure Compilation (PriSC 2022). Philadelphia, PA, 22 January 2022.

• An extended account of trace-relating compiler correctness and secure compilation, by Carmine Abate, Roberto Blanco, Ștefan Ciobâcă, Adrien Durier, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Éric Tanter and Jérémy Thibault. ACM Transactions on Programming Languages and Systems, vol. 43, no. 4, pp. 1-48, December 2021.

• Assistant editor (collector) in: Secure compilation (Dagstuhl seminar 21481), by David Chisnall, Deepak Garg, Cătălin Hriţcu and Mathias Payer (eds.). Dagstuhl Reports, vol. 11(10), pp. 173-204, November 2021.

• Security properties for stack safety, by Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce and Andrew Tolmach. In Workshop on Foundations of Computer Security 2021 (FCS 2021). Online, 21 June 2021.

• FPC-Coq: using ELPI to elaborate external proof evidence into Coq proofs (system description), by Roberto Blanco, Matteo Manighetti and Dale Miller. In Coq Workshop 2020. Online, 5 July 2020.

• Linking a lambda Prolog proof checker to the Coq kernel: an extended abstract, by Roberto Blanco, Matteo Manighetti and Dale Miller. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020). Online, 30 June 2020.

• On the proof theory of property-based testing of coinductive specifications, or: PBT to infinity and beyond, by Roberto Blanco, Dale Miller and Alberto Momigliano. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020). Online, 29 June 2020.

• Trace-relating compiler correctness and secure compilation, by Carmine Abate, Roberto Blanco, Ștefan Ciobâcă, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Éric Tanter and Jérémy Thibault. In: Peter Müller (ed.), Proceedings of the 29th European Symposium on Programming (ESOP 2020), pp. 1-28. Dublin, Ireland, 25-30 April 2020 (meeting not held due to the COVID-19 pandemic).

• On the proof theory of property-based testing of coinductive specifications, or: PBT to infinity and beyond, by Roberto Blanco, Dale Miller and Alberto Momigliano. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Turin, Italy, 2-5 March 2020 (meeting not held due to the COVID-19 pandemic).

• Trace-relating compiler correctness and secure compilation (extended abstract), by Carmine Abate, Roberto Blanco, Ștefan Ciobâcă, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Éric Tanter and Jérémy Thibault. In 4th Workshop on Principles of Secure Compilation (PriSC 2020). New Orleans, LA, 25 January 2020.

• Property-based testing via proof reconstruction, by Roberto Blanco, Dale Miller and Alberto Momigliano. In: Ekaterina Komendantskaya (ed.), Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019), pp. 5:1-5:13. Porto, Portugal, 7 October 2019.

• Journey beyond full abstraction: exploring robust property preservation for secure compilation, by Carmine Abate, Roberto Blanco, Deepak Garg, Cătălin Hriţcu, Marco Patrignani and Jérémy Thibault. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF2019), pp. 256-271. Hoboken, NJ, 27 June 2019. Distinguished paper award.

• When good components go bad: formally secure compilation despite dynamic compromise, by Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hriţcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati and Andrew Tolmach. In: David Lie, Mohammad Mannan, Michael Backes and XiaoFeng Wang (eds.), Proceedings of the 25th ACM Conference on Computer and Communications Security (CCS 2018), pp. 1351-1368. Toronto, Canada, 18 October 2018.

• Design and verification of functional proof checkers, by Roberto Blanco. In ML Family Workshop 2018. Saint Louis, MO, 28 September 2018.

• Assistant editor (collector) in: Secure compilation (Dagstuhl seminar 18201), by Amah Ahmed, Deepak Garg, Cătălin Hriţcu and Frank Piessens (eds.). Dagstuhl Reports, vol. 8(5), pp. 1-30, May 2018.

• Applications of Foundational Proof Certificates in theorem proving, by Roberto Blanco. Ph.D. dissertation, École polytechnique, Université Paris-Saclay, 21 December 2017.

• Property-based testing via proof reconstruction: work-in-progress, by Roberto Blanco, Alberto Momigliano and Dale Miller. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2017), Oxford, UK, 8 September 2017.

• Translating between implicit and explicit versions of proof, by Roberto Blanco, Zakaria Chihani and Dale Miller. In: L. de Moura (ed.), Proceedings of the 26th International Conference on Automated Deduction (CADE-26). Gothenburg, Sweden, 9 August 2017. Lecture Notes in Computer Science, vol. 10395, pp. 255-273.

• An interactive assistant for the definition of proof certificates, by Roberto Blanco and Zakaria Chihani. In the seminar in honor of the 60th birthday of Dale Miller (Dale Fest). Paris, France, 15 December 2016.

• Proof outlines as proof certificates: a system description, by Roberto Blanco and Dale Miller. In: I. Cervesato and C. Schürmann (eds.), Proceedings of the First International Workshop on Focusing (WoF’15). Suva, Fiji, 23 November 2015. Electronic Proceedings in Theoretical Computer Science, vol. 197, pp. 7-14.

• Defining the meaning of TPTP formatted proofs, by Roberto Blanco, Tomer Libal and Dale Miller. In: B. Konev, S. Schulz and L. Simon (eds.), Proceedings of the 11th International Workshop on the Implementation of Logics (IWIL-2015). Suva, Fiji, 23 November 2015. EPiC Series in Computing, vol. 40, pp. 78-90.

Older publications

• Temporal logics for phylogenetic analysis via model checking, by José Ignacio Requeno, Gregorio de Miguel Casado, Roberto Blanco and José Manuel Colom. IEEE/ACM Transactions on Computational Biology and Bioinformatics, vol. 10, pp. 1058–1070, July 2013.

• Sliced model checking for phylogenetic analysis, by José Ignacio Requeno, Roberto Blanco, Gregorio de Miguel Casado and José Manuel Colom. In: M. P. Rocha, N. Luscombe, F. Fdez Riverola and J. M. Corchado Rodríguez (eds.), Proceedings of the 6th International Conference on Practical Applications of Computational Biology & Bioinformatics (PACBB 2012). Salamanca, Spain, March 2012. Advances in Intelligent and Soft Computing, vol. 154, pp. 95-103.

• Simplification methods for maximum parsimony: a relational view, by Roberto Blanco. In: F.-X. Wu, M. Zaki, S. Morishita, Y. Pan, S. Wong, A. Christianson and X. Hu (eds.), Proceedings of the 2011 IEEE International Conference on Bioinformatics and Biomedicine (BIBM 2011). Atlanta, GA, November 2011, pp. 49-56.

• Rebooting the human mitochondrial phylogeny: an automated and scalable methodology with expert knowledge, by Roberto Blanco, Elvira Mayordomo, Julio Montoya and Eduardo Ruiz-Pesini. BMC Bioinformatics, vol. 12, pp. 174, May 2011.

• Workflows with model selection: a multilocus approach to phylogenetic analysis, by Jorge Álvarez, Roberto Blanco and Elvira Mayordomo. In: M. P. Rocha, J. M. Corchado Rodríguez, F. Fdez Riverola and A. Valencia (eds.), Proceedings of the 5th International Conference on Practical Applications of Computational Biology & Bioinformatics (PACBB 2011). Salamanca, Spain, April 2011. Advances in Intelligent and Soft Computing, vol. 93, pp. 39-47.

• Phylogenetic analysis using an SMV tool, by José Ignacio Requeno, Roberto Blanco, Gregorio de Miguel Casado and José Manuel Colom. In: M. P. Rocha, J. M. Corchado Rodríguez, F. Fdez Riverola and A. Valencia (eds.), Proceedings of the 5th International Conference on Practical Applications of Computational Biology & Bioinformatics (PACBB 2011). Salamanca, Spain, April 2011. Advances in Intelligent and Soft Computing, vol. 93, pp. 167-174.

• Structural parsimony: reductions in sequence space, by Roberto Blanco. In: T. Park and L. Chen and L. Wong and S. Tsui and M. Ng and X. Hu (eds.), Proceedings of the 2010 IEEE International Conference on Bioinformatics and Biomedicine (BIBM 2010). Hong Kong, December 2010, pp. 57-61.

• Temporal logics for phylogenetic analysis via model checking, by Roberto Blanco, Gregorio de Miguel Casado, José Ignacio Requeno and José Manuel Colom. In: Proceedings of the 2010 IEEE International Conference on Bioinformatics and Biomedicine Workshops (BIBMW 2010). Hong Kong, December 2010, pp. 152-157.

• Scalable phylogenetics through input preprocessing, by Roberto Blanco, Elvira Mayordomo, Esther Montes, Rafael Mayo and Angelines Alberto. In: M. P. Rocha, F. Fernández Riverola, F. Shatkay and J. M. Corchado Rodríguez (eds.), Proceedings of the 4th International Workshop on Practical Applications of Computational Biology and Bioinformatics (IWPACBB 2010). Guimarães, Portugal, June 2010. Advances in Intelligent and Soft Computing, vol. 74, pp. 123-130.

• Computational phylogenetics for human mitochondrial DNA, by Roberto Blanco. Master’s thesis, Universidad de Zaragoza, 2009.

• ZARAMIT: a system for the evolutionary study of human mitochondrial DNA, by Roberto Blanco and Elvira Mayordomo. In: Proceedings of the 3rd International Workshop on Practical Applications of Computational Biology and Bioinformatics (IWPACBB 2009). Salamanca, Spain, June 2009. Lecture Notes in Computer Science, vol. 5518, pp. 1139-1142.

• Definición y prototipo de herramienta de análisis filogenético para el estudio del ADNmt humano, by Roberto Blanco. Master’s thesis, Universidad de Zaragoza, 2008.