Analysis and Verification | Faculty of Engineering

<!DOCTYPE html> <html class="no-js" lang="en-GB"> <head> <title>Analysis and Verification | Faculty of Engineering | Imperial College London</title> <meta charset="utf-8" /> <meta http-equiv="X-UA-Compatible" content="IE=edge" />  <script type="text/javascript" src="https://cdn-ukwest.onetrust.com/consent/6d9efb9d-b605-406f-b8b3-c9644859d064/OtAutoBlock.js" ></script><script src="https://cdn-ukwest.onetrust.com/scripttemplates/otSDKStub.js" type="text/javascript" charset="UTF-8" data-domain-script="6d9efb9d-b605-406f-b8b3-c9644859d064" ></script> <script type="text/javascript">function OptanonWrapper() { }</script>  <link rel="preconnect" href="https://pxl-imperialacuk.terminalfour.net"> <link rel="dns-prefetch" href="https://pxl-imperialacuk.terminalfour.net">  <meta name="SectionType" content="website"> <meta name="Department" content="Department of Computing"> <meta name="Faculty" content="Faculty of Engineering">  <meta name="twitter:dnt" content="on"> <meta name="twitter:card" content="summary"> <meta name="twitter:site" content="@imperialcollege"> <meta name="twitter:title" content="Analysis and Verification"> <meta name="twitter:description" content="We face a fundamental problem: computer systems are critical to modern society but traditional non-mathematical computer engineering techniques, such..."> <meta name="twitter:image" content="https://www.imperial.ac.uk/T4Assets/favicon-196x196.png"> <meta name="fb:app_id" content="674884772674087"> <meta property="og:title" content="Analysis and Verification" /> <meta property="og:type" content="website" /> <meta property="og:image" content="https://www.imperial.ac.uk/T4Assets/favicon-196x196.png" /> <meta property="og:image:type" content="image/png" /> <meta property="og:image:secure_url" content="https://www.imperial.ac.uk/T4Assets/favicon-196x196.png" /> <meta property="og:image:width" content="200" /><meta property="og:image:height" content="200" /><meta property="og:url" content="https://www.imperial.ac.uk/engineering/departments/computing/research/analysis-and-verification/" /> <meta property="og:description" content="We face a fundamental problem: computer systems are critical to modern society but traditional non-mathematical computer engineering techniques, such..." /> <meta property="og:locale" content="en_GB" /> <meta property="og:site_name" content="Imperial College London" /> <meta name="viewport" content="width=device-width, initial-scale=1.0" />  <link rel="preload" href="/assets/website/fonts/icons/fonts/imperial-icons.woff?vrmf2d" as="font" type="font/woff" crossorigin> <link rel="preload" href="/assets/website/fonts/imperial-sans/ImperialText-VF.woff2" as="font" type="font/woff2" crossorigin> <link href="/assets/website/stylesheets/css/screen.2.0.10.css" media="all" rel="stylesheet" type="text/css" /> <link href="/assets/website/stylesheets/css/print.2.0.10.css" media="print" rel="stylesheet" type="text/css" /> <link rel="icon" type="image/svg+xml" href="/assets/website/images/favicon/favicon.svg"> <link rel="alternate icon" href="/assets/website/images/favicon/favicon.ico"> <link rel="icon" href="/assets/website/images/favicon/favicon-32.png" sizes="32x32"> <link rel="icon" href="/assets/website/images/favicon/favicon-57.png" sizes="57x57"> <link rel="icon" href="/assets/website/images/favicon/favicon-76.png" sizes="76x76"> <link rel="icon" href="/assets/website/images/favicon/favicon-96.png" sizes="96x96"> <link rel="icon" href="/assets/website/images/favicon/favicon-128.png" sizes="128x128"> <link rel="icon" href="/assets/website/images/favicon/favicon-192.png" sizes="192x192"> <link rel="icon" href="/assets/website/images/favicon/favicon-228.png" sizes="228x228"> <link rel="shortcut icon" href="/assets/website/images/favicon/favicon-196.png" sizes="196x196"> <link rel="apple-touch-icon" href="/assets/website/images/favicon/favicon-120.png" sizes="120x120"> <link rel="apple-touch-icon" href="/assets/website/images/favicon/favicon-152.png" sizes="152x152"> <link rel="apple-touch-icon" href="/assets/website/images/favicon/favicon-180.png" sizes="180x180"> <meta name="msapplication-TileColor" content="#C8D8E4"> <meta name="msapplication-TileImage" content="/assets/website/images/favicon/favicon-144.png"> <meta name="msapplication-config" content="/assets/website/images/favicon/browserconfig.xml" /> <script src="/assets/website/js/lib/jquery3.min.js" id="jquery3"></script> <script defer src="/assets/website/js/build/application.2.0.10.min.js" type="text/javascript"></script> <script defer src="//cdnjs.cloudflare.com/ajax/libs/gsap/3.10.4/gsap.min.js"></script>  <link rel="canonical" href="https://www.imperial.ac.uk/engineering/departments/computing/research/analysis-and-verification/" /> </head> <body class="theme-5"> <noscript><iframe src="https://www.googletagmanager.com/ns.html?id=GTM-NDH95W87" height="0" width="0" style="display:none;visibility:hidden"></iframe></noscript><script>(function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':聽new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],聽 j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src=聽'https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);聽})(window,document,'script','dataLayer','GTM-NDH95W87');</script> <a class="skip-to" id="skip-to-content" href="#content">Skip to main content</a> <a class="skip-to" id="link-to-accessibility" href="/about-the-site/accessibility/">View accessibility support page</a> <header class="header"> <div class="header__inner"> <a class="header__logo" href="/" aria-label="Homepage"> <svg width="727" height="80" viewBox="0 0 727 80" fill="none" xmlns="http://www.w3.org/2000/svg"> <path d="M301.453 0V80H353.346V66H316.622V46H350.152V32.4H316.622V14H353.346V0H301.453Z" fill="currentcolor" /> <path d="M238.397 12.9177H227.22V39.8776H238.397C247.142 39.8776 253.566 35.6376 253.566 26.3953C253.566 16.8 247.142 12.9177 238.397 12.9177ZM239.196 52.8H227.22V80H212.052V0H239.196C256.219 0 269.533 7.72706 269.533 26.4C269.533 44.8 256.121 52.8 239.196 52.8Z" fill="currentcolor" /> <path d="M485.079 0V14H503.84V66H485.079V80H537.77V66H519.009V14H537.77V0H485.079Z" fill="currentcolor" /> <path d="M434.191 24.8C434.191 34.4377 428.602 37.4777 419.022 37.4777H406.248V12.9177H419.022C429.419 12.9224 434.191 16.8 434.191 24.8ZM450.158 24.8C450.158 6.12706 437.384 0 420.619 0H391.08V80H406.248V50.4H419.022C419.722 50.4 420.417 50.3859 421.107 50.3624L436.562 80H453.37L436.224 47.1906C444.565 43.4777 450.158 36.3435 450.158 24.8Z" fill="currentcolor" /> <path d="M604.324 14.1929L615.238 49.4777H593.406L604.324 14.1929ZM594.345 0L567.999 80H583.966L589.409 62.4H619.235L624.678 80H640.645L614.299 0H594.345Z" fill="currentcolor" /> <path d="M674.889 0V80H726.914V66H690.058V0H674.889Z" fill="currentcolor" /> <path d="M151.908 0L132.747 47.04L113.587 0H92.0312V80H106.402V20.1882L124.764 62.4H140.731L159.093 20.1882V80H173.463V0H151.908Z" fill="currentcolor" /> <path d="M0 0V14H18.7613V66H0V80H52.6912V66H33.93V14H52.6912V0H0Z" fill="currentcolor" /> </svg> </a> <div class="header__buttons"> <search class="header__search"> <form action="/search/"> <label class="sr-only" for="search">Search</label> <input placeholder="Search" type="search" id="search" name="searchStudioQuery" /> <button type="submit" value="Search" aria-label="Submit search"> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#search"></use> </svg> </button> </form> </search> <button class="header__search-toggle toggler" data-targets=".header__search--mobile"> Search <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#search"></use> </svg> </button> <button class="header__nav-open" aria-label="Open navigation overlay">Menu<span></span></button> </div> <nav class="header__nav-fallback"> <ul class="cluster cluster--pad-m"> <li><a href="/study/">Study</a></li><li><a href="/research-and-innovation/">Research</a></li><li><a href="/faculties-and-departments/">Faculties</a></li><li><a href="/latest-news-events/">News and events</a></li><li><a href="/about/">About</a></li><li><a href="/get-involved/">Get involved</a></li><li><a href="/giving/">Giving</a></li> <li><a href="/search">Search</a></li> </ul> </nav> <search class="header__search header__search--mobile"> <form action="/search/"> <label class="sr-only" for="search">Search</label> <input placeholder="Search" type="search" id="search" name="searchStudioQuery" /> <button type="submit" value="Search" aria-label="Submit search"> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#search"></use> </svg> </button> </form> </search> </div> <div id="#overlay" role="dialog" aria-modal="true" aria-labelledby="overlay-title" class="hidden"> <h2 class="sr-only" id="overlay-title">Website navigation</h2> <div class="container"> <div class="header__drawer"> <button class="header__nav-close" aria-label="Close navigation overlay">Close<span></span></button> <a class="header__drawer__logo" href="/" aria-label="Homepage"> <svg width="727" height="80" viewBox="0 0 727 80" fill="none" xmlns="http://www.w3.org/2000/svg"> <path d="M301.453 0V80H353.346V66H316.622V46H350.152V32.4H316.622V14H353.346V0H301.453Z" fill="currentcolor"/> <path d="M238.397 12.9177H227.22V39.8776H238.397C247.142 39.8776 253.566 35.6376 253.566 26.3953C253.566 16.8 247.142 12.9177 238.397 12.9177ZM239.196 52.8H227.22V80H212.052V0H239.196C256.219 0 269.533 7.72706 269.533 26.4C269.533 44.8 256.121 52.8 239.196 52.8Z" fill="currentcolor"/> <path d="M485.079 0V14H503.84V66H485.079V80H537.77V66H519.009V14H537.77V0H485.079Z" fill="currentcolor"/> <path d="M434.191 24.8C434.191 34.4377 428.602 37.4777 419.022 37.4777H406.248V12.9177H419.022C429.419 12.9224 434.191 16.8 434.191 24.8ZM450.158 24.8C450.158 6.12706 437.384 0 420.619 0H391.08V80H406.248V50.4H419.022C419.722 50.4 420.417 50.3859 421.107 50.3624L436.562 80H453.37L436.224 47.1906C444.565 43.4777 450.158 36.3435 450.158 24.8Z" fill="currentcolor"/> <path d="M604.324 14.1929L615.238 49.4777H593.406L604.324 14.1929ZM594.345 0L567.999 80H583.966L589.409 62.4H619.235L624.678 80H640.645L614.299 0H594.345Z" fill="currentcolor"/> <path d="M674.889 0V80H726.914V66H690.058V0H674.889Z" fill="currentcolor"/> <path d="M151.908 0L132.747 47.04L113.587 0H92.0312V80H106.402V20.1882L124.764 62.4H140.731L159.093 20.1882V80H173.463V0H151.908Z" fill="currentcolor"/> <path d="M0 0V14H18.7613V66H0V80H52.6912V66H33.93V14H52.6912V0H0Z" fill="currentcolor"/> </svg> </a> <div class="header__pane-switchers"> <button class="header__pane-switcher" data-tab-id="site-nav">Key links</button> <button class="header__pane-switcher" data-tab-id="section-nav">This section</button> </div> <div class="header__pane header__pane--global" id="site-nav"> <a class="header__skip-link" href="#section-nav">Skip to section navigation</a> <nav class="header__nav header__nav--global" aria-labelledby="global-nav-title"> <h3 class="sr-only" id="global-nav-title">Global site navigation</h3> <ul> <li> <a href="/study/">Study</a> <ul> <li><a href="/study/courses/">Course search</a></li> <li><a href="/study/apply/">Apply</a></li> <li><a href="/study/fees-and-funding/">Fees and funding</a></li> <li><a href="/study/student-life/">Student life</a></li> <li><a href="/study/visit/">Visit</a></li> <li><a href="/study/help-centre/">Help centre</a></li> <li><a href="/study/request-info/">Request info</a></li> <li><a href="/study/international-students/">International students</a></li> <li><a href="https://www.imperial.ac.uk/business-school/executive-education/">Executive education</a></li> <li></li> <li><a href="/study/visit/summer-schools/">Summer schools</a></li> </ul> </li><li> <a href="/research-and-innovation/">Research</a> </li><li> <a href="/faculties-and-departments/">Faculties</a> <ul> <li><a href="/engineering/">Faculty of Engineering</a></li> <li><a href="/medicine/">Faculty of Medicine</a></li> <li><a href="/natural-sciences/">Faculty of Natural Sciences</a></li> <li><a href="https://www.imperial.ac.uk/business-school/">Imperial College Business School</a></li> <li><a href="/admin-services/">Administrative and support services</a></li> </ul> </li><li> <a href="/latest-news-events/">News and events</a> <ul> <li><a href="https://www.imperial.ac.uk/news/">News</a></li> <li><a href="/whats-on/">What's on</a></li> <li><a href="/be-inspired/stories/">Imperial Stories</a></li> <li><a href="/be-inspired/festival/">Great Exhibition Road Festival</a></li> <li><a href="/be-inspired/magazine/">Imperial Magazine</a></li> <li><a href="/be-inspired/lates/">Imperial Lates</a></li> <li><a href="/students/graduation/">Graduation</a></li> </ul> </li><li> <a href="/about/">About</a> <ul> <li><a href="/about/leadership-and-strategy/president/">President</a></li> <li><a href="/about/leadership-and-strategy/provost/">Provost</a></li> <li><a href="/about/leadership-and-strategy/strategy/">Imperial Strategy</a></li> <li><a href="/about/leadership-and-strategy/provost/academic-strategy/">Academic Strategy</a></li> <li><a href="/about/global/">Imperial Global</a></li> <li><a href="/about/sustainability/">Sustainable Imperial</a></li> <li><a href="/about/governance/">Governance</a></li> <li><a href="/visit/campuses/">Campuses</a></li> <li><a href="https://profiles.imperial.ac.uk/">Our academics</a></li> <li><a href="/jobs/">Jobs at Imperial</a></li> </ul> </li><li> <a href="/get-involved/">Get involved</a> <ul> <li><a href="/giving/">Giving</a></li> <li><a href="/be-inspired/schools-outreach/">Schools outreach</a></li> <li><a href="/be-inspired/global-summer-school/">Imperial Global Summer School</a></li> <li><a href="/be-inspired/societal-engagement/">Societal engagement</a></li> <li><a href="/be-inspired/volunteering/">Volunteering and outreach</a></li> <li><a href="/get-involved/women-at-imperial/">Women at Imperial</a></li> </ul> </li><li> <a href="/giving/">Giving</a> </li> </ul> </nav> <nav aria-labelledby="user-nav-title" role="navigation"> <h3 class="sr-only" id="user-nav-title">User links navigation</h3> <ul class="header__user-links"> <li><a href="/staff/">For staff</a></li> <li><a href="/students/">Current students</a></li> <li><a href="/for-business/">Imperial for business</a></li> <li><a href="/be-inspired/schools-outreach/">For schools</a></li> <li><a href="/alumni/">Alumni</a></li> </ul> </nav> </div> <div class="header__pane header__pane--section" id="section-nav"> <nav class="header__nav header__nav--section" aria-labelledby="section-nav-title"> <a class="header__nav__breadcrumb" href="/engineering/departments/"> <span>Departments, institutes and centres</span> </a> <h3 class="header__nav__title" id="section-nav-title"><a href="/engineering/departments/computing/">Department of Computing</a><span class="sr-only"> navigation</span></h3> <ul> <li><a href="/engineering/departments/computing/about/">About</a> <ul class="multilevel-linkul-0"> <li><a href="/engineering/departments/computing/about/getting-here/">Getting here</a></li> <li><a href="/engineering/departments/computing/about/our-values/">Our values</a></li> <li><a href="/engineering/departments/computing/about/facilities/">Our facilities</a></li> <li><a href="/engineering/departments/computing/about/useful-contacts/">Useful contacts</a></li> <li><a href="/engineering/departments/computing/about/equality-and-diversity/">Equity and Diversity</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/about/equality-and-diversity/edcc/">Equity, Diversity and Culture Committee</a></li> <li><a href="/engineering/departments/computing/about/equality-and-diversity/women-in-computing/">Women in Computing</a></li> <li><a href="/engineering/departments/computing/about/equality-and-diversity/athena-swan/">Athena SWAN</a></li> <li><a href="/engineering/departments/computing/about/equality-and-diversity/resources/">Resources</a></li> </ul> </li> <li><a href="/engineering/departments/computing/about/job-vacancies/">Vacancies</a></li> <li><a href="/engineering/departments/computing/about/news/">News and events</a></li> <li><a href="/engineering/departments/computing/about/health-and-safety/">Health and safety</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/about/health-and-safety/qualified-first-aiders/">Qualified first aiders</a></li> <li><a href="/engineering/departments/computing/about/health-and-safety/theft/">Theft</a></li> <li><a href="/engineering/departments/computing/about/health-and-safety/students-welcome-information/">Students Welcome Information</a></li> </ul> </li> <li><a href="/engineering/departments/computing/about/awards-and-honours/">Awards and honours </a></li> </ul> </li><li><a href="/engineering/departments/computing/people/">People</a> <ul class="multilevel-linkul-0"> <li><a href="https://imperiallondon.sharepoint.com/sites/foe/doc/DoCStaff/SitePages/Home.aspx" target="_blank">Staff intranet</a></li> <li><a href="/engineering/departments/computing/people/academic-staff/">Academic staff</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/people/academic-staff/new-staff/">Welcome to new academics</a></li> </ul> </li> <li><a href="/engineering/departments/computing/people/teaching-fellows/">Teaching fellows</a></li> <li><a href="/engineering/departments/computing/people/research/">Research staff</a></li> <li><a href="/engineering/departments/computing/people/administrative-staff/">Administrative staff</a></li> <li><a href="/engineering/departments/computing/people/csg/">CSG</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/people/csg/recent-changes/">Recent changes</a></li> <li><a href="/engineering/departments/computing/people/csg/new-users/">New users</a> <ul class="multilevel-linkul-2"> <li><a href="/engineering/departments/computing/people/csg/new-users/students/">Students</a> <ul class="multilevel-linkul-3"> <li><a href="/engineering/departments/computing/people/csg/new-users/students/regulations/">Lab regulations</a></li> </ul> </li> <li><a href="/engineering/departments/computing/people/csg/new-users/staff-and-phds/">Staff and PhDs</a></li> </ul> </li> <li><a href="/engineering/departments/computing/people/csg/services/">Services</a></li> <li><a href="/engineering/departments/computing/people/csg/guides/">Guides</a> <ul class="multilevel-linkul-2"> <li><a href="/engineering/departments/computing/people/csg/guides/remote-access/">Remote Access</a></li> </ul> </li> <li><a href="/engineering/departments/computing/people/csg/facilities/">Facilities</a> <ul class="multilevel-linkul-2"> <li><a href="/engineering/departments/computing/people/csg/facilities/loans/">Loans</a></li> <li><a href="/engineering/departments/computing/people/csg/facilities/lab/">Lab</a> <ul class="multilevel-linkul-3"> <li><a href="/engineering/departments/computing/people/csg/facilities/lab/workstations/">Workstations</a></li> </ul> </li> <li><a href="/engineering/departments/computing/people/csg/facilities/theatres/">Theatres</a></li> </ul> </li> <li><a href="https://otrs.doc.ic.ac.uk/" target="_blank">Help desk</a></li> <li><a href="/engineering/departments/computing/people/csg/policies/">Policies</a></li> <li><a href="/engineering/departments/computing/people/csg/activities/">Activities</a> <ul class="multilevel-linkul-2"> <li><a href="/engineering/departments/computing/people/csg/activities/csg-systems-activities/">CSG Systems Activities</a></li> <li><a href="/engineering/departments/computing/people/csg/activities/information-systems-activities/">Information Systems Activities</a></li> </ul> </li> </ul> </li> <li><a href="/engineering/departments/computing/people/honorary-staff/">Honorary staff</a></li> <li><a href="/engineering/departments/computing/people/emeritus-staff/">Emeritus staff</a></li> <li><a href="/engineering/departments/computing/people/alumnus/">Alumnus</a></li> </ul> </li><li><span class="currentbranch0"><a href="/engineering/departments/computing/research/">Research</a></span> <ul class="multilevel-linkul-0"> <li><span class="currentbranch1"><a href="/engineering/departments/computing/research/analysis-and-verification/">Analysis and Verification</a></span> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/research/analysis-and-verification/events/">Events</a></li> </ul> </li> <li><a href="/engineering/departments/computing/research/artificial-intelligence/">Artificial Intelligence</a></li> <li><a href="/engineering/departments/computing/research/data-science/">Data Science</a></li> <li><a href="/engineering/departments/computing/research/programming-languages/">Programming Languages</a></li> <li><a href="/engineering/departments/computing/research/cyber-security/">Cyber Security</a></li> <li><a href="/engineering/departments/computing/research/software-engineering/">Software Engineering</a></li> <li><a href="/engineering/departments/computing/research/systems/">Systems</a></li> <li><a href="/engineering/departments/computing/research/theory-and-algorithms/">Theory and Algorithms</a></li> <li><a href="/engineering/departments/computing/research/visual-computing/">Visual Computing</a></li> <li><a href="/engineering/departments/computing/research/research-groups-listed-alphabetically/">Research groups listed alphabetically</a></li> <li><a href="/engineering/departments/computing/research/quantum-computing/">Quantum Computing</a></li> </ul> </li><li><a href="/engineering/departments/computing/csg/">CSG</a> <ul class="multilevel-linkul-0"> <li><a href="/engineering/departments/computing/csg/recent-changes/">Recent changes</a></li> <li><a href="/engineering/departments/computing/csg/new-users/">New users</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/csg/new-users/students/">Students</a> <ul class="multilevel-linkul-2"> <li><a href="/engineering/departments/computing/csg/new-users/students/regulations/">Lab regulations</a></li> </ul> </li> <li><a href="/engineering/departments/computing/csg/new-users/staff-and-phds/">Staff and PhDs</a></li> </ul> </li> <li><a href="/engineering/departments/computing/csg/services/">Services</a></li> <li><a href="/engineering/departments/computing/csg/guides/">Guides</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/csg/guides/remote-access/">Remote Access</a></li> </ul> </li> <li><a href="/engineering/departments/computing/csg/facilities/">Facilities</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/csg/facilities/loans/">Loans</a></li> <li><a href="/engineering/departments/computing/csg/facilities/lab/">Lab</a> <ul class="multilevel-linkul-2"> <li><a href="/engineering/departments/computing/csg/facilities/lab/workstations/">Workstations</a></li> </ul> </li> <li><a href="/engineering/departments/computing/csg/facilities/theatres/">Theatres</a></li> </ul> </li> <li><a href="https://otrs.doc.ic.ac.uk/" target="_blank">Help desk</a></li> <li><a href="/engineering/departments/computing/csg/policies/">Policies</a></li> <li><a href="/engineering/departments/computing/csg/activities/">Activities</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/csg/activities/csg-systems-activities/">CSG Systems Activities</a></li> <li><a href="/engineering/departments/computing/csg/activities/information-systems-activities/">Information Systems Activities</a></li> </ul> </li> </ul> </li><li><a href="/engineering/departments/computing/prospective-students/">Prospective students</a> <ul class="multilevel-linkul-0"> <li><a href="https://www.imperial.ac.uk/computing/prospective-students/" target="_blank">Welcome</a></li> <li><a href="/engineering/departments/computing/prospective-students/ug/">Undergraduate courses</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/prospective-students/ug/beng-meng-computing/">BEng/MEng Computing</a></li> <li><a href="/engineering/departments/computing/prospective-students/ug/beng-meng-jmc/">BEng/MEng Joint Mathematics and Computer Science</a></li> </ul> </li> <li><a href="/engineering/departments/computing/prospective-students/pg/">Postgraduate courses</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/prospective-students/pg/msc-computing/">MSc Computing</a></li> <li><a href="/engineering/departments/computing/prospective-students/pg/mac/">MSc Advanced Computing</a></li> <li><a href="/engineering/departments/computing/prospective-students/pg/mai/">MSc Artificial Intelligence</a></li> <li><a href="/engineering/departments/computing/prospective-students/pg/msc-specialist-degrees/">MSc Specialist Degrees</a> <ul class="multilevel-linkul-2"> <li><a href="/engineering/departments/computing/prospective-students/pg/msc-specialist-degrees/aiml/">MSc in Computing (Artificial Intelligence and Machine Learning)</a></li> <li><a href="/engineering/departments/computing/prospective-students/pg/msc-specialist-degrees/cms/">MSc in Computing (Management and Finance)</a></li> <li><a href="/engineering/departments/computing/prospective-students/pg/msc-specialist-degrees/sr/">MSc in Computing (Security and Reliability)</a></li> <li><a href="/engineering/departments/computing/prospective-students/pg/msc-specialist-degrees/se/">MSc in Computing (Software Engineering)</a></li> <li><a href="/engineering/departments/computing/prospective-students/pg/msc-specialist-degrees/vcr/">MSc in Computing (Visual Computing and Robotics)</a></li> </ul> </li> <li><a href="/engineering/departments/computing/prospective-students/pg/mresphd/">Integrated MRes/PhD Degrees</a></li> <li><a href="/engineering/departments/computing/prospective-students/pg/mres-artificial-intelligence-and-machine-learning/">MRes AI and Machine Learning</a></li> </ul> </li> <li><a href="/engineering/departments/computing/prospective-students/phd/">PhD</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/prospective-students/phd/faqs/">FAQs</a></li> <li><a href="/engineering/departments/computing/prospective-students/phd/scholarships/">Scholarships</a></li> <li><a href="https://ai4health.io/" target="_blank">AI4Health Centre for Doctoral Training</a></li> <li><a href="/engineering/departments/computing/prospective-students/phd/phd-stories/">PhD success stories</a></li> <li><a href="/engineering/departments/computing/prospective-students/phd/phd-application-guidelines/">PhD application guidelines</a></li> </ul> </li> <li><a href="/engineering/departments/computing/prospective-students/deepmind-scholars/">DeepMind scholarships</a></li> <li><a href="/engineering/departments/computing/prospective-students/open-days/">Open days and taster courses</a></li> <li><a href="/engineering/departments/computing/prospective-students/scholarships/">Scholarships and Bursaries</a></li> </ul> </li><li><a href="/engineering/departments/computing/current-students/">Current students</a> <ul class="multilevel-linkul-0"> <li><a href="/engineering/departments/computing/current-students/student-welfare/">Student welfare</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/current-students/student-welfare/exams--mitigating-circumstances/">Exams & Mitigating Circumstances</a></li> </ul> </li> <li><a href="/engineering/departments/computing/current-students/computing/">Undergraduate Computing: degree and course information</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/current-students/computing/ug/">Undergraduate degrees</a></li> <li><a href="/engineering/departments/computing/current-students/computing/ug-handbook/">UG handbook</a></li> </ul> </li> <li><a href="/engineering/departments/computing/current-students/jmc/">Undergraduate JMC: degree and course information</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/current-students/jmc/jmc-degrees/">JMC undergraduate degrees</a></li> <li><a href="/engineering/departments/computing/current-students/computing/ug-handbook/">UG handbook</a></li> </ul> </li> <li><a href="/engineering/departments/computing/current-students/pg-info/">Postgraduate degrees and course information</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/current-students/pg-info/pg-handbook/">PG handbook</a></li> </ul> </li> <li><a href="/engineering/departments/computing/current-students/phd-info/">PhD information</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/current-students/phd-info/facewall-phd-1st-year---cohort-2020--2021/">Facewall PhD 1st Year - Cohort 2020 / 2021</a></li> <li><a href="/engineering/departments/computing/current-students/phd-info/phd-diary/">PhD diary</a></li> <li><a href="/engineering/departments/computing/current-students/phd-info/phdmatters/">PhD Matters</a> <ul class="multilevel-linkul-2"> <li><a href="/engineering/departments/computing/current-students/phd-info/phdmatters/policies-and-forms/">Policies and forms</a></li> <li><a href="/engineering/departments/computing/current-students/phd-info/phdmatters/milestones-guidance-notes/">Milestones guidance notes</a></li> <li><a href="/engineering/departments/computing/current-students/phd-info/phdmatters/faqs/">FAQs</a></li> <li><a href="/engineering/departments/computing/current-students/phd-info/phdmatters/the-team/">The team</a></li> <li><a href="/engineering/departments/computing/current-students/phd-info/phdmatters/casual-work/">Casual work</a></li> </ul> </li> </ul> </li> <li><a href="/engineering/departments/computing/current-students/scholarships/">Scholarships and Bursaries</a></li> <li><a href="/engineering/departments/computing/current-students/studenthub/">DoC student hub</a></li> </ul> </li><li><a href="/engineering/departments/computing/outreach/">Outreach and Engagement</a> <ul class="multilevel-linkul-0"> <li><a href="/engineering/departments/computing/outreach/outreach-news-and-events/">Outreach news and events</a></li> <li><a href="/engineering/departments/computing/outreach/public-lecture-series/">Public Lecture Series</a></li> <li><a href="/engineering/departments/computing/outreach/computing-in-schools/">Computing in Schools</a></li> <li><a href="/engineering/departments/computing/outreach/beyond-the-classroom/">Beyond the Classroom</a></li> <li><a href="/engineering/departments/computing/outreach/girls-in-computing/">Girls in Computing</a></li> <li><a href="/engineering/departments/computing/outreach/child/">Bring your child to work day</a></li> </ul> </li><li><a href="/engineering/departments/computing/industry/">Industry</a> <ul class="multilevel-linkul-0"> <li><a href="/engineering/departments/computing/industry/campus-recruitment/">Recruit our Students</a></li> <li><a href="/engineering/departments/computing/industry/cpp/">Corporate Partnership Programme</a></li> <li><a href="/engineering/departments/computing/industry/placements/">Industrial Placements & Internships</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/industry/placements/undergraduate-placements/">Undergraduate Placements</a></li> <li><a href="/engineering/departments/computing/industry/placements/mai-internships/">MSc AI Internships</a></li> </ul> </li> <li><a href="/engineering/departments/computing/industry/industrial-liaison/">Industrial Advisory Board</a> <ul class="multilevel-linkul-1"> <li><a href="/engineering/departments/computing/industry/industrial-liaison/membership/">Membership</a></li> <li><a href="/engineering/departments/computing/industry/industrial-liaison/terms/">Terms of reference</a></li> </ul> </li> <li><a href="/engineering/departments/computing/industry/aci/">Applications of Computing in Industry</a></li> <li><a href="/engineering/departments/computing/industry/sponsorship/">Prizes and sponsorship</a></li> <li><a href="/engineering/departments/computing/industry/consultancy/">Consultancy</a></li> <li><a href="/engineering/departments/computing/industry/collaborations/">Collaborations</a></li> </ul> </li>  </ul> </nav> </div> </div> </div> </div> </header> <main id="page"> <div class="show-no-js"> <div class="container"> <p class="step-1">In this section</p> <nav class="nav-fallback"> <ul class="nav-fallback__parent"> <li> <a class="lwi" href="/engineering/departments/computing/"> Department of Computing </a> </li> </ul> <ul class="cluster cluster--pad-m"><li><a href="/engineering/departments/computing/research/analysis-and-verification/events/">Events</a></li></ul> </nav> </div> </div> <div class="container content-template" id="content"> <nav class="page-area-heading"> <a href="/engineering/departments/computing/">Department of Computing</a> </nav> <div class="page-heading lg-8 sm-12"> <div class="breadcrumbs"> <ul> <li><a href="/">Imperial Home</a></li> <li><a href="/engineering/">Faculty of Engineering</a></li><li><a href="/engineering/departments/">Departments, institutes and centres</a></li><li><a href="/engineering/departments/computing/">Department of Computing</a></li><li><a href="/engineering/departments/computing/research/">Research</a></li><li><a href="/engineering/departments/computing/research/analysis-and-verification/">Analysis and Verification</a></li> </ul> </div> <h1>Analysis and Verification</h1> </div> <div class="row row--space-between flow-opposite top" id=""> <aside class="col lg-3 md-4 sm-12"> <div class="section-sidebar section-sidebar--consistent"> <div class="section-sidebar__parent"> <a class="lwi" href="/engineering/departments/computing/research/"><svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"><use xlink:href="/assets/website/images/svg/icons.svg#arrow-left"></use></svg>Research</a></div> <div class="section-sidebar__content" id="section-sidebar-content"> <ul class="section-sidebar__list flow-xs"> <li><a href="/engineering/departments/computing/research/analysis-and-verification/events/">Events</a></li></ul> </div> </div> </aside> <div class="col lg-8 sm-12" role="main" id="primary-content">  <div class="module flow-m"> <div class="row wysiwyg"> <p>We face a fundamental problem: computer systems are critical to modern society but traditional non-mathematical computer engineering techniques, such as informal prose specification and ad-hoc testing, cannot make them safe, reliable and secure. The only solution is to bring a mathematically rigorous, scientific method to the specification, testing and verification of the complex computer infrastructure on which society depends.</p> <p>The Verification theme comprises academics unified by a common interest in symbolic analysis at scale, at the forefront of research developments in fundamental theories and industrial-strength tools, targeting real-world applications ranging from multi-core systems, programming languages, autonomous vehicles and web services. Our specialist research uses techniques such as symbolic testing, program logics, type theories, model checking and process algebras.</p> </div> <div class="row video-playlist keyline"> <div class="heading"> <h3 class="title not-sr-only">Related videos</h3> </div> <div class="col lg-7 sm-12"> <div class="now-playing">   <div class="video-player" data-src="https://www.youtube.com/watch?v=Fze1DD5-cvY"> <div class="caption"> <div class="video-placeholder "> <img src="/assets/website/images/placeholder/video-placeholder.jpg" alt="Specification and verification of x86 machine-level code"> <a href="#" class="play-button">Play video</a> </div> <h4 class="fake-h3">Specification and verification of x86 machine-level code</h4> <div class="longdesc"> <p><span>We are using theorem-proving techniques to model and analyze x86 software for the purpose of increasing the accuracy and reliability of x86-based products. We have developed an ISA-level x86 emulator in the ACL2 logic; this emulator serves as a precise specification for x86 software.</span></p> </div> </div> </div>   </div> </div> <div class="col lg-5 sm-12 hatch"> <div class="playlist">   <div class="video-playlist-item" data-src="https://www.youtube.com/watch?v=Fze1DD5-cvY" tabindex="0"> <div class="col lg-4 md-0 sm-12"> <div class="video-placeholder "> <img src="/assets/website/images/placeholder/video-placeholder.jpg" alt="Specification and verification of x86 machine-level code"> </div> </div> <div class="col lg-8 md-12"> <h4>Specification and verification of x86 machine-level code</h4> <p>We are using theorem-proving techniques to model and analyze x86 software</p> <div class="longdesc"> <p><span>We are using theorem-proving techniques to model and analyze x86 software for the purpose of increasing the accuracy and reliability of x86-based products. We have developed an ISA-level x86 emulator in the ACL2 logic; this emulator serves as a precise specification for x86 software.</span></p> </div> </div> </div>   <div class="video-playlist-item" data-src="https://www.youtube.com/watch?v=l8ysBPV8OvA&t" tabindex="0"> <div class="col lg-4 md-0 sm-12"> <div class="video-placeholder "> <img src="/assets/website/images/placeholder/video-placeholder.jpg" alt="GPUVerify: Introduction and overview"> </div> </div> <div class="col lg-8 md-12"> <h4>GPUVerify: Introduction and overview</h4> <p>The video demonstrates GPUVerify in action on some practical examples</p> <div class="longdesc"> <p><span>In this video, Alastair Donaldson provides an overview of GPUVerify, which is a tool for analysing OpenCL and CUDA kernels to check for data races and barrier divergence. The video demonstrates GPUVerify in action on some practical examples.</span></p> </div> </div> </div>   <div class="video-playlist-item" data-src="https://www.youtube.com/watch?v=MIL1eiMJPao" tabindex="0"> <div class="col lg-4 md-0 sm-12"> <div class="video-placeholder "> <img src="/assets/website/images/placeholder/video-placeholder.jpg" alt="GPUVerify: Verification method"> </div> </div> <div class="col lg-8 md-12"> <h4>GPUVerify: Verification method</h4> <p>Alastair Donaldson explains how the technique works behind the hood</p> <div class="longdesc"> <p><span>In this second video about GPUVerify, Alastair Donaldson explains about GPUVerify, how the technique works behind the hood, showing how data race analysis for a massively parallel kernel is reduced to analysis of a sequential program.</span></p> </div> </div> </div>   <div class="video-playlist-item" data-src="https://www.youtube.com/watch?v=7v_MZZOqXa4" tabindex="0"> <div class="col lg-4 md-0 sm-12"> <div class="video-placeholder "> <img src="/assets/website/images/placeholder/video-placeholder.jpg" alt="GPUVerify: Predicated execution and invariant inference"> </div> </div> <div class="col lg-8 md-12"> <h4>GPUVerify: Predicated execution and invariant inference</h4> <p>Alastair Donaldson covers two topics: the lock-step predicated execution technique and looping code</p> <div class="longdesc"> <p><span>In the final video about GPUVerify, Alastair Donaldson covers two advanced topics: the lock-step predicated execution technique that the tool uses to handle conditional and looping code, and the manner by which loop invariants are automatically inferred using the Houdini algorithm.</span></p> </div> </div> </div>  </div> </div> </div>  <div class="row equal-height-columns"> <div class="heading"> <h2 class="title fake-h3 not-sr-only">Research groups and centres</h2> </div> <div class="col lg-6 wysiwyg"> <div class="media-item full secondary reverse equal-height"> <div class="content"> <h3 class="title">Groups</h3> <ul> <li><a title="Multicore Programming link opens in a new window" href="http://multicore.doc.ic.ac.uk/ " target="_blank">Multicore Programming Group</a></li> <li><a title="Program Specification and Verification Group" href="https://vtss.doc.ic.ac.uk/">Program Specification and Verification Group</a></li> <li><a class="bannerTitle" href="https://wp.doc.ic.ac.uk/verificationgroup">Research Cluster in Verification and Testing</a></li> <li><a href="https://srg.doc.ic.ac.uk/">Software Reliability Group (SRG)</a></li> <li><a style="font-size: 15px;" title="Sound Programming Languages link opens in a new window" href="http://slurp.doc.ic.ac.uk/" target="_blank">Sound Programming Languages (SLURP)</a></li> <li><a style="font-size: 15px;" title="Verification of Autonomous Systems link opens in a new window" href="http://vas.doc.ic.ac.uk/" target="_blank">Verification of Autonomous Systems (VAS)</a></li> </ul> </div> </div> </div> <div class="col lg-6 wysiwyg"> <div class="media-item full primary reverse equal-height"> <div class="content"> <h3 class="title">Centres</h3> <ul> <li><a title="Research Institute in Verified Trustworthy Software Systems link opens in a new window" href="https://vetss.org.uk/" target="_blank">Research Institute in Verified Trustworthy Software Systems</a></li> </ul> </div> </div> </div> </div>  <div class="row wysiwyg"> <h2>Events</h2> <p>PhD students, RAs, and faculty whose work is related to the <a title="https://www.imperial.ac.uk/computing/research/programming-languages/" href="https://www.imperial.ac.uk/computing/research/programming-languages/" target="_blank" rel="noopener noreferrer" data-auth="NotApplicable" data-safelink="true" data-linkindex="1">Programming Languages</a> or <a title="https://www.imperial.ac.uk/computing/research/analysis-and-verification/" href="https://www.imperial.ac.uk/computing/research/analysis-and-verification/" target="_blank" rel="noopener noreferrer" data-auth="NotApplicable" data-safelink="true" data-linkindex="2">Analysis & Verification</a> themes are invited to take part in a <a href="/engineering/departments/computing/research/analysis-and-verification/events/">regular get together for the theme</a>. </p> <p> </p> </div><div class="row wysiwyg"> <h2>Academics</h2> </div> <div class="row wysiwyg"> <h2 class="sr-only">Academics</h2> </div> <ul class="people list wysiwyg">  <li> <h3 class="sr-only">Dr Cristian Cadar</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/cadar__s--tojpeg_1491825861878_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="https://www.doc.ic.ac.uk/~cristic/"><span class="person-name">Dr Cristian Cadar</span></a> <span class="job-title">Professor in Software Reliability</span> <p class="contact"><a class="email" href="mailto:c.cadar@imperial.ac.uk">Send email</a><span class="tel">+44 (0)20 7594 8244</span></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>435, Huxley Building</p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> Software engineering, computer systems, software security, practical techniques for improving software reliability and security. </p> </div> </li> <li> <h3 class="sr-only">Prof Alastair Donaldson</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/pwpimage-(3)--tojpeg_1491818712736_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="http://www.imperial.ac.uk/people/alastair.donaldson"><span class="person-name">Prof Alastair Donaldson</span></a> <span class="job-title">Professor</span> <p class="contact"><a class="email" href="mailto:alastair.donaldson@imperial.ac.uk">Send email</a><span class="tel">+44 (0)20 7594 8266</span></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>422, Huxley Building</p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> Formal verification for multicore software, software performance optimization. <strong> <br> </strong> </p> </div> </li> <li> <h3 class="sr-only">Prof. Sophia Drossopoulou</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/pwpimage-(6)--tojpeg_1491819965444_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="https://wp.doc.ic.ac.uk/sd/"><span class="person-name">Prof. Sophia Drossopoulou</span></a> <span class="job-title">Professor of Programming Languages</span> <p class="contact"><a class="email" href="mailto:s.drossopoulou@imperial.ac.uk">Send email</a><span class="tel">+44 (0)20 7594 8368</span></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>559, Huxley Building</p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> Concurrent programming, program verification, characterization of program evolution, theorem proving. </p> </div> </li> <li> <h3 class="sr-only">Prof. Susan Eisenbach</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/pwpimage-(7)--tojpeg_1491820389281_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="http://wp.doc.ic.ac.uk/susan/"><span class="person-name">Prof. Susan Eisenbach</span></a> <span class="job-title">Emeritus Professor</span> <p class="contact"><a class="email" href="mailto:s.eisenbach@imperial.ac.uk">Send email</a><span class="tel">+44 (0)20 7594 8264</span></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>569<span>, Huxley Building</span></p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> <span> Programming Languages, Concurrency and Testing. </span> </p> </div> </li> <li> <h3 class="sr-only">Prof. Philippa Gardner</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/pwpimage-(5)--tojpeg_1491819615308_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="http://www.imperial.ac.uk/people/p.gardner"><span class="person-name">Prof. Philippa Gardner</span></a> <span class="job-title">Professor of Theoretical Computer Science</span> <p class="contact"><a class="email" href="mailto:p.gardner@imperial.ac.uk">Send email</a><span class="tel">+44 (0)20 7594 8292</span></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>453, Huxley Building</p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> Programming languages, program analysis and verification, concurrency and resource reasoning. </p> </div> </li> <li> <h3 class="sr-only">Dr Ben Livshits</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/portrait-dark-2016--tojpeg_1496831027211_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="https://www.doc.ic.ac.uk/~livshits/"><span class="person-name">Dr Ben Livshits</span></a> <span class="job-title">Reader</span> <p class="contact"><a class="email" href="mailto:b.livshits@imperial.ac.uk">Send email</a></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>569, Huxley Building</p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> Security, privacy, program analysis, compilers, software engineering and crowd-sourcing. </p> </div> </li> <li> <h3 class="sr-only">Prof. Alessio Lomuscio</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/alessio--tojpeg_1578925991297_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="http://www.doc.ic.ac.uk/~alessio/"><span class="person-name">Prof. Alessio Lomuscio</span></a> <span class="job-title">Professor of Safe Artificial Intelligence</span> <p class="contact"><a class="email" href="mailto:a.lomuscio@imperial.ac.uk">Send email</a><span class="tel">+ 44 (0)20 7594 8414</span></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>I-X<strong>, </strong>Translation and Innovation Hub (I-HUB), White City Campus</p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> Logic-based specification, verification of autonomous systems. </p> </div> </li> <li> <h3 class="sr-only">Dr Sergio Maffeis</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/photo--tojpeg_1491819715229_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="https://www.doc.ic.ac.uk/~maffeis/"><span class="person-name">Dr Sergio Maffeis</span></a> <span class="job-title">Senior Lecturer</span> <p class="contact"><a class="email" href="mailto:sergio.maffeis@imperial.ac.uk">Send email</a><span class="tel">+44 (0)20 7594 8390</span></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>441, Huxley Building</p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> Software security; network and web security; applications of machine learning to security; security of machine learning; formal methods. </p> </div> </li> <li> <h3 class="sr-only">Dr. Azalea Raad</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/Azalea-Raad--tojpeg_1569237152157_x4-3.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="http://www.soundandcomplete.org/"><span class="person-name">Dr. Azalea Raad</span></a> <span class="job-title">Reader in Programming Languages</span> <p class="contact"><a class="email" href="mailto:azalea.raad06@imperial.ac.uk">Send email</a></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>Huxley Building</p> </div> </li> <li> <h3 class="sr-only">Dr Herbert Wiklicky</h3> <div class="person-wrapper"> <img src="https://pxl-imperialacuk.terminalfour.net/fit-in/428x572/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/herbert--tojpeg_1491818987912_x4.jpg" alt="" class="thumbnail"> </div> <div class="name-wrapper"> <h4>Personal details</h4> <a class="name-link" target="_blank" href="https://www.doc.ic.ac.uk/~herbert/"><span class="person-name">Dr Herbert Wiklicky</span></a> <span class="job-title">Reader in Computer Science</span> <p class="contact"><a class="email" href="mailto:h.wiklicky@imperial.ac.uk">Send email</a><span class="tel">+44 (0)20 7594 8206</span></p> </div> <div class="address-wrapper"> <h4>Location</h4> <p>424, Huxley Building</p> </div> <div class="dept-wrapper"> <h4>Research interests</h4> <p> Program analysis, programming languages, semantics, probabilistic models, program synthesis, semantics in computer security, quantum computation. <strong> <br> <br> </strong> </p> </div> </li>  </ul>  </div> <section class="supplementary-content row"> <div class="supplementary-content__sizer col"></div> <div class="col lg-12 link-list "> <div class="module">  <h2>Find out more</h2> <nav> <ul> <li> <a href='/engineering/departments/computing/research/tech-reports/'> View our Technical Reports </a> </li> <li> <a href='/engineering/departments/computing/prospective-students/phd/'> Apply for PhD studentships </a> </li> </ul> </nav> </div> </div>   <div class="col lg-12 news"> <div class="module"> <a href="/engineering/departments/computing/about/news/"> <div class="media"><img srcset="https://pxl-imperialacuk.terminalfour.net/fit-in/302x302/prod01/channel_3/media/migration/faculty-of-engineering/sunrise-1765027_960_720--tojpeg_1502292816320_x4.jpg 302w, https://pxl-imperialacuk.terminalfour.net/fit-in/604x604/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/sunrise-1765027_960_720--tojpeg_1502292816320_x4.jpg 604w, https://pxl-imperialacuk.terminalfour.net/fit-in/1208x1208/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/sunrise-1765027_960_720--tojpeg_1502292816320_x4.jpg 1208w, https://pxl-imperialacuk.terminalfour.net/fit-in/302x302/prod01/channel_3/media/migration/faculty-of-engineering/sunrise-1765027_960_720--tojpeg_1502292816320_x4.jpg 1x, https://pxl-imperialacuk.terminalfour.net/fit-in/604x604/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/sunrise-1765027_960_720--tojpeg_1502292816320_x4.jpg 2x, https://pxl-imperialacuk.terminalfour.net/fit-in/1208x1208/filters:upscale()/prod01/channel_3/media/migration/faculty-of-engineering/sunrise-1765027_960_720--tojpeg_1502292816320_x4.jpg 3x" sizes="(min-width: 1520px) 302px, (min-width: 1025px) calc(25vw - 76px), (min-width: 930px) calc(25vw - 76px), (min-width: 481px) calc(50vw - 68px), calc(100vw - 48px)" alt="" width="1208" height="1208" loading="lazy" src="https://pxl-imperialacuk.terminalfour.net/prod01/channel_3/media/migration/faculty-of-engineering/sunrise-1765027_960_720--tojpeg_1502292816320_x4.jpg"></div> <ul class="tags"> <li class="parent topic not-reverse"> <span>News</span> </li> <li class="feature topic teal"><span>Events</span></li> </ul> <div class="content"> <h3 class="title">News and events</h3> <p class="description">Click here to discover what we've been up to and how you can get involved.</p> </div> </a> </div> </div>  </section>  </div> </div> </div> </main> <footer class="footer" role="contentinfo"> <section class="footer__sub"> <header class="sr-only"> <h2 class="sr-only">Contact and Links</h2> </header> <div class="container"> <div class="bordered-section"><div class="row row--space-between row--gap-on-collapse" itemscope itemtype="https://schema.org/Organization"> <div class="col lg-4 sm-12"> <h3 class="step-4"><span itemprop="name">Department of Computing</span></h3></div> <div class="col lg-7 md-8 sm-12"> <div class="row row--sub-footer" itemscope itemtype="http://schema.org/PostalAddress"> <div class="col lg-6 xs-12"> <div class="flow-xs"> <h4 class="step-0">Faculty of Engineering</h4> <p>Imperial College London<br />South Kensington Campus<br />London SW7 2AZ</p> <a href="https://goo.gl/maps/b75oKUXoByt" target="_blank" class="location-link" >Map</a> </div> </div><div class="col lg-6 xs-12"> <div class="flow-xs"> <h4 class="step-0">Get in touch</h4> <nav class="flow-xs"> <p><a href="/engineering/departments/computing/about/useful-contacts/">Useful contacts</a></p> <p><a href="mailto:ugadmissions@doc.ic.ac.uk" target="_blank" >UG admissions enquiries</a></p> <p><a href="mailto:doc-mscadmissions@imperial.ac.uk" target="_blank" >MSc admissions enquiries</a></p> <p><a href="mailto:a.o.el-kholy@imperial.ac.uk" target="_blank" >PhD admissions enquiries</a></p> </nav> </div> </div><div class="col lg-6 xs-12"> <div class="flow-xs"> <h4 class="step-0">Quick links</h4> <nav class="flow-xs"> <p><a href="/engineering/departments/computing/about/job-vacancies/">Job opportunities</a></p> <p><a href="/engineering/departments/computing/industry/cpp/">Recruit our students</a></p> <p><a href="/engineering/departments/computing/outreach/">Outreach</a></p> <p><a href="/engineering/departments/computing/people/csg/">Computing Support Group (CSG)</a></p> </nav> </div> </div><div class="col lg-6 xs-12"> <div class="flow-xs"> <h4 class="step-0">Find us on social media</h4> <nav> <ul class="footer__social cluster"> <li><a href="https://twitter.com/ICComputing" target="_blank" itemprop="sameAs"> <span class="sr-only">X, formerly known as Twitter</span> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#twitter"></use> </svg> </a></li> <li><a href="https://www.linkedin.com/company/69234403/admin/" target="_blank" itemprop="sameAs"> <span class="sr-only">LinkedIn</span> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#linkedin"></use> </svg> </a></li> </ul> </nav> </div> </div></div> </div> </div> </div> </div></section> <section class="footer__main"> <h2 class="sr-only">Useful Links</h2> <div class="container"> <div class="row row--gap-on-collapse"> <nav class="col lg-3 sm-12"> <div class="flow-s"> <h3 class="step--1">Popular links</h3> <ul> <li><a href="/admin-services/ict/self-service/digital-education-services/digital-education-platforms/blackboard/">Blackboard</a></li> <li><a href="/admin-services/ict/contact-ict-service-desk/">Contact the Service Desk</a></li> <li><a href="/jobs/">Jobs</a></li> <li><a href="/admin-services/library/">Library services</a></li> <li><a href="https://email.imperial.ac.uk" target="_blank" rel="noopener">Outlook email online</a></li> </ul> </div> </nav> <nav class="col lg-3 sm-12"> <div class="flow-s"> <h3 class="step--1">Faculties</h3> <ul> <li><a href="/engineering/">Engineering</a></li> <li><a href="/medicine/">Medicine</a></li> <li><a href="/natural-sciences/">Natural Sciences</a></li> <li><a href="https://www.imperial.ac.uk/business-school/" target="_blank" rel="noopener">Imperial College Business School</a></li> </ul> </div> </nav> <nav class="col lg-3 sm-12"> <div class="flow-s"> <h3 class="step--1">Directories</h3> <ul> <li><a href="/admin-services/">Admin and support services </a></li> <li><a href="/multidisciplinary-research/">Networks and Centres </a></li> <li><a href="/a-z-research/">Research groups </a></li> <li><a href="https://profiles.imperial.ac.uk/" target="_blank" rel="noopener">Search all staff</a></li> </ul> </div> </nav> <nav class="col lg-3 sm-12"> <div class="flow-s"> <h3 class="step--1">Partners</h3> <ul> <li><a href="https://ahsc.org.uk/" target="_blank" rel="noopener">Imperial College Academic Health Science Centre </a></li> <li><a href="https://imperialcollegehealthpartners.com/" target="_blank" rel="noopener">Imperial College Health Partners </a></li> <li><a href="https://www.imperial.nhs.uk/" target="_blank" rel="noopener">Imperial College Healthcare NHS Trust </a></li> <li><a href="https://www.imperial-consultants.co.uk/" target="_blank" rel="noopener">Imperial Consultants</a></li> </ul> </div> </nav> </div> </div> </section> <section itemscope itemtype="http://schema.org/CollegeOrUniversity"> <h2 class="sr-only">College Information</h2> <div class="container"> <div class="footer__common"> <div class="row"> <div class="col lg-3 sm-12"> <div class="footer__contact flow-s"> <a href="#" class="footer__brand"> <span class="sr-only" itemprop="name">Imperial College London</span> <svg width="727" height="80" viewBox="0 0 727 80" fill="none" xmlns="http://www.w3.org/2000/svg"> <path d="M301.453 0V80H353.346V66H316.622V46H350.152V32.4H316.622V14H353.346V0H301.453Z" fill="currentcolor"/> <path d="M238.397 12.9177H227.22V39.8776H238.397C247.142 39.8776 253.566 35.6376 253.566 26.3953C253.566 16.8 247.142 12.9177 238.397 12.9177ZM239.196 52.8H227.22V80H212.052V0H239.196C256.219 0 269.533 7.72706 269.533 26.4C269.533 44.8 256.121 52.8 239.196 52.8Z" fill="currentcolor"/> <path d="M485.079 0V14H503.84V66H485.079V80H537.77V66H519.009V14H537.77V0H485.079Z" fill="currentcolor"/> <path d="M434.191 24.8C434.191 34.4377 428.602 37.4777 419.022 37.4777H406.248V12.9177H419.022C429.419 12.9224 434.191 16.8 434.191 24.8ZM450.158 24.8C450.158 6.12706 437.384 0 420.619 0H391.08V80H406.248V50.4H419.022C419.722 50.4 420.417 50.3859 421.107 50.3624L436.562 80H453.37L436.224 47.1906C444.565 43.4777 450.158 36.3435 450.158 24.8Z" fill="currentcolor"/> <path d="M604.324 14.1929L615.238 49.4777H593.406L604.324 14.1929ZM594.345 0L567.999 80H583.966L589.409 62.4H619.235L624.678 80H640.645L614.299 0H594.345Z" fill="currentcolor"/> <path d="M674.889 0V80H726.914V66H690.058V0H674.889Z" fill="currentcolor"/> <path d="M151.908 0L132.747 47.04L113.587 0H92.0312V80H106.402V20.1882L124.764 62.4H140.731L159.093 20.1882V80H173.463V0H151.908Z" fill="currentcolor"/> <path d="M0 0V14H18.7613V66H0V80H52.6912V66H33.93V14H52.6912V0H0Z" fill="currentcolor"/> </svg> </a> <meta itemprop="url" content="https://www.imperial.ac.uk/"> <meta itemprop="image" content="https://www.imperial.ac.uk/ImageCropToolT4/imageTool/uploaded-images/homepage-default-social--tojpeg_1523872141375_x1.jpg"> <meta itemprop="logo" content="https://www.imperial.ac.uk/assets/website/images/logo/imperial-600.png"> <meta itemprop="sameAs" content="https://en.wikipedia.org/wiki/Imperial_College_London"> <div class="address"> <h3 class="sr-only">Address</h3> <p itemscope itemtype="http://schema.org/PostalAddress" itemprop="address"> <span itemprop="name">Imperial College London</span><br /> <span itemprop="streetAddress">South Kensington Campus</span><br /> <span itemprop="addressLocality">London</span> <span itemprop="postalCode">SW7 2AZ</span>, <span itemprop="addressCountry">UK</span><br /> <span itemprop="telephone">tel: +44 (0)20 7589 5111</span> </p> </div> </div> </div> <div class="col lg-9 sm-12"> <div class="footer__info flow-s" id="footer-info"> <div class="footer__social cluster cluster--pad-m"> <a href="https://www.facebook.com/imperialcollegelondon" target="_blank" itemprop="sameAs"> <span class="sr-only">Facebook</span> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#facebook"></use> </svg> </a> <a href="https://twitter.com/imperialcollege" target="_blank" itemprop="sameAs"> <span class="sr-only">X, formerly known as Twitter</span> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#twitter"></use> </svg> </a> <a href="https://www.youtube.com/user/imperialcollegevideo" target="_blank" itemprop="sameAs"> <span class="sr-only">YouTube</span> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#youtube"></use> </svg> </a> <a href="https://www.linkedin.com/edu/imperial-college-london-12598" target="_blank" itemprop="sameAs"> <span class="sr-only">LinkedIn</span> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#linkedin"></use> </svg> </a> <a href="https://instagram.com/imperialcollege" target="_blank" itemprop="sameAs"> <span class="sr-only">Instagram</span> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#instagram"></use> </svg> </a> <a href="https://www.tiktok.com/@imperialcollege" target="_blank" itemprop="sameAs"> <span class="sr-only">TikTok</span> <svg role="img" aria-hidden="true" focusable="false" class="icon icon--m"> <use xlink:href="/assets/website/images/svg/icons.svg#tiktok"></use> </svg> </a> </div> <nav> <h3 class="sr-only">Site Information</h3> <ul class="footer__meta"> <li><a href="/sitemap/">Sitemap</a></li> <li><a href="/about-the-site/accessibility/">Accessibility</a></li> <li><a href="/admin-services/finance/purchasing/related-policy-statements/modern-slavery/">Modern slavery statement</a></li> <li><a href="/about-the-site/privacy/">Privacy notice</a></li> <li><a href="/about-the-site/use-of-cookies/">Use of cookies</a></li> <li><a href="/about-the-site/incorrect-content/">Report incorrect content</a></li> <li class="hide-sm"><a class="t4Edit-page" href="https://t4-cms.imperial.ac.uk/terminalfour/page/section#edit/105001/contents">Log in</a></li> </ul> </nav> <p class="footer__copyright">© 2025 Imperial College London</p> </div> </div> </div> </div> </div> </section> </footer> </body> </html>

CINXE.COM

Analysis and Verification | Faculty of Engineering | Imperial College London