José Fragoso Santos

Welcome to my home page. I am an Assistant Professor in the Department of Computer Science and Engineering at Instituto Superior Técnico, and a member of INESC-ID, where I conduct my research as a member of the SAT group.

My goal, both as a researcher and as an educator, is to contribute to the effort to embed formal methods into the heart of the software development process, grounding it on well-established mathematical principles and certified analyses and tools. So far, I have been mainly focused on Web programs written in JavaScript. At Imperial, I led the development of JaVerT, the first separation-logic-based tool for JavaScript analysis and testing. The JaVerT project has been highly successful thus far, gathering interest from researchers in both industry and academia. JaVerT was awarded a FB research award and the JaVerT team is currently working with R&D engineers at Amazon, using JaVerT to verify critical components of the JavaScript implementation of the AWS Encryption SDK.

Service:

• PLDI'20 (External Review Committee)
• OOPSLA'20 (Program Committee)
• IJCAI'20 (Program Committee)

[ECOOP'20]	Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, Philippa Gardner: A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications, in European Conference on Object-Oriented Programming (ECOOP 2020).
[PLDI'20]	José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, Philippa Gardner: Gillian, Part I: A Multi-language Platform for Symbolic Execution, in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020).
[POPL'19]	José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, Philippa Gardner: JaVerT 2.0: Compositional Symbolic Execution for JavaScript, in Symposium on Principles of Programming Languages (POPL 2019).
[PPDP'18]	José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby, Philippa Gardner: Symbolic Execution for JavaScript, in Symposium on Principles and Practice of Declarative Programming (PPDP 2018).
[POPL'18]	José Fragoso Santos, Petar Maksimović, Daiva Naudžiuniene, Thomas Wood, Philippa Gardner: JaVerT: JavaScript Verification Toolchain, in Symposium on Principles of Programming Languages (POPL 2018).
[CADE'17]	José Fragoso Santos, Philippa Gardner, Petar Maksimovic, Daiva Naudžiuniene: Towards Logic-Based Verification of JavaScript Programs, in International Conference on Automated Deduction (CADE 2017).
[JCS'16]	Zhengqin Luo, José Fragoso Santos, Ana Almeida-Matos, Tamara Rezk: Mashic compiler: Mashup sandboxing based on inter-frame communication, in Journal of Computer Security.
[APLAS'16]	Azalea Raad, José Fragoso Santos, Philippa Gardner: DOM: Specification and Client Reasoning, in Asian Symposium on Programming Languages and Systems (APLAS 2016).
[TGC'15(a)]	José Fragoso Santos, Thomas Jensen, Alan Schmitt, Tamara Rezk: Hybrid Typing of Secure Information Flow in a JavaScript-like Language, in Symposium on Trustworthy Global Computing (TGC 2015).
[TGC'15(b)]	José Fragoso Santos, Ana Almeida Matos, and Tamara Rezk: Modular Monitor Extensions for Information Flow Security in JavaScript, in Symposium on Trustworthy Global Computing (TGC 2015).
[TGC'14]	Ana Almeida Matos, José Fragoso Santos, Tamara Rezk: An Information Flow Monitor for a Core of DOM - Introducing references and live primitives, in Symposium on Trustworthy Global Computing (TGC 2014).
[SEC'14]	José Fragoso Santos, Tamara Rezk: An Information Flow Monitor-Inlining Compiler for Securing a Core of JavaScript, in IFIP International Information Security and Privacy Conference (IFIP SEC 2014).
[PLAS'12]	Ana Almeida Matos, José Fragoso Santos: Typing Illegal Information Flows as Program Effects, in Workshop on Programming Languages and Analysis for Security (PLAS 2012).
[IROS'10]	José Fragoso Santos, Alexandre Bernardino, José Santos-Victor: Sensor Based Self Calibration of the iCub’s Head, in International Conference on Intelligent Robots and Systems (IROS 2010).
[IWIL'08]	José Fragoso Santos, Vasco Manquinho: Learning Techniques for Pseudo-Boolean Solving, in International Workshop on the Implementation of Logics (IWIL 2008).

[PhD'14]	José Fragoso Santos: Enforcing Secure Information Flow in Client-side Web Applications, PhD thesis, University of Nice Sophia Antipolis, 2014 .
[MSc'08]	José Fragoso Santos: Learning Techniques for Pseudo-Boolean Solving and Optimization, Master's thesis, Instituto Superior Técnico, Universidade de Lisboa, 2008.

A Live JavaScript Specification (joint with David M. Matos)

A Formal Semantics of JavaScript Regular Expressions

Code-Stepping Regular Expressions in the Browser

A Reference Implementation of Web Workers

Compositional Symbolic Execution for Typescript

A Semi-Automatic Separation-Logic Solver

A First-Order Solver for Program Analysis

Understanding the Evolution of the Web

Scalable Symbolic Execution for Preact Web Applications

Gabriela Cunha Sampaio

PhD Computer Science, Imperial College London
Joint supervision with P. Gardner.

Pedro Lopes

Project: Study and mitigation of XSS attacks based on WebAssembly code vulnerabilities
MSc. Information Systems and Computer Engineering, IST
Joint supervision with N. Santos.

Carolina Costa

Project: Sensitive data tracking for emerging web pages featuring WebAssembly code
MSc. Information Systems and Computer Engineering, IST
Joint supervision with N. Santos.

André Ribeiro

Project: A JavaScript Information Flow Monitor for Symbolic Testing
MSc. Telecommunications and Informatics Engineering, IST
Joint supervision with A. Almeida Matos.

Eric Wenhao Ruan Zhu

Project: Multi-theory First Order Solver for Program Analysis and Verification
MEng Joint Mathematics and Computing, Imperial College London
Joint supervision with Philippa Gardner and P. Maksimovic.

Priyanka Shah

Project: Compiling JavaScript Regular Expressions
MEng Computing, Imperial College London
Joint supervision with Philippa Gardner and P. Maksimovic.

Si Wei Tan

Project: Trusted Infrastructure for JavaScript (ES5) Analysis
MEng Computing, Imperial College London
Joint supervision with Philippa Gardner and P. Maksimovic.

Radu-Andrei Szasz (IBM Project Prize)

Project: Typing JavaScript Through Symbolic Execution
MEng Computing, Imperial College London
Joint supervision with Philippa Gardner and P. Maksimovic.

Beatrix de Wilde

Project: Towards Automatic Verification of JavaScript Programs
MEng Computing, Imperial College London
Joint supervision with Philippa Gardner and P. Maksimovic.

Iván Matellanes

Project: A Verification Tool for JavaScript.
MSc Computing, Imperial College London
Joint supervision with Philippa Gardner and P. Maksimovic.

Analysis and Synthesis of Algorithms (ASA)

Object Oriented Programming (PO)

Tutorial Sheet
Slides
Tutorial Sheet - Solutions

Aula 1
Aula 2
Aula 3
Aula 4
Aula 5
Aulas 6&7
Aula 8
Aula 9
Aula 10
Aula 11
Aula 12
Aula 13
Aula 14
Aula 15
Aula 16
Aula 17
Aula 18
Aula 19
Aula 20
Aula 21