Rajeev Goré

Mukesh Tiwari

Proceedings of the 32nd USENIX Security Symposium, 2023

A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised.

[BibT_eX]

[DOI]

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

2022

Direct elimination of additive-cuts in GL4ip: verified and extracted.

[BibT_eX]

[DOI]

Ian Shillito

Proceedings of the Advances in Modal Logic, AiML 2022, Rennes, France, 2022

2021

Improved Verifiability for BeleniosVS.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2021

Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq.

[BibT_eX]

[DOI]

Ian Shillito

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

CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-Learning and SAT.

[BibT_eX]

[DOI]

Cormac Kikkert

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

A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic.

[BibT_eX]

[DOI]

Caitlin D'Abrera

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

2020

Machine-checking the universal verifiability of ElectionGuard.

[BibT_eX]

[DOI]

Jack Stodart

IACR Cryptol. ePrint Arch., 2020

Did you mix me? Formally Verifying Verifiable Mix Nets in Electronic Voting.

[BibT_eX]

[DOI]

Bhavesh Sharma

IACR Cryptol. ePrint Arch., 2020

N-PAT: A Nested Model-Checker.

[BibT_eX]

[DOI]

CoRR, 2020

Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents.

[BibT_eX]

[DOI]

Proceedings of the 28th EACSL Annual Conference on Computer Science Logic, 2020

N-PAT: A Nested Model-Checker - (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Bi-Intuitionistic Logics: A New Instance of an Old Problem.

[BibT_eX]

[DOI]

Ian Shillito

Proceedings of the 13th Conference on Advances in Modal Logic, 2020

2019

A Correct Polynomial Translation of S4 into intuitionistic Logic.

[BibT_eX]

[DOI]

J. Symb. Log., 2019

Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version).

[BibT_eX]

[DOI]

Björn Lellmann

CoRR, 2019

Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents.

[BibT_eX]

[DOI]

Björn Lellmann

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

A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic.

[BibT_eX]

[DOI]

Camillo Fiorentini

Stéphane Graham-Lengrand

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

Verified Decision Procedures for Modal Logics.

[BibT_eX]

[DOI]

Minchao Wu

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Verified Verifiers for Verifying Elections.

[BibT_eX]

[DOI]

Mukesh Tiwari

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 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

A case study in formal verification of a Java program.

[BibT_eX]

[DOI]

Dmitry Brizhinev

CoRR, 2018

Modular Formalisation and Verification of STV Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Electronic Voting - Third International Joint Conference, 2018

Well-Founded Unions.

[BibT_eX]

[DOI]

Nachum Dershowitz

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

No More Excuses: Automated Synthesis of Practical and Verifiable Vote-Counting Programs for Complex Voting Schemes.

[BibT_eX]

[DOI]

Proceedings of the Electronic Voting - Second International Joint Conference, 2017

A Formally Verified Single Transferable Voting Scheme with Fractional Values.

[BibT_eX]

[DOI]

Milad K. Ghale

Dirk Pattinson

Proceedings of the Electronic Voting - Second International Joint Conference, 2017

Issues in Machine-Checking the Decidability of Implicational Ticket Entailment.

[BibT_eX]

[DOI]

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

2016

Separata: Isabelle tactics for Separation Algebra.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2016

Simulating STV Hand-Counting by Computers Considered Harmful: A.C.T.

[BibT_eX]

[DOI]

Ekaterina Lebedeva

Proceedings of the Electronic Voting - First International Joint Conference, 2016

Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi.

[BibT_eX]

[DOI]

James Brotherston

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

Efficient error localisation and imputation for real-world census data using SMT.

[BibT_eX]

[DOI]

Daniel Alarcón

Proceedings of the Australasian Computer Science Week Multiconference, 2016

2015

Formal Certification of Android Bytecode.

[BibT_eX]

[DOI]

Hendra Gunadi

CoRR, 2015

Machine-Checked Reasoning About Complex Voting Schemes Using Higher-Order Logic.

[BibT_eX]

[DOI]

Thomas Meumann

Proceedings of the E-Voting and Identity - 5th International Conference, 2015

Sequent Calculus in the Topos of Trees.

[BibT_eX]

[DOI]

Ranald Clouston

Proceedings of the Foundations of Software Science and Computation Structures, 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

Implementing Modal Tableaux Using Sentential Decision Diagrams.

[BibT_eX]

[DOI]

Jason Jingshi Li

Thomas Pagram

Proceedings of the AI 2015: Advances in Artificial Intelligence, 2015

2014

Cut-elimination for Weak Grzegorczyk Logic Go.

[BibT_eX]

[DOI]

Stud Logica, 2014

Computer-aided decision-making with trust relations and trust domains (cryptographic applications).

[BibT_eX]

[DOI]

Simon Kramer

Eiji Okamoto

J. Log. Comput., 2014

Verifying voting schemes.

[BibT_eX]

[DOI]

J. Inf. Secur. Appl., 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

Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting.

[BibT_eX]

[DOI]

Thomas Meumann

Proceedings of the 6th International Conference on Electronic Voting: Verifying the Vote, 2014

A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description.

[BibT_eX]

[DOI]

Jesse Wu

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

Implementing Tableau Calculi Using BDDs: BDDTab System Description.

[BibT_eX]

[DOI]

Kerry Olesen

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Book Reviews.

[BibT_eX]

[DOI]

Stud Logica, 2013

ExpTime Tableaux for ALC Using Sound Global Caching.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

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

[BibT_eX]

[DOI]

CoRR, 2013

On the Specification and Verification of Voting Schemes.

[BibT_eX]

[DOI]

Carsten Schürmann

Proceedings of the E-Voting and Identify - 4th International Conference, 2013

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic.

[BibT_eX]

[DOI]

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

An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election Scheme.

[BibT_eX]

[DOI]

Carsten Schürmann

Proceedings of the Automated Deduction - CADE-24, 2013

2012

Valentini's Cut-Elimination for Provability Logic resolved.

[BibT_eX]

[DOI]

Rev. Symb. Log., 2012

An iterative approach to synthesize business process templates from compliance rules.

[BibT_eX]

[DOI]

Inf. Syst., 2012

BDD-based automated reasoning in propositional non-classical logics: progress report.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics.

[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

Labelled Tree Sequents, Tree Hypersequents and Nested (Deep) Sequents.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 9, 2012

2011

Computer-Aided Decision-Making for Formal Relations and Domains of Trust, Distrust, and Mistrust with Cryptographic Applications.

[BibT_eX]

[DOI]

Simon Kramer

Eiji Okamoto

IACR Cryptol. ePrint Arch., 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

An Experimental Comparison of Theorem Provers for CTL.

[BibT_eX]

[DOI]

Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Craig Interpolation in Displayable Logics.

[BibT_eX]

[DOI]

James Brotherston

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

An Iterative Approach for Business Process Template Synthesis from Compliance Rules.

[BibT_eX]

[DOI]

Proceedings of the Advanced Information Systems Engineering, 2011

2010

Formal definitions and complexity results for trust relations and trust domains fit for TTPs, the web of trust, PKIs, and ID-based cryptography.

[BibT_eX]

[DOI]

Simon Kramer

Eiji Okamoto

SIGACT News, 2010

Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic.

[BibT_eX]

[DOI]

J. Log. Comput., 2010

A Proof Theoretic Analysis of Intruder Theories

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2010

Optimal Tableaux for Propositional Dynamic Logic with Converse

[BibT_eX]

[DOI]

CoRR, 2010

Optimal Tableau Algorithms for Coalgebraic Logics.

[BibT_eX]

[DOI]

Clemens Kupke

Dirk Pattinson

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

Short Paper: Semantic Sensor Composition.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Workshop on Semantic Sensor Networks, 2010

Generic Methods for Formalising Sequent Calculi Applied to Provability Logic.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Global Caching for Coalgebraic Description Logics.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

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

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 8, 2010

2009

Termination of Abstract Reduction Systems.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2009

Clausal Tableaux for Multimodal Logics of Belief.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2009

A decidable policy language for history-based transaction monitoring

[BibT_eX]

[DOI]

Andreas Bauer

CoRR, 2009

Sound Global State Caching for ALC with Inverse Roles.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 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

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

[BibT_eX]

[DOI]

Andreas Bauer

Proceedings of the Theoretical Aspects of Computing, 2009

Machine Checking Proof Theory: An Application of Logic to Logic.

[BibT_eX]

[DOI]

Proceedings of the Logic and Its Applications, Third Indian Conference, 2009

Global Caching, Inverse Roles and Fixpoint Logics.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Workshop on Description Logics (DL 2009), 2009

An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

An Experimental Evaluation of Global Caching for (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 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

An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability.

[BibT_eX]

[DOI]

Proceedings of the 5th Workshop on Methods for Modalities, 2007

The Tableau Workbench.

[BibT_eX]

[DOI]

Proceedings of the 5th Workshop on Methods for Modalities, 2007

A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version

[BibT_eX]

[DOI]

Linda Buisman

CoRR, 2007

EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies.

[BibT_eX]

[DOI]

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

A Cut-Free Sequent Calculus for Bi-intuitionistic Logic.

[BibT_eX]

[DOI]

Linda Buisman

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

One-Pass Tableaux for Computation Tree Logic.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2007

EXPTIME Tableaux for ALC Using Sound Global Caching.

[BibT_eX]

[DOI]

Proceedings of the 2007 International Workshop on Description Logics (DL2007), 2007

Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic in Multi-Agent Systems, 8th International Workshop, 2007

2005

Completeness of hyper-resolution via the semantics of disjunctive logic programs.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2005

A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics.

[BibT_eX]

[DOI]

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

2004

Forthcoming Papers.

[BibT_eX]

[DOI]

Valeria de Paiva

Michael Mendler

J. Log. Comput., 2004

Editorial.

[BibT_eX]

[DOI]

Valeria de Paiva

Michael Mendler

J. Log. Comput., 2004

On Two-Sided Approximate Model-Checking: Problem Formulation and Solution via Finite Topologies.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques, 2004

A General Theorem on Termination of Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

A New Machine-checked Proof of Strong Normalisation for Display Logic.

[BibT_eX]

[DOI]

Proceedings of the Computing: the Australasian Theory Symposiumm, 2003

The Tableaux Work Bench.

[BibT_eX]

[DOI]

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

A Logical Formalisation of the Fellegi-Holt Method of Data Cleaning.

[BibT_eX]

[DOI]

Agnes Boskovitz

Markus Hegland

Proceedings of the Advances in Intelligent Data Analysis V, 2003

2002

Display Calculi for Nominal Tense Logics.

[BibT_eX]

[DOI]

J. Log. Comput., 2002

Theoremhood-preserving Maps Characterizing Cut Elimination for Modal Provability Logics.

[BibT_eX]

[DOI]

J. Log. Comput., 2002

Formalised Cut Admissibility for Display Logic.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Machine-Checking the Timed Interval Calculus.

[BibT_eX]

[DOI]

Proceedings of the AI 2002: Advances in Artificial Intelligence, 2002

2001

Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle.

[BibT_eX]

[DOI]

Proceedings of the Computing: The Australasian Theory Symposium, 2001

Free-Variable Tableaux for Propositional Modal Logics.

[BibT_eX]

[DOI]

Stud Logica, 2001

CardS4: Modal Theorem Proving on Java Smartcards.

[BibT_eX]

[DOI]

Phuong Thê Nguyên

Proceedings of the Smart Card Programming and Security, 2001

2000

Displaying Modal Logic, Heinrich Wansing.

[BibT_eX]

[DOI]

J. Log. Lang. Inf., 2000

Display Calculi for Logics with Relative Accessibility Relations.

[BibT_eX]

[DOI]

J. Log. Lang. Inf., 2000

Editorial.

[BibT_eX]

[DOI]

Bernd-Holger Schlingloff

Log. J. IGPL, 2000

Dual Intuitionistic Logic Revisited.

[BibT_eX]

[DOI]

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

CardKt: Automated Multi-modal Deduction on Java Cards for Multi-application Security.

[BibT_eX]

[DOI]

Lan Duy Nguyen

Proceedings of the Java on Smart Cards: Programming and Security, 2000

Bimodal Logics for Reasoning About Continuous Dynamics.

[BibT_eX]

[DOI]

Jennifer M. Davoren

Proceedings of the Advances in Modal Logic 3, 2000

1999

Cut-Free Display Calculi for Nominal Tense Logics.

[BibT_eX]

[DOI]

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

KtSeqC: System Description.

[BibT_eX]

[DOI]

Vijay Boyapati

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

Tractable Transformations from Modal Provability Logics into First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

Gaggles, Gentzen and Galois: How to display your favourite substructural logic.

[BibT_eX]

[DOI]

Log. J. IGPL, 1998

Substructural Logics on Display.

[BibT_eX]

[DOI]

Log. J. IGPL, 1998

leanK 2.0.

[BibT_eX]

[DOI]

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

A Mechanised Proof System for Relation Algebra using Display Logic.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, European Workshop, 1998

An O ((n·log n)3)-Time Transformation from Grz into Decidable Fragments of Classical First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

System Description: card TAP: The First Theorem Prover on a Smart Card.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1998

System Description: leanK 2.0.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1998

cardTAP: Automated Deduction on a Smart Card.

[BibT_eX]

[DOI]

Proceedings of the Advanced Topics in Artificial Intelligence, 1998

A Mechanisation of Classical Modal Tense Logics Using Isabelle.

[BibT_eX]

[DOI]

Proceedings of the Advanced Topics in Artificial Intelligence, 1998

A Labelled Sequent System for Tense Logic Kt.

[BibT_eX]

[DOI]

Nicolette Bonnette

Proceedings of the Advanced Topics in Artificial Intelligence, 1998

1997

Relations Between Propositional Normal Modal Logics: An Overview.

[BibT_eX]

[DOI]

Wolfgang Heinle

Alain Heuerding

J. Log. Comput., 1997

1996

Cut-free Display Calculi for Relation Algebras.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 10th International Workshop, 1996

1995

Editorial.

[BibT_eX]

[DOI]

Log. J. IGPL, 1995

1994

Cut-free sequent and tableau systems for propositional Diodorean modal logics.

[BibT_eX]

[DOI]

Stud Logica, 1994

1989

Automatic Synthesis of Boolean Equations Using Programmable Array Logic.

[BibT_eX]

[DOI]