???global.info.a_carregar???
The main goal of my research is the verification, specification, and testing of JavaScript applications with a particular focus on client-side Web applications that interact with the DOM API. I am primarily interested in the enforcement of security properties (such as secure information flow) and the automated verification of functional correctness properties of critical JavaScript code. To achieve these goals, I make use of program analyses and instrumentation techniques well established for static languages, advancing them to the setting of a highly complex, dynamic language, such as JavaScript. My research goes from theory to practice delivering industrial-strength tools that enable JavaScript programmers to better test, verify, and understand their code. As JavaScript is the key element of the internet of today, these tools can significantly impact the quality of current web applications, potentially improving the experience of users on a global scale.
Ler resumo completo ↓
Identificação

Identificação pessoal

Nome completo
José Fragoso Santos

Nomes de citação

  • José Fragoso Santos

Identificadores de autor

Ciência ID
1319-F56C-0E1E
ORCID iD
0000-0001-5077-300X

Domínios de atuação

  • Ciências Exatas - Ciências da Computação e da Informação

Idiomas

Idioma Conversação Leitura Escrita Compreensão Peer-review
Francês Utilizador independente (B2) Utilizador independente (B2) Utilizador independente (B2) Utilizador independente (B2)
Inglês Utilizador proficiente (C1) Utilizador proficiente (C1) Utilizador proficiente (C1) Utilizador proficiente (C1)
Formação
Grau Classificação
2014
Concluído
 Doctorat en Informatique (Doutoramento)
Université de Nice Sophia Antipolis, França
"Enforcing Secure Information Flow in Client-Side Web Applications" (TESE/DISSERTAÇÃO)
 Mention Très Honorable
2008
Concluído
 Mestrado em Engenharia Informática e de Computadores (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
"Learning Techniques: From SAT to Pseudo-Boolean Optimization" (TESE/DISSERTAÇÃO)
 18
2006
Concluído
 Licenciatura em Ciências da Engenharia Informática e de Computadores (Licenciatura)
Universidade de Lisboa Instituto Superior Técnico, Portugal
"Learning Techniques: From SAT to Pseudo-Boolean Optimization" (TESE/DISSERTAÇÃO)
 16
Percurso profissional

Ciência

Categoria Profissional
Instituição de acolhimento 		Empregador
2019/09/01 - Atual Investigador (Investigação) Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
2015/03/01 - 2019/08/31 Pós-doutorado (Investigação) Imperial College London, Reino Unido
2009/08/01 - 2010/08/01 Estagiário de Investigação (Investigação) Instituto de Telecomunicações, Portugal
2009/01/01 - 2009/06/30 Estagiário de Investigação (Investigação) Laboratório de Robótica e Sistemas de Engenharia, Portugal
2007/10/01 - 2008/10/31 Estagiário de Investigação (Investigação) Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal

Docência no Ensino Superior

Categoria Profissional
Instituição de acolhimento 		Empregador
2019/09/01 - Atual Professor Auxiliar (Docente Universitário) Universidade de Lisboa Instituto Superior Técnico, Portugal
Projetos

Projeto

Designação Financiadores
2017/01/01 - 2019/08/31 REMS: Rigorous Engineering for Mainstream Systems
EP/K008528/1
Investigador
2013/09/30 - 2016/12 Certified Verification of Client-Side Web Programs
EP/K032089/1
 UK Research and Innovation
2009/08/01 - 2010/08/01 KLog - Logics for Security
PTDC/MAT/68723/2006
Bolseiro de Mestrado
2009/01/01 - 2009/07/31 BIO-LOOK - Biomimetic Oculomotor Control for Humanoid Robots
PTDC/EEA-ACR/71032/2006
2007/09/01 - 2008/09/01 BSOLO - Boolean constraint SOLving and Optimization
PTDC/EIA/76572/2006
Bolseiro de Iniciação Científica
Produções

Publicações

Artigo em conferência
  1. Petar Maksimovic; Sacha Elie Ayoun; José Fragoso Santos; Philippa Gardner. "Gillian, Part II: Real-World Verification for JavaScript and C". Trabalho apresentado em Computer Aided Verification-33rd International Conference, CAV, 2021.
    Aceite para publicação
  2. Gabriela Sampaio; José Fragoso Santos; Petar Maksimovic; Philippa Gardner. "A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications". Trabalho apresentado em European Conference on Object Oriented Programming (ECOOP), 2020.
  3. José Fragoso Santos; Petar Maksimovic; Sacha Elie Ayoun; Philippa Gardner. "Gillian, Part I: A Multi-language Platform for Symbolic Execution". Trabalho apresentado em Programming Language Design and Implementation (PLDI), London, 2020.
  4. Santos, José. "Symbolic Execution for JavaScript". 2018.
    10.1145/3236950.3236956
  5. Matos, A.A.; Santos, J.F.. "Typing illegal information flows as program effects". 2012.
    10.1145/2336717.2336718
  6. Santos, J.; Bernardino, A.; Santos-Victor, J.. "Sensor-based self-calibration of the iCub's head". 2010.
    10.1109/IROS.2010.5651275
  7. Santos, J.; Manquinho, V.. "Learning techniques for pseudo-boolean solving". 2008.
Artigo em revista
  1. "The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets". Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021): https://drops.dagstuhl.de/opus/volltexte/2021/15322/.
    10.4230/LIPICS.CP.2021.31
  2. Fragoso Santos, José (1319-F56C-0E1E). "JaVerT 2.0: Compositional Symbolic Execution for JavaScript". Proc. ACM Program. Lang. 3 POPL (2019): 66:1-66:31. http://doi.acm.org/10.1145/3290379.
    10.1145/3290379
  3. Santos, José. "JaVerT: JavaScript Verification Toolchain". Proc. ACM Program. Lang. 2 POPL (2017): 50:1-50:33. http://doi.acm.org/10.1145/3158138.
    10.1145/3158138
  4. Luo, Z.; Santos, J.F.; Matos, A.A.; Rezk, T.. "Mashic compiler: Mashup sandboxing based on inter-frame communication". Journal of Computer Security 24 1 (2016): 91-136. http://www.scopus.com/inward/record.url?eid=2-s2.0-84960408868&partnerID=MN8TOARS.
    10.3233/JCS-160542
Capítulo de livro
  1. "Hybrid Information Flow Control for Low-Level Code". 141-159. Springer International Publishing, 2021.
    10.1007/978-3-030-92124-8_9
Livro
  1. Santos, J.F.; Gardner, P.; Maksimovic, P.; Naudžiuniene, D.. Towards logic-based verification of javascript programs. 2017.
    10.1007/978-3-319-63046-5_2
  2. Santos, J.F.; Rezk, T.; Matos, A.A.. Modular monitor extensions for information flow security in javascript. 2016.
    10.1007/978-3-319-28766-9_4
  3. Fragoso Santos, J.; Jensen, T.; Rezk, T.; Schmitt, A.. Hybrid typing of secure information flow in a JavaScript-like language. 2016.
    10.1007/978-3-319-28766-9_5
  4. Raad, A.; Santos, J.F.; Gardner, P.. DOM: Specification and client reasoning. 2016.
    10.1007/978-3-319-47958-3_21
  5. Fragoso Santos, J.; Rezk, T.. An information flow monitor-inlining compiler for securing a core of Javascript. 2014.
  6. Almeida-Matos, A.; Santos, J.F.; Rezk, T.. An information flow monitor for a core of DOM: Introducing references and live primitives. 2014.
    10.1007/978-3-662-45917-1_1
Distinções

Prémio

2018 Research Award on Continuous Reasoning Research (USD 50K)
Facebook Inc, Estados Unidos