César Sánchez
César Sánchez
Ph.D. Stanford University, 2007
Associate Research Professor

In January 2008, I became a researcher at Madrid Institute for Advanced Studies in Software Development Technologies (IMDEA-Software).
In November 2013, I was promoted to Associate Research Professor at IMDEA Software Institute.

Research

Research Interests

My main research interest is the study of mathematically rigorous approaches to understanding and developing complex software, particularly using reactive systems. More general, I am interested in applications of logic to computer science, and formal methods for the design, analysis and verification of systems. Some particular topics include:

Selected Publications

  1. Montserrat Hermo, Paqui Lucio and César Sánchez. Tableaux for Realizability of Safety Specifications, In Proc. of the 25th International Symposium on Formal Methods (FM'23) vol 14000 of LNCS, pp. 495--513. Springer, 2023. DOI: 10.1007/978-3-031-19992-9_8 [Abstract] [BiB] [PDF]
  2. Felipe Gorostiaga, Sebastian Zudaire, César Sánchez, Gerardo Schneider and Sebastian Uchitel. Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification, In Proc. of the 11th Int'l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2022). Verification Principles. Part I vol. 13701 of LNCS, pp 397-414. Springer, 2022. DOI: 10.1007/978-3-031-19849-6_23. [Abstract] [BiB] [PDF]
  3. Hannes Kallwies, Martin Leucker and César Sánchez. Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions, In Proc. of 20th Int'l Symp. on Automated Technology for Verification and Analysis (ATVA'22) vol 13505 of LNCS, pp. 117-134. Springer, 2022. DOI: 10.1007/978-3-031-19992-9_8 [Abstract] [BiB] [PDF]
  4. Margarita Capretto, Martin Ceresa and César Sánchez. Transaction Monitoring of Smart Contracts, In Proc. of the 22nd Int'l Conference on Runtime Verification (RV'22) vol 13498 of LNCS, pp. 162-180. Springer, 2022. DOI: 10.1007/978-3-031-17196-3_9 [Abstract] [BiB] [PDF]
  5. Laura Bozzelli, Adriano Peron and César Sánchez. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties, In Proc. of CONCUR 2022 vol. 243 of Leibniz International Proceedings in Informatics (LIPIcs), pp 27:1--27:16, Schloss Dagstuhl Leibniz-Zentrum für Informatik 2022. DOI: 10.4230/LIPIcs.CONCUR.2022.27. [Abstract] [BiB] [PDF]
  6. Margarita Capretto, Martin Ceresa, , and César Sánchez. Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers, In Proc. of the 2022 IEEE Int'l Conf. on Blockchain (Blockchain'22), pp-87-96, IEEE, 2022. DOI: 10.1109/Blockchain55522.2022.00022. [Abstract] [BiB] [PDF]
  7. Martin Ceresa and César Sánchez. Multi: A Formal Playground for Multi-Smart Contract Interaction, In Proc. of the 4th Int'l Workshop on Formal Methods for Blockchains (FMBC 2022) vol. 105 of Open Access Series in Informatics (OASIcs), pp 5:1--5:16. Schloss Dagstuhl -- Leibniz-Zentrum für Informatik, 2022. DOI: 10.4230/OASIcs.FMBC.2022.5. [Abstract] [BiB] [PDF]
  8. Hannes Kallwies, Martin Leucker, César Sánchez and Torben Scheffel. Anticipatory Recurrent Monitoring with Uncertainty and Assumptions, In Proc. of the 22nd Int'l Conference on Runtime Verification (RV'22) vol 13498 of LNCS, pp. 181-199. Springer, 2022. DOI: 10.1007/978-3-031-17196-3_10 [Abstract] [BiB] [PDF]
  9. Felipe Gorostiaga and César Sánchez. Monitorability of Expressive Verdicts, In Proc. of the 14th Int'l Symp. on NASA Formal Methods (NFM'22) vol 13260 of LNCS, pp 693-712. Springer, 2022. DOI: 10.1007/978-3-031-06773-0_37. [Abstract] [BiB] [PDF]
  10. Felipe Gorostiaga and César Sánchez. Nested Monitors: Monitors as Expressions to Build Monitors, In Proc. of the 21st Int'l Conference on Runtime Verification (RV'21) vol 12974 of LNCS, pp 164-183. Springer, 2021. DOI: 10.1007/978-3-030-88494-9_9. [Abstract] [BiB] [PDF]
  11. César Sánchez. Synchronous and Asynchronous Stream Runtime Verification, In Proc. of the 5th ACM Int'l Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21) ACM, pp 5-7, 2021. DOI: 10.1145/3464974.3468453. [Abstract] [BiB] [PDF]
  12. Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner and César Sánchez. A Temporal Logic for Asynchronous Hyperproperties, In Proc. of the 33rd Int'l Conf. on Computer Aided Verification (CAV'21), Part I vol 12759 of LNCS, pp 694-717. Springer, 2021. DOI: 10.1007/978-3-030-81685-8_33. [Abstract] [BiB] [PDF]
  13. Felipe Gorostiaga and César Sánchez. HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams, In Proc. of the 24th Int'l Symp. on Formal Methods (FM'21) vol 13047 of LNCS, pp 563-580. Springer, 2021. DOI: 10.1007/978-3-030-90870-6_30. [Abstract] [BiB] [PDF]
  14. Sebastian Zudaire, Felipe Gorostiaga, César Sánchez, Gerardo Schneider and Sebastian Uchitel. Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions, In Proc. of the {IEEE} Int'l Conf. on Robotics and Automation, (ICRA'21). pp6824-6830, IEEE, 2021. DOI: 10.1109/ICRA48506.2021.9561671. [Abstract] [BiB] [PDF]
  15. Laura Bozzelli, Adriano Peron and César Sánchez. Asynchronous Extensions of HyperLTL, In Proc. of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'21). pp1-13, IEEE. DOI: 10.1109/LICS52264.2021.9470583. [Abstract] [BiB] [PDF]
  16. Felipe Gorostiaga and César Sánchez. Stream runtime verification of real-time event streams with the Striver language, In International Journal on Software Tools for Technology Transfer pp 157-183. Springer, 2021. DOI: 10.1007/s10009-021-00605-3. [Abstract] [BiB] [PDF]
  17. Felipe Gorostiaga and César Sánchez. HLola: A very functional tool for extensible Stream Runtime Verification, In Proc. of the 27th Intl Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21). Part II vol 12652 of LNCS, pp 349-356. Springer, 2021. DOI: 10.1007/978-3-030-72013-1_18. [Abstract] [BiB] [PDF]
  18. Tzu Han Hsu, César Sánchez and Borzoo Bonakdarpour. Bounded Model Checking for Hyperproperties, In Proc. of the 27th Intl Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21). Part I vol 12651 of LNCS, pp 94-112. Springer, 2021. DOI: 10.1007/978-3-030-72016-2_6. [Abstract] [BiB] [PDF]
  19. Sandro Stucki, César Sánchez and Gerardo Schneider and Borzoo Bonakdarpour. Gray-Box Monitoring of Hyperproperties with an Application to Privacy, In Formal Methods in Systems Desing p1-34. Springer, 2021. DOI: https://doi.org/10.1007/s10703-020-00358-w. [Abstract] [BiB] [PDF]
  20. Gordon Pace, César Sánchez and Gerardo Schneider. Reliable Smart Contracts, In Proc. of the 9th Int'l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2020). Verification. Part III vol 12478 of LNCS, pp3-8. Springer, 2020. DOI: 10.1007/978-3-030-61467-6_1. [Abstract] [BiB] [PDF]
  21. Martin Ceresa, Felipe Gorostiaga and César Sánchez. Declarative Stream Runtime Verification (hLola), In Proc. of the 18th Asian Symposium on Programming Languages and Systems (APLAS 2020) vol 12470 of LNCS, pp 25-43. Springer, 2020. DOI: 10.1007/978-3-030-64437-6_2. [Abstract] [BiB] [PDF]
  22. Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz and Alexander Schramm. Runtime verification of real-time event streams under non-synchronized arrival, Software Quality Journal 28(2):745-787. DOI: 10.1007/s11219-019-09493-y. [Abstract] [BiB] [PDF]
  23. Borzoo Bonakdarpour, Pavithra Prabhakar and César Sánchez. Model Checking Timed Hyperproperties in Discrete-Time Systems, In Proc. of the 12th International NASA Symposium on Formal Methods (NFM 2020) vol 12229 of LNCS, pp 311-328, Springer, 2020. DOI: 10.1007/978-3-030-55754-6_18. [Abstract] [BiB] [PDF]
  24. Felipe Gorostiaga, and César Sánchez. Unifying the Time-Event Spectrum for Stream Runtime Verification, In Proc. of the 20th International Conference on Runtime Verification (RV 2020) vol 12399 of LNCS, pp 462-481, Springer, 2020. DOI: 10.1007/978-3-030-60508-7_26. [Abstract] [BiB] [PDF]
  25. César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, , Yli&‌egrave;s Falcone, Adrian Francalanza, Srdan Krstic, João M. Lourenço, Dejan Nickovic, Gordon Pace, José Rufino, Julien Signoles, Dmitriy Traytel and Alexander Weiss. A survey of challenges for runtime verification from advanced application domains (beyond software), Formal Methods in Systems Design 54(3):279-335 (2019). DOI: 10.1007/s10703-019-00337-w. [Abstract] [BiB] [PDF]
  26. Norine Coenen, Bernd Finkbeiner, César Sánchez and Lender Tentrup. Verifying Hyperliveness, In Proc. of the 31st Intl Conf. on Computer Aided Verification (CAV'19) vol 11561 of LNCS, pp 121-139, Springer 2019 DOI: 10.1007/s10703-019-00337. [Abstract] [BiB] [PDF]
  27. Sandro Stucki, César Sánchez, Gerardo Schneider and Borzoo Bonakdarpour. Gray-Box Monitoring of Hyperproperties, In Proc. of Formal Methods - The Next 30 Years - Third World Congress, (FM'19) vol 11800 of LNCS, pp 496-424, Springer, 2019 DOI: 10.1007/978-3-030-30942-8_25. [Abstract] [BiB] [PDF]
  28. Luis Miguel Danielsson and César Sánchez. Decentralized Stream Runtime Verification, In Proc. of the 19th Int'll Conf. on Runtime Verification (RV 19) vol 11757 of LNCS, pp 185-201, Springer, 2019 DOI: 10.1007/978-3-030-32079-9_11. [Abstract] [BiB] [PDF]
  29. Martin Leucker and César Sánchez, , Malte Schmitzand Daniel Thoma. Runtime Verification for Timed Event Streams with Partial Information, In Proc. of the 19th Int'l Conf. on Runtime Verification (RV'19) vol 11757 of LNCS, pp 273-291, Springer, 2019 DOI: 10.1007/978-3-030-32079-9_16. [Abstract] [BiB] [PDF]
  30. Raúl Pardo, César Sánchez and Gerardo Schneider. Timed Epistemic Knowledge Bases for Social Networks, In Proc. of the 22nd International Symposium on Formal Methods, (FM'18) vol 10951 of LNCS, pp 185-202, Springer, 2018 DOI: 10.1007/978-3-319-95582-7_11. [Abstract] [BiB] [PDF]
  31. Borzoo Bonakdarpour, César Sánchez and Gerardo Schneider. Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification, In Proc. of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLa'18), Part II vol 11245 of LNCS, pp 8-27, Springer, 2018 DOI: 10.1007/978-3-030-03421-4_2. [Abstract] [BiB] [PDF]
  32. Pablo Chico de Guzmán, Felipe Gorostiaga and César Sánchez. Pipekit: A Deployment Tool with Advanced Scheduling and Inter-Service Communication for Multi-Tier Applications, In Proc. of the 22nd International Symposium on Formal Methods, (FM'18) vol 10951 of LNCS, pp 185-202, Springer, 2018 DOI: 10.1007/978-3-319-95582-7_11. [Abstract] [BiB] [PDF]
  33. César Sánchez, Gerardo Schneider and Martin Leucker. Reliable Smart Contracts: State-of-the-Art, Applications, Challenges and Future Directions, In Proc. of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'18), Part IV vol 11247 of LNCS, pp 275-279, Springer, 2018 10.1007/978-3-030-03427-6_21. [Abstract] [BiB] [PDF]
  34. Yli&‌egrave;s Falcone, César Sánchez. Introduction to the special issue on Runtime Verification, Formal Methods in Systems Design 53(1):1-5 (2018). DOI: 10.1007/s10703-018-0320-4 [Abstract] [BiB] [PDF]
  35. Christian Colombo, Yli&‌egrave;s Falcone, Martin Leucker, Giles Reger, César Sánchez, Gerardo Schneider and Volker Stolz. COST Action IC1402 Runtime Verification Beyond Monitoring, In Proc. of the 18th International Conference on Runtime Verification (RV'18) vol 11237 of LNCS, pp 18-26, Springer, 2018. DOI: 10.1007/978-3-030-03769-7_2. [Abstract] [BiB] [PDF]
  36. César Sánchez. Online and Offline Stream Runtime Verification of Synchronous Systems, In Proc. of the 18th International Conference on Runtime Verification (RV'18) vol 11237 of LNCS, pp 138-163, Springer, 2018. DOI: 10.1007/978-3-030-03769-7_9. [Abstract] [BiB] [PDF]
  37. Felipe Gorostiaga and César Sánchez. Striver: Stream Runtime Verification for Real-Time Event-Streams, In Proc. of the 18th International Conference on Runtime Verification (RV'18) vol 11237 of LNCS, pp 282-298, Springer, 2018. DOI: 10.1007/978-3-030-03769-7_16. [Abstract] [BiB] [PDF]
  38. Pablo Chico de Guzmán, Felipe Gorostiaga and César Sánchez. i2kit: A Deployment Tool with the Simplicity of Containers and the Security of Virtual Machines, In Proc. of the 19th International Conference on Web Information Systems Engineering, (WISE 2018) Part I, vol 11233 of LNCS, pp 81-95, Springer, 2019 10.1007/978-3-030-02922-7_6. [Abstract] [BiB] [PDF]
  39. Adrian Francalanza, Jorge A. Pérez and César Sánchez. Runtime Verification for Decentralised and Distributed Systems, Lectures on Runtime Verification 2018:176-210. DOI: 10.1007/978-3-319-75632-5_6. [Abstract] [BiB] [PDF]
  40. Laura Bozzelli and César Sánchez. Visibly Linear Temporal Logic, Journal of Automated Reasoning (62)2:177-220, 2018. DOI: 10.1007/s10817-017-9410-z. [Abstract] [BiB] [PDF]
  41. Laura Bozzelli and César Sánchez. Foundations of Boolean Stream Runtime Verification, Theoretical Computer Science 631:118-138(2016). DOI: 10.1016/j.tcs.2016.04.019. [Abstract] [BiB] [PDF]
  42. Raúl Pardo, Ivana Kellyerova,César Sánchez and Gerardo Schneider. Specification of Evolving Privacy Policies for Online Social Networks, In Proc. of the 23rd Intl Symp. on Temporal Representation and Reasoning (TIME 2016), pp 77-79, IEEE Computer Society, 2014. ISBN: 978-1-5090-3825-1. DOI: 10.1109/TIME.2016.15. [Abstract] [BiB] [PDF]
  43. Bernd Finkbeiner, Markus N. Rabe and César Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL*, In Proc. of the 27th Intl Conf. on Computer Aided Verification (CAV'15), vol 9206 of LNCS, pp 30-48, Springer, 2015. ISBN: 978-3-319-21689-8. [Abstract] [BiB] [PDF]
  44. Alejandro Sánchez and César Sánchez. Parametrized invariance for infinite state processes, In Acta Informatica, 52(?), pp 1-33. ISSN: 0001-5903. DOI: 10.1007/s00236-015-0222-5. [Abstract] [BiB] [PDF]
  45. Laura Bozzelli and César Sánchez. Visibly rational expressions, In Acta Informatica 51(1): 25-49 (2014). [Abstract] [BiB] [PDF]
  46. Alejandro Sánchez and César Sánchez. Formal Verification of Skiplists with Arbitrary Many Levels, In Proc. of 12th Int'l Symp. on Automated Technology for Verification and Analysis (ATVA'14), vol 8837 of LNCS, pp 314-329, Springer, 2014. ISBN 978-3-319-11935-9. [Abstract] [BiB] [PDF]
  47. Laura Bozzelli and César Sánchez. Visibly Linear Temporal Logic, In Proc. of the 7th Int'l Joint Conf. on Automated Reasoning (IJCAR'14), vol 8562 of LNCS, pp 418-433, Springer, 2014. ISBN 978-3-319-08586-9. [Abstract] [BiB] [PDF]
  48. Alejandro Sánchez and César Sánchez. LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes, In Proc. of the 26th Int'l Conf. on Computer Aided Verification (CAV'14), vol 8559 of LNCS, pp 620-627, Springer, 2014. ISBN 978-3-319-08866-2 [Abstract] [BiB] [PDF]
  49. Alejandro Sánchez and César Sánchez. Parametrized Verification Diagrams, In Proc. of the 21st Int'l Symp. on Temporal Representation and Reasoning (TIME 2014), pp132-141, IEEE Computer Society, 2014. ISBN 978-1-4799-4228-2 [Abstract] [BiB] [PDF]
  50. Laura Bozzelli and César Sánchez. Foundations of Boolean Stream Runtime Verification (Extended Version), In Proc. of the 5th Int'l Conf. on Runtime Verification (RV'14), vol 8734 of LNCS, pp 64-79, Springer, 2014. ISBN 978-3-319-11163-6. Extended version. [Abstract] [BiB] [PDF]
  51. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe and César Sánchez. Temporal Logics for Hyperproperties, In Proceedings of the Third Int'l Conf on Principles of Security and Trust (POST 2014), vol 8414 of LNCS, pp 265-284, Springer, 2014. [Abstract] [BiB] [PDF]
  52. Bernd Finkbeiner, Markus N. Rabe and César Sánchez. A Temporal Logic for Hyperproperties, arXiv preprint arXiv:1306.6657 [Abstract] [BiB] [PDF]
  53. César Sánchez and Alejandro Sánchez. A Decidable Theory of Skiplists of Unbounded Size and Arbitrary Height, arXiv preprint arXiv:1301.4372 [Abstract] [BiB] [PDF]
  54. Mark Marron, César Sánchez, Zhendong Su, and Manuel Fähndrich. Abstracting Runtime Heaps for Program Understanding, In IEEE Transactions in Software Engineering 39(6): 774-786 (2013) [Abstract] [BiB] [PDF]
  55. Maria-Cristina Marinescu and César Sánchez. Fusing Statecharts and Java, In ACM Transactions in Embedded Computing Systems, vol 12, number 1s, pages 45:1-45:21, ACM, 2013. [Abstract] [BiB] [PDF]
  56. Laura Bozzelli and César Sánchez. Visibly Rational Expressions, In IARCS Proceedings of the Annual Conference on Foundations of Software Technology and Theoretical Computer Science, (FSTTCS 2012) December 15-17, 2012, Hyderabad, India. [Abstract] [BiB] [PDF]
  57. César Sánchez and Julian Samborski-Forlese. How to Efficiently Translate Extensions of Temporal Logics into Alternating Automata, In Proceedings of the 9th International Conference on Theoretical Aspects of Computing (ICTAC 2012), Bangalore, India, September 24-27, vol 7521 of LNCS, pp30-45, Springer, 2012. [Abstract] [BiB] [PDF]
  58. César Sánchez and Julian Samborski-Forlese. Efficient Regular Linear Temporal Logic using Dualization and Stratification, In Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME 2012), Leicester, United Kingdom, September 12-14, 2012. IEEE Computer Society 2012, ISBN 978-1-4673-2659-9. [Abstract] [BiB] [PDF]
  59. Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, and Evan Chang. Invariant Generation for Parametrized Systems using Self-Reflection, In Proceedings of the 19th International Symposium on Static Analysis (SAS 2012), September 11-13, Deauville, France. 2012. vol 7460 of Lecture Notes in Computer Science pp146-163, Springer 2012, ISBN 978-3-642-33124-4. [Abstract] [BiB] [PDF]
  60. Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez, and Evan Chang. Invariant Generation for Parametrized Systems using Self-Reflection (Extended Version), Technical Report CU-CS-1094-12, University of Colorado Boulder, 2012. [Abstract] [BiB] [PDF]
  61. Marina Zapater, César Sánchez, José Luis Ayala, José Manuel Moya, and José Luis Risco-Martín. Ubiquitous Green Computing Techniques for High Demand Applications in Smart Environments, In Sensors, vol. 12, issue 8, pp. 10659--10677, ISSN 1424-8220, 2012. [Abstract] [BiB] [PDF]
  62. Alejandro Sánchez and César Sánchez. A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes, In Proceedings of the Third International Symposium on NASA Formal Methods (NFM'11), Pasadena, CA, USA, April 18-20, 2011. vol 6617 of Lecture Notes in Computer Science, pp343--358, Springer 2011. [Abstract] [BiB] [PDF]
  63. Krishnendu Chaterjee, Luca de Alfaro, Vishwanath Raman, and César Sánchez. Analyzing the Impact of Change in Multi-threaded Programs, In Proceedings of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE'2010), vol. 6013 of Lecture Notes in Computer Science, pp293-307. Springer-Verlag, 2010. [Abstract] [BiB] [PDF]
  64. Alejandro Sánchez and César Sánchez. Decision Procedures for the Temporal Verification of Concurrent Lists, In Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM'2010) vol. 6447 Lecture Notes in Computer Science, pp74-89, Springer-Verlag, 2010. [Abstract] [BiB] [PDF]
  65. Martin Leucker and César Sánchez. Regular Linear-Time Temporal Logic, In Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), Paris, France, 6-8 September 2010. pp3-5, IEEE Computer Society, 2010. [Abstract] [BiB] [PDF]
  66. César Sánchez and Martin Leucker. Regular Linear Temporal Logic with Past, In Proceedings of the Eleventh International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'10), vol. 5944 of Lecture Notes of Computer Science, pp295-311. Springer-Verlag, 2010. [Abstract] [BiB] [PDF]
  67. César Sánchez, Matteo Slanina, Henny Sipma, and Zohar Manna. The Reaction Algebra: A Formal Language for Event Correlation, In Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, vol 4800 of Lecture Notes in Computer Science, pp586-609. Springer-Verlag, Berlin, 2008. [Abstract] [BiB] [PDF]
  68. César Sánchez. Deadlock Avoidance for Distributed Real-Time and Embedded Systems, Ph.D. thesis, Stanford University, May 2007. [Abstract] [BiB] [PDF]
  69. César Sánchez, Henny Sipma, and Zohar Manna. A Family of Distributed Deadlock Avoidance Protocols and their reachable State Spaces, In Proceedings of the 10th International Conference on Fundamental Approaches to Software Engineering (FASE'07), colocated with ETAPS'07, vol. 4422 of Lecture Notes in Computer Science, pp155-169. Springer-Verlag, 2007. [Abstract] [BiB] [PDF]
  70. Martin Leucker and César Sánchez. Regular Linear Temporal Logic, In Proceedings of The 4th International Colloquium on Theoretical Aspects of Computing (ICTAC'07), vol. 4711 of Lecture Notes in Computer Science, pp291-305. Springer-Verlag, 2007. [Abstract] [BiB] [PDF]
  71. César Sánchez, Henny Sipma, and Zohar Manna. Generating Efficient Distributed Deadlock Avoidance Controllers, In The Fifteenth International Workshop on Parallel and Distributed Real-Time Systems (WPDRTS 2007), collocated with IPDPS'07 (21st IEEE International Parallel and Distributed Processing Symposium). IEEE Computer Society Press, 2007. [Abstract] [BiB] [PDF]
  72. César Sánchez, Henny Sipma, Zohar Manna, Venkita Subramonian, and Christopher D. Gill. Efficient Distributed Deadlock Avoidance with Liveness Guarantees, In Proceedings of the 6th ACM & IEEE Conference on Embedded Software (EMSOFT'06), pp12-20. ACM Press, 2006. [Abstract] [BiB] [PDF]
  73. Venkita Subramonian, Christopher D. Gill, César Sánchez, and . Reusable Models for Timing and Liveness Analysis of Middleware for Distributed Real-Time Embedded Systems, In Proceedings of the 6th ACM & IEEE Conference on Embedded Software (EMSOFT'06), pp252-261. ACM Press, 2006. [Abstract] [BiB] [PDF]
  74. César Sánchez, Henny Sipma, Zohar Manna, Venkita Subramonian, and Christopher D. Gill. On Efficient Distributed Deadlock Avoidance for Real-Time and Embedded Systems, In 20th IEEE Int'l Parallel and Distributed Processing Symposium (IPDPS'06). IEEE Computer Society Press, 2006. [Abstract] [BiB] [PDF]
  75. César Sánchez and Henny Sipma. Reachable State Spaces of Distributed Deadlock Avoidance Protocols, Technical Report REACT-TR-2006-01, Stanford University, Computer Science Dept., REACT Group, June, 2006. [Abstract] [BiB] [PDF]
  76. César Sánchez, Henny Sipma, Christopher D. Gill, and Zohar Manna. Distributed Priority Inheritance for Real-Time and Embedded Systems, In Proceedings of the 10th International Conference On Principles Of Distributed Systems (OPODIS'06), vol. 4305 of Lecture Notes in Computer Science, pp110-125. Springer-Verlag, 2006. [Abstract] [BiB] [PDF]
  77. César Sánchez, Henny Sipma, and Zohar Manna. On Efficient Distributed Deadlock Avoidance for Distributed Recursive Processes, Unpublished. [Abstract] [BiB] [PDF]
  78. César Sánchez, Henny Sipma, Matteo Slanina, and Zohar Manna. Final Semantics for Event-Pattern Reactive Programs, In Algebra and Coalgebra in Computer Science (CALCO'05), vol 3629 of Lecture Notes in Computer Science, pp364-378. Springer-Verlag, 2005. [Abstract] [BiB] [PDF]
  79. César Sánchez, Henny Sipma, Venkita Subramonian, Christopher D. Gill, and Zohar Manna. Thread Allocation Protocols for Distributed Real-Time and Embedded Systems, In 25th IFIP WG 2.6 Int'l Conf. on Formal Techniques for Networked and Distributed Systems (FORTE'05), vol. 3731 of Lecture Notes in Computer Science. Springer-Verlag, pp 159-173, 2005. [Abstract] [BiB] [PDF]
  80. César Sánchez, Matteo Slanina, Henny Sipma, and Zohar Manna. Expressive Completeness of an Event-Pattern Reactive Programming Language, In Formal Techniques for Networked and Distributed Systems (FORTE'05), vol. 3731 of Lecture Notes in Computer Science. Springer-Verlag, pp 529-532, 2005. [Abstract] [BiB] [PDF]
  81. Ben D'Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny Sipma, Sandeep Menhotra, and Zohar Manna. LOLA: Runtime Monitoring of Synchronous Systems, In Proc. of the 12th International Symposium of Temporal Representation and Reasoning (TIME 2005), pp. 166-174. IEEE Computer Society Press, 2005. [Abstract] [BiB] [PDF]
  82. César Sánchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang, David L. Dill, and Zohar Manna. Event Correlation: Language and Semantics, In Embedded Software (EMSOFT'03), vol 2855 of Lecture Notes in Computer Science, pp323-339. Springer-Verlag, 2003. [Abstract] [BiB] [PDF]
  83. César Sánchez and Angel Alvarez. A lightweight asynchronous algorithm for causal delivery using extra message insertion, Short paper in DISC 2000, 14th International Symposium on DIStributed Computing, Toledo (Spain), October 2000. [Abstract] [BiB] [PDF]

Awards

2007: Juan de la Cierva Scholarship, awarded by the Spanish Ministry of Science and Education, partially funding 3 years as a young post-doctoral researcher.

2006: ACM SIGBED-SIGSOFT Frank Anger Memorial Student Award.

2000: Champion team of (Southwestern European region). 11th place in the World Finals.

1999: La Caixa Graduate Fellowship , funding graduate studies from 1999 to 2001.

1998: Graduation with honors for the graduation thesis Communication with Causal Order in Asynchronous Distributed systems. Thesis advisor: Ángel Álvarez.

1997: IEEE Award for Outstanding Leaderships and Service.

Biographical sketch

I am nowadays a tenured researcher professor (position title "Associate Research Professor") at the Madrid Institute for Advanced Studies in Software Development Technologies.

In October 2008 I won a competition for a Scientific Researcher position at Consejo Superior de Investigaciones Científicas (CSIC).

During all of 2008 I was partially funded by a Juan de la Cierva Scholarship.

Between May 2007 and December 2007, I was a post-doctoral Scholar at the University of California at Santa Cruz, working with Luca de Alfaro.

In 2007 I received a Ph.D. in Computer Science from Stanford University. My dissertation can be accessed here:

In the Summer of 2005 I worked as a research intern for Intel.

In 2001 I received a Masters in Computer Science from Stanford University, specializing in Software Theory and Theoretical Computer Science.

Between 1997 and 1999 I worked for Lucent Technologies (Development Center in Madrid), and the School of Computer Science of UPM, and the department of Mathematics of UPM.

I received a degree in "Ingeniería de Telecomunicación"(6 years degree, BS + MSEE) from the Technical University of Madrid (UPM) in 1998. My graduation thesis Communication with Causal Order in Asynchronous Distributed Systems was awarded with "graduation with honors".

I am member of ACM, IEEE, the Computer Society of IEEE, and Mensa.