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
  • Formal Methods for Neurosymbolic computing
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, Irfansha Shaik, Davide Corsi, Roy Fox, César Sánchez (2025). Explanations for Unrealizability of Infinite-State Safety Shields. Proc. of the 22nd Int’l Conf. on Principles of Knowledge Representation and Reasoning, KR in Planning and Scheduling (KR'25), pp858-868, 2025.

PDF Cite DOI URL

Davide Corsi, Kaushik Mallik, Andoni Rodríguez, César Sánchez (2025). Efficient Dynamic Shielding for Parametric Safety Specifications. Proc. of the 23rd Int’l Symp. on Automated Technology for Verification and Analysis (ATVA'25), pp157-179, vol 16145 of LNCS, Springer 2025.

PDF Cite DOI URL

Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sanchez, César Sánchez (2025). A Secure Sequencer and Data Availability Committee for Rollups. Proc. of the 2025 ACM SIGSAC Conf. on Computer and Communications Security (CCS'25), pp2129-2143, ACM 2025.

PDF Cite DOI URL

Andoni Rodríguez, Felipe Gorostiaga, César Sánchez (2025). Counter Example Guided Reactive Synthesis for LTL Modulo Theories. Proc. of the 37th Int’l Conf. on Computer Aided Verification (CAV'25), Part IV, pp224-248, vol 15934 of LNCS, Springer 2025.

PDF Cite DOI URL

Matias Brizzio, Felipe Gorostiaga, César Sánchez (2025). Mode-Based Reactive Synthesis. Proc. of the 17th Int’l Symp. on NASA Formal Methods (NFM'25), pp116-137, vol 15682 of LNCS, Springer 2025.

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 Neurosymbolic computing, hyperproperties, runtime verification, reactive synthesis, formal methods and smart contract reasoning. In case you are interested, contact me via email.

Contact