Skip to main content


  • Reasoning about Information-flow Security
    • In low level information flow analysis, each variable is usually assigned a security level. The basic model comprises two distinct levels: low and high, meaning, respectively, publicly observable information, and secret information. To ensure confidentiality, flowing information from high to low variables should not be allowed. On the other hand, to ensure integrity, flows to high variables should be restricted. We are working on the broad area of reasonng about information-flow security policies using hyperproperties. This includes verification, monitoring, synthesis, and testing.


  • Decentralized Autonomous Vehicles Path Planning
    • The vehicle routing problem (VRP) is one of the most studied combinatorial optimization problems and is concerned with the optimal design of routes to be used by a fleet of vehicles to service a set of customers. With the growing popularity of autonomous vehicles (e.g., driverless cars and unmanned aerial systems) in the modern world, there is pressing need to revisit this problem in the context of decentralized multi-agent systems. We are developing distributed algorithms that attempt to optimize the global cost of routes for a set of autonomous vehicles


  • Runtime Monitoring
    • Runtime monitoring and enforcement of desirable properties is an effective technique that ensures correctness at execution time. Runtime monitoring is particularly useful in large systems, where exhaustive analysis is not practical and conventional testing may fail to identify complex corner cases. The challenging problem in this area is to implement resource-efficient runtime monitors that do not intervene in the normal execution of the program under inspection. We are conducting research on automated design and development of runtime monitors for distributed real-time systems that (1) need to provide certain security and privacy policies and (2) take into consideration resource constraints (e.g., power, time budget, CPU cycles, memory, etc), while effectively exploiting the heterogeneous nature of today's computing platforms, such as many-core GPUs and multi-core processors.


  • Model-based Implementation of Distributed Real-time Systems
    • Model-based software development advocates the system design flow as a chain of steps starting from a high-level specification and leading to an implementation on a given execution platform. It involves the use of methods and tools for progressively deriving the implementation by making adequate design choices and step-by-step transformations that terminate when a correct-by-construction implementation is obtained. We are developing a novel framework for automated implementation of parallel/distributed real-time applications that are correct-by-construction from an abstract model specified in terms of a set of heterogeneous components, synchronization primitives, and priority rules for scheduling purposes. Our approach is based on algorithmic transformation techniques. These algorithms take as input a model of system processes and generate as output distributed and/or multi-threaded code, while ensuring that the execution of the code is observationally equivalent to the input abstract model and, hence, all the functional properties of the high-level model are preserved.


  • Distributed Synthesis