Filter
Conference contribution

Search results

  • 2024

    A CHERI C memory model for verified temporal safety

    Zaliva, V., Memarian, K., Campbell, B., Almeida, R., Filardo, N., Stark, I. & Sewell, P., 19 Nov 2024, (Accepted/In press) Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’25). New York, NY, USA: ACM, p. 1-15 15 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour

    Zaliva, V., Memarian, K., De Oliveira Almeida, R., Clarke, J., Davis, B., Richardson, A., Chisnall, D., Campbell, B., Stark, I., Watson, R. N. M. & Sewell, P., 17 Apr 2024, ASPLOS 2024: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ACM, Vol. 1. p. 181-196 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2022

    Verified Security for the Morello Capability-enhanced Prototype Arm Architecture

    Bauereiss, T., Campbell, B., Sewell, T., Armstrong, A., Esswood, L., Stark, I., Barnes, G., Watson, R. N. M. & Sewell, P., 29 Mar 2022, Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings. Sergey, I. (ed.). Springer, p. 174-203 30 p. (Lecture Notes in Computer Science; vol. 13240).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2020

    Property-Directed Verified Monitoring of Signal Temporal Logic

    Stark, I. & Wright, T., 2 Oct 2020, Runtime Verification: 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings. Springer, p. 339–358 20 p. (Lecture Notes in Computer Science; vol. 12399).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process

    Nienhuis, K., Joannou, A., Bauereiss, T., Fox, A., Roe, M., Campbell, B., Naylor, M., Norton, R. M., Moore, S. W., Neumann, P. G., Stark, I., Watson, R. N. M. & Sewell, P., 30 Jul 2020, 2020 IEEE Symposium on Security and Privacy (SP). San Francisco, CA, USA: Institute of Electrical and Electronics Engineers, p. 1003-1020 18 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2018

    Triangulating Context Lemmas

    McLaughlin, C., McKinna, J. & Stark, I., 8 Jan 2018, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York, NY, USA: ACM, p. 102-114 13 p. (CPP 2018).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2017

    Extracting Behaviour from an Executable Instruction Set Model

    Campbell, B. & Stark, I., 27 Mar 2017, Proceedings of the 16th Conference on Formal Methods in Computer - Aided Design (FMCAD 2016). Mountain View, CA, USA: FMCAD Inc, p. 33-40 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2015

    Analysis of a Post-translational Oscillator Using Process Algebra and Spatio-temporal Logic

    Banks, C., Seaton, D. D. & Stark, I., 2015, Computational Methods in Systems Biology: 13th International Conference, CMSB 2015, Nantes, France, September 16-18, 2015, Proceedings. Springer, p. 222-238 17 p. (Lecture Notes in Computer Science; vol. 9308).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2014

    Certified Complexity (CerCo)

    Amadio, R., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D., Piccolo, M., Pollack, R., Régis-Giannas, Y., Sacerdoti Coen, C., Stark, I. & Tranquilli, P., 2014, Foundational and Practical Aspects of Resource Analysis: Revised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013. Springer, p. 1-18 18 p. (Lecture Notes in Computer Science; vol. 8552).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation

    Campbell, B. & Stark, I., 2014, Formal Methods for Industrial Critical Systems: 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings. Lang, F. & Flammini, F. (eds.). Springer, p. 185-199 15 p. (Lecture Notes in Computer Science; vol. 8718).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2012

    Stochastic Modelling of the Kai-based Circadian Clock

    Banks, C., Clark, A., Georgoulas, A.-A., Gilmore, S., Hillston, J., Milios, D. & Stark, I., 17 Sept 2012, Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling (PASM) and the Eleventh International Workshop on Parallel and Distributed Methods in Verification (PDMC).. Elsevier, Vol. 296. p. 43-60 18 p. (Electronic Notes in Theoretical Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2008

    Monitoring External Resources in Java MIDP

    Aspinall, D., Maier, P. & Stark, I., 21 Feb 2008, Proceedings of the First International Workshop on Run Time Enforcement for Mobile and Distributed Systems (REM 2007). Vol. 197. p. 17-30 14 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Safety Guarantees from Explicit Resource Management

    Aspinall, D., Maier, P. & Stark, I., 2008, Formal Methods for Components and Objects. de Boer, F., Bonsangue, M., Graf, S. & de Roever, W.-P. (eds.). Springer, Vol. 5382. p. 52-71 20 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • The Continuous π-Calculus: A Process Algebra for Biochemical Modelling

    Kwiatkowski, M. & Stark, I., 2008, Computational Methods in Systems Biology. Heiner, M. & Uhrmacher, A. (eds.). Springer, p. 103-122 20 p. (Lecture Notes in Computer Science; vol. 5307).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2007

    Mobile Resource Guarantees

    Sannella, D., Hofmann, M., Aspinall, D., Gilmore, S., Stark, I., Beringer, L., Loidl, H.-W., MacKenzie, K., Momigliano, A. & Shkaravska, O., 2007, Trends in Functional Programming. Intellect, Vol. 6. p. 211-226 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • MOBIUS: Mobility, ubiquity, security - Objectives and progress report

    Barthe, G., Beringer, L., Cregut, P., Gregoire, B., Hofmann, M., Mueller, P., Poll, E., Puebla, G., Stark, I. & Vetillard, E., 2007, Trustworthy Global Computing: Second Symposium, TGC 2006, Lucca, Italy, November 7-9, 2006, Revised Selected Papers. Montanari, U., Sannella, D. & Bruni, R. (eds.). Berlin: Springer, p. 10-29 20 p. (Lecture Notes in Computer Science; vol. 4661).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2005

    Automatic verification of design patterns in Java

    Blewitt, A., Bundy, A. & Stark, I., 2005, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering. New York, NY, USA: ACM, p. 224-232 9 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Free-algebra models for the pi-calculus

    Stark, I., 2005, Foundations of Software Science and Computational Structures. Sassone, V. (ed.). Berlin: Springer, p. 155-169 15 p. (Lecture Notes in Computer Science; vol. 3441).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Mobile Resource Guarantees (Project Evaluation Paper)

    Sannella, D., Hofmann, M., Aspinall, D., Gilmore, S., Stark, I., Beringer, L., Loidl, H.-W., MacKenzie, K., Momigliano, A. & Shkaravska, O., 2005, 6th Symposium on Trends in Functional Programming TFP 2005. Institute of Cybernetics, p. 7-16 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Mobile Resource Guarantees for Smart Devices

    Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D. & Stark, I., 2005, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers. Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L. & Muntean, T. (eds.). Berlin: Springer, Vol. 3362. p. 1-26 26 p. (Lecture Notes in Computer Science; vol. 3362).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Reducibility and TT-lifting for computation types

    Lindley, S. & Stark, I., 2005, Typed Lambda Calculi and Applications. Urzyczyn, P. (ed.). Berlin: Springer, p. 262-277 16 p. (Lecture Notes in Computer Science; vol. 3461).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    File
  • 2004

    A dependent type theory with names and binding

    Schopp, U. & Stark, I., 2004, Computer Science Logic: 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004. Proceedings. Marcinkowski, J. & Tarlecki, A. (eds.). Berlin: Springer, p. 235-249 15 p. (Lecture Notes in Computer Science; vol. 3210).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Nominal games and full abstraction for the nu-calculus

    Abramsky, S., Ghica, D., Murawski, A., Ong, C. & Stark, I., 2004, Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on. Institute of Electrical and Electronics Engineers, p. 150-159 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2001

    Automatic verification of Java design patterns

    Blewitt, A., Bundy, A. & Stark, I., 2001, Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on. Institute of Electrical and Electronics Engineers, p. 324-327 4 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1997

    Names, Equations, Relations: Practical Ways to Reason about new

    Stark, I., 1997, Typed Lambda Calculi and Applications: Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Nancy, France, April 2–4, 1997. de Groote, P. & Hindley, J. R. (eds.). Springer, p. 336-353 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 1210).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Presheaf models for the π-calculus

    Cattani, G. L., Stark, I. & Winskel, G., 1997, Category Theory and Computer Science: 7th International Conference, CTCS '97 Santa Margherita Ligure Italy, September 4–6, 1997 Proceedings. Moggi, E. & Rosolini, G. (eds.). Springer, p. 106-126 21 p. (Lecture Notes in Computer Science; vol. 1290).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1996

    A fully abstract domain model for the π-calculus

    Stark, I., 1 Jul 1996, Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on. Institute of Electrical and Electronics Engineers, p. 36-42 7 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution