Professor Paul Curzon, BA MA PhD (Cantab) PGCert(HE) NTFS FBCS CITPProfessor of Computer ScienceEmail: p.curzon@qmul.ac.ukTelephone: +44 20 7882 5815Room Number: Peter Landin, CS 304Website: http://www.eecs.qmul.ac.uk/~pcTeachingResearchPublicationsPublic EngagementTeachingProcedural Programming (Undergraduate) This is an introductory module in computer programming focussing on procedural programming using Java. You will learn the basic concepts of procedural programming and learn to write and reason about simple programs. A focus is on writing good defensive code that is easy for others to understand. The main topics covered are: storing and manipulating data, control structures, methods and recursion, and algorithms for searching and sorting data. Classes include weekly lectures and lab sessions. You will be assessed by coursework throughout the term and by an end-of-semester exam. Both will require you to demonstrate that you can write programs and understand theory. Interactive System Design (Postgraduate/Undergraduate) The main areas of study are (i) interaction and design (ii) modelling of interaction (iii) the design process (iv) design principles and (v) usability evaluation. Various types of interfaces will be considered including those encountered on the web and mobile computing devices. A historical perspective is encouraged in order to provide a means of understanding current and projected developments in the discipline and profession of interactive computer system design. The module will include seminars and group laboratory classes in which analysis, design and evaluation methods will be used in practical contexts. Students will be expected to participate fully in the seminars by presenting and discussing their own designs and evaluations. Students will be required to construct prototype interfaces using techniques of their own choice (e.g. Java, Director).ResearchResearch Interests:My research combines the areas of Computer Science Education, and interaction design for healthcare. In the past I worked primarily in the areas of automated reasoning and formal verification. I also have a strong interest in the public understanding of science. Formal Cognitive Modelling and Human Error My main focus at the moment is on human error, extending my work on the verification of hardware/software systems to human-computer systems. The idea is to consider the human operators of such interactive systems as part of the system under verification, so bringing systematic human error, not just software and hardware error, within the scope of the approach. I am, in particular, exploring the use of formal models of human behaviour based on results from cognitive psychology in the design of interactive systems. This work is in collaboration with UCL Interaction Center. Questions we are exploring include: 'How can formal models of human behaviour form the basis of verification methods that can detect design flaws that lead to systematic human error?'; 'How can empirical investigations inform the development of formal models of human behaviour used for verification, and vice versa?' and 'How can formally-based usability evaluation methods best support the analyst?' Verification of Verification Systems My work on the design and verification of hybrid verification systems is in collaboration with Concordia University. We developed a verification system that combined the power of the MDG and HOL tools. It harnesses the abstraction techniques of the automated MDG multiway decision diagram (which is superior to boolean decision diagrams) system combined with theorem proving power of HOL to manage the process. In related work we developed a novel methodology that justifies importing results into a theorem prover using verified linkage theorems. It is based on a combination of compiler verification techniques. Social Aspects of Interaction Design I am also working on several projects investigating social aspects of interaction design, for example related to navigation and design for all. Questions of interest include: 'How can systems be designed so as to build on our cognitive strengths, especially as we age?'. Navigation systems designed to exploit and extend our cognitive maps rather than replace them are being used as an exemplar of this. Public Engagement in Science A major aspect of my work is in the public engagement in computer science (and science, maths and engineering more generally). I aim to generate excitement not just about the School's research but about interdisciplinary research in the subject more generally. The main way of achieving this is through the internationally renowned public engagement project cs4fn (cs4fn.blog) that I created with Peter McOwan, and its sister project for teachers Teaching London Computing (teachinglondoncomputing.org)Publications Curzon P, Waite J, Maton K (2024). Teaching CS with and through other forms of knowledge. nameOfConference DOI: 10.1145/3677619.3678104 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/98252 MacBrayne A, Curzon P, Soyel H et al. (publicationYear). Attitudes to technology supported rheumatoid arthritis care: investigating patient and clinician perceived opportunities and barriers. nameOfConference DOI: 10.1093/rap/rkad089 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/92300 Dowse A, Curzon P, Morrissey D (2023). Willingness, Motivators and Barriers to using Anxiety-focused Apps in people with and without chronic pain: A Questionnaire Study.. British Pain Society - 56th Annual Scientific Meeting DOI: doi QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/88827 Curzon P, Macbrayne A, Humby F et al. (2023). Attitudes to Technology supported Rheumatoid Arthritis care Questionnaire study: Barriers to People with RA & their clinicians using Technology in the care pathway. British Society for Rheumatology Annual COnference 2023 DOI: 10.1093/rheumatology/kead104.154 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/84912 Curzon P, Macbrayne A, Soyel H et al. (2023). Attitudes to Technology supported Rheumatoid Arthritis care, questionnaire study: Opportunities for technology to improve RA care. British Society for Rheumatology Annual Conference, 2023 DOI: 10.1093/rheumatology/kead104.322 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/84913 Curzon P, Macbrayne A, Soyel H et al. (2023). Attitudes to Technology supported Rheumatoid Arthritis care: Opportunities & Barriers for technology in RA -Key themes from Qualitative arm of Mixed-Methods Study. British SOciety for Rheumatology Annual COnference, 2023 DOI: 10.1093/rheumatology/kead104.174 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/84914 Curzon P, McOwan PW (2023). Conjuring with Computation, A Manual of Magic and Computing for Beginners. nameOfConference DOI: 10.1142/13085 QMRO: qmroHref Fahmi A, Soyel H, Marsh DWR et al. (2020). From Personalised Predictions to Targeted Advice: Improving Self-Management in Rheumatoid Arthritis. Integrated Citizen Centered Digital Health and Social Care DOI: 10.3233/SHTI200695 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/69045 Fahmi A, Soyel H, Marsh W et al. (2020). From personalised predictions to targeted advice: Improving self-management in rheumatoid arthritis. nameOfConference DOI: 10.3233/SHTI200695 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/69046 Curzon P, Waite J, Maton K et al. (2020). Using Semantic Waves to Analyse the Effectiveness of Unplugged Computing Activities. The 15th Workshop in Primary and Secondary Computing Education DOI: 10.1145/3421590.3421606 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/66685 Waite J, Curzon P, Marsh W et al. (2020). Difficulties with design: The challenges of teaching design in K-5 programming. nameOfConference DOI: 10.1016/j.compedu.2020.103838 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/62819 Waite JL, Maton K, Curzon P et al. (2019). Unplugged Computing and Semantic Waves: Analysing Crazy Characters. The UK and Ireland Computing Education Research Conference DOI: 10.1145/3351287.3351291 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/62375 CURZON P, Bell T, Waite JL et al. (2019). Computational Thinking. nameOfConference DOI: 10.1017/9781108654555.018 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/57010 Waite JL, CURZON P, MARSH DW et al. (2018). Comparing K-5 teachers’ reported use of design in teaching programming and planning in teaching writing. WiPSCE 2018 (13th Workshop in Primary and Secondary Computing Education) DOI: 10.1145/3265757.3265761 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/54383 Waite JL, CURZON P, MARSH D et al. (2018). Abstraction in action: K-5 teachers' uses of levels of abstraction, particularly the design level, in teaching programming. nameOfConference DOI: 10.21585/ijcses.v2i1.23 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/32505 CURZON P, Furniss D, Blandford A (2017). Exploring organisational competences in Human Factors and UX project work: Managing careers, project tactics and organisational strategy. nameOfConference DOI: 10.1080/00140139.2017.1405081 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/28989 Waite JL, curzon P, marsh D et al. (2017). K-5 Teachers' Uses of Levels of Abstraction Focusing on Design. WiPSCE 2017 DOI: doi QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/28463 McOwan PW, Curzon P (2017). Coding cleverness. nameOfConference DOI: 10.4324/9781315545813-5 QMRO: qmroHref Harrison MD, Masci P, Campos JC et al. (2017). Demonstrating that Medical Devices Satisfy User Related Safety Requirements. nameOfConference DOI: 10.1007/978-3-319-63194-3_8 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24766 Masci P, Oladimeji P, Curzon P et al. (2017). Using PVSio-web to Demonstrate Software Issues in Medical User Interfaces. nameOfConference DOI: 10.1007/978-3-319-63194-3_14 QMRO: qmroHref Harrison MD, MASCI P, CAMPOS JC et al. (2017). Verification of User Interface Software: the Example of Use-Related Safety Requirements and Programmable Medical Devices. nameOfConference DOI: 10.1109/THMS.2017.2717910 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24745 CURZON P, Myketiak C, Concannon S (2017). Narrative perspective, person references, and evidentiality in clinical incident reports. nameOfConference DOI: 10.1016/j.pragma.2017.06.018 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24947 Curzon P, Rukšėnas R (2017). Modelling the User. nameOfConference DOI: 10.1007/978-3-319-51838-1_8 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/14961 Harrison MD, Masci PM, Campos JC et al. (2017). The Specification and Analysis of Use Properties of a Nuclear Control System. nameOfConference DOI: 10.1007/978-3-319-51838-1_14 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/14963 Waite JL, Curzon P, marsh D et al. (2016). Abstraction and Common Classroom Activities. WiPSCE 2016 11th Workshop in Primary and Secondary Computing Education DOI: 10.1145/2978249.2978272 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/15115 Curzon P, McOwan PW (2017). The Power of Computational Thinking, Games, Magic and Puzzles to Help You Become a Computational Thinker. nameOfConference DOI: 10.1142/q0054 QMRO: qmroHref Harrison M, Campos JC, Ruksenas R et al. (2016). Modelling information resources and their salience in medical device design. Engineering Interactive Computing Systems 2016 DOI: 10.1145/2933242.2933250 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/12062 Furniss D, Curzon P, Blandford A (publicationYear). Using FRAM beyond safety: A case study to explore how sociotechnical systems can flourish or stall. nameOfConference DOI: 10.1080/1463922X.2016.1155238 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/11597 Rukšenas R, Masci P, Curzon P (2016). Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. nameOfConference DOI: 10.1201/b20053-21 QMRO: qmroHref Ruksenas R, Masci P, Curzon P (2016). Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. nameOfConference DOI: 10.14279/tuj.eceasst.69.964 QMRO: qmroHref CURZON P, Lee P, Meagher L (2015). Impact on procurement and training by research on the interaction design of medical devices. nameOfConference DOI: 10.4108/eai.14-10-2015.2261766 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24774 CURZON P, Thimbleby H, Oladimeji P et al. (2015). Issues in number entry user interface styles: Recommendations for mitigation. nameOfConference DOI: 10.4108/eai.14-10-2015.2261763 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24769 CURZON P, Myketiak, Concannon (2015). New/s Design: Informing Future Design Processes by Understanding Media Reporting of Medical Errors with Medical Devices. nameOfConference DOI: 10.4108/eai.14-10-2015.2261762 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24770 CURZON P, Masci P, Oladimeji P et al. (2015). PVSio-web: mathematically based tool support for the design of interactive and interoperable medical systems. nameOfConference DOI: 10.4108/eai.14-10-2015.2261720 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24773 CURZON P, Blandford AE, Thimbleby H et al. (2015). Safer Interactive Medical Device Design: Insights from the CHI+MED Project. nameOfConference DOI: 10.4108/eai.14-10-2015.2261752 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24768 Harrison M, Campos JC, Masci P et al. (2015). Templates as heuristics for proving properties of medical devices. nameOfConference DOI: 10.4108/eai.14-10-2015.2261743 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/24771 Masci P, Curzon P, Thimbleby H (2015). Early identification of software causes of use-related hazards in medical devices. nameOfConference DOI: 10.4108/eai.14-10-2015.2261754 QMRO: qmroHref Cinzia Bernardeschi PM (2015). Towards a Formalization of System Requirements for an Integrated Clinical Environment. nameOfConference DOI: 10.4108/eai.14-10-2015.2261701 QMRO: qmroHref Wilson J, Curzon P, Duncker E (2015). Exploring older women’s confidence during route planning. nameOfConference DOI: 10.1080/0144929X.2014.960001 QMRO: qmroHref Masci P, Oladimeji P, Zhang Y et al. (2015). PVSio-web 2.0: Joining PVS to HCI. nameOfConference DOI: 10.1007/978-3-319-21690-4_30 QMRO: qmroHref Masci P, Curzon P, Mallozzi P et al. (2015). Using PVSio-web and SAPERE for rapid prototyping of user interfaces in Integrated Clinical Environments. nameOfConference DOI: doi QMRO: qmroHref Campos JC, Curzon P, Harrison MD et al. (2015). Layers, resources and property templates in the specification and analysis of two interactive systems. nameOfConference DOI: doi QMRO: qmroHref Masci P, Rukšėnas R, Oladimeji P et al. (2015). The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. nameOfConference DOI: 10.1007/s11334-013-0200-4 QMRO: qmroHref Masci P, Curzon P, Furniss D et al. (2015). Using PVS to support the analysis of distributed cognition systems. nameOfConference DOI: 10.1007/s11334-013-0202-2 QMRO: qmroHref Furniss D, Masci P, Curzon P et al. (2015). Exploring medical device design and use through layers of distributed cognition: How a glucometer is coupled with its context. nameOfConference DOI: 10.1016/j.jbi.2014.12.006 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/22601 Bella G, Curzon P, Lenzini G (2015). Service Security and Privacy as a Socio-Technical Problem: Literature review, analysis methodology and challenge domains. nameOfConference DOI: 10.3233/JCS-150536 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/10296 Curzon P, McOwan PW, Plant N et al. (2014). Introducing teachers to computational thinking using unplugged storytelling. Proceedings of the 9th Workshop in Primary and Secondary Computing Education DOI: 10.1145/2670757.2670767 QMRO: qmroHref enas RR, Curzon P, Blandford A et al. (2014). Combining Human Error Verification and Timing Analysis: a Case Study on an Infusion Pump. nameOfConference DOI: 10.1007/s00165-013-0288-1 QMRO: qmroHref Bella G, Curzon P, Giustolisi R et al. (2014). A Socio-Technical Methodology for the Security and Privacy Analysis of Services. 2014 IEEE 38th International Computer Software and Applications Conference Workshops DOI: 10.1109/compsacw.2014.69 QMRO: qmroHref Harrison MD, Masci P, Campos J et al. (2014). Automated theorem proving for the systematic analysis of interactive systems. nameOfConference DOI: 10.14279/tuj.eceasst.69.962.943 QMRO: qmroHref Oladimeji P, Masci P, Curzon P et al. (2014). PVSio-web: a tool for rapid prototyping device user interfaces in PVS. nameOfConference DOI: 10.14279/tuj.eceasst.69.963.944 QMRO: qmroHref Masci P, Zhang Y, Jones P et al. (2014). A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software. nameOfConference DOI: 10.4230/OASIcs.MCPS.2014.1 QMRO: qmroHref Masci P, Zhang Y, Jones P et al. (2014). Combining PVSio with Stateflow. nameOfConference DOI: 10.1007/978-3-319-06200-6_16 QMRO: qmroHref Masci P, Zhang Y, Jones P et al. (2014). Formal Verification of Medical Device User Interfaces Using PVS. nameOfConference DOI: 10.1007/978-3-642-54804-8_14 QMRO: qmroHref Curzon P (2013). cs4fn and computational thinking unplugged. nameOfConference DOI: 10.1145/2532748.2611263 QMRO: qmroHref Masci P, Ayoub A, Curzon P et al. (2013). Model-based development of the Generic PCA infusion pump user interface prototype in PVS. nameOfConference DOI: 10.1007/978-3-642-40793-2_21 QMRO: qmroHref Black J, Brodie J, Curzon P et al. (2013). Making Computing Interesting to School Students: Teachers’ Perspectives. ITiCSE '13 Proceedings of the 18th ACM conference on Innovation and technology in computer science education DOI: 10.1145/2462476.2466519 QMRO: qmroHref Masci P, Ayoub A, Curzon P et al. (2013). Verification of interactive software for medical devices. Proceedings of the 5th ACM SIGCHI symposium on Engineering interactive computing systems DOI: 10.1145/2494603.2480302 QMRO: qmroHref Rukšenas R, Curzon P, Harrison MD (2013). Integrating Formal Predictions of Interactive System Behaviour with User Evaluation. nameOfConference DOI: 10.1007/978-3-642-38613-8_17 QMRO: qmroHref Masci P, Ayoub A, Curzon P et al. (2013). Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. nameOfConference DOI: 10.1145/2480296.2480302 QMRO: qmroHref Huang H, Curzon P, White G et al. (2013). Evaluating the methodological constraints and affordances of investigation manuals and their methodologies. nameOfConference DOI: doi QMRO: qmroHref Black J, Curzon P, Myketiak C et al. (2012). Teachers' perceptions of the value of research-based school lectures. nameOfConference DOI: 10.1145/2481449.2481485 QMRO: qmroHref Myketiak C, Curzon P, Black J et al. (2012). cs4fn. nameOfConference DOI: 10.1145/2325296.2325366 QMRO: qmroHref Masci P, Huang H, Curzon P et al. (2012). Using PVS to investigate incidents through the lens of distributed cognition. nameOfConference DOI: 10.1007/978-3-642-28891-3_27 QMRO: qmroHref Masci P, Furniss D, Curzon P et al. (2012). Supporting Field Investigators with PVS: A Case Study in the Healthcare Domain. nameOfConference DOI: 10.1007/978-3-642-33176-3_11 QMRO: qmroHref Blandford A, Cauchi A, Curzon P et al. (2011). Comparing actual practice and user manuals:A case study based on programmable infusion pumps. nameOfConference DOI: doi QMRO: qmroHref Cauchi A, Curzon P, Eslambolchilar P et al. (2011). Towards dependable number entry for medical devices. nameOfConference DOI: doi QMRO: qmroHref Black J, Curzon P, Myketiak C et al. (2011). A Study in Engaging Female Students in Computer Science Using Role Models. nameOfConference DOI: 10.1145/1999747.1999768 QMRO: qmroHref Bell T, Curzon P, Cutts Q et al. (2011). Introducing Students to Computer Science With Programmes That Don’t Emphasise Programming. nameOfConference DOI: 10.1145/1999747.1999904 QMRO: qmroHref Masci P, Curzon P, Huang H et al. (2011). Towards a formal framework for reasoning about the resilience of dynamic interactive systems. nameOfConference DOI: 10.1145/1978582.1978606 QMRO: qmroHref Black J, Myketiak C, Curzon P et al. (2011). Engaging Female Students in Computer Science Using Role Models. nameOfConference DOI: doi QMRO: qmroHref Rukšenas R, Curzon P (2011). Abstract models and cognitive mismatch in formal verification. nameOfConference DOI: 10.14279/tuj.eceasst.45.655.661 QMRO: qmroHref Huang H, Rukšenas R, Ament MGA et al. (2011). Capturing the distinction between task and device errors in a formal model of user behaviour. nameOfConference DOI: 10.14279/tuj.eceasst.45.656.679 QMRO: qmroHref Masci P, Curzon P (2011). Checking User-Centred Design Principles in Distributed Cognition Models: A Case Study in the Healthcare Domain. nameOfConference DOI: 10.1007/978-3-642-25364-5_10 QMRO: qmroHref Masci P, Curzon P, Blandford A et al. (2011). Modelling distributed cognition systems in PVS. nameOfConference DOI: 10.14279/tuj.eceasst.45.653.659 QMRO: qmroHref Masci P, Rukšenas R, Oladimeji P et al. (2011). On formalising interactive number entry on infusion pumps. nameOfConference DOI: 10.14279/tuj.eceasst.45.654.660 QMRO: qmroHref Bell T, Curzon P, Cutts Q et al. (2011). Overcoming Obstacles to CS Education by Using Non-programming Outreach Programmes. nameOfConference DOI: 10.1007/978-3-642-24722-4_7 QMRO: qmroHref Furniss D, Blandford A, Curzon P (2010). Confessions from a Grounded Theory PhD: Experiences and Lessons Learnt. nameOfConference DOI: 10.1145/1978942.1978960 QMRO: qmroHref Blandford A, Buchanan G, Curzon P et al. (2010). Who’s looking? Invisible problems with interactive medical devices. nameOfConference DOI: doi QMRO: qmroHref Ruksenas R, Back J, Curzon P et al. (2009). Verification-guided modelling of salience and cognitive load. nameOfConference DOI: 10.1007/s00165-008-0102-7 QMRO: qmroHref Cerone A, Curzon P, Duce D (2009). Editorial. nameOfConference DOI: 10.1007/s00165-009-0121-z QMRO: qmroHref Curzon P, Peckham J, Taylor H et al. (2009). Computational thinking (CT). nameOfConference DOI: 10.1145/1595496.1562941 QMRO: qmroHref Curzon P, McOwan PW, Cutts Q et al. (2009). Enthusing & inspiring with reusable kinaesthetic activities. nameOfConference DOI: 10.1145/1595496.1562911 QMRO: qmroHref Curzon P, McOwan PW, Black J (2009). The magic of HCI: Enthusing kids in playful ways to help solve the Computer Science recruitment problem. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Peckham J, Taylor H et al. (2009). Computational Thinking (CT): On Weaving It In. nameOfConference DOI: 10.1145/1562877.1562941 QMRO: qmroHref Curzon P, McOwan PW, Cutts QI et al. (2009). Enthusing & Inspiring with Reusable Kinaesthetic Activities. nameOfConference DOI: 10.1145/1595496.1562911 QMRO: qmroHref Curzon P, Black J, Meagher LR et al. (2009). cs4fn.org: Enthusing students about Computer Science. nameOfConference DOI: doi QMRO: qmroHref Ruksenas R, Curzon P, Blandford A (2008). Modelling and Analysing Cognitive Causes of Security Breaches. nameOfConference DOI: 10.1007/s11334-008-0050-7 QMRO: qmroHref Cerone A, Curzon P (2008). Formal methods for interactive systems. nameOfConference DOI: 10.1007/s11334-008-0051-6 QMRO: qmroHref Cerone A, Curzon P (2008). Preface. nameOfConference DOI: 10.1016/j.entcs.2008.03.103 QMRO: qmroHref Ruksenas R, Curzon P, Blandford A et al. (2008). Combining Human Error Verification and Timing Analysis. nameOfConference DOI: 10.1007/978-3-540-92698-6_2 QMRO: qmroHref Blandford A, Curzon P, Hyde J et al. (2008). EMU in the Car: Evaluating Multimodal Usability of a Satellite Navigation System. nameOfConference DOI: 10.1007/978-3-540-70569-7_1 QMRO: qmroHref Blandford A, Curzon P, Hyde J et al. (2008). EMU in the car: Evaluating multimodal usability of a satellite navigation system. nameOfConference DOI: 10.1007/978-3-540-70569-7 QMRO: qmroHref Curzon P, McOwan PW (2008). Engaging with Computer Science Through Magic Shows. nameOfConference DOI: 10.1145/1384271.1384320 QMRO: qmroHref Curzon P, McOwan PW (2008). Engaging with Computer Science through Magic Shows. nameOfConference DOI: 10.1145/1384271.1384320 QMRO: qmroHref Ruksenas R, Curzon P, Back J et al. (2008). Formal Modelling of Salience and Cognitive Load. nameOfConference DOI: 10.1016/j.entcs.2008.03.107 QMRO: qmroHref Papatzanis G, Curzon P, Blandford A (2008). Identifying Phenotypes and Genotypes: A Case Study Evaluating an In-Car Navigation System. nameOfConference DOI: 10.1007/978-3-540-92698-6_14 QMRO: qmroHref Ruksenas R, Curzon P, Blandford A (2008). Modelling Rational User Behaviour as Games between an Angel and a Demon. nameOfConference DOI: 10.1109/SEFM.2008.43 QMRO: qmroHref Furniss D, Blandford A, Curzon P (2008). Usability Work in Professional Website Design: Insights from Practitioners’ Perspectives. nameOfConference DOI: 10.1007/978-1-84628-941-5 QMRO: qmroHref Curzon P, Ruksenas R, Blandford A (2007). An approach to formal verification of human-computer interaction. nameOfConference DOI: 10.1007/s00165-007-0035-6 QMRO: qmroHref Curzon P (2007). Serious Fun in Computer Science. nameOfConference DOI: 10.1145/1269900.1268785 QMRO: qmroHref Furniss D, Blandford A, Curzon P (2007). Usability evaluation methods in practice. Proceedings of the 14th European conference on Cognitive ergonomics: invent! explore! DOI: 10.1145/1362550.1362602 QMRO: qmroHref Back J, Blandford A, Curzon P (2007). Slip Errors and Cue Salience. nameOfConference DOI: 10.1145/1362550.1362595 QMRO: qmroHref Ruksenas R, Curzon P, Blandford A (2007). Detecting Cognitive Causes of Confidentiality Leaks. nameOfConference DOI: doi QMRO: qmroHref Cerone A, Curzon P (2007). Preface. nameOfConference DOI: 10.1016/j.entcs.2007.03.011 QMRO: qmroHref Curzon P (2007). Serious fun in computer science. Proceedings of the 12th annual SIGCSE conference on Innovation and technology in computer science education DOI: 10.1145/1268784.1268785 QMRO: qmroHref Wilson J, Curzon P, Whitney G (2007). Seniors route-planning: a reality check for the design of navigation systems. nameOfConference DOI: doi QMRO: qmroHref Xiong H, Curzon P, Tahar S et al. (2007). Providing a formal linkage between MDG and HOL. nameOfConference DOI: 10.1007/s10703-006-0017-y QMRO: qmroHref Curzon P, Cerone A (2007). 2nd International Workshop on Formal Methods for Interactive Systems. nameOfConference DOI: 10.14236/ewic/hci2007.91 QMRO: qmroHref Curzon P, Ruksenas R, Blandford A (2007). An Approach to Formal Verification of Human-Computer Interaction. nameOfConference DOI: 10.1007/s00165-007-0035-6 QMRO: qmroHref Ruksenas R, Curzon P, Blandford A (2007). Detecting Cognitive Causes of Confidentiality Leaks. nameOfConference DOI: 10.1016/j.entcs.2007.01.059 QMRO: qmroHref Back J, Cheng WL, Dann R et al. (2007). Does being motivated to avoid procedural errors influence their systematicity?. nameOfConference DOI: 10.1007/978-1-84628-664-3_12 QMRO: qmroHref Papatzanis G, Curzon P, Blandford A (2007). Evaluation of Car Navigation Systems: On-Road Studies or Analytical Tools. nameOfConference DOI: doi QMRO: qmroHref Ruksenas R, Curzon P, Back J et al. (2007). Formal Modelling of Cognitive Interpretation. nameOfConference DOI: doi QMRO: qmroHref Ruksenas R, Curzon P, Back J et al. (2007). Formal modelling of cognitive interpretation. nameOfConference DOI: 10.1007/978-3-540-69554-7_10 QMRO: qmroHref Back J, Blandford A, Curzon P (2007). Recognising Erroneous and Exploratory Interactions. nameOfConference DOI: 10.1007/978-3-540-74800-7_10 QMRO: qmroHref Furniss D, Blandford A, Curzon P (2007). Resilience in Usability Consultancy Practice: The Case for a Positive Resonance Model. nameOfConference DOI: doi QMRO: qmroHref Graham TCN, Curzon P, Doherty G et al. (2007). Usability and Computer Games: Working Group Report. nameOfConference DOI: 10.1007/978-3-540-69554-7_22 QMRO: qmroHref Perkins VD, Butterworth R, Curzon P et al. (2006). Representation of the National Memory: digitising historical photograph collections in the UK. nameOfConference DOI: doi QMRO: qmroHref Mizouni R, Tahar S, Curzon P (2006). Hybrid Verification Integrating HOL Theorem Proving with MDG Model Checking. nameOfConference DOI: 10.1016/j.mejo.2006.07.019 QMRO: qmroHref Mizouni R, Tahar S, Curzon P (2006). Hybrid verification integrating HOL theorem proving with MDG model checking. nameOfConference DOI: 10.1016/j.mejo.2006.07.019 QMRO: qmroHref Curzon P, McOwan P, Burton E et al. (2006). Engaging with Computer Science through Play and Performance. nameOfConference DOI: doi QMRO: qmroHref Wilson J, Curzon P (2006). Older People’s Experiences Route-planning. nameOfConference DOI: doi QMRO: qmroHref Curzon P (2006). Backwards Compatible. nameOfConference DOI: doi QMRO: qmroHref Perkins VD, Butterworth R, Fields B et al. (2006). Keeping stuff safe: using guidelines and standards for digital preservation. nameOfConference DOI: doi QMRO: qmroHref Back J, Cheng WL, Dann R et al. (2006). Does being motivated to avoid procedural errors influence their systemacity?. nameOfConference DOI: 10.1007/978-1-84628-664-3_12 QMRO: qmroHref Jagne J, Smith S, Curzon P et al. (2006). Integrating social and cultural variances into international eCommerce interface design. nameOfConference DOI: doi QMRO: qmroHref Blandford A, Back J, Curzon P et al. (2006). Reasoning about human error by modeling cognition and interaction. nameOfConference DOI: doi QMRO: qmroHref Romijn J, Smith G, Van De Pol J et al. (2005). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Wilson J, Whitney G (2005). Successful strategies of older people for finding information. nameOfConference DOI: 10.1016/j.intcom.2005.09.006 QMRO: qmroHref Curzon P (2005). Perfect usability - The one-button machine?. nameOfConference DOI: doi QMRO: qmroHref Curzon P (2005). The extreme Challenge of Moore’s Law and what Stormy Petrels have to do with it. nameOfConference DOI: doi QMRO: qmroHref Perkins VD, Butterworth R, Curzon P (2005). "Don't forget the STAGES"! Searching for values in digital surrogates of historical photographs. nameOfConference DOI: doi QMRO: qmroHref Davis-Perkins V, Butterworth R, Curzon P et al. (2005). A Study into the Effect of Digitisation Projects on the Management and Stability of Historic Photograph Collections. nameOfConference DOI: 10.1007/11551362_25 QMRO: qmroHref Davis-Perkins V, Butterworth R, Curzon P et al. (2005). A study into the effect of digitisation projects on the management and stability of historic photograph collections. nameOfConference DOI: 10.1007/11551362 QMRO: qmroHref Jagne J, Smith S, Duncker E et al. (2005). Cross-Cultural Factors of Physical-Shopping and eShopping. Proceedings of HCI International 2005 DOI: doi QMRO: qmroHref Mizouni R, Tahar S, Curzon P (2004). Hybrid tool integrating HOL theorem proving with MDG model checking. nameOfConference DOI: doi QMRO: qmroHref Curzon P (2004). Flexing Paper’s Muscle. nameOfConference DOI: doi QMRO: qmroHref Jagne J, Smith SG, Duncker E et al. (2004). Cross-cultural Interface Design Strategy. nameOfConference DOI: doi QMRO: qmroHref CURZON P, Butterworth R, Blandford A (2004). Models of Interactive systems: a case study on a programmable user modelling. nameOfConference DOI: 10.1016/j.ijhcs.2003.08.004 QMRO: qmroHref Blandford A, Butterworth R, Curzon P (2004). Models of interactive systems: a case study on programmable user modelling. nameOfConference DOI: 10.1016/j.ijhcs.2003.08.004 QMRO: qmroHref Curzon P (2004). When smart thinking is not enough. nameOfConference DOI: doi QMRO: qmroHref CURZON P, Tahar S, Mizouni R (2004). A Hybrid Tool Integrating HOL Theorem Proving with MDG Model Checking. Proceedings of the 16th IEEE International Conference on Microelectronics, Tunisia DOI: 10.1016/j.mejo.2006.07.019 QMRO: qmroHref Curzon P, Blandford A (2004). Formally justifying user-centred design rules: A case study on post-completion errors. nameOfConference DOI: 10.1007/978-3-540-24756-2_25 QMRO: qmroHref CURZON P, Wilson J, Whitney G et al. (2004). Information Seeking Strategies used by older people. HCI and the older population, workshop at HCI2004, Design for Life: The 18th British HCI Group Annual conference DOI: doi QMRO: qmroHref Blandford A, Butterworth R, Curzon P (2004). Models of Interactive systems: a case study on programmable user modelling. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Keith S, Whitney G et al. (2004). Strategies for finding government information by older people. nameOfConference DOI: 10.1007/978-3-540-30111-0_3 QMRO: qmroHref Curzon P (2003). Spit-not-so, or what’s in the layout. nameOfConference DOI: doi QMRO: qmroHref Curzon P (2003). Maori Culture? Who Cares?. nameOfConference DOI: doi QMRO: qmroHref Mizouni R, Tahar S, Curzon P (2003). On the Embedding of MDG specification Languages in HOL. nameOfConference DOI: doi QMRO: qmroHref CURZON P, Tahar S, Kort S (2003). Hierarchical Formal Verification Using a Hybrid Tool. nameOfConference DOI: 10.1007/s10009-002-0082-5 QMRO: qmroHref Curzon P, Blandford A (2003). A formal justification of a design rule for avoiding post-completion errors. nameOfConference DOI: doi QMRO: qmroHref Curzon P (2003). Middlesex University Interaction Design Centre. nameOfConference DOI: doi QMRO: qmroHref Xiong H, Curzon P, Tahar S et al. (2003). Providing a formal linkage between the MDG verification system and HOL proof system. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Harding J (2003). Spreading the word about pedagogic research: the virtual reading group. nameOfConference DOI: 10.4324/9780203417041-18 QMRO: qmroHref Xiong H, Curzon P, Tahar S et al. (2002). Formally Linking MDG and HOL based on a verified MDG system. Proc. of the 3rd International Conference on Integrated Formal Methods DOI: 10.1007/3-540-47884-1 QMRO: qmroHref Xiong H, Curzon P, Tahar S et al. (2002). Formally Linking MDG and HOL Based on a Verified MDG System. nameOfConference DOI: 10.1007/3-540-47884-1_12 QMRO: qmroHref Curzon P, Blandford AE (2002). From a formal user model to design rules. nameOfConference DOI: 10.1007/3-540-36235-5_1 QMRO: qmroHref Curzon P, Blandford A, Butterworth R et al. (2002). Interaction Design Issues for Car Navigation Systems. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Harding J (2002). Spreading the word about pedagogic research. nameOfConference DOI: doi QMRO: qmroHref Thimbleby H, Blandford A, Cairns P et al. (2002). User interface design as systems design. nameOfConference DOI: doi QMRO: qmroHref Blandford AE, Butterworth R, Curzon P (2001). PUMA Footprints: linking theory and craftskill in usability evaluation. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Blandford AE (2001). A user model for avoiding design induced errors in soft-key interactive systems. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Tahar S (2001). Automating the Verification of Parameterized Hardware using a Hybrid Tool. nameOfConference DOI: 10.1109/ICM.2001.997659 QMRO: qmroHref Curzon P, Tahar S (2001). Automating the verification of parameterized hardware using a hybrid tool. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Blandford A (2001). Detecting multiple classes of user errors. nameOfConference DOI: 10.1007/3-540-45348-2_9 QMRO: qmroHref CURZON P, Tahar S, Kort S (2001). Hierarchical Formal Verification using an MDGHOL Hybrid Tool. Correct Hardware Design and Verification methods, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference DOI: 10.1007/3-540-44798-9_21 QMRO: qmroHref Butterworth R, Blandford A, Curzon P (2001). Lab Overview: Interaction Design Centre, Middlesex University. nameOfConference DOI: doi QMRO: qmroHref Blandford A, Butterworth R, Curzon P (2001). PUMA Footprints: linking theory and craft skill in usability evaluation. nameOfConference DOI: doi QMRO: qmroHref Xiong H, Curzon P, Tahar S et al. (2001). Proving Existential Theorems when Importing Results from MDG to HOL. nameOfConference DOI: doi QMRO: qmroHref Hasan M, Tahar S, Curzon P (2000). Impact of Design Changes on Verification Using MDGs. nameOfConference DOI: doi QMRO: qmroHref Kort S, Pisini VK, Tahar S et al. (2000). Un outil hybride pour la vérification formelle de circuits. nameOfConference DOI: doi QMRO: qmroHref Kort S, Tahar S, Curzon P et al. (2000). HOL-MDG: A Hybrid Tool for Formal Verification. nameOfConference DOI: doi QMRO: qmroHref Curzon P (2000). Learning Computer Science Through Games and Puzzles. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Blandford A (2000). Reasoning about Order Errors and Interaction. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Blandford A (2000). Reasoning about Order Errors in Interaction. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Blandford A (2000). Using a Verification System to Reason about Post-Completion Errorsteraction. nameOfConference DOI: doi QMRO: qmroHref Xiong H, Curzon P, Tahar S et al. (2000). Embedding and Verification of an MDG-HDL Compiler in HOL. nameOfConference DOI: doi QMRO: qmroHref Pisini VK, Tahar S, Curzon P et al. (2000). Formal Hardware Verification by Integrating HOL and MDG. nameOfConference DOI: 10.1145/330855.330947 QMRO: qmroHref Curzon P, Blandford A (2000). Reasoning about Order Errors in Interaction. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Blandford A (2000). Using a Verification System to Reason About Post-Completion Errors. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Tahar S (1999). Comparing HOL and MDG: A Case Study on the Verification of an ATM Switch Fabric. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Harding J (1999). A Summary of the Virtual Reading Group Project. nameOfConference DOI: doi QMRO: qmroHref Pisini VK, Tahar S, Aït-Mohamed O et al. (1999). An Approach to Link HOL and MDG for Hardware Verification. nameOfConference DOI: doi QMRO: qmroHref Xiong H, Curzon P, Blandford A (1999). Combining Verification Systems in a Trusted Way to Reap the Benefits of Both. nameOfConference DOI: doi QMRO: qmroHref Xiong H, Curzon P, Tahar S et al. (1999). Verification of a Translator for MDG’s Library in HOL. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1999). Chocolate Vending Machines in HOL. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Tahar S, Lu J (1999). Comparing HOL, MDG and VIS A Case Study on the Verification of an ATM Switch Fabric. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Harding J (1999). Drip Fed Academic Staff Development Using a Virtual Reading Group. nameOfConference DOI: doi QMRO: qmroHref H Xiong PC, Tahar S (1999). Importing MDG Verification Results into HOL. nameOfConference DOI: 10.1007/3-540-48256-3_20 QMRO: qmroHref Curzon P (1999). Learning Computer Science through Games and Puzzles. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1998). Progress Setting up a Virtual HE Teaching and Learning Reading Group. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Rix J (1998). Why do students take programming modules?. nameOfConference DOI: 10.1145/290320.283022 QMRO: qmroHref Xiong H, Curzon P (1998). Verification of a Translator for MDG’s Components in HOL. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1998). Read, summarise, debate, write. nameOfConference DOI: doi QMRO: qmroHref Tahar SE, Curzon P, Lu J (1998). Three Approaches to Hardware Verification: HOL, MDG and VIS compared. nameOfConference DOI: 10.1007/3-540-49519-3_28 QMRO: qmroHref Curzon P, Tahar SE, Mohamed OA (1998). Verification of the MDG Components Library Using HOL. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Rix J (1998). Why do Students take Programming Modules?. nameOfConference DOI: 10.1145/282991.283022 QMRO: qmroHref Jakubiec L, Coupet-Grimal S, Curzon P (1997). A Comparison of the Coq and HOL Proof Systems for Specifying Hardware. nameOfConference DOI: doi QMRO: qmroHref Wong W, Curzon P (1997). Towards an Efficient Proof Recorder for HOL90. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Blandford A, Jones M et al. (1997). Supporting a Large-class Programming Course with Intranet Tools. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1996). Hardware Verification and ATM Switches. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1996). Hierarchical Formal Verification of a Communication Network. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Wong W (1996). Checking Proofs from Linked Tools. nameOfConference DOI: doi QMRO: qmroHref Tahar S, Curzon P (1996). A Comparison of MDG and HOL for Hardware Verification. nameOfConference DOI: 10.1007/bfb0105419 QMRO: qmroHref Curzon P, Leslie I (1996). Improving Hardware Designs Whilst Simplifying their Proof. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Leslie I (1995). A Case Study on Design for Provability. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1995). Bridging the Gap Between Theory and Practice. nameOfConference DOI: doi QMRO: qmroHref Curzon P, Leslie I, Gordon M (1995). Conclusions from a Study to Verify a Real Network Component. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1995). Problems Encountered with the Machine-assisted Proof of Hardware. nameOfConference DOI: 10.1007/3-540-60385-9_4 QMRO: qmroHref Curzon P (1995). The Importance of Proof Maintenance and Reengineering. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1995). Tracking Design Changes with Formal Machine-Checked Proof. nameOfConference DOI: 10.1007/s10009-002-0082-5 QMRO: qmroHref Curzon P (1995). Tracking design changes with formal machine-checked proof. nameOfConference DOI: 10.1093/comjnl/38.2.91 QMRO: qmroHref Curzon P (1995). Virtual Theories. nameOfConference DOI: 10.1007/3-540-60275-5_62 QMRO: qmroHref Curzon P, Wong W (1994). A Theory of Lists for HOL Based on Higher-Order Functions. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1994). Tracking Design Changes with Formal Verification. nameOfConference DOI: 10.1007/3-540-58450-1_42 QMRO: qmroHref Curzon P (1994). The Formal Verification of an ATM Network. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1994). The Formal Verification of the Fairisle ATM Switching Element. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1994). The Formal Verification of the Fairisle ATM Switching Element: an Overview. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1994). The Formal Verification of the Fairisle Switch: The 4x4 Switching Fabric.. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1994). Experiences formally verifying a network component. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1994). The Verified Compilation of Vista Programs. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1993). A Verified Vista Implementation. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1993). Deriving Correctness Properties of Compiled Code. nameOfConference DOI: 10.1007/BF01383985 QMRO: qmroHref Curzon P (1993). Compiler Correctness and Input/Output. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1993). Deriving Correctness Properties of Compiled Code. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1992). Of What Use is a Verified Compiler Specification?. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1992). A Programming Logic For a Verified Structured Assembly Language. nameOfConference DOI: 10.1007/BFb0013078 QMRO: qmroHref Curzon P (1992). A Verified Compiler for a Structured Assembly Language. nameOfConference DOI: 10.1109/HOL.1991.596292 QMRO: qmroHref Curzon P (1991). A Structured Approach to the Verification of Low Level Microcode. nameOfConference DOI: doi QMRO: qmroHref Curzon P (1990). A Verified Vista Implementation of the Viper Microprocessor. nameOfConference DOI: doi QMRO: qmroHref Public EngagementA major aspect of my work is in the public engagement in computer science (and science, maths and engineering more generally). I aim to generate excitement not just about the School's research but about interdisciplinary research in the subject more generally. The main way of achieving this is through the internationally renowned public engagement project cs4fn (cs4fn.blog) that I created with Peter McOwan, and its sister project for teachers Teaching London Computing (teachinglondoncomputing.org) In 2020 I won the International IEEE Computer Society Taylor L. Booth Education Award: “For outstanding contributions to the rebirth of computer science as a school subject.” I gave an invited keynote at the ACM ITiCSE (Innovation & Technology in Computer Science Education ) conference on this work. cs4fn was commended in the 2006 EPSRC International Review of Computer Science.