Research
My research interests and areas of focus.
Cyber-Security Systems
Research on formal methods applied to cybersecurity, analyzing security protocols and developing verification techniques for secure systems.
Cyber-Physical Systems
Modeling and verification of systems that integrate computational and physical processes, ensuring safety and reliability in critical applications.
Distributed Systems
Modeling and verifying distributed systems, focusing on protocols, algorithms, and formal verification techniques for concurrent systems.
Real-Time Systems
Research on modeling, verification, and analysis of real-time systems using timed automata and temporal logic specifications.
Critical Embedded Systems
Developing formal verification techniques for embedded systems in safety-critical domains, ensuring correctness and reliability.
Timed Automata
Core research on timed automata with partially independent clocks, developing new models and verification algorithms for real-time systems.
Temporal Logics
Research on temporal logics for specifying and verifying properties of real-time and distributed systems, including TCTL and other temporal formalisms.
Simulation and Bisimulation
Developing equivalence relations and refinement techniques for timed and distributed systems using simulation and bisimulation theory.
Model Checking
Applying model checking techniques using tools like UPPAAL and SCADE to verify correctness of real-time and distributed systems.
Formal Methods
Applying mathematical techniques and formal specifications to design, develop, and verify software and hardware systems with rigorous correctness guarantees.
Theorem Proving
Research on interactive theorem proving and proof assistants for verifying complex properties of real-time systems and automata models.
Model-Based Testing
Developing testing methodologies derived from formal models to automatically generate test cases for complex systems and software product lines.
Mutation Testing
Research on mutation testing techniques for evaluating test suite quality and improving testing effectiveness in highly-configurable systems.
Software Product Lines
Research on variability modeling, testing highly-configurable systems, and scaling up variability analysis in software product lines.
Analysis and Symbolic Representation
Developing symbolic techniques and data structures for efficient analysis and verification of large state spaces in timed and distributed systems.