Dr Alwen Tiu
Associate Professor
ANU College of Engineering, Computing and Cybernetics
T:
02 6125 3666
Areas of expertise
- Computer System Security 080303
- Computational Logic And Formal Languages 080203
- Computation Theory And Mathematics 0802
- Programming Languages 080308
- Computer Software 0803
Biography
Research interests:
My main interests are in logic, proof theory and process algebra, and their applications in computer science, in particular, in specifying and reasoning about models of computation and programming languages. I have recently taken interest in modeling security protocols in process algebra, using extensions of the pi-calculus, and in reasoning about such specifications using proof theoretic techniques. Other related areas of interest include theorem proving, logic programming, type theory, and formal verification of algorithms.
Bio:
I obtained my PhD degree from the Pennsylvania State University in 2004. I spent about a year as a visiting student at Ecole Polytechnique (France) during my PhD. I did a one-year postdoc at LORIA/INRIA Lorraine (2004 - 2005), prior to joining the ANU in 2006.
Duties:
I am a Fellow (senior researcher) in the Logic and Computation group in the School of Computer Science.
My main interests are in logic, proof theory and process algebra, and their applications in computer science, in particular, in specifying and reasoning about models of computation and programming languages. I have recently taken interest in modeling security protocols in process algebra, using extensions of the pi-calculus, and in reasoning about such specifications using proof theoretic techniques. Other related areas of interest include theorem proving, logic programming, type theory, and formal verification of algorithms.
Bio:
I obtained my PhD degree from the Pennsylvania State University in 2004. I spent about a year as a visiting student at Ecole Polytechnique (France) during my PhD. I did a one-year postdoc at LORIA/INRIA Lorraine (2004 - 2005), prior to joining the ANU in 2006.
Duties:
I am a Fellow (senior researcher) in the Logic and Computation group in the School of Computer Science.
Publications
- Ahn, K, Horne, R & Tiu, A 2021, 'A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic', Logical Methods in Computer Science, vol. 17, no. 3, pp. 1-40.
- Ramanayake, D, Tiu, A, Ciabattoni, A et al. 2021, 'Display to Labeled Proofs and Back Again for Tense Logics', ACM Transactions on Computational Logic, vol. 22, no. 3.
- Phetsouvanh, S, Datta, A & Tiu, A 2021, 'On unlinkability and denial of service attacks resilience of whistleblower platforms', Future Generation Computer Systems, vol. 118, pp. 438-452.
- Du, X, Tiu, A, Cheng, K et al. 2019, 'Trace-Length Independent Runtime Monitoring of Quantitative Policies', IEEE Transactions on Dependable and Secure Computing, vol. 18, no. 3, pp. 1489 - 1510.
- Hou, Z, Sanan, D, Tiu, A et al. 2021, 'An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model', Journal of Automated Reasoning, vol. 65, no. 4, pp. 569-598.
- Broad, E, Sheel, M, Lazar, S et al. 2020, Starting With SOAP: rapid deployment of contract tracing in a pandemic.
- Lyon, T, Tiu, A, Gore, R et al. 2020, 'Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents', 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, ed. M Fernandez, A Muscholl, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, pp. 1-16.
- Hamer, T, Taylor, K, Ng, K et al. 2019, 'Private digital identity on blockchain', 2019 Blockchain Enabled Semantic Web Workshop and Contextualized Knowledge Graphs Workshop, BlockSW-CKG 2019, CEUR-WS.ORG, United States, pp. 1-7.
- Horne, R, Mauw, S & Tiu, A 2019, 'The attacker does not always hold the initiative: Attack trees with external refinement', 5th International Workshop on Graphical Models for Security, GraMSec 2018, ed. George Cybenko, David Pym & Barbara Fila, Springer Nature, Switzerland, pp. 90-110.
- Horne, R & Tiu, A 2019, 'Constructing weak simulations from linear implications for processes with private names', Mathematical Structures in Computer Science, vol. 29, no. 8, pp. 1275-1308.
- Horne, R, Tiu, A, Aman, B et al. 2019, 'De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic', ACM Transactions on Computational Logic, vol. 20, no. 4., pp. 22:1-22:44.
- Li, D & Tiu, A 2019, 'Combining proverif and automated theorem provers for security protocol verification', International Conference on Automated Deduction, ed. Pascal Fontaine, Springer Link, London, pp. 354-365.
- Zhang, F, Zhao, Y, Sanan, D et al. 2018, 'Compositional reasoning for shared-variable concurrent programs', 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018, ed. Havelund K.Roscoe B., Springer Verlag, Switzerland, pp. 523-541.
- Horne, R, Ahn, K, Lin, S et al. 2018, 'Quasi-Open Bisimilarity with Mismatch is Intuitionistic', 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, ACM, TBC, pp. 26-35.
- Chen, H, Tiu, A, Xu, Z et al 2018, 'A permission-dependent type system for secure information flow analysis', 31st IEEE Computer Security Foundations Symposium, CSF 2018, IEEE, USA, pp. 218-232pp.
- Hou, Z, Clouston, R, Gore, R et al. 2018, 'Modular Labelled Sequent Calculi for Abstract Separation Logics', ACM Transactions on Computational Logic, vol. 19, no. 2, pp. 1-35pp.
- Hou, Z, Clouston, R, Gore, R et al 2014, 'Proof Search for Propositional Abstract Separation Logics via Labelled Sequents', 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2014, Association for Computing Machinery (ACM), San Diego, CA, pp. 465-476.
- Miller, D & Tiu, A 2013, 'Extracting proofs from tabled proof search', 3rd International Conference on Certified Programs and Proofs, CPP 2013, Conference Organising Committee, Melbourne, VIC, pp. 194-210.
- Clouston, R, Dawson, J, Gore, R, et al 2013, 'Annotation-Free Sequent Calculi for full Intuitionistic Linear Logic - Extended Version', Logical Methods in Computer Science, vol. Online (published dates tbc), pp. 1-18.
- Hou, Z, Tiu, A & Gore, 2013,'A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search', TABLEAUX 2013, ed. D. Galmiche and D. Larchey-Wendling, Springer-Verlag Berlin Heidelberg, USA, pp. 172-187.
- Tiu, A 2012, 'Stratification in Logics of Definitions', Lecture Notes in Computer Science (LNCS), pp. 544-558.
- Tiu, A & Momigliano, A 2012, 'Cut elimination for a logic with induction and co-induction', Journal of Applied Logic, vol. 10, no. 4, pp. 330-367.
- Deng, Y & Tiu, A 2012, 'Characterisations of testing preorders for a finite probabilistic pi-calculus', Formal Aspects of Computing, vol. 24, no. 4-Jun, pp. 701-726.
- Tiu, A, Ianovski, E & Gore, R 2012, 'Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures', Advances in Modal Logic (AiML 2012), College Publications, Kings College London, pp. 1-22.
- Gore, R, Postniece, L & Tiu, A 2011, 'On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics', Logical Methods in Computer Science, vol. 7, no. 2, p. 38.
- Tiu, A 2011, 'A Hypersequent System for Godel-Dummett Logic with Non-constant Domains', International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2011), ed. Kai Brünnler, George Metcalfe, Springer, Berlin Germany, p. 15.
- Gore, R, Postniece, L & Tiu, A 2010, 'Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic', Advances in Modal Logic (AiML 2010), ed. Lev Beklemishev et al, College Publications, , pp. 156-177.
- Tiu, A & Dawson, J 2010, 'Automating Open Bisimulation Checking for the Spi Calculus', IEEE Computer Security Foundations Symposium 2010, IEEE Computer Society, pp. 307 - 321.
- Tiu, A & Miller, D 2010, 'Proof search specifications of bisimulation and modal logics for the n-calculus', ACM Transactions on Computational Logic, vol. 11, no. 2, p. 37.
- Tiu, A, Gore, R & Dawson, J 2010, 'A Proof Theoretic Analysis of Intruder Theories', Logical Methods in Computer Science, vol. 6, no. 3, pp. 1-37.
- Dawson, J & Tiu, A 2009, 'Formalising Observer Theory for Environment-Sensitive Bisimulation', in S. Berghofer, S Nipkow, C Urban, M Wenzel (ed.), Theorem Proving in Higher Order Logics (TPHOLs), Springer, Berlin, pp. 180-195.
- Tiu, A & Gore, R 2009, 'A Proof Theoretic Analysis of Intruder Theories', International conference on Rewriting Techniques and Applications (RTA 2009), ed. Ralf Treinen, Springer, Brasilia, Brazil, pp. 103-117.
- Gore, R, Postniece, L & Tiu, A 2009, 'Taming displayed tense logics using nested sequents with deep inference', International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2009), ed. Conference Program Committee, Springer, Oslo, Norway, pp. 189-204.
- Bauer, A, Gore, R & Tiu, A 2009, 'A first-order policy language for history-based transaction monitoring', International Colloquium on Theoretical Aspects of Computing (ICTAC 2009), ed. Martin Leucker, Charles C. Morgan, Springer, Berlin, Germany, pp. 96-111.
- Baader, F, Bauer, A & Tiu, A 2009, 'Matching trace patterns with regular policies', in A.H. Dediu, A.M. Ionescu, C. Martin-Vide (ed.), Language and Automata Theory and Applications, Springer, Germany, pp. 105-116.
- Tiu, A 2009, 'On the role of names in reasoning about lambda-tree syntax specifications', Electronic Notes in Theoretical Computer Science, vol. 228, pp. 135-150.
- Gore, R, Postniece, L & Tiu, A 2008, 'Cut-elimination and proof-search for bi-intutionistic logic using nested sequents', Advances in Modal Logic (AiML 2008), ed. Carlos Areces and Robert Goldblatt, College Publications, United Kingdom, pp. 43-66.
- Baader, F, Bauer, A & Tiu, A 2008, 'Matching linear and non-linear trace patterns with regular policies', International Workshop on Unification (UNIF 2008), ed. Mircea Marin, Conference Organising Committee, Linz, Austria, pp. 16-24.
- Tiu, A 2007, 'A trace based bisimulation for the spi calculus', ASIAN Symposium on Programming Languages and Systems (APLAS 2007), ed. Shao Zhong, Springer, New York, pp. 367-382.
- Gore, R & Tiu, A 2007, 'Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5', Journal of Logic and Computation, vol. 17, no. 4, pp. 767-794.
- Tiu, A 2007, 'A logic for reasoning about generic judgments', Electronic Notes in Theoretical Computer Science, vol. 174, no. 5, pp. 3-18.
- Barsotti, D, Prensa-Nieto, L & Tiu, A 2007, 'Verification of clock synchronization algorithms: Experiments on a combination of deductive tools', Formal Aspects of Computing, vol. 19, no. 3, pp. 321-341.
- Baelde, D, Gacek, A, Miller, D et al 2007, 'The Bedwyr system for model checking over syntactic expressions', International Conference on Automated Deduction (CADE 2007), ed. Frank Pfenning, Springer, New York, pp. 391-397.
- Fontaine, P, Marion, J, Merz, S et al 2006, 'Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants', International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, ed. Holger Hermanns, Jens Palsberg, Springer, United States, pp. 167-181.
- Tiu, A 2006, 'A local system for intuitionistic logic', International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2006), ed. Miki Hermann, Andrei Voronkov, Springer, New York, pp. 242-256.
- Tiu, A 2006, 'A system of interaction and structure II: The need for deep inference', Logical Methods in Computer Science, vol. 2, no. 4, pp. 1-24.
- Miller, D & Tiu, A 2005, 'A proof theory for generic judgments', ACM Transactions on Computational Logic, vol. 6, no. 4, pp. 749-783.
- Barsotti, D, Prensa-Nieto, L & Tiu, A 2005, 'Verification of clock synchronisation algorithms: Experiments on a combination of deductive tools', International Workshop on Automated Verfication of Critical Systems (AVoCS 2005), ed. R Lazic and R Nagarajan, Elsevier, Netherlands, pp. 63-78.
- Tiu, A 2005, 'Model checking for pi-calculus using proof search', International Conference on Concurrency Theory (CONCUR 2005), ed. Martin Abadi and Luca de Alfaro, Springer, New York, pp. 36-50.
- Tiu, A & Miller, D 2005, 'A Proof Search Specification of the Ï?-Calculus', Electronic Notes in Theoretical Computer Science, vol. 138, no. 1, pp. 79-101.
- Momigliano, A & Tiu, A 2003, 'Induction and Co-induction in Sequent Calculus', International Workshop on Types for Proofs and Programs (TYPES 2003), ed. S. Berardi, M. Coppo, and F. Damiani (Eds.), Springer, Berlin, Heidelberg, pp. 293-308.
Projects and Grants
Grants information is drawn from ARIES. To add or update Projects or Grants information please contact your College Research Office.
- Cybersecurity Skills and Technology Accelerator - Fifth Domain/Austcyber (Primary Investigator)
- Experiment in the application of FMME techniques for scaling up assurance efforts by enhancing popular proof tools via the use of theory morphisms between sessions (Primary Investigator)
- Proof Theoretical Methods for Reasoning about Process Equivalence (Primary Investigator)
