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

Palmse, Estonia, March 4 - 9, 2018

Student Talks 2018 (abstracts)

Qualification of assertion based verification

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.

Using EasyCrypt to model an online voting protocol

Kristjan Krips
Cybernetica AS, Estonia

This talk is about modelling and formal verification of a few integrity properties of an online voting protocol. The voting protocol provides post-election vote verification mechanisms that help to detect vote manipulation attacks by the malicious voting application and by the voting server. EasyCrypt was used to model the protocol and to verify the selected integrity properties.
Co-authors of related paper: Ivo Kubjas and Jan Willemson.

Certified Foata normalization for generalized traces

Hendrik Maarand
Tallinn University of Technology Dept. of Software Science, Estonia

Mazurkiewicz traces are a well-known model of concurrency with a notion of equivalence for interleaving executions. Interleaving executions of a concurrent system are represented as strings over an alphabet equipped with an independence relation, and two strings are taken to be equivalent if they can be transformed into each other by repeatedly commuting independent consecutive letters. Analyzing all behaviors of the system can be reduced to analyzing one canonical representative from each equivalence class; normal forms such as the Foata normal form can be used for this purpose. In some applications, it is useful to have commutability of two adjacent letters in a string depend on their left context. We develop Foata normal forms and normalization for Sassone et al.'s context-dependent generalization of traces, formalize this development in the dependently typed programming language Agda and show generalized Foata normalization in action on an example from relaxed shared-memory concurrency (local reads in TSO).

This is joint work with Tarmo Uustalu.

Privacy-Enhanced Business Process Model and Notation

Pille Pullonen
Cybernetica AS, Estonia

Privacy Enhancing Technologies (PETs) play an important role in preventing privacy leakage of data along information flows. Although business process modeling is well-suited for expressing stakeholder collaboration and process support by technical solutions, little is done to visualize and analyze the flow of private information as it is disclosed to process participants. We propose a model where PETs can be viewed at multiple levels of abstraction in BPMN. This forms the foundation of PE-BPMN – a privacy-enhanced BPMN language for capturing PET-related activities in order to study the disclosure of private information.

Co-authors: Aivo Toots, Jake Tom, Raimundas Matulevicius, Dan Bogdanov.

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/