I am a full professor at the IMDEA Software Institute. Before that, I completed a Ph.D. at the Computer Science Department at Stanford University in 2007, where I worked with Zohar Manna. I did a short post-doc with Luca de Alfaro in 2007 before joining IMDEA. In 2012 I was granted tenure and promoted to Associate Professor at the IMDEA Software Institute and in 2023 I was promoted to Full Professor.

I graduated with a degree in Telecommunication Engineering from Universidad Politécnica de Madrid in 1999. Then I moved to Stanford where I obtained a M.S. in Computer science in 2001 and then a Ph.D. in Computer Science in 2006.

I do research in formal methods, and in general in rigorous techniques for the design, implementation, verification and understanding of computational devices, mostly software. Most of my work is rooted in the areas of automata, game theory and logic, and particularly in the intersection of these areas.

Interests
  • Formal Methods
  • Logic, Game Theory and Automata Theory
  • Reactive Synthesis Modulo Theories
  • Logics for Hyperproperties
  • Foundations of Blockchain and Smart contracts
  • Neurosymbolic Formal Methods
Education

  • PhD in Computer Science, 2007

    Stanford University

  • M.S in Computer Science, 2001

    Stanford University

  • M.Eng in Telecomunication Engineering, 1998

    Universidad Politécnica de Madrid

News

Recent Publications

DBLP       Google Scholar       ORCID

Andoni Rodríguez, Guy Amir, Davide Corsi, César Sánchez, Guy Katz (2025). Shield Synthesis for LTL Modulo Theories. Proc. of the 39th AAAI Conf. on Artificial Intelligence (AAAI'25), pp5037-5044, AAAI Press, 2025.

PDF Cite URL

Alberto Bombardelli, Laura Bozzelli, César Sánchez, Stefano Tonetta (2024). Unifying Asynchronous Logics for Hyperproperties. Proc. of the 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'24), pp. 14:1-14:18, LIPIcs vol 323, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2024.

PDF Cite DOI URL

Davide Corsi, Guy Amir, Andoni Rodríguez, Guy Katz, César Sánchez, Roy Fox (2024). Verification-Guided Shielding for Deep Reinforcement Learning. Reinforcement Learning Journal, vol 4, pp. 1759-1780, 2024.

PDF Cite URL

Margarita Capretto, Martín Ceresa, Felipe Gorostiaga, Fernando Macías, Paloma Pegregal, César Sánchez (2024). Offchain Runtime Verification (for The Tezos Blockchain). Computer Security. ESORICS 2024 International Workshops, vol 15263 of LNCS, Springer, 2025.

PDF Cite URL

Raik Hipler, Hannes Kallwies, Martin Leucker, César Sánchez (2024). General Anticipatory Runtime Verification. Proc. of the 36th International Conference on Computer Aided Verification (CAV'24), vol 15682 of LNCS, pp. 133-255. Springer, Cham, 2024.

PDF Cite DOI URL

See all publications

Service

Some recent service includes:

  • PC member of CAV'25 37th International Conference on Computer Aided Verification
  • PC member of ATVA'24 22nd International Symposium on Automated Technology for Verification and Analysis
  • PC member of TACAS'24 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
  • PC member of DAPPS'23 5th IEEE International Conference on Decentralized Applications and Infrastructures
  • PC member of TACAS'23 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
  • PC member of RV'23 23rd International Conference on Runtime Verification
  • PC member of PROLE’22 21st Jornadas de PROgramación y LEnguajes
  • PC member of FMBC’22 4th International Workshop on Formal Methods for Blockchains
  • PC member of DAPSS’22 2022 IEEE International Conference on Decentralized Applications and Infrastructures
  • PC member of VORTEX’22 5th Workshop on Verification and mOnitoring at Runtime EXecution
  • PC member of ATVA’22 20th International Symposium on Automated Technology for Verification and Analysis
  • PC member of TACAS’22 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Open Positions

I am looking for talented researchers (research interns, PhD students, and postdocs) to join my research group at the IMDEA Software Institute to work on Hyperproperties, runtime verification, reactive synthesis, formal methods and smart contract reasoning. In case you are interested, contact me via email.

Contact