Alwen Tiu - RankMe

112 papers A* 4A 8B 25C 3Journal 58Unranked 13

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Security Analysis of CheriBSD and Morello Linux. CoRR Dariy Guzairov, Alex Potanin, Stephen Kell, Alwen Tiu
2025	B	`conf`	Open Bisimilarity for the π-Calculus with Mismatch. CONCUR Tiange Liu, Alwen Tiu, Ross Horne
2025	B	`conf`	Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents. CSL Tim S. Lyon, Ian Shillito, Alwen Tiu
2024	A*	`conf`	Security and Privacy Analysis of Samsung's Crowd-Sourced Bluetooth Location Tracking System. USENIX Security Symposium Tingfeng Yu, James Henderson, Alwen Tiu, Thomas Haines
2024	J	`jnl`	Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents. CoRR Tim S. Lyon, Ian Shillito, Alwen Tiu
2024	J	`jnl`	Tamgram: A Frontend for Large-scale Protocol Modeling in Tamarin. CoRR Di Long Li, Jim de Groot, Alwen Tiu
2023	A*	`conf`	Dagster: Parallel Structured Search. AAAI Mark Alexander Burgess, Charles Gretton, Josh Milthorpe, Luke Croak, Thomas Willingham, Alwen Tiu
2023	B	`conf`	Modal Logics for Mobile Processes Revisited. CONCUR Tiange Liu, Alwen Tiu, Jim de Groot
2022	B	`conf`	A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk). FSCD Alwen Tiu
2022	J	`jnl`	An Executable Formal Model of the VHDL in Isabelle/HOL. CoRR Wilayat Khan, Zhe Hou, David Sanán, Jamel Nebhen, Yang Liu, Alwen Tiu
2022	—	`conf`	Dagster: Parallel Structured Search with Case Studies. PRICAI (1) Mark Alexander Burgess, Charles Gretton, Josh Milthorpe, Luke Croak, Thomas Willingham, Alwen Tiu
2022	A	`conf`	Is Eve nearby? Analysing protocols under the distant-attacker assumption. CSF Reynaldo Gil Pons, Ross Horne, Sjouke Mauw, Alwen Tiu, Rolando Trujillo-Rasua
2022	C	`conf`	PFMC: A Parallel Symbolic Model Checker for Security Protocol Verification. ICFEM Alex James, Alwen Tiu, Nisansala Yatapanage
2022	J	`jnl`	PFMC: a parallel symbolic model checker for security protocol verification. CoRR Alex James, Alwen Tiu, Nisansala Yatapanage
2022	J	`jnl`	Privacy Analysis of Samsung's Crowd-Sourced Bluetooth Location Tracking System. CoRR Tingfeng Yu, James Henderson, Alwen Tiu, Thomas Haines
2021	J	`jnl`	A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. Log. Methods Comput. Sci. Ki Yung Ahn, Ross Horne, Alwen Tiu
2021	J	`jnl`	A permission-dependent type system for secure information flow analysis. J. Comput. Secur. Zhiwu Xu, Hongxu Chen, Alwen Tiu, Yang Liu, Kunal Sareen
2021	J	`jnl`	An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model. J. Autom. Reason. Zhé Hóu, David Sanán, Alwen Tiu, Yang Liu, Koh Chuen Hoa, Jin Song Dong
2021	J	`jnl`	Display to Labeled Proofs and Back Again for Tense Logics. ACM Trans. Comput. Log. Agata Ciabattoni, Tim S. Lyon, Revantha Ramanayake, Alwen Tiu
2021	J	`jnl`	On unlinkability and denial of service attacks resilience of whistleblower platforms. Future Gener. Comput. Syst. Silivanxay Phetsouvanh, Anwitaman Datta, Alwen Tiu
2021	—	`ed.`	Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020. LFMTP Claudio Sacerdoti Coen, Alwen Tiu
2021	J	`jnl`	Trace-Length Independent Runtime Monitoring of Quantitative Policies. IEEE Trans. Dependable Secur. Comput. Xiaoning Du, Alwen Tiu, Kun Cheng, Yang Liu
2020	B	`conf`	Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. CSL Tim S. Lyon, Alwen Tiu, Rajeev Goré, Ranald Clouston
2019	J	`jnl`	A formalisation of the SPARC TSO memory model for multi-core machine code. CoRR Zhe Hou, David Sanán, Alwen Tiu, Yang Liu, Jin Song Dong
2019	A	`conf`	Combining ProVerif and Automated Theorem Provers for Security Protocol Verification. CADE Di Long Li, Alwen Tiu
2019	J	`jnl`	Constructing weak simulations from linear implications for processes with private names. Math. Struct. Comput. Sci. Ross Horne, Alwen Tiu
2019	J	`jnl`	De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic. ACM Trans. Comput. Log. Ross Horne, Alwen Tiu, Bogdan Aman, Gabriel Ciobanu
2019	J	`jnl`	Display to Labelled Proofs and Back Again for Tense Logics. CoRR Agata Ciabattoni, Tim S. Lyon, Revantha Ramanayake, Alwen Tiu
2019	—	`conf`	Private Digital Identity on Blockchain. BlockSW/CKG@ISWC Tom Hamer, Kerry Taylor, Kee Siong Ng, Alwen Tiu
2019	J	`jnl`	Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. CoRR Tim S. Lyon, Alwen Tiu, Rajeev Goré, Ranald Clouston
2018	A	`conf`	A Permission-Dependent Type System for Secure Information Flow Analysis. CSF Hongxu Chen, Alwen Tiu, Zhiwu Xu, Yang Liu
2018	J	`jnl`	A labelled sequent calculus for BBI: proof theory and proof search. J. Log. Comput. Zhe Hou, Rajeev Goré, Alwen Tiu
2018	B	`conf`	Compositional Reasoning for Shared-Variable Concurrent Programs. FM Fuyuan Zhang, Yongwang Zhao, David Sanán, Yang Liu, Alwen Tiu, Shang-Wei Lin, Jun Sun
2018	J	`jnl`	Modular Labelled Sequent Calculi for Abstract Separation Logics. ACM Trans. Comput. Log. Zhe Hou, Ranald Clouston, Rajeev Goré, Alwen Tiu
2018	A*	`conf`	Quasi-Open Bisimilarity with Mismatch is Intuitionistic. LICS Ross Horne, Ki Yung Ahn, Shang-Wei Lin, Alwen Tiu
2018	—	`conf`	The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement. GraMSec Ross Horne, Sjouke Mauw, Alwen Tiu
2017	B	`conf`	A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. CONCUR Ki Yung Ahn, Ross Horne, Alwen Tiu
2017	J	`jnl`	A Characterisation of Open Bisimulation using an Intuitionistic Modal Logic. CoRR Ki Yung Ahn, Ross Horne, Alwen Tiu
2017	J	`jnl`	A Permission-Dependent Type System for Secure Information Flow Analysis. CoRR Hongxu Chen, Alwen Tiu, Zhiwu Xu, Yang Liu
2017	—	`conf`	CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. TACAS (1) David Sanán, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu
2017	A	`conf`	Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-Bounded Processes. CSF Emanuele D'Osualdo, Luke Ong, Alwen Tiu
2017	J	`jnl`	Generating Witness of Non-Bisimilarity for the pi-Calculus. CoRR Ki Yung Ahn, Ross Horne, Alwen Tiu
2017	J	`jnl`	Modular Labelled Sequent Calculi for Abstract Separation Logics. CoRR Zhe Hou, Ranald Clouston, Rajeev Goré, Alwen Tiu
2017	B	`conf`	Proof Tactics for Assertions in Separation Logic. ITP Zhe Hou, David Sanán, Alwen Tiu, Yang Liu
2017	J	`jnl`	Semantics for Specialising Attack Trees based on Linear Logic. Fundam. Informaticae Ross Horne, Sjouke Mauw, Alwen Tiu
2017	—	`conf`	Steelix: program-state based binary fuzzing. ESEC/SIGSOFT FSE Yuekang Li, Bihuan Chen, Mahinthan Chandramohan, Shang-Wei Lin, Yang Liu, Alwen Tiu
2017	—	`conf`	VeriFormal: An Executable Formal Model of a Hardware Description Language. SG-CRC Wilayat Khan, Alwen Tiu, David Sanán
2016	J	`jnl`	A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor. Arch. Formal Proofs Zhe Hou, David Sanán, Alwen Tiu, Yang Liu
2016	B	`conf`	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. FM Zhe Hou, David Sanán, Alwen Tiu, Yang Liu, Koh Chuen Hoa
2016	B	`conf`	Completeness for a First-Order Abstract Separation Logic. APLAS Zhe Hou, Alwen Tiu
2016	J	`jnl`	Completeness for a First-order Abstract Separation Logic. CoRR Zhe Hou, Alwen Tiu
2016	J	`jnl`	Compositional Reasoning for Shared-variable Concurrent Programs. CoRR Fuyuan Zhang, Yongwang Zhao, David Sanán, Yang Liu, Alwen Tiu, Shang-Wei Lin, Zhimin Wu, Jun Sun
2016	B	`conf`	Private Names in Non-Commutative Logic. CONCUR Ross Horne, Alwen Tiu, Bogdan Aman, Gabriel Ciobanu
2016	J	`jnl`	Private Names in Non-Commutative Logic. CoRR Ross Horne, Alwen Tiu, Bogdan Aman, Gabriel Ciobanu
2016	B	`conf`	SPEC: An Equivalence Checker for Security Protocols. APLAS Alwen Tiu, Nam Nguyen, Ross Horne
2016	J	`jnl`	Separata: Isabelle tactics for Separation Algebra. Arch. Formal Proofs Zhe Hou, David Sanán, Alwen Tiu, Rajeev Goré, Ranald Clouston
2016	J	`jnl`	Termination of Monotone Programs. CoRR Omar I. Al-Bataineh, Xiaofei Xie, Alwen Tiu, Mark Reynolds
2015	A	`conf`	Automated Theorem Proving for Assertions in Separation Logic with All Connectives. CADE Zhe Hou, Rajeev Goré, Alwen Tiu
2015	J	`jnl`	Formal Certification of Android Bytecode. CoRR Hendra Gunadi, Alwen Tiu, Rajeev Goré
2015	B	`ed.`	Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015 CPP Xavier Leroy, Alwen Tiu
2015	B	`conf`	Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL. FM Xiaoning Du, Yang Liu, Alwen Tiu
2014	J	`jnl`	Abella: A System for Reasoning about Relational Specifications. J. Formaliz. Reason. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang
2014	B	`conf`	Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System. FM Hendra Gunadi, Alwen Tiu
2014	—	`conf`	From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic. IFIP TCS Jeremy E. Dawson, Ranald Clouston, Rajeev Goré, Alwen Tiu
2014	A*	`conf`	Proof search for propositional abstract separation logics via labelled sequents. POPL Zhe Hou, Ranald Clouston, Rajeev Goré, Alwen Tiu
2013	J	`jnl`	A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search CoRR Zhe Hou, Alwen Tiu, Rajeev Goré
2013	B	`conf`	A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search. TABLEAUX Zhe Hou, Alwen Tiu, Rajeev Goré
2013	J	`jnl`	Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic - Extended Version. CoRR Ranald Clouston, Jeremy E. Dawson, Rajeev Goré, Alwen Tiu
2013	B	`conf`	Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. CSL Ranald Clouston, Jeremy E. Dawson, Rajeev Goré, Alwen Tiu
2013	J	`jnl`	Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System. CoRR Hendra Gunadi, Alwen Tiu
2013	B	`conf`	Extracting Proofs from Tabled Proof Search. CPP Dale Miller, Alwen Tiu
2013	J	`jnl`	Proof search for propositional abstract separation logics via labelled sequents. CoRR Zhe Hou, Ranald Clouston, Rajeev Goré, Alwen Tiu
2012	J	`jnl`	Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus CoRR Yuxin Deng, Alwen Tiu
2012	J	`jnl`	Characterisations of testing preorders for a finite probabilistic π-calculus. Formal Aspects Comput. Yuxin Deng, Alwen Tiu
2012	J	`jnl`	Cut elimination for a logic with induction and co-induction. J. Appl. Log. Alwen Tiu, Alberto Momigliano
2012	J	`jnl`	Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures CoRR Alwen Tiu, Egor Ianovski, Rajeev Goré
2012	B	`conf`	Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures. Advances in Modal Logic Alwen Tiu, Egor Ianovski, Rajeev Goré
2012	A	`conf`	Stratification in Logics of Definitions. IJCAR Alwen Tiu
2011	B	`conf`	A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains. TABLEAUX Alwen Tiu
2011	J	`jnl`	On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics Log. Methods Comput. Sci. Rajeev Goré, Linda Postniece, Alwen Tiu
2011	—	`conf`	On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics. TABLEAUX (Workshops, Tutorials, and Short Papers) Alwen Tiu
2010	J	`jnl`	A Proof Theoretic Analysis of Intruder Theories Log. Methods Comput. Sci. Alwen Tiu, Rajeev Goré, Jeremy E. Dawson
2010	A	`conf`	Automating Open Bisimulation Checking for the Spi Calculus. CSF Alwen Tiu, Jeremy E. Dawson
2010	J	`jnl`	Cut Elimination for a Logic with Induction and Co-induction CoRR Alwen Tiu, Alberto Momigliano
2010	J	`jnl`	Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic CoRR Rajeev Goré, Linda Postniece, Alwen Tiu
2010	B	`conf`	Cut-elimination and Proof Search for Bi-Intuitionistic Tense Logic. Advances in Modal Logic Rajeev Goré, Linda Postniece, Alwen Tiu
2010	J	`jnl`	Proof search specifications of bisimulation and modal logics for the pi-calculus. ACM Trans. Comput. Log. Alwen Tiu, Dale Miller
2009	C	`conf`	A First-Order Policy Language for History-Based Transaction Monitoring. ICTAC Andreas Bauer, Rajeev Goré, Alwen Tiu
2009	—	`conf`	A Proof Theoretic Analysis of Intruder Theories. RTA Alwen Tiu, Rajeev Goré
2009	J	`jnl`	A Trace Based Bisimulation for the Spi Calculus CoRR Alwen Tiu
2009	J	`jnl`	A decidable policy language for history-based transaction monitoring CoRR Andreas Bauer, Rajeev Goré, Alwen Tiu
2009	—	`conf`	Formalising Observer Theory for Environment-Sensitive Bisimulation. TPHOLs Jeremy E. Dawson, Alwen Tiu
2009	C	`conf`	Matching Trace Patterns with Regular Policies. LATA Franz Baader, Andreas Bauer, Alwen Tiu
2009	B	`conf`	Taming Displayed Tense Logics Using Nested Sequents with Deep Inference. TABLEAUX Rajeev Goré, Linda Postniece, Alwen Tiu
2008	J	`jnl`	A proof theoretic analysis of intruder theories CoRR Alwen Tiu, Rajeev Goré
2008	J	`jnl`	Cut Elimination for a Logic with Generic Judgments and Induction CoRR Alwen Tiu
2008	B	`conf`	Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. Advances in Modal Logic Rajeev Goré, Linda Postniece, Alwen Tiu
2008	J	`jnl`	Induction and Co-induction in Sequent Calculus CoRR Alwen Tiu, Alberto Momigliano
2008	—	`conf`	Matching linear and non-linear trace patterns with regular policies. UNIF Franz Baader, Andreas Bauer, Alwen Tiu
2008	—	`conf`	On the Role of Names in Reasoning about lambda-tree Syntax Specifications. LFMTP@LICS Alwen Tiu
2008	J	`jnl`	Proof Search Specifications for Bisimulation and Modal Logics for the pi-Calculus CoRR Alwen Tiu, Dale Miller
2007	B	`conf`	A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract. APLAS Alwen Tiu
2007	J	`jnl`	Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5. J. Log. Comput. Rajeev Goré, Alwen Tiu
2007	A	`conf`	The Bedwyr System for Model Checking over Syntactic Expressions. CADE David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
2007	J	`jnl`	The Bedwyr system for model checking over syntactic expressions CoRR David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
2007	J	`jnl`	Verification of clock synchronization algorithms: experiments on a combination of deductive tools. Formal Aspects Comput. Damián Barsotti, Leonor Prensa Nieto, Alwen Tiu
2006	B	`conf`	A Local System for Intuitionistic Logic. LPAR Alwen Tiu
2006	—	`conf`	A Logic for Reasoning about Generic Judgments. LFMTP@FLoC Alwen Tiu
2006	J	`jnl`	A System of Interaction and Structure II: The Need for Deep Inference. Log. Methods Comput. Sci. Alwen Tiu
2005	J	`jnl`	A System of Interaction and Structure II: The Need for Deep Inference CoRR Alwen Tiu
2005	J	`jnl`	A proof theory for generic judgments. ACM Trans. Comput. Log. Dale Miller, Alwen Tiu
2005	J	`jnl`	Formalization of a Generalized Protocol for Clock Synchronization. Arch. Formal Proofs Alwen Tiu