معرفی
Alejandro Sánchez is a Post-doctoral Researcher at the IMDEA Software Institute in Madrid, Spain. His research focuses on formal methods, decision procedures, and the verification of parametrized concurrent systems and data structures. He holds a PhD in Computer Science from the Universidad Politécnica de Madrid (2015), a Master's in Programming and Software Technology from Universidad Complutense de Madrid (2011), and a Bachelor's in Computer Science from Universidad Nacional de Córdoba (2007).
Education Background:
- PhD in Computer Science, Universidad Politécnica de Madrid (2012–2015)
- Master in Programming and Software Technology, Universidad Complutense de Madrid (2010–2011)
- Bachelor of Science in Computer Science, Universidad Nacional de Córdoba (2002–2007)
Research Interests:
His work emphasizes formal verification techniques for concurrent systems, including parametrized systems, dynamic memory analysis, and specialized decision procedures. Key areas include temporal logics, deductive reasoning, and the verification of complex data structures like skiplists and concurrent lists. He has developed tools like LEAP for parametrized verification and contributed decision procedures integrated with SMT solvers (Yices, Z3).
Professional Contributions:
He has published extensively on formal methods and concurrency, including work on invariant generation, parametrized verification diagrams, and skiplist theory. His research bridges theoretical foundations with practical tool development, addressing challenges in verifying safety and liveness properties in complex concurrent systems.
Tool Development:
LEAP, an interactive theorem prover he maintains, enables deductive verification of concurrent systems. He has also implemented decision procedures for pointer-based data structures, demonstrating practical applications of formal methods in real-world systems.
