כדי להצטרף לרשימת תפוצה של קולוקוויום מדעי המחשב, אנא בקר בדף מנויים של הרשימה.

Computer Science events calendar in HTTP ICS format for of Google calendars, and for Outlook.

Academic Calendar at Technion site.

- פתירת פסוקיות הורן מאולצות בחלקים הולכים וגדלים, על פי צורךמנחה: Prof. Orna Grumberg and Dr. Yakir VizelConstrained Horn Clauses (CHCs) is a fragment of First Order Logic (FOL), that has gained a lot of attention in recent years. One of the main reasons for the rising interest in CHCs is the ability to reduce many verification problems to satisfiability of CHCs. For example, program verification can naturally be described as the satisfiability of CHCs modulo a background theory such as linear arithmetic and arrays. To this end, CHC-solvers can be used as the back-end for different verification tools and allow to separate the generation of verification conditions from the decision procedure that decides if the verification conditions are correct or not. In our work, we present a novel framework, called LazyHorn, that is aimed at solving the satisfiability problem of CHCs modulo a background theory. The framework is driven by the idea that a set of CHCs can be solved in parts, making it an easier problem for the CHC-solver. Furthermore, solving a set of CHCs can benefit from an interpretation revealed by the solver for its subsets. LazyHorn is lazy in that it gradually extends the set of checked CHCs, as needed. It is also incremental in its use of a CHC solver, supplying it with an interpretation, obtained for previously checked subsets. We have implemented an efficient instance of the framework that is restricted to a fragment of CHCs called linear CHCs.
- Pixel Club: TextAdaIN: Paying Attention to Shortcut Learning in TextRecognizersאורן נוריאל (AWS)יום שלישי, 25.1.2022, 11:30Zoom Lecture: https://technion.zoom.us/my/chaimbaskinLeveragingthe characteristics of convolutional layers, neural networks are extremelyeffective for pattern recognition tasks. However in some cases,their decisions are based on unintended information leading to high performanceon standard benchmarks but also to a lack of generalization to challengingtesting conditions and unintuitive failures. Recentworkhas termed this “shortcut learning” and addressed its presence in multipledomains. In text recognition, we reveal another such shortcut, whereby recognizersoverly depend on local image statistics. Motivated by this, we suggest anapproach to regulate the reliance on local statisticsthat improves text recognition performance. Ourmethod, termed TextAdaIN, creates local distortions in the feature map whichprevent the network from overfitting to localstatistics. It does so by viewing each feature map as a sequence of elementsand deliberately mismatching fine-grained feature statistics between elementsin a mini-batch. Despite TextAdaIN’s simplicity, extensive experiments show its effectiveness compared to other, morecomplicated methods. TextAdaIN achieves state-of-the-art results on standardhandwritten text recognition benchmarks. Additionally, it generalizes tomultiple architectures and to the domain of scene text recognition. Furthermore, we demonstrate that integrating TextAdaINimproves robustness towards more challenging testing conditions. Short bio: Oren Nurielis an applied computer vision scientist at AWS. He holds an MSc degree inComputer Science from the Tel-Aviv University.
- pISTA אלגוריתם סף איטרטיבי בעל טיפול מקדים עבור בעיית LASSOמנחה: Prof. Irad Yavneh and Dr. Eran Treister
We propose a novel quasi-Newton method for solving the sparse inverse covariance estimation problem also known as the graphical least absolute shrinkage and selection operator (GLASSO). This problem is often solved using a second order quadratic approximation. However, in such algorithms the Hessian term is complex and computationally expensive to handle. To this end,our algorithm uses the inverse of the Hessian as a preconditioner to simplify and approximate the quadratic element at the cost of a more complex l1 element. The variables of the resulting preconditioned problem are coupled only by the l1 sub-derivative of each other, which can be guessed with minimal cost using the gradient itself, allowing the algorithm to be parallelized and implemented efficiently on GPU hardware accelerators. Numerical results on synthetic and real data demonstrate that our method is competitive with other state-of-the-art approaches.

- CGGC Seminar: Trading Memory for Computations: Scaling Range Matching on the Critical Pathאלון רשלבך (הנדסת חשמל, טכניון)יום ראשון, 30.1.2022, 13:30טאוב 337Range matching (RM) is a crucial component in computer systems, widely used in address translation, hard drives, network switches, and many more applications. RM is performed whenever one wishes to locate a range that contains an input number, given a large set of ranges. Any page-based mechanism uses RM, as pages are basically ranges. Longest prefix matching (LPM) uses ternary rules, which are also ranges. Firewalls are one example of multidimensional RM since ACL rules consist of several wildcarded fields that can be represented as ranges. Existing algorithms for RM are either page-based, tree-based, or hash-table-based. Either way, they all rely on pointer-chasing techniques, which impede their scalability to large range sets that spill out of the CPU core cache. Furthermore, their inherent lack of access locality and the data-dependent nature of their memory accesses make hardware prefetchers ineffective. Our research focuses on a new data structure, the Range Query Recursive Model Index (RQ-RMI). RQ-RMI uses shallow neural-nets (NN) for learning the distribution of a given set of ranges, turning the costly lookup operations into NN inference. Crucially, the RQ-RMI training algorithm guarantees a tight bound on its lookup latency, ensures its correctness, and converges fast: it can index 500K ranges in a few hundred milliseconds on a single CPU core. We develop NuevoMatch (NM), an algorithm for multi-field packet classification, and integrate it into the critical path of the popular, open-source, virtual switch Open vSwitch (OVS). NM scales OVS to support 500K OpenFlow rules with a 12.3X geomean throughput speedup and up to 50K updates per second.
- הגירת נתונים מבוססת קיבוץ במערכות אחסון עם דדופליקציהמנחה: Dr. Gala YadgarDeduplication is a leading method for reducing physical storage capacity when duplicate data is present. This method can be applied on chunks, files, containers, and more. Instead of storing the same physical data multiple times, a pointer is created from each logical copy to the same physical copy, saving the space of the duplicate data. Due to this, data is shared between objects, such as files or entire directories, which result in garbage collection overhead and migration challenges. In our work, we addressed the general migration problem where files are remapped between different volumes due to system expansion or maintenance. The question of which files and blocks to migrate has been extensively studied in systems without deduplication. However, only simplified migration problems have been considered in the context of deduplicated storage. As part of a migration plan, we aim to minimize the system's size while simultaneously ensuring that the storage load is evenly distributed across the volumes and that the network traffic required for the migration does not exceed its allocation. Following that, we outline a way to develop effective migration plans using hierarchical clustering. Clustering refers to grouping objects based on their similarity. Hierarchical clustering, in particular, takes the distance between those objects into account. Each object is initially clustered separately, and the process of iterative clustering merges, in each step, two clusters with a minimal distance between them. We are interested in clustering files with high similarity together in order to reduce the amount of physical data while still maintaining low network traffic and a balanced system. Based on each cluster, we calculate data savings, traffic consumed, and load balance achieved and determine the plan's quality. We show that this method has different tradeoffs between computation time and migration efficiency compared to other algorithms such as greedy and ILP (Integer Linear Programming). Our algorithm achieves almost identical results (and sometimes even better) than ILP, which, theoretically, is optimal, but in much less time.
- איזון עומסים מבוסס ILP במערכות אחסון עם דדופליקציהמנחה: Dr. Gala Yadgar
Deduplication reduces the size of the data stored in large-scale storage systems by replacing duplicate data blocks with references to their unique copies. This creates dependencies between files that contain similar content and complicates the management of data in the system. In the work presented in this seminar, we have addressed the problem of data migration, where files are remapped between different volumes because of system expansion or maintenance. The challenge of determining which files and blocks to migrate has been studied extensively for systems without deduplication. In the context of deduplicated storage, however, only simplified migration scenarios were considered. In our work we have formulated the general migration problem for deduplicated systems as an optimization problem whose objective is to minimize the system’s size while ensuring that the storage load is evenly distributed between the system’s volumes, and that the network traffic required for the migration does not exceed its allocation. We then modeled an ILP algorithm to solve the migration problem generated, and compared it’s results to two other algorithms solving the same generated migration problem: the greedy algorithm and the clustering algorithm. Our ILP algorithm manages to consistently obtain the best solutions to the problem though it requires significantly larger execution times.