## 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.

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/