Skip to main content
Research

Publications: Prof Paul Curzon

Fahmi A, Soyel H, Marsh DWR, Curzon P, Macbrayne A, Humby F ( 2020 ) . From Personalised Predictions to Targeted Advice: Improving Self-Management in Rheumatoid Arthritis . Conference: Integrated Citizen Centered Digital Health and Social Care from: 26/11/2020 to: 27/11/2020 ,
Fahmi A, Soyel H, Marsh W, Curzon P, MacBrayne A, Humby F ( 2020 ) . From personalised predictions to targeted advice: Improving self-management in rheumatoid arthritis . Studies in Health Technology and Informatics vol. 275 , 62 - 66 .
Curzon P, Waite J, Maton K, Donohue J ( 2020 ) . Using Semantic Waves to Analyse the Effectiveness of Unplugged Computing Activities . ACM digital library . Conference: The 15th Workshop in Primary and Secondary Computing Education ( Online ) from: 28/10/2020 to: 30/10/2020 ,
Waite J, Curzon P, Marsh W, Sentance S ( 2020 ) . Difficulties with design: The challenges of teaching design in K-5 programming . Computers & Education Article 103838 , 103838 - 103838 .
Waite JL, Maton K, Curzon P, Tuttiett L ( 2019 ) . Unplugged Computing and Semantic Waves: Analysing Crazy Characters . Conference: The UK and Ireland Computing Education Research Conference ( Kent, UK ) from: 05/09/2019 to: 06/09/2019 ,
CURZON P, Bell T, Waite JL, DORLING M ( 2019 ) . Computational Thinking . The Cambridge Handbook of Computing Education Research , Editors: Fincher, S, Robins, A , Cambridge University Press
Waite JL, CURZON P, MARSH DW, Sentance S ( 2018 ) . Comparing K-5 teachers’ reported use of design in teaching programming and planning in teaching writing . ACM ISBN 978-1-4503-6588-8/18/10 . Editors: Muhling, A, Cutts, Q, Schwill, A , Conference: WiPSCE 2018 (13th Workshop in Primary and Secondary Computing Education) ( Potsdam, Germany ) from: 04/10/2018 to: 06/10/2018 ,
Waite JL, CURZON P, MARSH D, Sentance S, Hawden-Bennett A ( 2018 ) . Abstraction in action: K-5 teachers' uses of levels of abstraction, particularly the design level, in teaching programming . International Journal Of Computer Science Education In Schools vol. 2 , ( 1 ) Article 2 , 14 - 40 .
CURZON P, Furniss D, Blandford A ( 2017 ) . Exploring organisational competences in Human Factors and UX project work: Managing careers, project tactics and organisational strategy . Ergonomics
Waite JL, curzon P, marsh D, Sentance S ( 2017 ) . K-5 Teachers' Uses of Levels of Abstraction Focusing on Design . Presented at: WiPSCE 2017 , Abstract: java.sql.Clob org.hibernate.engine.jdbc.WrappedClob java.io.Serializable ,
Harrison MD, MASCI P, CAMPOS JC, CURZON P ( 2017 ) . Verification of User Interface Software: the Example of Use-Related Safety Requirements and Programmable Medical Devices . IEEE Transactions on Human-Machine Systems
CURZON P, Myketiak C, Concannon S ( 2017 ) . Narrative perspective, person references, and evidentiality in clinical incident reports . Journal of Pragmatics vol. 117 , ( August ) 139 - 154 .
Curzon P, Rukšėnas R ( 2017 ) . Modelling the User . The Handbook of Formal Methods in Human-Computer Interaction ,
Harrison MD, Masci PM, Campos JC, Curzon P ( 2017 ) . The Specification and Analysis of Use Properties of a Nuclear Control System . The Handbook of Formal Methods in Human-Computer Interaction ,
Harrison MD, Masci P, Campos JC, Curzon P ( 2017 ) . Demonstrating that medical devices satisfy user related safety requirements . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 9062 LNCS , 113 - 128 .
Masci P, Oladimeji P, Curzon P, Thimbleby H ( 2017 ) . Using pvsio-web to demonstrate software issues in medical user interfaces . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 9062 LNCS , 214 - 221 .
Waite JL, Curzon P, marsh D, Sentance S ( 2016 ) . Abstraction and Common Classroom Activities . Conference: WiPSCE 2016 11th Workshop in Primary and Secondary Computing Education ( Munster, Germany ) from: 13/10/2016 to: 15/10/2016 ,
Harrison M, Campos JC, Ruksenas R, Curzon P ( 2016 ) . Modelling information resources and their salience in medical device design . "Engineering Interactive Computing Systems" . Conference: Engineering Interactive Computing Systems 2016194 - 203 .
Furniss D, Curzon P, Blandford A ( 2016 ) . Using FRAM beyond safety: A case study to explore how sociotechnical systems can flourish or stall . Theoretical Issues in Ergonomics Science vol. 17 , ( 5-6 ) 507 - 532 .
Rukšenas R, Masci P, Curzon P ( 2016 ) . Developing and verifying user interface requirements for infusion pumps: A Refinement approach . From Action Systems to Distributed Systems: The Refinement Approach ,
Ruksenas R, Masci P, Curzon P ( 2016 ) . Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach . From Action Systems to Distributed Systems: The Refinement Approach , Editors: Petre, L, Sekerinski, E , Chapman and Hall/CRC
CURZON P, Lee P, Meagher L ( 2015 ) . Impact on procurement and training by research on the interaction design of medical devices . EAI Endorsed Transactions on Collaborative Computing vol. 16 , ( 7 )
CURZON P, Thimbleby H, Oladimeji P, Masci P ( 2015 ) . Issues in number entry user interface styles: Recommendations for mitigation . EAI Endorsed Transactions on Creative Technologies vol. 16 , ( 8 )
CURZON P, Myketiak, Concannon ( 2015 ) . New/s Design: Informing Future Design Processes by Understanding Media Reporting of Medical Errors with Medical Devices . EAI Endorsed Transactions on Smart Cities vol. 16 , ( 3 ) 1 - 4 .
CURZON P, Masci P, Oladimeji P, Mallozzi P ( 2015 ) . PVSio-web: mathematically based tool support for the design of interactive and interoperable medical systems . EAI Endorsed Transactions on Collaborative Computing vol. 16 , ( 7 )
CURZON P, Blandford AE, Thimbleby H, Cox A ( 2015 ) . Safer Interactive Medical Device Design: Insights from the CHI+MED Project . EAI Endorsed Transactions on Security and Safety vol. 16 , ( 9 )
Harrison M, Campos JC, Masci P, CURZON P ( 2015 ) . Templates as heuristics for proving properties of medical devices . EAI Endorsed Transactions on Creative Technologies vol. 16 , ( 8 )
Masci P, Curzon P, Thimbleby H ( 2015 ) . Early identification of software causes of use-related hazards in medical devices . 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies" . Editors: Alomainy, A, Whittow, W, Hao, Y, Nikita, KS et al. ,
Cinzia Bernardeschi PM ( 2015 ) . Towards a Formalization of System Requirements for an Integrated Clinical Environment . 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies" . Editors: Alomainy, A, Whittow, W, Hao, Y, Nikita, KS et al. ,
Wilson J, Curzon P, Duncker E ( 2015 ) . Exploring older women’s confidence during route planning . Behaviour and Information Technology vol. 34 , Article 7 , 725 - 740 .
Masci P, Oladimeji P, Zhang Y, Jones P, Curzon P, Thimbleby H ( 2015 ) . PVSio-web 2.0: Joining PVS to HCI . Computer Aided Verification: 27th International Conference, CAV2015, Proceedings, Part I . vol. 9206 , 470 - 478 .
Masci P, Curzon P, Mallozzi P, Angelis FLD, Serugendo GDM ( 2015 ) . Using PVSio-web and SAPERE for rapid prototyping of user interfaces in Integrated Clinical Environments . Proceedings of Verisure2015, Workshop on Verification and Assurance, co-located with CAV2015 .
Campos JC, Curzon P, Harrison MD, Masci P ( 2015 ) . Layers, resources and property templates in the specification and analysis of two interactive systems . 1st Workshop on Formal Methods in Human Computer Interaction (FoMHCI), co-located with EICS2015 .
Masci P, Rukšėnas R, Oladimeji P, Cauchi A, Gimblett A, Li Y, Curzon P, Thimbleby H ( 2015 ) . The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps . Innovations in Systems and Software Engineering vol. 11 , ( 2 ) 73 - 93 .
Masci P, Curzon P, Furniss D, Blandford A ( 2015 ) . Using PVS to support the analysis of distributed cognition systems . Innovations in Systems and Software Engineering vol. 11 , ( 2 ) 113 - 130 .
Furniss D, Masci P, Curzon P, Mayer A, Blandford A ( 2015 ) . Exploring medical device design and use through layers of distributed cognition: How a glucometer is coupled with its context . Journal of Biomedical Informatics vol. 53 , 330 - 341 .
Bella G, Curzon P, Lenzini G ( 2015 ) . Service Security and Privacy as a Socio-Technical Problem: Literature review, analysis methodology and challenge domains . Journal of Computer Security
Curzon P, McOwan PW, Plant N, Meagher LR ( 2014 ) . Introducing teachers to computational thinking using unplugged storytelling . ACM International Conference Proceeding Series . 89 - 92 .
Bella G, Curzon P, Giustolisi R, Lenzini G ( 2014 ) . A socio-technical methodology for the security and privacy analysis of services . Proceedings - IEEE 38th Annual International Computers, Software and Applications Conference Workshops, COMPSACW 2014 . 401 - 406 .
enas RR, Curzon P, Blandford A, Back J ( 2014 ) . Combining Human Error Verification and Timing Analysis: a Case Study on an Infusion Pump . Formal Aspects of Computing vol. 26 , Article 5 , 1033 - 1076 .
Harrison MD, Masci P, Campos J, Curzon P ( 2014 ) . Automated theorem proving for the systematic analysis of interactive systems . Electronic Communications of the EASST vol. 69: Formal Methods f ,
Oladimeji P, Masci P, Curzon P, Thimbleby H ( 2014 ) . PVSio-web: a tool for rapid prototyping device user interfaces in PVS . Electronic Communications of the EASST vol. 69: Formal Methods f ,
Masci P, Zhang Y, Jones P, Thimbleby H, Curzon P ( 2014 ) . A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software . 5th Workshop on Medical Cyber-Physical Systems . Editors: Turau, V, Kwiatkowska, M, Mangharam, R, Weyer, C et al. , vol. 36 , 1 - 14 .
Masci P, Zhang Y, Jones P, Oladimeji P, D Urso E, Bernardeschi C, Curzon P, Thimbleby H ( 2014 ) . Combining PVSio with Stateflow . NASA Formal Methods: Proceedings of the 6th International Symposium NFM 2014 . vol. 8430 , 209 - 214 .
Masci P, Zhang Y, Jones P, Curzon P, Thimbleby H ( 2014 ) . Formal Verification of Medical Device User Interfaces Using PVS . ETAPS/FASE2014, 17th International Conference on Fundamental Approaches to Software Engineering . vol. 8411 , 200 - 214 .
Curzon P ( 2013 ) . cs4fn and computational thinking unplugged . The 8th Workshop in Primary and Secondary Computing Education (WIPSCE) . 47 - 50 .
Masci P, Ayoub A, Curzon P, Lee I, Sokolsky O, Thimbleby H ( 2013 ) . Model-based development of the Generic PCA infusion pump user interface prototype in PVS . Computer Safety, Reliability and Security: Proceedings of the 32nd International Conference, SAFECOMP . Editors: Bitsch, F, Guiochet, J, Kaâniche, M , vol. 8153 , 228 - 240 .
Black J, Brodie J, Curzon P, Myketiak C, McOwan PW, Meagher LR ( 2013 ) . Making Computing Interesting to School Students: Teachers’ Perspectives . Proceedings of the 18th ACM Conference on Innovation and Technology in Computer Science Education (ITiCSE) . Editors: Carter, J, Utting, I, Clear, A , Conference: ITiCSE '13 Proceedings of the 18th ACM conference on Innovation and technology in computer science education ( Canterbury, UK ) from: 01/07/2013 to: 03/07/2013 , 255 - 260 .
Rukšenas R, Curzon P, Harrison MD ( 2013 ) . Integrating Formal Predictions of Interactive System Behaviour with User Evaluation . Proceedings of Integrated Formal Methods: LNCS 7940 . Editors: Johnsen, EB, Petre, L , from: 10/06/2013 to: 14/06/2013 , 238 - 252 .
Masci P, Ayoub A, Curzon P, Harrison MD, Lee I, Thimbleby H ( 2013 ) . Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example . Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS’13 . Editors: Forbrig, P, Dewan, P, Harrison, MD, Luyten, K et al. , from: 24/06/2013 to: 27/06/2013 , 81-90 - 81-90 .
Huang H, Curzon P, White G, Blandford A ( 2013 ) . Evaluating the methodological constraints and affordances of investigation manuals and their methodologies . Proceedings of Workshop on Human Factors in the Safety and Security of Critical Systems .
Masci P, Ayoub A, Curzon P, Harrison MD, Lee I, Thimbleby H ( 2013 ) . Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example . Conference: Proceedings of the 5th ACM SIGCHI symposium on Engineering interactive computing systems - EICS '1381 - 90 .
Black J, Curzon P, Myketiak C, McOwan PW, Meagher LR ( 2012 ) . Teachers' perceptions of the value of research-based school lectures . ACM International Conference Proceeding Series145 - 146 .
Myketiak C, Curzon P, Black J, McOwan PW, Meagher LR ( 2012 ) . cs4fn: A flexible model for computer science outreach . Annual Conference on Innovation and Technology in Computer Science Education, ITiCSE297 - 302 .
Masci P, Huang H, Curzon P, Harrison MD ( 2012 ) . Using PVS to investigate incidents through the lens of distributed cognition . 4th International Symposium: NASA Formal Methods 2012 . Editors: Goodloe, AE, Person, S , vol. 7226 , 273 - 278 .
Masci P, Furniss D, Curzon P, Harrison MD, Blandford A ( 2012 ) . Supporting field investigators with PVS: A case study in the healthcare domain . vol. 7527 LNCS ,
Blandford A, Cauchi A, Curzon P, Eslambolchilar P, Furniss D, Gimblett A, Huang H, Lee P et al. ( 2011 ) . Comparing actual practice and user manuals:A case study based on programmable infusion pumps . CEUR Workshop Proceedings . vol. 727 , 59 - 64 .
Cauchi A, Curzon P, Eslambolchilar P, Gimblett A, Huang H, Lee P, Li Y, Masci P et al. ( 2011 ) . Towards dependable number entry for medical devices . CEUR Workshop Proceedings . vol. 727 , 53 - 58 .
Masci P, Curzon P ( 2011 ) . Checking user-centred design principles in distributed cognition models: A case study in the healthcare domain . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 7058 LNCS , 95 - 108 .
Bell T, Curzon P, Cutts Q, Dagiene V, Haberman B ( 2011 ) . Overcoming obstacles to CS education by using non-programming outreach programmes . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 7013 LNCS , 71 - 81 .
Masci P, Curzon P, Huang H, Rukšenas R, Blandford A, Furniss D, Rajkomar A ( 2011 ) . Towards a formal framework for reasoning about the resilience of dynamic interactive systems . ACM International Conference Proceeding Series109 - 110 .
Black J, Curzon P, Myketiak C, McOwan PW ( 2011 ) . A Study in Engaging Female Students in Computer Science Using Role Models . Proceedings of ITiCSE 2011, The 16th Annual Conference on Innovation and Technology in Computer Science Education ACM SIGCSE . 63-67 - 63-67 .
Bell T, Curzon P, Cutts Q, Dagiene V, Haberman B ( 2011 ) . Introducing Students to Computer Science With Programmes That Don’t Emphasise Programming . Proceedings of ITiCSE 2011, The 16th Annual Conference on Innovation and Technology in Computer Science Education ACM SIGCSE . 391 - 391 .
Black J, Myketiak C, Curzon P, McOwan PW ( 2011 ) . Engaging Female Students in Computer Science Using Role Models . Poster presented at The 42nd ACM Technical Symposium on Computer Science Education, SIGCSE 2011: Reaching Out .
Rukšenas R, Curzon P ( 2011 ) . Abstract models and cognitive mismatch in formal verification . Electronic Communications of the EASST vol. 45 ,
Huang H, Rukšenas R, Ament MGA, Curzon P, Cox AL, Blandford A, Brumby D ( 2011 ) . Capturing the distinction between task and device errors in a formal model of user behaviour . Electronic Communications of the EASST vol. 45 ,
Masci P, Curzon P, Blandford A, Furniss D ( 2011 ) . Modelling distributed cognition systems in PVS . Electronic Communications of the EASST . vol. 45 ,
Masci P, Rukšenas R, Oladimeji P, Cauchi A, Gimblett A, Li Y, Curzon P, Thimbleby H ( 2011 ) . On formalising interactive number entry on infusion pumps . Electronic Communications of the EASST vol. 45 ,
Furniss D, Blandford A, Curzon P ( 2010 ) . Confessions from a Grounded Theory PhD: Experiences and Lessons Learnt . Proceedings of the ACM CHI Conference on Human Factors in Computing Systems . 113-122 - 113-122 .
Blandford A, Buchanan G, Curzon P, Furniss D, Thimbleby H ( 2010 ) . Who’s looking? Invisible problems with interactive medical devices . Proceedings of Workshop on Interactive Systems in Healthcare .
Cerone A, Curzon P, Duce D ( 2009 ) . Formal Aspects of Computing: Editorial . Formal Aspects of Computing vol. 21 , ( 6 ) 511 - 512 .
Ruksenas R, Back J, Curzon P, Blandford A ( 2009 ) . Verification-guided modelling of salience and cognitive load . Formal Aspects of Computing: applicable formal methods vol. 21 , ( 6 ) 541 - 569 .
Curzon P, Peckham J, Taylor H, Settle A, Roberts E ( 2009 ) . Computational thinking (CT) . ACM SIGCSE Bulletin vol. 41 , ( 3 ) 201 - 202 .
Curzon P, McOwan PW, Cutts Q, Bell T ( 2009 ) . Enthusing & inspiring with reusable kinaesthetic activities . ACM SIGCSE Bulletin vol. 41 , Article 3 , 94 - 98 .
Curzon P, McOwan PW, Black J ( 2009 ) . The magic of HCI: Enthusing kids in playful ways to help solve the Computer Science recruitment problem . Proceedings of HCI Educators 2009 - Playing with our Education .
Curzon P, Peckham J, Taylor H, Settle A, Roberts E ( 2009 ) . Computational Thinking (CT): On Weaving It In . ITICSE 2009: PROCEEDING OF THE 2009 ACM SIGSE ANNUAL CONFERENCE ON INNOVATION AND TECHNOLOGY IN COMPUTER SCIENCE EDUCATION . 201 - 202 .
Curzon P, McOwan PW, Cutts QI, Bell T ( 2009 ) . Enthusing & Inspiring with Reusable Kinaesthetic Activities . ITICSE 2009: PROCEEDING OF THE 2009 ACM SIGSE ANNUAL CONFERENCE ON INNOVATION AND TECHNOLOGY IN COMPUTER SCIENCE EDUCATION . 94 - 98 .
Curzon P, Black J, Meagher LR, McOwan PW ( 2009 ) . cs4fn.org: Enthusing students about Computer Science . Proceedings of Informatics Education Europe IV .
Blandford A, Curzon P, Hyde J, Papatzanis G ( 2008 ) . EMU in the car: Evaluating multimodal usability of a satellite navigation system . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 5136 LNCS , 1 - 14 .
Cerone A, Curzon P ( 2008 ) . Formal methods for interactive systems . Innovations in Systems and Software Engineering vol. 4 , ( 2 )
Ruksenas R, Curzon P, Blandford A ( 2008 ) . Modelling and Analysing Cognitive Causes of Security Breaches . Innovations in Systems and Software Engineering vol. 30 , Article 2 , 143 - 160 .
Cerone A, Curzon P ( 2008 ) . Preface . Electronic Notes in Theoretical Computer Science vol. 208 , ( C ) 1 - 3 .
Ruksenas R, Curzon P, Blandford A, Back J ( 2008 ) . Combining Human Error Verification and Timing Analysis . ENGINEERING INTERACTIVE SYSTEMS . Editors: Gulliksen, J, Harning, MB, Papanque, P, VanderVeer, G et al. , vol. 4940 , 18 - 35 .
Blandford A, Curzon P, Hyde J, Papatzanis G ( 2008 ) . EMU in the car: Evaluating multimodal usability of a satellite navigation system . INTERACTIVE SYSTEMS: DESIGN, SPECIFICATION, AND VERIFICATION, PROCEEDINGS . Editors: Graham, TCN, Palanque, P , vol. 5136 , 1 - 14 .
Curzon P, McOwan PW ( 2008 ) . Engaging with Computer Science Through Magic Shows . ITICSE '08: PROCEEDINGS OF THE 13TH ANNUAL CONFERENCE ON INNOVATION AND TECHNOLOGY IN COMPUTER SCIENCE EDUCATION . 179 - 183 .
Curzon P, McOwan PW ( 2008 ) . Engaging with Computer Science through Magic Shows . ACM SIGCSE Bulletin vol. 40 , Article 3 , 179 - 183 .
Ruksenas R, Curzon P, Back J, Blandford A ( 2008 ) . Formal Modelling of Salience and Cognitive Load . Electronic Notes in Theoretical Computer Science vol. 208 , 57 - 75 .
Papatzanis G, Curzon P, Blandford A ( 2008 ) . Identifying Phenotypes and Genotypes: A Case Study Evaluating an In-Car Navigation System . ENGINEERING INTERACTIVE SYSTEMS . Editors: Gulliksen, J, Harning, MB, Papanque, P, VanderVeer, G et al. , vol. 4940 , 227 - 242 .
Ruksenas R, Curzon P, Blandford A ( 2008 ) . Modelling Rational User Behaviour as Games between an Angel and a Demon . SEFM 2008: SIXTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS . Editors: Cerone, A, Gruner, S , 355 - 364 .
Furniss D, Blandford A, Curzon P ( 2008 ) . Usability Work in Professional Website Design: Insights from Practitioners’ Perspectives . Maturing Usability: Quality in Software, Interaction and Value , Editors: Law, E, Hvannberg, E, Cockton, G, Vanderdonckt, J et al. , Springer
Furniss D, Blandford A, Curzon P ( 2007 ) . Usability evaluation methods in practice: Understanding the context in which they are embedded . ACM International Conference Proceeding Series . vol. 250 , 253 - 256 .
Curzon P, Ruksenas R, Blandford A ( 2007 ) . An approach to formal verification of human-computer interaction . FORM ASP COMPUT vol. 19 , ( 4 ) 513 - 550 .
Curzon P ( 2007 ) . Serious Fun in Computer Science . ACM SIGCSE Bulletin vol. 39 , Article 3 , 1 - 1 .
Curzon P ( 2007 ) . Serious fun in computer science . ITiCSE 2007: 12th Annual Conference on Innovation and Technology in Computer Science Education - Inclusive Education in Computer Science .
Back J, Blandford A, Curzon P ( 2007 ) . Slip Errors and Cue Salience . Proceedings of ECCE2007. Invent! Explore! European Conference on Cognitive Ergonomics 2007 The 25th Anniversary conference of the European Association of Cognitive Ergonomics (EACE) . Editors: Brinkman, W, Ham, D, Wong, BLW , vol. 4663 ,
Cerone A, Curzon P ( 2007 ) . Preface . Electronic Notes in Theoretical Computer Science vol. 183 , ( SPEC. ISS. ) 1 - 2 .
Ruksenas R, Curzon P, Blandford A ( 2007 ) . Detecting Cognitive Causes of Confidentiality Leaks . Proceedings of the 1st International Workshop on Formal Methods for Interactive Systems . Editors: Curzon, P, Cerone, A , vol. 183 , 21-38 - 21-38 .
Wilson J, Curzon P, Whitney G ( 2007 ) . Seniors route-planning: a reality check for the design of navigation systems . Proceedings of TRANSED 2007 - 11th International Conference on Mobility and Transport for Elderly and Disabled Persons .
Xiong H, Curzon P, Tahar S, Blandford A ( 2007 ) . Providing a formal linkage between MDG and HOL . Formal Methods in System Design vol. 30 , Article 2 , 83-116 - 83-116 .
Curzon P, Cerone A ( 2007 ) . 2<sup>nd</sup> international workshop on formal methods for interactive systems . People and Computers XXI HCI.But Not as We Know It - Proceedings of HCI 2007: The 21st British HCI Group Annual Conference . vol. 2 ,
Curzon P, Ruksenas R, Blandford A ( 2007 ) . An Approach to Formal Verification of Human-Computer Interaction . Formal Aspects of Computing vol. 19 , Article 4 , 513 - 550 .
Ruksenas R, Curzon P, Blandford A ( 2007 ) . Detecting Cognitive Causes of Confidentiality Leaks . Electronic Notes in Theoretical Computer Science vol. 183 , 21-38 - 21-38 .
Back J, Cheng WL, Dann R, Curzon P, Blandford A ( 2007 ) . Does being motivated to avoid procedural errors influence their systematicity? . People and Computers XX - Engage . Editors: BryanKinns, N, Blandfor, A, Curzon, P, Nigay, L et al. , 151 - 157 .
Papatzanis G, Curzon P, Blandford A ( 2007 ) . Evaluation of Car Navigation Systems: On-Road Studies or Analytical Tools . In Proceedings of the Interact 2007 Workshop: Technology has escaped from the zoo: studying usability in the wild .
Ruksenas R, Curzon P, Back J, Blandford A ( 2007 ) . Formal Modelling of Cognitive Interpretation . Interactive Systems. Design, Specification, and Verification: 13th International Workshop, DSVIS 2006 . Editors: Doherty, GJ, Blandford, A , vol. 4323 , 123-136 - 123-136 .
Ruksenas R, Curzon P, Back J, Blandford A ( 2007 ) . Formal modelling of cognitive interpretation . Interactive Systems: Design, Specification, and Verification . Editors: Doherty, G, Blandford, A , vol. 4323 , 123 - 136 .
Back J, Blandford A, Curzon P ( 2007 ) . Recognising Erroneous and Exploratory Interactions . Human-Computer Interaction - INTERACT 2007 . Editors: Baranauskas, C, Palanque, P, Abascal, J, Barbosa, SDJ et al. , vol. 4663 , 127 - 140 .
Furniss D, Blandford A, Curzon P ( 2007 ) . Resilience in Usability Consultancy Practice: The Case for a Positive Resonance Model . Proceedings of the Resilience Engineering Workshop, June, 2007, Vadstena, Sweden. . Editors: Woltjer, R, Johansson, B, Lundberg, J , vol. 23 , 31-35 - 31-35 .
Graham TCN, Curzon P, Doherty G, Palanque P, Potter R, Roast C, Smith SP ( 2007 ) . Usability and computer games: Working group report . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 4323 LNCS , 265 - 268 .
Perkins VD, Butterworth R, Curzon P, Fields B ( 2006 ) . Representation of the National Memory: digitising historical photograph collections in the UK . Performance Research Journal vol. 11 , Article 4 , 83-116 - 83-116 .
Mizouni R, Tahar S, Curzon P ( 2006 ) . Hybrid Verification Integrating HOL Theorem Proving with MDG Model Checking . Microelectronics Journal vol. 37 , Article 11 , 1200 - 1207 .
Mizouni R, Tahar S, Curzon P ( 2006 ) . Hybrid verification integrating HOL theorem proving with MDG model checking . MICROELECTRONICS JOURNAL . vol. 37 , 1200 - 1207 .
Curzon P, McOwan P, Burton E, Gould M ( 2006 ) . Engaging with Computer Science through Play and Performance . Designing the Not-Quite-Yet: Ideas and Methods for Engaging the Public in a Digital Future of their Choice .
Wilson J, Curzon P ( 2006 ) . Older People’s Experiences Route-planning . Volume 2 Proceedings of the British Computer Society Annual Conference on Human Computer Interaction: HCI 2006. Engage .
Curzon P ( 2006 ) . Backwards Compatible . Medium: Paul’s Interactions, usabilitynews.com, British HCI Group , Notes: optkey: optnote: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.usabilitynews.com/news/ ,
Perkins VD, Butterworth R, Fields B, Curzon P ( 2006 ) . Keeping stuff safe: using guidelines and standards for digital preservation . The Institute of Physics and University of the Arts London Third International Conference on: Preservation and Conservation Issues Related to Digital Printing and Digital Photography . 40-43 - 40-43 .
Back J, Cheng WL, Dann R, Curzon P, Blandford A ( 2006 ) . Does being motivated to avoid procedural errors influence their systemacity? . People and Computers XX � Engage. Proceedings of HCI 2006 . Editors: Bryan-Kinns, N, Blandford, A, Curzon, P, Nigay, L et al. , 151-157 - 151-157 .
Jagne J, Smith S, Curzon P, Fields B ( 2006 ) . Integrating social and cultural variances into international eCommerce interface design . Volume 2 Proceedings of the British Computer Society Annual Conference on Human Computer Interaction: HCI 2006. Engage .
Blandford A, Back J, Curzon P, Li S, Ruksenas R ( 2006 ) . Reasoning about human error by modeling cognition and interaction . Proceedings of the Resilience Engineering Symposium . Editors: Hollnagel, E, Rigaud, E , 36 - 43 .
Davis-Perkins V, Butterworth R, Curzon P, Fields B ( 2005 ) . A study into the effect of digitisation projects on the management and stability of historic photograph collections . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 3652 LNCS , 278 - 289 .
Romijn J, Smith G, Van De Pol J, Bert D, Boiten E, Bowen J, Butler M, Curzon P et al. ( 2005 ) . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface .
Curzon P, Wilson J, Whitney G ( 2005 ) . Successful strategies of older people for finding information . Interacting with Computers: Special issue on HCI and the Older Population vol. 17 , Article 6 , 660-671 - 660-671 .
Curzon P ( 2005 ) . Perfect usability - The one-button machine? . Medium: Paul’s Interactions, usabilitynews.com, British HCI Group , Notes: Also in: uiGuardian.net, Weaving Usability and Cultures, October 2005 optkey: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.usabilitynews.com/news/ ,
Curzon P ( 2005 ) . The extreme Challenge of Moore’s Law and what Stormy Petrels have to do with it . Medium: Paul’s Interactions, usabilitynews.com, British HCI Group , Notes: optkey: optnote: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.usabilitynews.com/news/ ,
Perkins VD, Butterworth R, Curzon P ( 2005 ) . "Don't forget the STAGES"! Searching for values in digital surrogates of historical photographs . Archiving 2005, Final Program and Proceedings . 26 - 31 .
Davis-Perkins V, Butterworth R, Curzon P, Fields B ( 2005 ) . A study into the effect of digitisation projects on the management and stability of historic photograph collections . RESEARCH AND ADVANCED TECHNOLOGY FOR DIGITAL LIBRARIES . Editors: Rauber, A, Christodoulakis, S, Tjoa, AM , vol. 3652 , 278 - 289 .
Jagne J, Smith S, Duncker E, Curzon P ( 2005 ) . Cross-Cultural Factors of Physical-Shopping and eShopping . Conference: Proceedings of HCI International 2005
Mizouni R, Tahar S, Curzon P ( 2004 ) . Hybrid tool integrating HOL theorem proving with MDG model checking . Proceedings of the International Conference on Microelectronics, ICM . 392 - 395 .
Curzon P ( 2004 ) . Flexing Paper’s Muscle . Medium: Paul’s Interactions, usabilitynews.com, British HCI Group , Notes: optkey: optnote: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: documenturl: http://www.usabilitynews.com/news/article1675.asp/ ,
Jagne J, Smith SG, Duncker E, Curzon P ( 2004 ) . Cross-cultural Interface Design Strategy . report no. IDC-TR-2004-006 ,
CURZON P, Butterworth R, Blandford A ( 2004 ) . Models of Interactive systems: a case study on a programmable user modelling . International Journal of Human-Computer Studies vol. 60 , ( 2 ) 149 - 200 .
Blandford A, Butterworth R, Curzon P ( 2004 ) . Models of interactive systems: a case study on programmable user modelling . INT J HUM-COMPUT ST vol. 60 , ( 2 ) 149 - 200 .
Curzon P ( 2004 ) . When smart thinking is not enough . Medium: Paul’s Interactions, usabilitynews.com, British HCI Group , Notes: optkey: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: documenturl: http://www.usabilitynews.com/news/article1540.asp ,
CURZON P, Tahar S, Mizouni R ( 2004 ) . A Hybrid Tool Integrating HOL Theorem Proving with MDG Model Checking . Conference: Proceedings of the 16th IEEE International Conference on Microelectronics, Tunisia
Curzon P, Blandford A ( 2004 ) . Formally justifying user-centred design rules: A case study on post-completion errors . INTEGRATED FORMAL METHODS, PROCEEDINGS . Editors: Boiten, EA, Derrick, J, Smith, G , vol. 2999 , 461 - 480 .
CURZON P, Wilson J, Whitney G, Keith S ( 2004 ) . Information Seeking Strategies used by older people . Conference: HCI and the older population, workshop at HCI2004, Design for Life: The 18th British HCI Group Annual conference
Blandford A, Butterworth R, Curzon P ( 2004 ) . Models of Interactive systems: a case study on programmable user modelling . International Journal of Human-computer Studies vol. 60 , Article 2 , 149-284 - 149-284 .
Curzon P, Keith S, Whitney G, Wilson J ( 2004 ) . Strategies for finding government information by older people . User-Centred Interaction Paradigms for Universal Access in the Information Society, 8th ERCIM International Workshop on User Interfaces for All . Editors: Stary, C, Stephanidis, C , 34-41 - 34-41 .
Curzon P ( 2003 ) . Spit-not-so, or what’s in the layout . Medium: Paul’s Interactions, usabilitynews.com, British HCI Group , Notes: optkey: optnote: http://www.usabilitynews.com/news/article1458.asp optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2003/ optkeywords: optdocumenturl: http://www.usabilitynews.com/news/article1458.asp ,
Curzon P ( 2003 ) . Maori Culture? Who Cares? . Medium: Paul’s Interactions, usabilitynews.com, British HCI Group , Notes: optkey: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2003/ optkeywords: optdocumenturl: http://www.usabilitynews.com/news/article1365.asp ,
Mizouni R, Tahar S, Curzon P ( 2003 ) . On the Embedding of MDG specification Languages in HOL . ACS/IEEE International Conference on Computer Systems and Applications (AICCSA’03) .
CURZON P, Tahar S, Kort S ( 2003 ) . Hierarchical Formal Verification Using a Hybrid Tool . International Journal on Software Tools for Technology Transfer vol. 4 , ( 3 ) 313 - 322 .
Curzon P, Blandford A ( 2003 ) . A formal justification of a design rule for avoiding post-completion errors . Middlesex University, Interaction Design Centre report no. IDC-TR-2003-005 ,
Curzon P ( 2003 ) . Middlesex University Interaction Design Centre . Proceedings of HCI 2003: Designing for Society . Editors: Gray, P, Johnson, H, Neill, EO , vol. 2 , 219-220 - 219-220 .
Xiong H, Curzon P, Tahar S, Blandford A ( 2003 ) . Providing a formal linkage between the MDG verification system and HOL proof system .
Curzon P, Harding J ( 2003 ) . Spreading the word about pedagogic research: the virtual reading group . Academic and Educational Development: Research, Evaluation and Changing Practice in Higher Education ,
Xiong H, Curzon P, Tahar S, Blandford A ( 2002 ) . Formally Linking MDG and HOL based on a verified MDG system . Lecture Notes in Computer Science . Conference: Proc. of the 3rd International Conference on Integrated Formal Methods ( Turku, Finland ) vol. 2335 , 205 - 224 .
Xiong H, Curzon P, Tahar S, Blandford A ( 2002 ) . Formally linking MDG and HOL based on a verified MDG system . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 2335 , 205 - 224 .
Curzon P, Blandford AE ( 2002 ) . From a formal user model to design rules . Interactive Systems. Design, Specification and Verification, 9th International Workshop . Editors: Forbrig, P, Urban, B, Vanderdonckt, J, Limbourg, Q et al. , vol. 2545 , 1-15 - 1-15 .
Curzon P, Blandford A, Butterworth R, Bhogal R ( 2002 ) . Interaction Design Issues for Car Navigation Systems . Proceedings of the 16th British HCI Conference . Editors: Sharp, H, Chalk, P, LePeuple, J, Rosbottom, J et al. , vol. 2 , 38-41 - 38-41 .
Curzon P, Harding J ( 2002 ) . Spreading the word about pedagogic research . Academic and Educational Development: Research, Evaluation and Changing Practice in Higher Education , Editors: Macdonald, R, Wisdom, J , Kogan Page
Thimbleby H, Blandford A, Cairns P, Curzon P, Jones M ( 2002 ) . User interface design as systems design . PEOPLE AND COMPUTERS XVI- MEMORABLE YET INVISIBLE, PROCEEDINGS . Editors: Faulkner, X, Finlay, J, Detienne, F , 281 - 301 .
Blandford AE, Butterworth R, Curzon P ( 2001 ) . PUMA Footprints: linking theory and craftskill in usability evaluation . Proceedings of Interact . 577-584 - 577-584 .
Curzon P, Blandford AE ( 2001 ) . A user model for avoiding design induced errors in soft-key interactive systems . TPHOLS 2001 Supplementary Proceedings . Editors: Bolton, RJ, Jackson, PB , 33-48 - 33-48 .
Curzon P, Tahar S ( 2001 ) . Automating the Verification of Parameterized Hardware using a Hybrid Tool . Proceedings of the IEEE 13th International Conference on Microelectronics (ICM’01) . 257-260 - 257-260 .
Curzon P, Tahar S ( 2001 ) . Automating the verification of parameterized hardware using a hybrid tool . ICM 2001: 13TH INTERNATIONAL CONFERENCE ON MICROELECTRONICS, PROCEEDINGS . 257 - 260 .
Curzon P, Blandford A ( 2001 ) . Detecting multiple classes of user errors . ENGINEERING FOR HUMAN-COMPUTER INTERACTION . Editors: Little, MR, Nigay, L , vol. 2254 , 57 - 71 .
CURZON P, Tahar S, Kort S ( 2001 ) . Hierarchical Formal Verification using an MDGHOL Hybrid Tool . Conference: Correct Hardware Design and Verification methods, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference
Butterworth R, Blandford A, Curzon P ( 2001 ) . Lab Overview: Interaction Design Centre, Middlesex University . Interaction without frontiers, IHM-HCI 2001 . Editors: Vanderdonckt, J, Blandford, A, Derycke, A , 299-300 - 299-300 .
Blandford A, Butterworth R, Curzon P ( 2001 ) . PUMA Footprints: linking theory and craft skill in usability evaluation . HUMAN-COMPUTER INTERACTION - INTERACT'01 . Editors: Hirose, M , 577 - 584 .
Xiong H, Curzon P, Tahar S, Blandford A ( 2001 ) . Proving Existential Theorems when Importing Results from MDG to HOL . TPHOLS 2001 Supplementary Proceedings . Editors: Bolton, RJ, Jackson, PB , 384-399 - 384-399 .
Hasan M, Tahar S, Curzon P ( 2000 ) . Impact of Design Changes on Verification Using MDGs . Proc. IEEE Canadian Conference on Electrical and Computer Engineering (CCECE’00) . 173-178 - 173-178 .
Kort S, Pisini VK, Tahar S, Aït-Mohamed O, Curzon P, Song X ( 2000 ) . Un outil hybride pour la vérification formelle de circuits . Proc. 68th ACFAS Symposium (ACFAS’00) .
Kort S, Tahar S, Curzon P, Song X ( 2000 ) . HOL-MDG: A Hybrid Tool for Formal Verification . Proceedings of the 2000 Micronet Workshop . 131-132 - 131-132 .
Curzon P ( 2000 ) . Learning Computer Science Through Games and Puzzles . Proceedings of C@MDX’00, Research Student’s Conference .
Curzon P, Blandford A ( 2000 ) . Reasoning about Order Errors and Interaction . Proceedings of C@MDX’00, Research Student’s Conference .
Curzon P, Blandford A ( 2000 ) . Reasoning about Order Errors in Interaction .
Curzon P, Blandford A ( 2000 ) . Using a Verification System to Reason about Post-Completion Errorsteraction .
Xiong H, Curzon P, Tahar S, Blandford A ( 2000 ) . Embedding and Verification of an MDG-HDL Compiler in HOL . The Supplementary Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics . Editors: Aagaard, M, Harrison, J, Schubert, T , 237-248 - 237-248 .
Pisini VK, Tahar S, Curzon P, Aït-Mohamed O, Song X ( 2000 ) . Formal Hardware Verification by Integrating HOL and MDG . Proceedings of the ACM 10th Great Lakes Symposium on VLSI . 23-28 - 23-28 .
Curzon P, Blandford A ( 2000 ) . Reasoning about Order Errors in Interaction . The Supplementary Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics . Editors: Aagaard, M, Harrison, J, Schubert, T , 33-48 - 33-48 .
Curzon P, Blandford A ( 2000 ) . Using a Verification System to Reason About Post-Completion Errors . Participants Proc. of DSV-IS 2000: 7th Int.Workshop on Design, Specification and Verification of Interactive Systems, at the 22nd Int. Conf. on Software Engineerings . Editors: Palanque, P, Paternò, F , 292-308 - 292-308 .
Curzon P, Tahar S ( 1999 ) . Comparing HOL and MDG: A Case Study on the Verification of an ATM Switch Fabric . Nordic Journal of Computing vol. 6 , Article 4 , 372 - 402 .
Curzon P, Harding J ( 1999 ) . A Summary of the Virtual Reading Group Project . Medium: The SEDA Newsletter , Notes: optkey: optvolume: optnumber: optpages: optnote: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2000/ optkeywords: optdocumenturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2000/ ,
Pisini VK, Tahar S, Aït-Mohamed O, Curzon P, Song X ( 1999 ) . An Approach to Link HOL and MDG for Hardware Verification . Proceedings of the 1999 Micronet Workshop . 156-157 - 156-157 .
Xiong H, Curzon P, Blandford A ( 1999 ) . Combining Verification Systems in a Trusted Way to Reap the Benefits of Both . 6th Workshop on Automated Reasoning - Bridging the Gap between Theory and Practice .
Xiong H, Curzon P, Tahar S, Blandford A ( 1999 ) . Verification of a Translator for MDG’s Library in HOL . 15th British Colloquium for Theoretical Computer Science .
Curzon P ( 1999 ) . Chocolate Vending Machines in HOL . Notes: User Interfaces and Personal Technologies, Middlesex University School of Computing Science Mini-conference optkey: optmonth: December optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ ,
Curzon P, Tahar S, Lu J ( 1999 ) . Comparing HOL, MDG and VIS A Case Study on the Verification of an ATM Switch Fabric . report no. Technical Report CS- ,
Curzon P, Harding J ( 1999 ) . Drip Fed Academic Staff Development Using a Virtual Reading Group . On Reflection: Professional development for the future, the 4th Annual SEDA Conference for Staff and Educational Developers .
H Xiong PC, Tahar S ( 1999 ) . Importing MDG Verification Results into HOL . Theorem Proving in Higher Order Logics: 12th International Conference . vol. 1690 , 293-310 - 293-310 .
Curzon P ( 1999 ) . Learning Computer Science through Games and Puzzles . Computers and Fun 2 .
Curzon P ( 1998 ) . Progress Setting up a Virtual HE Teaching and Learning Reading Group . Creative Pathways to Development: 3rd Annual SEDA Conference for Staff and Educational Developers .
Xiong H, Curzon P ( 1998 ) . Verification of a Translator for MDG’s Components in HOL . mucort98: Computers and Engineering in the Millenium .
Curzon P ( 1998 ) . Read, summarise, debate, write . Improving the quality of argument in Higher Education: trial materials , Editors: Mitchell, S , Middlesex University
Tahar SE, Curzon P, Lu J ( 1998 ) . Three Approaches to Hardware Verification: HOL, MDG and VIS compared . Formal Methods in Computer Aided Design . Editors: Gopalakrishnan, G, Windley, P , vol. 1522 , 433-450 - 433-450 .
Curzon P, Tahar SE, Mohamed OA ( 1998 ) . Verification of the MDG Components Library Using HOL . The Supplementary Proceedings of Theorem Proving in Higher Order Logics: 11th International Conference .
Curzon P, Rix J ( 1998 ) . Why do Students take Programming Modules? . Proceedings of the 6th Annual Conference on the Teaching of Computing .
Curzon P, Rix J ( 1998 ) . Why do students take programming modules? . SIGCSE Bulletin (Association for Computing Machinery, Special Interest Group on Computer Science Education) vol. 30 , ( 3 ) 59 - 63 .
Jakubiec L, Coupet-Grimal S, Curzon P ( 1997 ) . A Comparison of the Coq and HOL Proof Systems for Specifying Hardware . Supplementary Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics . Editors: Gunter, EL, Felty, A , 63-78 - 63-78 .
Wong W, Curzon P ( 1997 ) . Towards an Efficient Proof Recorder for HOL90 . Supplementary Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics . Editors: Gunter, EL, Felty, A , 135-149 - 135-149 .
Curzon P, Blandford A, Jones M, Marsden G, Smith M ( 1997 ) . Supporting a Large-class Programming Course with Intranet Tools . Proceedings of the 5th Annual Conference on the Teaching of Computing . 270 - 270 .
Curzon P ( 1996 ) . Hardware Verification and ATM Switches . Notes: Colloquium on Formal Methods and Security, Isaac Newton Institute, Cambridge. optkey: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ ,
Curzon P ( 1996 ) . Hierarchical Formal Verification of a Communication Network . Notes: Poster presented at EPSRC ITeC’96, Leeds optkey: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ ,
Curzon P, Wong W ( 1996 ) . Checking Proofs from Linked Tools . Notes: Presented at the 4th ProCoS Working Group Meeting, Oldenburg, Germany optcrossref: optkey: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ ,
Tahar S, Curzon P ( 1996 ) . A Comparison of MDG and HOL for Hardware Verification . Theorem Proving in Higher Order Logics: 9th International Conference . Editors: Wright, JV, Grundy, J, Harrison, J , vol. 1125 ,
Curzon P, Leslie I ( 1996 ) . Improving Hardware Designs Whilst Simplifying their Proof . Designing Correct Circuits .
Curzon P, Leslie I ( 1995 ) . A Case Study on Design for Provability . The Proceedings of the First International Conference on Engineering of Complex Computer Systems . 59-62 - 59-62 .
Curzon P ( 1995 ) . Bridging the Gap Between Theory and Practice . Notes: Invited panel session at the Second AISB Workshop on Automated Reasoning: Bridging the Gap Between Theory and Practice optkey: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ ,
Curzon P, Leslie I, Gordon M ( 1995 ) . Conclusions from a Study to Verify a Real Network Component . Proceedings of the Second Workshop on Automated Reasoning: Bridging the Gap Between Theory and Practice .
Curzon P ( 1995 ) . Problems Encountered with the Machine-assisted Proof of Hardware . Correct Hardware Design and Verification Methods . Editors: Camurati, PE, Eveking, H , vol. 987 , 56-70 - 56-70 .
Curzon P ( 1995 ) . The Importance of Proof Maintenance and Reengineering . International Workshop on Higher Order Logic Theorem Proving and Its Applications: B-Track: Short Presentations . Editors: Alves-Foss, J , 17-32 - 17-32 .
Curzon P ( 1995 ) . Tracking Design Changes with Formal Machine-Checked Proof . The Computer Journal vol. 38 , Article 2 , 91-100 - 91-100 .
Curzon P ( 1995 ) . Tracking design changes with formal machine-checked proof . Computer Journal vol. 38 , ( 2 ) 91 - 100 .
Curzon P ( 1995 ) . Virtual Theories . Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications . Editors: Schubert, ET, Windley, PJ, Alves-Foss, J , vol. 971 , 138-153 - 138-153 .
Curzon P, Wong W ( 1994 ) . A Theory of Lists for HOL Based on Higher-Order Functions . Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications . Editors: Melham, TF, Camilleri, J ,
Curzon P ( 1994 ) . Tracking Design Changes with Formal Verification . Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop . Editors: Melham, TF, Camilleri, J , vol. 859 , 177-192 - 177-192 .
Curzon P ( 1994 ) . The Formal Verification of an ATM Network . Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing . 392 - 392 .
Curzon P ( 1994 ) . The Formal Verification of the Fairisle ATM Switching Element . report no. 329 ,
Curzon P ( 1994 ) . The Formal Verification of the Fairisle ATM Switching Element: an Overview . report no. 328 ,
Curzon P ( 1994 ) . The Formal Verification of the Fairisle Switch: The 4x4 Switching Fabric . ATM Document Collection 3 (The Blue Book) , University of Cambridge Computer Laboratory ( University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG. England ),
Curzon P ( 1994 ) . Experiences formally verifying a network component . Proceedings of the 9th Annual IEEE Conference on Computer Assurance . 183-193 - 183-193 .
Curzon P ( 1994 ) . The Verified Compilation of Vista Programs . Notes: Presented at the 1st ProCoS Working Group Meeting, Gentofte, Denmark. optcrossref: optkey: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ ,
Curzon P ( 1993 ) . A Verified Vista Implementation . report no. 311 ,
Curzon P ( 1993 ) . Deriving Correctness Properties of Compiled Code . Formal Methods in System Design vol. 3 , Article 1/2 , 83-115 - 83-115 .
Curzon P ( 1993 ) . Compiler Correctness and Input/Output . Dependable Computing for Critical Applications 3 . Editors: Landwehr, CE, Randell, B, Simoncini, L , vol. 8 , 189-209 - 189-209 .
Curzon P ( 1993 ) . Deriving Correctness Properties of Compiled Code . Higher Order Logic Theorem Proving and its Applications . Editors: Claesen, L, Gordon, M , 327-346 - 327-346 .
Curzon P ( 1992 ) . Of What Use is a Verified Compiler Specification? . report no. 274 ,
Curzon P ( 1992 ) . A Programming Logic For a Verified Structured Assembly Language . Logic Programming and Automated Reasoning . Editors: Voronkov, A , vol. 624 , 403-408 - 403-408 .
Curzon P ( 1992 ) . A Verified Compiler for a Structured Assembly Language . Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications . Editors: Archer, M, Joyce, JJ, Levitt, KN, Windley, PJ et al. ,
Curzon P ( 1991 ) . A Structured Approach to the Verification of Low Level Microcode . report no. 215 ,
Curzon P ( 1990 ) . A Verified Vista Implementation of the Viper Microprocessor . Notes: Poster at the International Workshop on the HOL Theorem Proving System and its Applications optkey: optmonth: optannote: optabstract: optabstracturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ optkeywords: optdocumenturl: http://www.dcs.qmul.ac.uk/%7Epc/publications/2004/ ,