Fundamentals
In this section, we present our fundamental work on formal methods for CPS that is trying to push the boundaries on what is possible across all areas of application. This involves tackling challenges related to control-theoretic considerations such as disturbances and system structure; model-based and data-driven approaches; uncertainty and missing prior knowledge; stochasticity; and other.
Learn more
Power Systems
As we strive towards net-zero energy systems and increase our renewable energy uses, our power system behaviours become uncertain and new challenges are introduced in balancing the energy supply and demand. As we phase away from large-scale generation devices, we will need nimble controllers that can act quickly to mitigate any issues that arise, as well as approaches which can scale to the size of these massive power systems.
Learn more
Quantum Systems
Quantum computers are starting to become a reality and there is a need to ensure that the computations they perform behave as we expect. Our research consists of looking at finding bugs within quantum programs and software. We are investigating how to use different automated formal methods techniques in order to verify different aspects of quantum computers with minimal manual work.
Learn more
Communication Systems
Verification of Cyber-Physical Systems (CPS) with Communication Networks explores the critical intersection of CPS and network technologies. It ensures the reliability and secure operation of smart systems, like self-driving cars and industrial automation, by verifying their coordination with communication networks, making It a fascinating field at the forefront of technology and safety.
Learn more
Brain Modelling & Control
Epilepsy is a common neurological condition estimated to have lifetime prevalence of 0.76% worldwide. The condition is life-limiting and occasionally life-threatening. First line treatment is pharmacological, but side effects are common, and it is estimated that up to a third of patients will not be seizure free on medication. Some of these patients may be suitable for resection surgery, if a suitable surgical target can be identified with sufficient confidence. Other modalities include electrical stimulation of the vagus nerve (VNS) and, to a lesser extent, direct stimulation of the brain itself.
Learn more
Water Treatment Systems
Water Resource Recovery Facilities operate under designed configurations for pollutant loads and flow. With the increasing likelihood of extreme weather events due to climate change, the risk of pollution incidents and the consequent release of dangerous pollutants into rivers and seas is also rising. The quantification of resilience could provide significant benefits to water companies. It can help them rank their facilities for better management and more efficient resource distribution.
Learn more
HyCoDeV Lab
Hybrid Systems: Control, Design and Verification Lab
Where we research about formal methods for control, design and verification of hybrid systems.
In association with
Fundamentals
In this section, we present our fundamental work on formal methods for CPS that is trying to push the boundaries on what is possible across all areas of application. This involves tackling challenges related to control-theoretic considerations such as disturbances and system structure; model-based and data-driven approaches; uncertainty and missing prior knowledge; stochasticity; and other.
Lean morePower Systems
As we strive towards net-zero energy systems and increase our renewable energy uses, our power system behaviours become uncertain and new challenges are introduced in balancing the energy supply and demand. As we phase away from large-scale generation devices, we will need nimble controllers that can act quickly to mitigate any issues that arise, as well as approaches which can scale to the size of these massive power systems.
Lean moreQuantum Systems
Quantum computers are starting to become a reality and there is a need to ensure that the computations they perform behave as we expect. Our research consists of looking at finding bugs within quantum programs and software. We are investigating how to use different automated formal methods techniques in order to verify different aspects of quantum computers with minimal manual work.
Lean moreCommunication Systems
Verification of Cyber-Physical Systems (CPS) with Communication Networks explores the critical intersection of CPS and network technologies. It ensures the reliability and secure operation of smart systems, like self-driving cars and industrial automation, by verifying their coordination with communication networks, making It a fascinating field at the forefront of technology and safety.
Lean moreBrain Modelling & Control
Epilepsy is a common neurological condition estimated to have lifetime prevalence of 0.76% worldwide. The condition is life-limiting and occasionally life-threatening. First line treatment is pharmacological, but side effects are common, and it is estimated that up to a third of patients will not be seizure free on medication. Some of these patients may be suitable for resection surgery, if a suitable surgical target can be identified with sufficient confidence. Other modalities include electrical stimulation of the vagus nerve (VNS) and, to a lesser extent, direct stimulation of the brain itself.
Lean moreWater Treatment Systems
Water Resource Recovery Facilities operate under designed configurations for pollutant loads and flow. With the increasing likelihood of extreme weather events due to climate change, the risk of pollution incidents and the consequent release of dangerous pollutants into rivers and seas is also rising. The quantification of resilience could provide significant benefits to water companies. It can help them rank their facilities for better management and more efficient resource distribution.
Lean moreNews
Paper Presentation
Marco Lewis presented his paper at QEST 2023 in Antwerp, Belgium. The paper is titled "Verification of Quantum Systems using Barrier Certificates" with Paolo Zuliani and Sadegh Soudjani as coauthors.
September 2023
Paper Accepted
Mahmoud Salamati has had a paper accepted in the EMSOFT conference. The paper will also be published in a special issue at ACM transactions. The paper is on neural abstraction-based synthesis with correctness guarantees.
July 2023