César Sánchez

César Sánchez

Research Professor

IMDEA Sofware Institute

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
  • Logics for Hyperproperties
  • Foundations of Blockchain and Smart contracts
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

Luis Miguel Danielsson, César Sánchez (2023). Decentralized Stream Runtime Verification for Timed Asynchronous Networks. IEEE Access, pp 84091-84112. IEEE, 2023.

PDF Cite DOI URL

Felipe Gorostiaga, César Sánchez (2023). Runtime verification of real-time event streams using the tool HStriver. Formal Methods in Systems Desing. Springer, 2023.

PDF Cite DOI URL

Felipe Gorostiaga, Paloma Pedregal, César Sánchez (2023). A Stream Runtime Verification Tool with Nested and Retroactive Parametrization. Proc. of the 23nd Int’l Conference on Runtime Verification (RV'23), vol 14245 of LNCS, pp. 351-362. Springer, Cham, 2023.

PDF Cite DOI URL

Andoni Rodriguez, César Sánchez (2023). Boolean Abstractions for Realizabilty Modulo Theories. Proc. of the 35th International Conference on Computer Aided Verification (CAV'23), vol 13966 of LNCS, pp. 1-24. Springer, Cham, 2023.

PDF Cite DOI URL

Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez (2023). Bounded Model Checking for Asynchronous Hyperproperties. Proc. of the 29th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), vol 13993 of LNCS, pp. 29-46. Springer, Cham, 2023.

PDF Cite DOI URL

See all publications

Service

Some recent service includes:

  • 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