Alexei Lisitsa

Department of Computer Science
University of Liverpool
Ashton Building 
Liverpool L69 7ZF
United Kingdom 

e-mail: A.Lisitsa@csc.liv.ac.uk
phone:  +44 151 795 4250
fax:    +44 151 795 4235
office:   1.18 (first floor) 

Position

Administrative duties

Research Interests

• DBLP:Alexei Lisitsa
• Google Scholar

Talks

• Finite Models for Safety Verification. Slides of the talk given on 22.06.12 in ENS Cachan, LSV
• Automated Deduction in the Exploration of Andrews-Curtis Conjecture, online seminar, 10.03.2025, Algebra and Cryptology Center, Stevens Institute of Technology

Summer School, Computer Science Summer in Russia, 2019

• Finite Countermodel Finding for Infinite State and Parameterized Verification
• Automated Reasoning for Experimental Mathematics
• (un)Knot detection
• SAT for Erdos Discrepancy Problem
• AR for the Andrews-Curtis Conjecture

Research

• Knowledge Transfer Partnership project (academic supervisor)
• Future AI and Robotics Hub for Space (FAIR-SPACE)
• Satisfiability Checking and Symbolic Computation
• Verification via Finite Countermodel Finding
• Supercompilation for Verification
• Logical, Computational and Algorithmic Approach to Knots
• Automated Reasoning, Symbolic Computations and Machine Learning in Experimental Mathematics
  • New: Automated Theorem Proving Reveals a Lengthy Andrews-Curtis Trivialization for a Miller-Schupp Trivial Group Presentation, submitted, available as a preprint at SSRN
  • New Andrews-Curtis Trivializations for Miller-Schupp Group Presentations
  • Machine Learning Discovers Invariants of Braids and Flat Braids
  • Counting graphs induced by Gauss diagrams and families of mutant alternating knots
  • Automated reasoning for proving non-orderability of groups
  • Describing realizable Gauss diagrams using the concepts of parity or bipartite graphs
  • A SAT Attack on Erdos Discrepancy Conjecture; see also A237695, Practically P=NP? and Discrepancies, puppet show
  • Detecting Unknots via Equational Reasoning, I: Exploration
  • Quandle coloring with SAT and #SAT for knot discrimination
  • Automated Reasoning for Knot Semigroups
  • Automated reasoning in the exploration of Andrews-Curtis Conjecture
• Temporal Logic and Stream Data Processing for Intrusion detection
• Engineering Autonomous Space Software

PhD students

PhD students successfully completed their studies

Forthcoming events (consider submission/participation)

• 18th International Conference on Verification and Evaluation of Computer and Communication Systems, 4-6 November, 2025, Paris, France

Verification and Program Transformation (VPT) series of Workshops (2013-2022)

Past events

Forthcoming events

• TBA

Recent events