Research

  Olga Tveretina

Research interests:

  • Propositional proof complexity
  • Hybrid systems
  • Parallel computing
  • Decision procedures for software and hardware verification


Recent talks:


Efficiency of Propositional Proof Systems


Abstract:


A classical question of propositional logic is one of the shortest proof of a tautology. There is a related  question of how to construct an algorithm that produces the shortest proof. Cook and Reckhow  proposed to  attack the NP versus co-NP problem by  focusing on   lower bounds for standard proof systems of increasing complexity. A related  fundamental problem  is to determine the relative efficiency of standard proof systems.


First we  present an overview of the area paying attention to  the relative efficiency of  proof systems based on resolution and ordered binary decision diagrams (OBDDs). Resolution is  very simple, yet forms the basis of  popular tools for  theorem proving, such as SAT solvers, that are used in  industrial applications.   An OBDD is a canonical data structure  for  symbolic representation of Boolean functions which occurs commonly in formal verification and CAD software for circuit synthesis.


The relative complexity of two proof systems can be measured using the notion of polynomial simulation. Zantema and Groote proved that resolution and OBDDs do not simulate each other polynomially on arbitrary inputs for limited OBDD derivations. However,  formal comparison of these methods is not straightforward because OBDDs work on arbitrary formulas, whereas resolution can only be applied to formulas in conjunctive normal form (CNF). Contrary to popular belief, I will argue that resolution simulates OBDDs polynomially if we limit both to CNFs.



Recent papers:


A. Sandler, O. Tveretina:    ParaPlan: a Tool for Parallel Reachability Analysis of Planar Polygonal Differential Inclusion Systems,  The 8th International Symposium on Games, Automata, Logics, and Formal Verification (Gandalf), 2017


P. Zaichenkov, O. Tveretina, A. Shafarenko:  A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces, 12th Int. Conference on integrated Formal Methods (iFM), 2016


P. Zaichenkov, O. Tveretina, A. Shafarenko:  Configuring Non-Local Interfaces of Closed-Sourced Cloud Services, iFMCloud'16: The First International Workshop on Formal Methods for and on the Cloud​, 2016


P. Zaichenkov, B. Gijsbers, C. Grelck, O. Tveretina, A. Shafarenko: The Cost    and  Benefits of Coordination Programming: Two Case Studies in Concurrent Collection and S-Net,   accepted to    Parallel Processing Letters, 2016


P. Zaichenkov, O. Tveretina, A. Shafarenko: Interface Reconciliation in Kahn Process Networks using CSP and SAT, 5th Int. Workshop on the Cross-Fertilization Between CSP and SAT, 2015 [pdf]

  


P. Zaichenkov, B. Gijsbers, C. Grelck, O. Tveretina, A. Shafarenko: A Case Study in Coordination Programming: S-Net vs Concurrent Collection, In 28th IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW'14) Workshop on Programming Models, Languages and Compilers for Manycore and Heterogeneous Architectures (PLC'14), Phoenix, USA,  IEEE Computer Society, 2014    [pdf]


 


Current research students:

  • Andrei Sandler, MSc by research


Past research students:

  • Pavel Zaichenkov, PhD  student, now at Google
  • Maksim Kuznetcov, MSc by research, now at        Yandex
  • Anna Tikhonova, MSc by research
  • Daniel Funke,  student research project

O. Tveretina, D. Funke: Deciding Reachability for 3-Dimensional Multi-Linear Systems.  International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2011: 250-262

  • Tamara Mendt, MSc

T. Mendt, C. Sinz, O. Tveretina: Probabilistic Model Checking of  Constraints in a Supply Chain Business Process. Business Information Systems - 14th International Conference, BIS 2011: 1-12

T. Mendt, C. Sinz, O. Tveretina: Analyzing Separation of Duties Constraints with a Probabilistic Model Checker. BIS (Workshops) 2011: 18-29