Alwen Tiu

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Modular Labelled Sequent Calculi for Abstract Separation Logics.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2018

A labelled sequent calculus for BBI: proof theory and proof search.

[BibT_eX]

[DOI]

Zhe Hou

J. Log. Comput., 2018

Quasi-Open Bisimilarity with Mismatch is Intuitionistic.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement.

[BibT_eX]

[DOI]

Sjouke Mauw

Proceedings of the 5th International Workshop on Graphical Models for Security, 2018

Compositional Reasoning for Shared-Variable Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

A Permission-Dependent Type System for Secure Information Flow Analysis.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017

Semantics for Specialising Attack Trees based on Linear Logic.

[BibT_eX]

[DOI]

Sjouke Mauw

Fundam. Informaticae, 2017

Generating Witness of Non-Bisimilarity for the pi-Calculus.

[BibT_eX]

[DOI]

Ki Yung Ahn

CoRR, 2017

A Characterisation of Open Bisimulation using an Intuitionistic Modal Logic.

[BibT_eX]

[DOI]

Ki Yung Ahn

CoRR, 2017

CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Steelix: program-state based binary fuzzing.

[BibT_eX]

[DOI]

Yuekang Li

Bihuan Chen

Mahinthan Chandramohan

Shang-Wei Lin

Yang Liu

Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017

VeriFormal: An Executable Formal Model of a Hardware Description Language.

[BibT_eX]

[DOI]

Wilayat Khan

David Sanán

Proceedings of the A Systems Approach to Cyber Security, 2017

Proof Tactics for Assertions in Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-Bounded Processes.

[BibT_eX]

[DOI]

Emanuele D'Osualdo

Luke Ong

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

2016

Compositional Reasoning for Shared-variable Concurrent Programs.

[BibT_eX]

[DOI]

CoRR, 2016

Termination of Monotone Programs.

[BibT_eX]

[DOI]

CoRR, 2016

A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Separata: Isabelle tactics for Separation Algebra.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor.

[BibT_eX]

[DOI]

Proceedings of the FM 2016: Formal Methods, 2016

Private Names in Non-Commutative Logic.

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Concurrency Theory, 2016

SPEC: An Equivalence Checker for Security Protocols.

[BibT_eX]

[DOI]

Nam Nguyen

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

Completeness for a First-Order Abstract Separation Logic.

[BibT_eX]

[DOI]

Zhe Hou

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015

Formal Certification of Android Bytecode.

[BibT_eX]

[DOI]

Hendra Gunadi

CoRR, 2015

Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL.

[BibT_eX]

[DOI]

Xiaoning Du

Yang Liu

Proceedings of the FM 2015: Formal Methods, 2015

Automated Theorem Proving for Assertions in Separation Logic with All Connectives.

[BibT_eX]

[DOI]

Zhe Hou

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Abella: A System for Reasoning about Relational Specifications.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2014

Proof search for propositional abstract separation logics via labelled sequents.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 2014

Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System.

[BibT_eX]

[DOI]

Hendra Gunadi

Proceedings of the FM 2014: Formal Methods, 2014

2013

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic - Extended Version.

[BibT_eX]

[DOI]

CoRR, 2013

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic 2013 (CSL 2013), 2013

Extracting Proofs from Tabled Proof Search.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

Cut elimination for a logic with induction and co-induction.

[BibT_eX]

[DOI]

Alberto Momigliano

J. Appl. Log., 2012

Characterisations of testing preorders for a finite probabilistic π-calculus.

[BibT_eX]

[DOI]

Yuxin Deng

Formal Aspects Comput., 2012

Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus

[BibT_eX]

[DOI]

Yuxin Deng

CoRR, 2012

Stratification in Logics of Definitions.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures.

[BibT_eX]

[DOI]

Egor Ianovski

Proceedings of the Advances in Modal Logic 9, 2012

2011

On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2011

On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics.

[BibT_eX]

Proceedings of the TABLEAUX 2011, 2011

A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

2010

Proof search specifications of bisimulation and modal logics for the pi-calculus.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2010

A Proof Theoretic Analysis of Intruder Theories

[BibT_eX]

[DOI]

Jeremy E. Dawson

Log. Methods Comput. Sci., 2010

Automating Open Bisimulation Checking for the Spi Calculus.

[BibT_eX]

[DOI]

Jeremy E. Dawson

Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Cut-elimination and Proof Search for Bi-Intuitionistic Tense Logic.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 8, 2010

2009

A decidable policy language for history-based transaction monitoring

[BibT_eX]

[DOI]

CoRR, 2009

A Trace Based Bisimulation for the Spi Calculus

[BibT_eX]

[DOI]

CoRR, 2009

Formalising Observer Theory for Environment-Sensitive Bisimulation.

[BibT_eX]

[DOI]

Jeremy E. Dawson

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Taming Displayed Tense Logics Using Nested Sequents with Deep Inference.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

A Proof Theoretic Analysis of Intruder Theories.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

Matching Trace Patterns with Regular Policies.

[BibT_eX]

[DOI]

Franz Baader

Proceedings of the Language and Automata Theory and Applications, 2009

A First-Order Policy Language for History-Based Transaction Monitoring.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2009

2008

On the Role of Names in Reasoning about lambda-tree Syntax Specifications.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

Cut Elimination for a Logic with Generic Judgments and Induction

[BibT_eX]

[DOI]

CoRR, 2008

Matching linear and non-linear trace patterns with regular policies.

[BibT_eX]

[DOI]

Franz Baader

Proceedings of the 22nd International Workshop on Unification, 2008

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 7, 2008

2007

Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5.

[BibT_eX]

[DOI]

J. Log. Comput., 2007

Verification of clock synchronization algorithms: experiments on a combination of deductive tools.

[BibT_eX]

[DOI]

Damián Barsotti

Leonor Prensa Nieto

Formal Aspects Comput., 2007

The Bedwyr System for Model Checking over Syntactic Expressions.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006

A System of Interaction and Structure II: The Need for Deep Inference.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2006

A Logic for Reasoning about Generic Judgments.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2006

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

A Local System for Intuitionistic Logic.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

2005

A proof theory for generic judgments.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2005

Formalization of a Generalized Protocol for Clock Synchronization.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2005

Model Checking for <i>pi</i>-Calculus Using Proof Search.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

2004

A Proof Search Specification of the pi-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Workshop 3rd on the Foundations of Global Ubiquitous Computing, 2004

2003

Induction and Co-induction in Sequent Calculus.

[BibT_eX]

[DOI]

Alberto Momigliano

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

A Proof Theory for Generic Judgments: An extended abstract.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

2002

Encoding Generic Judgments.

[BibT_eX]

[DOI]

Proceedings of the FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 2002

2001

A Local System for Classical Logic.

[BibT_eX]

[DOI]

Kai Brünnler