PhD Position in Formalizing Number Systems

We have an open PhD position in Bridging the Gap Between Mathematical Numbers and Software Systems. To fill this position, we are seeking an enthusiastic PhD candidate with a strong background in computer science, software engineering, mathematics, or closely related fields. Expertise in formal methods such as program reasoning, programming language semantics, model checking, theorem proving, or computational logic is essential.

Imperceptible Black-box Adversarial Perturbations

Over the last few decades, deep neural networks (DNNs) have exhibited remarkable success in natural language processing (NLP). However, despite their impressive performance, DNNs have been shown to be highly vulnerable to adversarial examples, which are carefully crafted inputs with small, often imperceptible perturbations that cause models to make incorrect predictions. This vulnerability poses growing threats to security and privacy in online and safety-critical environments.

Verification of Stateful Protocols

There are at least three reasons why it is desirable to perform proofs of security in a proof assistant like Isabelle/HOL or Rocq. First, it gives us an overwhelming assurance that the proof of security is actually a proof and not just the result of a bug in a complex verification tool.

Test and Proof Track and FM 2026

Since 2007, the Test and Proof (TAP) conference has long been a leading venue for research on the intersection of software testing and formal verification. Now, TAP is joining the 27th International Symposium on Formal Methods (FM 2026) as a new special track. This integration places the ground-breaking work of the Test and Proofs community at the heart of the world’s premier conference on formal methods.

 

Welcome to the blog of the Software Assurance & Security Research Team at the University of Exeter. We blog regularly news, tips & tricks, as well as fun facts about software assurance, reliability, security, testing, verification, hacking, and logic.

You can also follow us on Twitter: @logicalhacking.

Categories

Archive

Tags

FormalMethods Isabelle/HOL ML/AI ProgramVerification SoftwareEngineering academia ai android apidesign appsec bitcoin blockchain bpmn browser browserextensions browsersecurity bug certification chrome composition confidentiality cordova dast devops devsecops dom dsbd efsm epsrc event events extensions fixeffort floss formaldocument formalmethods formalverification funding hol-ocl hol-testgen humanfactor hybridapps iast industry internetofthings iot isabelle/hol isabelledof isabellehol isadof itp latex logic maintance malicous mathematics mbst mobile mobile apps modelinference modeling monads monitoring msc neuralnetwork ocl ontology opensource owasp patches pedadogy pet phd phdlife phishing policy programminglanguages protocols protocolverfication publishing reliability research safelinks safety sap sast sdlc secdevops secureprogramming security securityengineering securitytesting semantics servicecomposition skills smartcontract smartcontracts smartthings smpc softwareeinginering softwaresecurity softwaresupplychain solidity staff&positions statemachine studentproject tcb teaching test&proof test@proof testing tips&tricks tools transport tuos uk uoe upgrade usability verification vulnerabilities vulnerableapplication webinar websecurity

Search


blog whole site