Alwen Tiu | Home

Publications

This list is outdated. See my DBLP page for the latest publication list.

Refereed journal and conference/workshop proceedings

2016

Ross Horne, Alwen Tiu, Bogdan Aman, Gabriel Ciobanu. Private names in non-commutative logic. CONCUR 2016. Extended version of the paper available at arxiv.

Zhe Hou, David Sanan, Alwen Tiu, Yang Liu, Koh Chuen Hoa. An executable formalisation of the SPARCv8 instruction set architecture: a case study for the LEON3 processor. FM 2016. Isabelle/HOL formalization.

Zhe Hou, Alwen Tiu. Completeness for a first-order abstract separation logic. APLAS 2016.

Alwen Tiu, Nguyen Thanh Nam, Ross Horne. SPEC: an equivalence checker for security protocols. APLAS 2016.

2015

Zhe Hou, Rajeev Gore, Alwen Tiu. Automated Theorem Proving in Separation Logic with All Connectives. CADE 2015.

Xiaoning Du, Yang Liu, Alwen Tiu. Trace-length independence runtime monitoring of quantitative policies in LTL. FM 2015.

2014

Hendra Gunadi and Alwen Tiu. Efficient runtime monitoring with metric temporal logic: a case study in the Android operating system. Accepted to FM 2014. The source code for the monitor generator and the kernel images for the customized Android with LTL-based monitors are available from Hendra's webpage.

Proof search for propositional abstract separation logic via labelleds equents. Joint work with Ranald Clouston, Zhe Hou and Rajeev Gore. Accepted to POPL 2014.

2013

Extracting proofs from tabled proof search. Joint work with Dale Miller. Accepted to Certified Proofs and Programs 2013.

Annotation-free sequent calculi for full intuitionistic linear logic. Joint work with Ranald Clouston, Jeremy Dawson and Rajeev Gore. Accepted to CSL 2013.

A labelled sequent calculus for BBI: proof theory and proof search. Joint work with Zhe Hou and Rajeev Gore. Accepted to TABLEAUX 2013.

2012

Cut elimination for a logic with induction and co-induction. Joint work with Alberto Momigliano. 2012. Journal of Applied Logic, Vol. 10(4), pages 330-367, 2012.

Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus. Joint work with Yuxin Deng. Formal Aspects of Computing, Vol. 24(4-6), pages 701-726, 2012.

Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Proceduresi. Joint work with Egor Ianovski and Rajeev Gore. Accepted to AiML 2012.

Stratification in logics of definitions. Accepted to IJCAR 2012. See also the extended version, and formalisations of some examples (in Abella): odd.thm and logic.thm.

2011

On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Joint work with Rajeev Gore and Linda Postniece. Logical Methods in Computer Science, Vol. 7 (2:8), 2011.

A hypersequent system for Goedel-Dummett logic. In the Proceedings of TABLEAUX 2011, LNCS Vol. 6793, Springer, 2011.

2010

A proof theoretic analysis of intruder theories. Joint work with Rajeev Gore and Jeremy Dawson. Logical Methods in Computer Science, Vol. 6, Issue 3.

Automating open bisimulation checking for the spi-calculus. Joint work with Jeremy Dawson. In the proceedings of Computer Security Foundations (CSF) 2010. See also the errata for the conference proceedings version.

Cut elimination and proof search for bi-intuitionistic tense logic. Joint work with Rajeev Gore and Linda Postniece. To appear in the proceedings of Advances in Modal Logic (AiML) 2010. See also the extended version.

Proof search specifications of bisimulation and modal logics for the pi-calculus. Joint work with Dale Miller. ACM Transactions on Computational Logic, vol. 11, issue 2, article no. 13, 2010. (pdf, arXiv)
A formalisation of the finite pi-calculus and bisimulation in the paper, together with verification of an example of bisimilar processes has been done in the Abella proof assistant. The proof scripts (developed jointly by Andrew Gacek, Dale Miller and myself) can be found here.

Errata: There is a gap in the proof of Lemma 47 (Appendix D in the Arxiv version). In the last paragraph in the proof, there is another case that is not covered, i.e., when Qm nabla y. Q_i |= A_i but it is not the case that Qm nabla y. P' |= A_i. Thanks to Sam Staton who pointed out this gap. A consequence of this is that the correctness of Lemma 47 remains unknown at this stage, and so does the correctness of Theorem 26 (the half that concerns the completeness of the logical characterisation of open bisimulation).

2009

A first-order policy language for history-based transaction monitoring. Joint work with Andreas Bauer and Rajeev Gore. Accepted to ICTAC 2009.

Formalising observer theory for environment-sensitive bisimulation. Joint work with Jeremy Dawson. Accepted to TPHOLs 2009.

Taming displayed tense logics using nested sequents with deep inference. Joint work with Linda Postniece and Rajeev Gore. Accepted to TABLEAUX 2009.

A proof theoretic analysis of intruder theories. Joint work with Rajeev Gore. Accepted to RTA 2009. See also the extended version.

Matching trace patterns with regular policies. Joint work with Franz Baader and Andreas Bauer. To appear in the proceedings of the 3rd international conference on Language and Automata Theory and Applications (LATA 2009).

2008

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. Joint work with Rajeev Gore and Linda Postniece. Accepted to AiML 2008.

On the role of names in reasoning about lamda-tree syntax specifications. May 2008. To appear in the proceedings of LFMTP 2008. Some of the proofs are verified using the proof assistant Abella. Here is the proof script.

2007

Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5. Joint work with Rajeev Gore. Journal of Logic and Computation, volume 17, number 4, pages 767 - 794, 2007.

A trace based bisimulation for the spi-calculus: an extended abstract. In Proceedings of APLAS 2007, LNCS 4807, pages 367 - 382, 2007. © Copyright Springer-Verlag.

Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools. Joint work with Damian Barsotti and Leonor Prensa Nieto. Formal Aspects of Computing, volume 19, number 3, Springer, 2007. © Copyright Springer-Verlag.

The Bedwyr system for model checking over syntactic expressions. Joint work with David Baelde, Andrew Gacek, Dale Miller and Gopalan Nadathur. In Proceedings of CADE 2007, LNAI 4603, pages 391-397. Springer, 2007. © Copyright Springer-Verlag.

A Logic for Reasoning about Generic Judgments. In Proceedings of LFMTP'06, volume 174, issue 5, ENTCS, pages 3 - 18, Elsevier, 2007. This is a revised version of the article in the proceedings. The original article contains a mistake in one of the examples. An extended version is available.

2006

A Local System for Intuitionistic Logic. In Proceedings of LPAR 2006, Volume 4246 of LNCS, Springer, 2006. © Copyright Springer-Verlag. An extended version is available.

A System of Interaction and Structure II: the Need for Deep Inference. Logical Methods in Computer Science, Vol. 2 (2:4) 2006, pages 1-24, April 2006.

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. Joint work with Pascal Fontaine, Jean-Yves Marion, Stephan Merz and Leonor Prensa Nieto. In the Proceedings of TACAS 2006, Volume 3920 of LNCS, pages 167 - 181, Springer, 2006. © Copyright Springer-Verlag.

2005

Mixing Finite Success and Finite Failure in an Automated Prover. Joint work with Dale Miller and Gopalan Nadathur. In the Proceedings of ESHOL'05: Emperically Successful Automated Reasoning in Higher-Order Logics. December, 2005.

Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools. Joint work with Damian Barsotti and Leonor Prensai. In Proceedings of AVOCS 2005, Volume 145 of ENTCS, pages 63-78, Elsevier, 2005.

Model checking for pi-calculus using proof search. In Proceedings of CONCUR 2005, LNCS Vol. 3653, pages 36 - 50, Springer-Verlag, 2005. © Copyright Springer-Verlag. An extended version is available. The implementation of the model checkers described in this paper is done in the Level 0/1 prover. The (executable) specifications for the model checker: pi.def (specification of the transition system for pi calculus) and modal.def (specification of the modal logics).

A Proof Search Specification of the pi-Calculus. Joint paper with Dale Miller. In Proceedings of the 3rd workshop in Foundations of Global Ubiquitous Computing 2004. ENTCS Vol. 138, Issue 1, pages 79 - 101, 2005. Here is an extended version with proofs.

A Proof Theory for Generic Judgments. Joint work with Dale Miller. ACM Transactions on Computational Logic, Vol. 6, No. 4, pages 749 - 783, October 2005.

2003

A proof theory for generic judgments: an extended abstract. Joint work with Dale Miller. Proceedings of LICS 2003, edited by Phokion Kolaitis. Ottawa, July 2003,pp. 118 - 127.

2002

Encoding generic judgments. Joint work with Dale Miller. Proceedings of FSTTCS 2002 (22nd Foundations of Software Technology and Theoretical Computer Science), edited by M. Agrawal and A. Seth (PDF, DVI). © Copyright Springer-Verlag.

2001

Thesis

A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Penn State University, May 2004. Adviser: Dale Miller. A copy of my thesis is also available at http://etda.libraries.psu.edu.

Properties of a Logical System in the Calculus of Structures. [ps.gz , pdf or dvi.gz] Master Thesis, TU Dresden, July 2001. Adviser: Alessio Guglielmi. Also available as Technical Report WV-01-06 at TU Dresden. A revised version has appeared in the LMCS journal.

Unpublished notes

A trace based bisimulation for the spi-calculus. January 2009. This is a revised and extended version of a conference paper presented at APLAS 2007.

Cut Elimination for a Logic with Generic Judgments and Induction. Contains technical proofs of the LFMTP'06 paper.

Formalization of a Generalized Clock Synchronization Protocol. Isabelle/HOL proof document. Here is the Isar proof script. Available also from Isabelle's Archive of Formal Proofs.

An Extension of L-lambda Unification. September 16, 2002. [_dvi , pdf ].