Trosolwg
Mae Dr Anton Setzer yn Ddarllenydd yn yr Adran Gyfrifiadureg, Prifysgol Abertawe.
Hafan Personol: https://csetzer.github.io/
Dr Anton Setzer
Reader
Computer Science
403
Pedwerydd Llawr
Y Ffowndri Gyfrifiadol
Campws y Bae
Pedwerydd Llawr
Y Ffowndri Gyfrifiadol
Campws y Bae
Ar gael ar gyfer Goruchwyliaeth Ôl-raddedig
Dolenni Ymchwil
Meysydd Arbenigedd
- Profi theoremau rhyngweithiol
- Damcaniaeth teip
- Damcaniaeth teip Martin-Loef
- Cyd-anwythiad
- Damcaniaeth prawf
- Rhaglennu wedi'i deipio'n ddibynnol
- Trefnolion
- Paru patrymau
Cyhoeddiadau
Uchafbwyntiau Ymchwil
-
BRYANT, H., Seisenberger, M., Setzer, A., & Lawrence, A. (n.d.) Formal Assurance for Railway Signalling: Expanding SAT Proof Checking to Certify Z3's Inequality-Based SMT Proofs for ERTMS. Proceedings of International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation, ISoLA 2026. To appear in Lecture Notes in Computer Science SpringerSU Repository: https://cronfa.swan.ac.uk/Record/cronfa72334
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (n.d.) Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq. In RocqPL 2026ACM.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa71163
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (2025). Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda. In Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea (pp. 1-5). Zenodo.
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (2025). Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda. In Fredrik Nordvall Forsberg. (Ed.), Types 2025 (pp. 186-189).SU Repository: https://cronfa.swan.ac.uk/Record/cronfa70913
-
Setzer, A. (n.d.) Predicativity of the Mahlo Universe in type theory. Pillars of enduring strength: learning from Hermann Weyl Oxford University PressSU Repository: https://cronfa.swan.ac.uk/Record/cronfa69298
-
Dogan, H. & Setzer, A. (2025). SABEC: Secure and Adaptive Blockchain-Enabled Coordination Protocol for Unmanned Aerial Vehicles(UAVs) Network. In Proceedings of the 11th International Conference on Information Systems Security and Privacy (pp. 377-388). SCITEPRESS - Science and Technology Publications.
-
Alhabardi, F. & Setzer, A. (2023). A simulator of Solidity-style smart contracts in the theorem prover Agda. In Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications (pp. 1-11). ACM.
-
Alhabardi, F. & Setzer, A. (2023). A model of Solidity-style smart contracts in the theorem prover Agda. In 2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings) (pp. 1-10). IEEE.
-
Vessio, M., Beckmann, A., Roach, M., Saintier, S., Clements, R., & Setzer, A. (2024). InPerpetuity{Challenging Misperceptions of the Term ‘Smart Contract’}. European Journal of Law and Technology, 15(2)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa67545
-
Vessio, M., Beckmann, A., Roach, M., Saintier, S., Clements, R., & Setzer, A. (2024). InPerpetuity{Challenging Misperceptions of the Term “Smart Contract”}. European Journal of Law and Technology, 15(2)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa68617
Holl Ymchwil
Erthyglau Cylchgronau
-
Vessio, M., Beckmann, A., Roach, M., Saintier, S., Clements, R., & Setzer, A. (2024). InPerpetuity{Challenging Misperceptions of the Term ‘Smart Contract’}. European Journal of Law and Technology, 15(2)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa67545
-
Vessio, M., Beckmann, A., Roach, M., Saintier, S., Clements, R., & Setzer, A. (2024). InPerpetuity{Challenging Misperceptions of the Term “Smart Contract”}. European Journal of Law and Technology, 15(2)SU Repository: https://cronfa.swan.ac.uk/Record/cronfa68617
-
Dybjer, P. & Setzer, A. (2024). The extended predicative Mahlo universe in Martin-Löf type theory. Journal of Logic and Computation, 34(6), 1032-1063.
-
Igried, B. & Setzer, A. (2018). Defining Trace Semantics for CSP-Agda. Leibniz International Proceedings in Informatics, LIPIcs, 97, 12:1-12:23.
-
Igried, B. & Setzer, A. (2017). Trace and Stable Failures Semantics for CSP-Agda. Electronic Proceedings in Theoretical Computer Science, 258, 36-51.
-
Abel, A., Adelsberger, S., & Setzer, A. (2017). Interactive programming in Agda – Objects and graphical user interfaces. Journal of Functional Programming, 27
-
Kanso, K. & Setzer, A. (2014). A light-weight integration of automated and interactive theorem proving. Mathematical Structures in Computer Science, 26(01), 129-153.
-
Kanso, K., Moller, F., & Setzer, A. (2009). Automated Verification of Signalling Principles in Railway Interlocking Systems. Electronic Notes in Theoretical Computer Science, 250(2), 19-31.
-
Kanso, K., Moller, F., & Setzer, A. (2009). Automated Verification of Signalling Principles in Railway Interlocking Systems. Electronic Notes in Theoretical Computer Science, 250(2), 19-31.
-
Abdul Rauf, R., Berger, U., & Setzer, A. (2008). A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++. Theory of Computing Systems, 43(3-4), 298-321.
-
Dybjer, P. & Setzer, A. (2006). Indexed induction–recursion. The Journal of Logic and Algebraic Programming, 66(1), 1
-
Dybjer, P. & Setzer, A. (2003). Induction–recursion and initial algebras. Annals of Pure and Applied Logic, 124(1-3), 1-47.
Penodau Llyfrau
-
Setzer, A. (2019). An Upper Bound for the Proof Theoretic Strength of Martin-Löf Type Theory with W-type and one Universe. SpringerSU Repository: https://cronfa.swan.ac.uk/Record/cronfa51297
-
Setzer, A. (2016). How to Reason Coinductively Informally. Advances in Proof Theory -408). Birkhäuser
-
Setzer, A. (2015). The Use of Trustworthy Principles in a Revised Hilbert’s Program. Gentzen's Centenary (pp. 45-60). Springer
-
Setzer, A. (2012). Coalgebras as Types Determined by Their Elimination Rules. Epistemology versus Ontology (pp. 351-369).
-
Nordvall Forsberg, F. & Setzer, A. (2010). Inductive-Inductive Definitions. Computer Science Logic (pp. 454-468). Springer
-
Kahle, R. & Setzer, A. (2010). An extended predicative definition of the Mahlo universe. Ways of Proof Theory (pp. 309-334). De Gruyter
-
Setzer, A. (2008). Universes in type theory part I—Inaccessibles and Mahlo. Logic Colloquium 2004 (pp. 123-156). Cambridge University Press
-
Setzer, A. (2008). Proof theory and Martin-Löf Type Theory. One Hundred Years of Intuitionism (1907–2007) (pp. 257-279). Birkhäuser
-
BRYANT, H., Seisenberger, M., Setzer, A., & Lawrence, A. (n.d.) Formal Assurance for Railway Signalling: Expanding SAT Proof Checking to Certify Z3's Inequality-Based SMT Proofs for ERTMS. Proceedings of International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation, ISoLA 2026. To appear in Lecture Notes in Computer Science SpringerSU Repository: https://cronfa.swan.ac.uk/Record/cronfa72334
-
Setzer, A. (n.d.) Predicativity of the Mahlo Universe in type theory. Pillars of enduring strength: learning from Hermann Weyl Oxford University PressSU Repository: https://cronfa.swan.ac.uk/Record/cronfa69298
Cyfraniadau Cynadleddau
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (2025). Verifying Z3 SAT Proofs with the Interactive Theorems Prover Coq/Rocq and Agda. In Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2025 Proceedings), Swansea (pp. 1-5). Zenodo.
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (2025). Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda. In Fredrik Nordvall Forsberg. (Ed.), Types 2025 (pp. 186-189).SU Repository: https://cronfa.swan.ac.uk/Record/cronfa70913
-
Dogan, H. & Setzer, A. (2025). SABEC: Secure and Adaptive Blockchain-Enabled Coordination Protocol for Unmanned Aerial Vehicles(UAVs) Network. In Proceedings of the 11th International Conference on Information Systems Security and Privacy (pp. 377-388). SCITEPRESS - Science and Technology Publications.
-
Alhabardi, F. & Setzer, A. (2023). A simulator of Solidity-style smart contracts in the theorem prover Agda. In Proceedings of the 2023 6th International Conference on Blockchain Technology and Applications (pp. 1-11). ACM.
-
Alhabardi, F. & Setzer, A. (2023). A model of Solidity-style smart contracts in the theorem prover Agda. In 2023 IEEE International Conference on Artificial Intelligence, Blockchain, and Internet of Things (AIBThings) (pp. 1-10). IEEE.
-
Alhabardi, F., Lazar, B., & Setzer, A. (2022). Verifying Correctness of Smart Contracts with Conditionals. In 2022 IEEE 1st Global Emerging Technology Blockchain Forum: Blockchain & Beyond (iGETblockchain) (pp. 1-25). IEEE.
-
Alhabardi, F., Beckmann, A., Lazar, B., & Setzer, A. (2022). Verification of Bitcoin Script in Agda using Weakest Preconditions for Access Control. In Henning Basold, Jesper Cockx, Silvia Ghilezan (Ed.), 27th International Conference on Types for Proofs and Programs (TYPES 2021) (pp. 1:1-1:25). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
-
Berger, U., Matthes, R., & Setzer, A. (2019). Martin Hofmann’s case for non-strictly positive data types. In Leibniz International Proceedings in Informatics, LIPIcs
-
Adelsberger, S., Igried, B., Moser, M., Savenkov, V., & Setzer, A. (2018). Formal Verification for Feature-Based Composition of Workflows. (pp. 173-181). SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems.
-
Berger, U. & Setzer, A. (2018). Undecidability of Equality for Codata Types. In Coalgebraic Methods in Computer Science (pp. 34-55). Springer International Publishing.
-
Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Declarative GUIs: Simple, Consistent, and Verified. In PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (pp. 1-15). Proceedings of PPDP 2018.
-
Adelsberger, S., Setzer, A., & Walkingshaw, E. (2018). Developing GUI Applications in a Verified Setting. In Dependable Software Engineering. Theories, Tools, and Applications (pp. 89-107). Springer International Publishing.
-
Igried, B. & Setzer, A. (2016). Programming with monadic CSP-style processes in dependent type theory. In TyDe 2016 (pp. 28-38). ACM.
-
Setzer, A., Abel, A., Pientka, B., & Thibodeau, D. (2014). Unnesting of Copatterns. In Rewriting and Typed Lambda Calculi (pp. 31-45). Springer.
-
James, P., Lawrence, A., Moller, F., Roggenbach, M., Seisenberger, M., Setzer, A., Kanso, K., & Chadwick, S. (2014). Verification of Solid State Interlocking Programs. In Software Engineering and Formal Methods-268).
-
Abel, A., Pientka, B., Thibodeau, D., & Setzer, A. (2013). Copatterns: programming infinite structures by observations. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 27-38). ACM, New York, NY, USA.
-
Ghani, N., Malatesta, L., Forsberg, F., & Setzer, A. (2013). Fibred Data Types. In Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on (pp. 243-252). IEEE.
-
Altenkirch, T., Morris, P., Forsberg, F., & Setzer, A. (2011). A Categorical Semantics for Inductive-Inductive Definitions. In Algebra and Coalgebra in Computer Science. 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings (pp. 70-84). Springer.
-
Kanso, K. & Setzer, A. (2009). Specifying railway interlocking systems. (pp. 233-236). Swansea University.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa106
-
Harwood, W., Moller, F., & Setzer, A. (2006). Weak Bisimulation Approximants. In Computer Science Logic (pp. 365
-
Bryant, H., Lawrence, A., Seisenberger, M., & Setzer, A. (n.d.) Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq. In RocqPL 2026ACM.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa71163
Goruchwyliaeth
-
Bridging Finite and Infinite State Verification: Generalised Property Directed Reachability, with a Proof of Correctness and Termination (cyfredol)
PhDGoruchwyliwr arall: Prof Markus Roggenbach -
Proof Checking for SMT-Solving and its application in the Railway Domain (cyfredol)
PhDGoruchwyliwr arall: Dr Monika Seisenberger -
Overcoming Information Silos: Semantic AI for Intelligent Interoperability in Pharmaceutical Supply Chains (cyfredol)
PhDGoruchwyliwr arall: Prof Arnold Beckmann -
Verification of Smart contracts using the interactive theorem prover Agda (dyfarnwyd 2024)
PhDGoruchwyliwr arall: Prof Arnold Beckmann -
Secure Identity Management System in Unmanned Aerial Vehicles Network (dyfarnwyd 2025)
PhDGoruchwyliwr arall: Dr Phillip James
Modiwlau a Addysgir
-
CSC313 Critical Systems
This module introduces various techniques for developing high integrity systems.
-
CSCM029 Blockchain Cryptocurrencies and Smart Contracts
This module offers a comprehensive introduction to blockchain technology, covering fundamental concepts such as the notions of money, smart contracts, and cryptography. It delves into the history of Bitcoin, the UTXO model, Bitcoin Script, and the intricacies of transactions and mining. The course also explores the basics of Ethereum, including its history, philosophy, and the smart contract language Solidity. Students will gain an understanding of the Ethereum Virtual Machine (EVM), Proof of Stake, and smart contract security. The module concludes with practical applications of blockchain technology.
-
CSPM20 MSc Project
This module will provide students with the opportunity to explore a particular topic in computer science in some considerable depth. It is only open to students studying MSc Computer Science, MSc Advanced Computer Science, MSc Data Science, MSc Cyber Security