Logic List Mailing Archive

Three PhD student positions in verification, Sheffield (England)

Up to three fully funded research and teaching assistant positions with 
the opportunity of undertaking a PhD are available within the Verification 
Group, Department of Computer Science, at the University of Sheffield: 
<https://www.sheffield.ac.uk/dcs/research/groups/verification> The 
verification group at Sheffield is growing rapidly. These posts provide 
excellent opportunities for graduate students (UK and overseas) to obtain 
a PhD in any active research area of the group, including semantics of 
concurrent and distributed systems, logics and complexity, algebraic and 
categorical approaches to program semantics, verification of multi-core 
programs and weak memory models, interactive theorem proving.

The posts are fully funded for 6 years with 60% devoted to research and 
40% to teaching support..

For more detailed information (including roles and responsibilities), 
please see


For details on possible supervisors and research projects, please contact 
our personal websites from our group webpage

<https://www.sheffield.ac.uk/dcs/research/groups/verification> For 
informal enquiries, please do not hesitate to contact any group member by 

Dr. Jonni Virtema is keen to supervise students in any area of his current 
research, which relate to the interplay of logic and complexity theory. 
Current topics include logics and complexity theory related to numerical 
data, and temporal logics designed to express so-called hyperproperties, 
which are important in information flow and security. A further emerging 
topic is to study foundations of neural networks using the machinery of 
logics and complexity theory related to numerical data. See 
http://www.virtema.fi/ <http://www.virtema.fi/> for further details.

Dr. Harsh Beohar is broadly interested in comparative concurrency 
semantics and in the interplay of category theory, logic, and semantics. 
Current topics include expressive modal logics, behavioural equivalence 
games, synthesising distinguishing/characteristic formulae all at the 
level of coalgebras. See https://dblp.org/pid/13/7482.html 
<https://dblp.org/pid/13/7482.html> for an uptodate list of publications.

Dr. Mike Stannett is interested in formal verification of physical 
theories, using Isabelle/HOL to verify first-order special and general 
relativity. Working with researchers at the Renyi Institute in Budapest he 
has successfully verified the “No Faster-than-Light Observers” theorem for 
special relativity; he is now collaborating on a locale-based extension of 
this proof to cover the corresponding theorem of general relativity. Other 
topics of interest include extending the Hungarian theories to generate a 
combined first-order quantum/relativistic theory. See 
<https://scholar.google.com/citations?user=kppqMecAAAAJ> for a list of 
[LOGIC] mailing list
Archive: http://www.illc.uva.nl/LogicList/

provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam