Verification and synthesis
Verification and synthesis are complementary approaches to ensure that computing systems behave as they are supposed to, across all possible situations.
In verification we check that a given system meets its specification to check if it is safe, resilient, or dependable. Synthesis turns the question around and asks to automatically construct a system that is correct by design. That is, instead of manually designing a system and then checking if it behaves as intended, synthesis aims to build systems straight from high-level requirements.
Together, these methods are powerful tools for building trust in critical technologies and infrastructure. They go beyond systematic testing and provide hard and provable guarantees based on rigorous mathematical analysis. These formal methods are typically employed at the design stage before any actual code is written and argue about mathematical abstractions of actual computing systems.
Unsurprisingly, the feasibility and efficiency of verification and synthesis algorithms depend on the level of abstraction we consider as well as what kind of specifications we are after. If we model a spacecraft controller as two-state machine that can only move up or down, then it is easier to prove correct than if we model its many interacting subcomponents and local program variables taking one of infinitely many possible values. Similarly, it matters how expressive we allow specifications to be. Simple examples of desirable system properties include safety (nothing bad can possibly happen) or liveness (something good can always happen). More generally, specifications are usually given in a temporal logic like Linear Temporal Logic (LTL) that can express the above and more. Beyond that, we may need to express real-time or probabilistic constraints (e.g. "with probability p>0.999 the breaks are engaged at most 0.5s after being triggered").
Formal Verification and Synthesis intersect with fields like Automata Theory, Logic, Game Theory, Programming Languages, and increasingly, machine learning. They also touch on application domains such as cyber-physical systems, hybrid and stochastic systems, and distributed protocols. Formal methods are regularly employed in industrial practice: modern software and hardware underlie everything from autonomous robots and medical devices to
financial systems and network infrastructure. Failures can be dearly consequential, which is why formal methods that can guarantee correctness, security, and reliability are sought-after.
Our research
In our research we design algorithms for verification and synthesis and clarify the trade-offs between expressiveness of abstractions/specs on the one hand and the effectiveness and efficiency of verification problems on the other. On a fundamental level, we study which tasks can be algorithmically solved in principle, and if so, determine their computational complexity. Towards practical applications, we design new formal analysis methods, simplify and improve existing ones, and apply them to new scenarios.
Our Team
The Verification group at Liverpool is at the forefront of research on reactive synthesis and related methods and has been for the past 20 years. Today, we are broadly positioned in the formal methods space, and our members are active on diverse topics including probabilistic verification, infinite-state systems, automata theory, temporal logics, and software tools realizing formal methods.
Opportunities
We welcome opportunities to engage with students, researchers, and industry partner:
- PhD opportunities: please contact us if you are interested in pursuing a PhD in verification and synthesis
- Consultancy and research collaborations: we welcome partnerships, consultancy, and knowledge exchange projects with academic, industry, and government partners.
Contact us
Please discuss with relevant academic staff if you are interested in their research.