What is the Logic of Computational Tasks? - Max I. Kanovich (Logic at Botik, 1989)

Efficient Program Synthesis in Computational Models. - Max I. Kanovich (J. Log. Program., 1990)

Efficient Program Synthesis: Semantics, Logic, Complexity. - Max I. Kanovich (TACS, 1991)

Horn Programming in Linear Logic Is NP-Complete - Max I. Kanovich (LICS, 1992)

The Rumors System Of Russian Synthesis. - Max I. Kanovich; Zoya M. Shalyapina (COLING, 1994)

Computational and Concurrency Aspects of Linear Logic. - Max I. Kanovich (IFIP Congress (1), 1994)

Computational and Concurrency Models of Linear Logic. - Max I. Kanovich (LFCS, 1994)

Simulating Guarded Programs in Linear Logic. - Max I. Kanovich (Theory and Practice of Parallel Programming, 1994)

The Complexity of Horn Fragments of Linear Logic. - Max I. Kanovich (Ann. Pure Appl. Log., 1994)

Linear Logic as a Logic of Computations. - Max I. Kanovich (Ann. Pure Appl. Log., 1994)

The Complexity of Neutrals in Linear Logic - Max I. Kanovich (LICS, 1995)

Petri Nets, Horn Programs, Linear Logic and Vector Games. - Max I. Kanovich (Ann. Pure Appl. Log., 1995)

Linear Logic Automata. - Max I. Kanovich (Ann. Pure Appl. Log., 1996)

Simulating Computations in Second Order Non-Commutative Linear Logic. - Max I. Kanovich (Linear Logic Tokyo Meeting, 1996)

Temporal Linear Logic Specifications for Concurrent Processes (Extended Abstract). - Max I. Kanovich; Takayasu Ito (LICS, 1997)

Specifying Real-Time Finite-State Systems in Linear Logic. - Max I. Kanovich; Mitsuhiro Okada; Andre Scedrov (COTIC, 1998)

Inductive methods and contract-signing protocols. - Rohit Chadha; Max I. Kanovich; Andre Scedrov (CCS, 2001)

The Expressive Power of Horn Monadic Linear Logic. - Max I. Kanovich (CSL, 2001)

The classical AI planning problems in the mirror of Horn linear logic: semantics, expressibility, complexity. - Max I. Kanovich; Jacqueline Vauzeilles (Math. Struct. Comput. Sci., 2001)

Bijections between Partitions by Two-Directional Rewriting Techniques. - Max I. Kanovich (CSL, 2002)

Coping Polynomially with Numerous but Identical Elements within Planning Problems. - Max I. Kanovich; Jacqueline Vauzeilles (CSL, 2003)

Phase semantics for light linear logic. - Max I. Kanovich; Mitsuhiro Okada; Andre Scedrov (Theor. Comput. Sci., 2003)

Finding direct partition bijections by two-directional rewriting techniques. - Max I. Kanovich (Discret. Math., 2004)

Intuitionistic phase semantics is almost classical. - Max I. Kanovich; Mitsuhiro Okada; Kazushige Terui (Math. Struct. Comput. Sci., 2006)

Collaborative Planning With Privacy. - Max I. Kanovich; Paul D. Rowe; Andre Scedrov (CSF, 2007)

A Note on Rewriting Proofs and Fibonacci Numbers. - Max I. Kanovich (LFCS, 2007)

The two-way rewriting in action: Removing the mystery of Euler-Glaisher's map. - Max I. Kanovich (Discret. Math., 2007)

Strong planning under uncertainty in domains with numerous but identical elements (a generic approach). - Max I. Kanovich; Jacqueline Vauzeilles (Theor. Comput. Sci., 2007)

Policy Compliance in Collaborative Systems. - Max I. Kanovich; Paul D. Rowe; Andre Scedrov (CSF, 2009)

Light Linear Logic with Controlled Weakening. - Max I. Kanovich (LFCS, 2009)

The Complexity of Abduction for Separated Heap Abstractions. - Nikos Gorogiannis; Max I. Kanovich; Peter W. O'Hearn (SAS, 2011)

Collaborative Planning with Confidentiality. - Max I. Kanovich; Paul D. Rowe; Andre Scedrov (J. Autom. Reason., 2011)

Linear logic as a tool for planning under temporal uncertainty. - Max I. Kanovich; Jacqueline Vauzeilles (Theor. Comput. Sci., 2011)

Towards an automated assistant for clinical investigations. - Vivek Nigam; Tajana Ban Kirigin; Andre Scedrov; Carolyn L. Talcott; Max I. Kanovich; Ranko Perovic (IHI, 2012)

A Rewriting Framework for Activities Subject to Regulations. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott; Ranko Perovic (RTA, 2012)

Light linear logics with controlled weakening: Expressibility, confluent strong normalization. - Max I. Kanovich (Ann. Pure Appl. Log., 2012)

Bounded Memory Protocols and Progressing Collaborative Systems. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov (ESORICS, 2013)

Foundations for Decision Problems in Separation Logic with General Inductive Predicates. - Timos Antonopoulos; Nikos Gorogiannis; Christoph Haase; Max I. Kanovich; Joël Ouaknine (FoSSaCS, 2014)

Bounded memory protocols. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov (Comput. Lang. Syst. Struct., 2014)

Bounded memory Dolev-Yao adversaries in collaborative systems. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov (Inf. Comput., 2014)

Undecidability of Propositional Separation Logic and Its Neighbours. - James Brotherston; Max I. Kanovich (J. ACM, 2014)

Multiset rewriting over Fibonacci and Tribonacci numbers. - Max I. Kanovich (J. Comput. Syst. Sci., 2014)

Discrete vs. Dense Times in the Analysis of Cyber-Physical Security Protocols. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (POST, 2015)

Horn Linear Logic and Minsky Machines. - Max I. Kanovich (CoRR, 2015)

Undecidability of the Lambek Calculus with a Relevant Modality. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (FG, 2016)

Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (FORMATS, 2016)

On Lambek's Restriction in the Presence of Exponential Modalities. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (LFCS, 2016)

Model checking for symbolic-heap separation logic with inductive predicates. - James Brotherston; Nikos Gorogiannis; Max I. Kanovich; Reuben Rowe (POPL, 2016)

Undecidability of the Lambek calculus with subexponentials and bracket modalities. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (CoRR, 2016)

The undecidability theorem for the Horn-like fragment of linear logic (Revisited). - Max I. Kanovich (Math. Struct. Comput. Sci., 2016)

Biabduction (and Related Problems) in Array Separation Logic. - James Brotherston; Nikos Gorogiannis; Max I. Kanovich (CADE, 2017)

Undecidability of the Lambek Calculus with Subexponential and Bracket Modalities. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (FCT, 2017)

A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order. - Max I. Kanovich; Stepan L. Kuznetsov; Glyn Morrill; Andre Scedrov (FSCD, 2017)

Simulating Linear Logic in 1-Only Linear Logic. - Max I. Kanovich (CoRR, 2017)

Time, computational complexity, and probability in the analysis of distance-bounding protocols. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (J. Comput. Secur., 2017)

A rewriting framework and logic for activities subject to regulations. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott; Ranko Perovic (Math. Struct. Comput. Sci., 2017)

On the Complexity of Pointer Arithmetic in Separation Logic. - James Brotherston; Max I. Kanovich (APLAS, 2018)

A Logical Framework with Commutative and Non-commutative Subexponentials. - Max I. Kanovich; Stepan L. Kuznetsov; Vivek Nigam; Andre Scedrov (IJCAR, 2018)

Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols. - Musab A. AlTurki; Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (CPS-SPC@CCS, 2018)

Bracket Induction for Lambek Calculus with Bracket Modalities. - Glyn Morrill; Stepan L. Kuznetsov; Max I. Kanovich; Andre Scedrov (FG, 2018)

On the Complexity of Pointer Arithmetic in Separation Logic (an extended version). - James Brotherston; Max I. Kanovich (CoRR, 2018)

Compliance in Real Time Multiset Rewriting Models. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (CoRR, 2018)

A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols. - Musab A. AlTurki; Tajana Ban Kirigin; Max I. Kanovich; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (Foundations of Security, Protocols, and Equational Reasoning, 2019)

Resource-Bounded Intruders in Denial of Service Attacks. - Abraão Aires Urquiza; Musab A. AlTurki; Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (CSF, 2019)

Undecidability of a Newly Proposed Calculus for CatLog3. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (FG, 2019)

The Complexity of Multiplicative-Additive Lambek Calculus: 25 Years Later. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (WoLLIC, 2019)

L-Models and R-Models for Lambek Calculus Enriched with Additives and the Multiplicative Unit. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (WoLLIC, 2019)

Subexponentials in non-commutative linear logic. - Max I. Kanovich; Stepan L. Kuznetsov; Vivek Nigam; Andre Scedrov (Math. Struct. Comput. Sci., 2019)

Soft Subexponentials and Multiplexing. - Max I. Kanovich; Stepan L. Kuznetsov; Vivek Nigam; Andre Scedrov (IJCAR (1), 2020)

Reconciling Lambek's restriction, cut-elimination and substitution in the presence of exponential modalities. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (J. Log. Comput., 2020)

On the Complexity of Verification of Time-Sensitive Distributed Systems. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (Protocols, Strands, and Logic, 2021)

On Security Analysis of Periodic Systems: Expressiveness and Complexity. - Musab A. Alturki; Tajana Ban Kirigin; Max I. Kanovich; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (ICISSP, 2021)

A Compositional Deadlock Detector for Android Java. - James Brotherston; Paul Brunet; Nikos Gorogiannis; Max I. Kanovich (ASE, 2021)

On the Complexity of Verification of Time-Sensitive Distributed Systems: Technical Report. - Max I. Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (CoRR, 2021)

Resource and timing aspects of security protocols. - Abraão Aires Urquiza; Musab A. Alturki; Tajana Ban Kirigin; Max I. Kanovich; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (J. Comput. Secur., 2021)

The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (J. Log. Lang. Inf., 2021)

Correction to: The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (J. Log. Lang. Inf., 2021)

Non-associative, Non-commutative Multi-modal Linear Logic. - Eben Blaisdell; Max I. Kanovich; Stepan L. Kuznetsov; Elaine Pimentel; Andre Scedrov (IJCAR, 2022)

On the Formalization and Computational Complexity of Resilience Problems for Cyber-Physical Systems. - Musab A. Alturki; Tajana Ban Kirigin; Max I. Kanovich; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (ICTAC, 2022)

Language models for some extensions of the Lambek calculus. - Max I. Kanovich; Stepan L. Kuznetsov; Andre Scedrov (Inf. Comput., 2022)

On the Security and Complexity of Periodic Systems. - Musab A. Alturki; Tajana Ban Kirigin; Max I. Kanovich; Vivek Nigam; Andre Scedrov; Carolyn L. Talcott (SN Comput. Sci., 2022)

Explorations in Subexponential non-associative non-commutative Linear Logic (extended version). - Eben Blaisdell; Max I. Kanovich; Stepan L. Kuznetsov; Elaine Pimentel; Andre Scedrov (CoRR, 2023)

Explorations in Subexponential Non-associative Non-commutative Linear Logic. - Eben Blaisdell; Max I. Kanovich; Stepan L. Kuznetsov; Elaine Pimentel; Andre Scedrov (AMSLO@ESSLLI, 2023)

Time-Bounded Resilience. - Tajana Ban Kirigin; Jesse Comer; Max I. Kanovich; Andre Scedrov; Carolyn L. Talcott (WRLA, 2024)

Technical Report: Time-Bounded Resilience. - Tajana Ban Kirigin; Jesse Comer; Max I. Kanovich; Andre Scedrov; Carolyn L. Talcott (CoRR, 2024)