A Local System for Classical Logic. - Kai Brünnler; Alwen Fernanto Tiu (LPAR, 2001)

Encoding Generic Judgments. - Dale Miller 001; Alwen Fernanto Tiu (FSTTCS, 2002)

A Proof Theory for Generic Judgments: An extended abstract. - Dale Miller 001; Alwen Fernanto Tiu (LICS, 2003)

Induction and Co-induction in Sequent Calculus. - Alberto Momigliano; Alwen Fernanto Tiu (TYPES, 2003)

A Proof Search Specification of the pi-Calculus. - Alwen Fernanto Tiu; Dale Miller 001 (FGUC, 2004)

Model Checking for pi-Calculus Using Proof Search. - Alwen Fernanto Tiu (CONCUR, 2005)

Formalization of a Generalized Protocol for Clock Synchronization. - Alwen Tiu (Arch. Formal Proofs, 2005)

A proof theory for generic judgments. - Dale Miller 001; Alwen Tiu (ACM Trans. Comput. Log., 2005)

A Local System for Intuitionistic Logic. - Alwen Tiu (LPAR, 2006)

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. - Pascal Fontaine; Jean-Yves Marion; Stephan Merz; Leonor Prensa Nieto; Alwen Fernanto Tiu (TACAS, 2006)

A Logic for Reasoning about Generic Judgments. - Alwen Tiu (LFMTP@FLoC, 2006)

A System of Interaction and Structure II: The Need for Deep Inference. - Alwen Tiu (Log. Methods Comput. Sci., 2006)

A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract. - Alwen Tiu (APLAS, 2007)

The Bedwyr System for Model Checking over Syntactic Expressions. - David Baelde; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu (CADE, 2007)

Verification of clock synchronization algorithms: experiments on a combination of deductive tools. - Damián Barsotti; Leonor Prensa Nieto; Alwen Tiu (Formal Aspects Comput., 2007)

Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5. - Rajeev Goré; Alwen Tiu (J. Log. Comput., 2007)

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. - Rajeev Goré; Linda Postniece; Alwen Tiu (Advances in Modal Logic, 2008)

Matching linear and non-linear trace patterns with regular policies. - Franz Baader; Andreas Bauer 002; Alwen Tiu (UNIF, 2008)

Cut Elimination for a Logic with Generic Judgments and Induction - Alwen Tiu (CoRR, 2008)

On the Role of Names in Reasoning about lambda-tree Syntax Specifications. - Alwen Tiu (LFMTP@LICS, 2008)

A First-Order Policy Language for History-Based Transaction Monitoring. - Andreas Bauer 002; Rajeev Goré; Alwen Tiu (ICTAC, 2009)

Matching Trace Patterns with Regular Policies. - Franz Baader; Andreas Bauer 002; Alwen Tiu (LATA, 2009)

A Proof Theoretic Analysis of Intruder Theories. - Alwen Tiu; Rajeev Goré (RTA, 2009)

Taming Displayed Tense Logics Using Nested Sequents with Deep Inference. - Rajeev Goré; Linda Postniece; Alwen Tiu (TABLEAUX, 2009)

Formalising Observer Theory for Environment-Sensitive Bisimulation. - Jeremy E. Dawson; Alwen Tiu (TPHOLs, 2009)

A Trace Based Bisimulation for the Spi Calculus - Alwen Tiu (CoRR, 2009)

A decidable policy language for history-based transaction monitoring - Andreas Bauer 002; Rajeev Goré; Alwen Tiu (CoRR, 2009)

Cut-elimination and Proof Search for Bi-Intuitionistic Tense Logic. - Rajeev Goré; Linda Postniece; Alwen Tiu (Advances in Modal Logic, 2010)

Automating Open Bisimulation Checking for the Spi Calculus. - Alwen Tiu; Jeremy E. Dawson (CSF, 2010)

A Proof Theoretic Analysis of Intruder Theories - Alwen Tiu; Rajeev Goré; Jeremy E. Dawson (Log. Methods Comput. Sci., 2010)

Proof search specifications of bisimulation and modal logics for the pi-calculus. - Alwen Tiu; Dale Miller 001 (ACM Trans. Comput. Log., 2010)

A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains. - Alwen Tiu (TABLEAUX, 2011)

On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics. - Alwen Tiu (TABLEAUX (Workshops, Tutorials, and Short Papers), 2011)

On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics - Rajeev Goré; Linda Postniece; Alwen Tiu (Log. Methods Comput. Sci., 2011)

Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures. - Alwen Tiu; Egor Ianovski; Rajeev Goré (Advances in Modal Logic, 2012)

Stratification in Logics of Definitions. - Alwen Tiu (IJCAR, 2012)

Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus - Yuxin Deng; Alwen Tiu (CoRR, 2012)

Characterisations of testing preorders for a finite probabilistic π-calculus. - Yuxin Deng; Alwen Tiu (Formal Aspects Comput., 2012)

Cut elimination for a logic with induction and co-induction. - Alwen Tiu; Alberto Momigliano (J. Appl. Log., 2012)

Extracting Proofs from Tabled Proof Search. - Dale Miller 001; Alwen Tiu (CPP, 2013)

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. - Ranald Clouston; Jeremy E. Dawson; Rajeev Goré; Alwen Tiu (CSL, 2013)

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic - Extended Version. - Ranald Clouston; Jeremy E. Dawson; Rajeev Goré; Alwen Tiu (CoRR, 2013)

Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System. - Hendra Gunadi; Alwen Tiu (FM, 2014)

From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic. - Jeremy E. Dawson; Ranald Clouston; Rajeev Goré; Alwen Tiu (IFIP TCS, 2014)

Proof search for propositional abstract separation logics via labelled sequents. - Zhe Hou; Ranald Clouston; Rajeev Goré; Alwen Tiu (POPL, 2014)

Abella: A System for Reasoning about Relational Specifications. - David Baelde; Kaustuv Chaudhuri; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu; Yuting Wang 001 (J. Formaliz. Reason., 2014)

Automated Theorem Proving for Assertions in Separation Logic with All Connectives. - Zhe Hou; Rajeev Goré; Alwen Tiu (CADE, 2015)

Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL. - Xiaoning Du 001; Yang Liu 003; Alwen Tiu (FM, 2015)

Formal Certification of Android Bytecode. - Hendra Gunadi; Alwen Tiu; Rajeev Goré (CoRR, 2015)

Completeness for a First-Order Abstract Separation Logic. - Zhe Hou; Alwen Tiu (APLAS, 2016)

SPEC: An Equivalence Checker for Security Protocols. - Alwen Tiu; Nam Nguyen; Ross Horne (APLAS, 2016)

Private Names in Non-Commutative Logic. - Ross Horne; Alwen Tiu; Bogdan Aman; Gabriel Ciobanu (CONCUR, 2016)

An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. - Zhe Hou; David Sanán; Alwen Tiu; Yang Liu 003; Koh Chuen Hoa (FM, 2016)

Separata: Isabelle tactics for Separation Algebra. - Zhe Hou; David Sanán; Alwen Tiu; Rajeev Goré; Ranald Clouston (Arch. Formal Proofs, 2016)

A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor. - Zhe Hou; David Sanán; Alwen Tiu; Yang Liu 003 (Arch. Formal Proofs, 2016)

Termination of Monotone Programs. - Omar I. Al-Bataineh; Xiaofei Xie; Alwen Tiu; Mark Reynolds 001 (CoRR, 2016)

Compositional Reasoning for Shared-variable Concurrent Programs. - Fuyuan Zhang; Yongwang Zhao; David Sanán; Yang Liu 003; Alwen Tiu; Shang-Wei Lin 001; Zhimin Wu; Jun Sun 001 (CoRR, 2016)

Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-Bounded Processes. - Emanuele D'Osualdo; Luke Ong; Alwen Tiu (CSF, 2017)

Proof Tactics for Assertions in Separation Logic. - Zhe Hou; David Sanán; Alwen Tiu; Yang Liu 003 (ITP, 2017)

VeriFormal: An Executable Formal Model of a Hardware Description Language. - Wilayat Khan; Alwen Tiu; David Sanán (SG-CRC, 2017)

Steelix: program-state based binary fuzzing. - Yuekang Li; Bihuan Chen 001; Mahinthan Chandramohan; Shang-Wei Lin 001; Yang Liu 003; Alwen Tiu (ESEC/SIGSOFT FSE, 2017)

CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. - David Sanán; Yongwang Zhao; Zhe Hou; Fuyuan Zhang; Alwen Tiu; Yang Liu 003 (TACAS (1), 2017)

A Characterisation of Open Bisimulation using an Intuitionistic Modal Logic. - Ki Yung Ahn; Ross Horne; Alwen Tiu (CoRR, 2017)

Generating Witness of Non-Bisimilarity for the pi-Calculus. - Ki Yung Ahn; Ross Horne; Alwen Tiu (CoRR, 2017)

Semantics for Specialising Attack Trees based on Linear Logic. - Ross Horne; Sjouke Mauw; Alwen Tiu (Fundam. Informaticae, 2017)

A Permission-Dependent Type System for Secure Information Flow Analysis. - Hongxu Chen 001; Alwen Tiu; Zhiwu Xu 001; Yang Liu 003 (CSF, 2018)

Compositional Reasoning for Shared-Variable Concurrent Programs. - Fuyuan Zhang; Yongwang Zhao; David Sanán; Yang Liu 003; Alwen Tiu; Shang-Wei Lin 001; Jun Sun 001 (FM, 2018)

The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement. - Ross Horne; Sjouke Mauw; Alwen Tiu (GraMSec@FLoC, 2018)

Quasi-Open Bisimilarity with Mismatch is Intuitionistic. - Ross Horne; Ki Yung Ahn; Shang-Wei Lin 001; Alwen Tiu (LICS, 2018)

A labelled sequent calculus for BBI: proof theory and proof search. - Zhe Hou; Rajeev Goré; Alwen Tiu (J. Log. Comput., 2018)

Modular Labelled Sequent Calculi for Abstract Separation Logics. - Zhe Hou; Ranald Clouston; Rajeev Goré; Alwen Tiu (ACM Trans. Comput. Log., 2018)

Combining ProVerif and Automated Theorem Provers for Security Protocol Verification. - Di Long Li; Alwen Tiu (CADE, 2019)

Private Digital Identity on Blockchain. - Tom Hamer; Kerry Taylor; Kee Siong Ng; Alwen Tiu (BlockSW/CKG@ISWC, 2019)

A formalisation of the SPARC TSO memory model for multi-core machine code. - Zhe Hou; David Sanán; Alwen Tiu; Yang Liu 003; Jin Song Dong (CoRR, 2019)

Display to Labelled Proofs and Back Again for Tense Logics. - Agata Ciabattoni; Tim S. Lyon; Revantha Ramanayake; Alwen Tiu (CoRR, 2019)

Constructing weak simulations from linear implications for processes with private names. - Ross Horne; Alwen Tiu (Math. Struct. Comput. Sci., 2019)

De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic. - Ross Horne; Alwen Tiu; Bogdan Aman; Gabriel Ciobanu (ACM Trans. Comput. Log., 2019)

Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. - Tim S. Lyon; Alwen Tiu; Rajeev Goré; Ranald Clouston (CSL, 2020)

On unlinkability and denial of service attacks resilience of whistleblower platforms. - Silivanxay Phetsouvanh; Anwitaman Datta; Alwen Tiu (Future Gener. Comput. Syst., 2021)

An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model. - Zhé Hóu; David Sanán; Alwen Tiu; Yang Liu 003; Koh Chuen Hoa; Jin Song Dong (J. Autom. Reason., 2021)

A permission-dependent type system for secure information flow analysis. - Zhiwu Xu 001; Hongxu Chen 001; Alwen Tiu; Yang Liu 003; Kunal Sareen (J. Comput. Secur., 2021)

A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. - Ki Yung Ahn; Ross Horne; Alwen Tiu (Log. Methods Comput. Sci., 2021)

Trace-Length Independent Runtime Monitoring of Quantitative Policies. - Xiaoning Du 001; Alwen Tiu; Kun Cheng; Yang Liu 003 (IEEE Trans. Dependable Secur. Comput., 2021)

Display to Labeled Proofs and Back Again for Tense Logics. - Agata Ciabattoni; Tim S. Lyon; Revantha Ramanayake; Alwen Tiu (ACM Trans. Comput. Log., 2021)

Is Eve nearby? Analysing protocols under the distant-attacker assumption. - Reynaldo Gil Pons; Ross Horne; Sjouke Mauw; Alwen Tiu; Rolando Trujillo-Rasua (CSF, 2022)

A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk). - Alwen Tiu (FSCD, 2022)

PFMC: A Parallel Symbolic Model Checker for Security Protocol Verification. - Alex James; Alwen Tiu; Nisansala Yatapanage (ICFEM, 2022)

Dagster: Parallel Structured Search with Case Studies. - Mark Alexander Burgess; Charles Gretton; Josh Milthorpe; Luke Croak; Thomas Willingham; Alwen Tiu (PRICAI (1), 2022)

An Executable Formal Model of the VHDL in Isabelle/HOL. - Wilayat Khan; Zhe Hou; David Sanán; Jamel Nebhen; Yang Liu 003; Alwen Tiu (CoRR, 2022)

Privacy Analysis of Samsung's Crowd-Sourced Bluetooth Location Tracking System. - Tingfeng Yu; James Henderson; Alwen Tiu; Thomas Haines (CoRR, 2022)

Dagster: Parallel Structured Search. - Mark Alexander Burgess; Charles Gretton; Josh Milthorpe; Luke Croak; Thomas Willingham; Alwen Tiu (AAAI, 2023)

Modal Logics for Mobile Processes Revisited. - Tiange Liu; Alwen Tiu; Jim de Groot (CONCUR, 2023)

Security and Privacy Analysis of Samsung's Crowd-Sourced Bluetooth Location Tracking System. - Tingfeng Yu; James Henderson; Alwen Tiu; Thomas Haines (USENIX Security Symposium, 2024)

Tamgram: A Frontend for Large-scale Protocol Modeling in Tamarin. - Di Long Li; Jim de Groot; Alwen Tiu (CoRR, 2024)

Open Bisimilarity for the π-Calculus with Mismatch. - Tiange Liu; Alwen Tiu; Ross Horne (CONCUR, 2025)

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents. - Tim S. Lyon; Ian Shillito; Alwen Tiu (CSL, 2025)