Accueil

Alexei Lisitsa

  1. First-order finite satisfiability vs tree automata in safety verification.

    Tue, 07/05/2011 - 15:01 — SomNambul
    Authors: Alexei Lisitsa
    Subjects: Logic in Computer Science
    Abstract

    In this paper we deal with verification of safety properties of
    term-rewriting systems. The verification problem is translated to a purely
    logical problem of finding a finite countermodel for a first-order formula,
    which further resolved by a generic finite model finding procedure. A finite
    countermodel produced during successful verification provides with a concise
    description of the system invariant sufficient to demonstrate a specific safety
    property.

  2. Finite Model Finding for Parameterized Verification.

    Wed, 11/03/2010 - 16:01 — SomNambul
    Authors: Alexei Lisitsa
    Subjects: Logic in Computer Science
    Abstract

    In this paper we investigate to which extent a very simple and natural
    "reachability as deducibility" approach, originated in the research in formal
    methods in security, is applicable to the automated verification of large
    classes of infinite state and parameterized systems. The approach is based on
    modeling the reachability between (parameterized) states as deducibility
    between suitable encodings of states by formulas of first-order predicate
    logic. The verification of a safety property is reduced to a pure logical
    problem of finding a countermodel for a first-order formula.

  3. Agent Based Approaches to Engineering Autonomous Space Software.

    Wed, 03/03/2010 - 16:01 — SomNambul
    Authors: Louise A. Dennis, Michael Fisher, Nicholas Lincoln, Alexei Lisitsa, Sandor M. Veres
    Subjects: Multiagent Systems
    Abstract

    Current approaches to the engineering of space software such as satellite
    control systems are based around the development of feedback controllers using
    packages such as MatLab's Simulink toolbox. These provide powerful tools for
    engineering real time systems that adapt to changes in the environment but are
    limited when the controller itself needs to be adapted.

Math-arch

Syndicate content