23rd Estonian Winter School in Computer Science (EWSCS)
XXIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 4 - 9, 2018

Student Talks 2018 (abstracts)

Tara Ghasempouri
Tallinn University of Technology, Dept. of Computer Systems, Estonia

The growing complexity and time-to-market pressure of modern large-scale software and hardware systems, make
verification process even more challenging. Verification proves the
consistency between the implementation of a complex system with
the designer’s intent and represented by the specification. One of
the promising ways to prove this consistency is Assertion-Based
Verification (ABV). However, ABV’s effectiveness depends on the
quality of assertions. Assertions can be manually or automatically
generated. In both cases, assertion generation is error prone
and needs high expertise. Moreover, the number of generated
assertions is generally too large. Thus, assertion qualification is
necessary to evaluate the quality of generated assertions to assist
verification engineers to select only the highest quality assertions
for systems’ verification. Most of the current works for assertion
qualification are based on fault injection analysis, by measuring
the percentage of the erroneous behavior of the Design Under
Verification (DUV) covered by the assertions, which requires long
simulation time. To fill in the gap, this work proposes a new
automatic data mining-based approach for assertions already
defined for a design, which in contrast to the state-of-the-art
can evaluate assertions’ quality precisely within a very short
simulation time. Experimental results support the benefit of the
proposed methodology.

On the decision trees with symmetries

Artur Riazanov
St. Petersburg Academic University, Dept. of Math. and IT, Russian Federation

We introduce a propositional proof system based on decision trees utilizing symmetries of formulas. We refer to this proof system as decision trees with symmetries (SDT).
SDT can be polynomially simulated by the proof system SR-I introduced by Krishnamurthy. SR-I extends Resolution with the symmetry rule. We show that there are polynomial-size proofs of the functional pigeonhole principle FPHP_n^(n+1) and of an encoding of the clique coloring principle. On the other hand we show that any SDT for the pigeonhole principle PHP_n^(n+1) has size 2^{Omega(n^{1/3-o(1)})} despite that PHP_n^{n+1} has a lot of symmetries. In 1999 Urquhart showed that PHP_n^(n+1) has a polynomial-size SR-I refutation. Thus SDT is strictly weaker than SR-I.
The smallest decision tree for PHP_n^(n+1) has size 2^{Omega(n log n)}; we show that there exists an SDT for PHP_n^(n+1) of size 2^{O(sqrt{n})}.

The corresponding paper was accepted to CSR 2018.

Graphical conjunctive queries

Jens Seeber
IMT School for Advanced Studies Lucca, Italy

Conjunctive queries are a fundamental class of queries to databases that every query language worthy of that name is able to express. In their seminal work, Chandra and Merlin associated to each conjunctive query a hypergraph with interface, called the universal model, in such a way that query inclusion corresponds to existence of a hypergraph homomorphism. We take that as inspiration to introduce a string-diagrammatic language of conjunctive queries where we can give an axiomatization of query inclusion that we prove to be sound and complete. Categorically, this axiomatization corresponds to the structure of cartesian bicategories as introduced by Carboni and Walters. To connect the two works, we see Chandra's and Merlin's hypergraphs with interfaces as cospans of hypergraphs, a category which we prove equivalent to the syntactic category of our language. This allows us to see databases as functors on hypergraphs and to obtain completeness via a representability result: Every such functor is of the form Hom(_,T) for a hypergraph T.

Valid CSS! Valid XHTML 1.0 Strict Last changed November 26, 2014 19:55 Europe/Helsinki (GMT +02:00) by local organizers, ewscs18(at)cs.ioc.ee
EWSCS'18 page: http://cs.ioc.ee/ewscs/2018/