Colloquia and Seminars

To join the email distribution list of the cs colloquia, please visit the list subscription page.

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

Academic Calendar at Technion site.

Upcoming Colloquia & Seminars

  • Incremental SAT solving based on analyzing previous resolution proofs.

    Ofer Guthmann, M.Sc. Thesis Seminar
    Sunday, 24.9.2017, 11:00
    Taub 601
    Prof. O. Strichman

    The majority of SAT solving applications are incremental in nature, i.e., instead of solving a single formula, a sequence of (syntactically) similar formulas are solved. In most cases the elements of the sequence are generated one after another at runtime, without a-priori knowledge of future instances. It is possible to accelerate the SAT search by using information gained from solving previous instances. Until recently, such information has been limited to sharing relevant learned clauses, as well as heuristic scores such as activity and weights. A new kind of information sharing, proposed in SAT'15 with a technique called Mining of Backbone Literals (MBL), can be used to further shorten the runtime for solving future formulas. MBL extracts backbone literals for the current formula by analyzing resolution proofs generated during the solving of previous instances in the sequence of formulas. This work starts by proposing a solution to a known open issue generally encountered in backbone literal extraction; using an increasing number of backbone literals is detrimental to further extraction of more such literals - meaning there exists a negative feedback loop regarding mining of backbone literals. Having proposed a solution that tackles this open problem, we go on to describe how to extend MBL in order to develop a new SMT-like architecture, which more thoroughly leverages knowledge gained by previous SAT solving iterations.

  • CGGC Seminar: IGATOOLS: a general purpose C++14 library for Isogeometric Analysis

    Pablo Antolin (Ecole Polytechnique F´ed´erale de Lausanne - EPFL, Switzerland)
    Monday, 25.9.2017, 14:00
    Room 337 Taub Bld.

    We present the design and the implementation of IGATOOLS [1], a C++14 general purpose library for solving PDEs using the isogeometric analysis framework [2]. The most remarkable aspect of isogeometric methods is the use of the same set of spline functions for representing the geometric domain and for describing the solution of PDEs.

    In the IGATOOLS design, the mathematical concepts of the isogeometric method and their relationships are directly mapped into classes and their interactions. This encapsulation gives flexibility to use the library in a wide range of scientific areas and applications. We provide a precise framework for a lot of loose, available information regarding the implementation of the isogeometric method, and also discuss the similarities and differences between this and the finite element method.

    The library uses advanced object oriented and generic programming techniques to ensure reusability, reliability, and maintainability of the source code. Among other capabilities, the library supports the development of dimension independent code (including manifolds and tensor-valued spaces), implements mutlithreaded methods and takes full advantage of the underlying tensor-product structure of the problem at hand (if any). The library also provides a plugin for interfacing with ParaView [3] in order to help the user to visualize the results. A bunch of code examples to illustrate the flexibility and power of the library are presented.

    Finally, new upcoming features are introduced: hierarchical B-Splines, which allows to perform local refinement; and computations in 2D and 3D trimmed domains (by using Irit [4]), in collaboration with Gershon Elber (Technion).

  • Pixel Club:On Thinning Transducer Arrays for Ultrasound Imaging using Multiplicative Beamforming

    ​​Omri Soceanu​ (EE, Technion)
    Tuesday, 26.9.2017, 11:30
    EE Meyer Building 861

    Element reduction in ultrasound transducers allows for several benefits, such asmore compact ultrasound systems and more efficient implementation of signal enhancement algorithms. However, element thinning poses two main challenges: SNR (signal to noise ratio) reduction and interference through grating lobes.

    Through the use of multiplicative beamforming in ultrasound systems, we decrease the number of processed elements in the transducer while preserving the beam pattern. Thus, we reduce the number of processed received elements by a square root factor. We improve the SNR by employing new algorithms developed for the smaller number of processed elements. Coherence factor multiplication is used for incoherent noise reduction. Strong reflectors separation allows for CNR (contrast to noise ratio) improvement. Retrospective transmit beamforming allows for improved lateral resolution. Our imaging results show improvement over full array echocardiography.

    ​*​M.Sc. research under the supervision of Prof. Moshe Porat (EE, Technion) and Dr. Zvi Friedman (GE Healthcare).

  • Complexity-Theoretic Foundations of Quantum Supremacy Experiments

    Scott Aaronson - COLLOQUIUM LECTURE
    Tuesday, 7.11.2017, 14:30
    Room 337 Taub Bld.
    University of Texas, Austin, Computer Science
    Yuval Filmus

    In the near future, there will likely be special-purpose quantum computers with 50 or so high-quality qubits. In this talk, I'll discuss general theoretical foundations for how to use such devices to demonstrate "quantum supremacy": that is, a clear quantum speedup for *some* task, motivated by the goal of overturning the Extended Church-Turing Thesis (which says that all physical systems can be efficiently simulated by classical computers) as confidently as possible. Based on recent joint work with Lijie Chen, Short Bio: ========== Scott Aaronson is David J. Bruton Centennial Professor of Computer Science at the University of Texas at Austin. He received his bachelor's from Cornell University and his PhD from UC Berkeley, and did postdoctoral fellowships at the Institute for Advanced Study as well as the University of Waterloo. Before coming to UT Austin, he spent nine years as a professor in Electrical Engineering and Computer Science at MIT. Aaronson's research in theoretical computer science has focused mainly on the capabilities and limits of quantum computers. His first book, Quantum Computing Since Democritus, was published in 2013 by Cambridge University Press. He has received the National Science Foundation's Alan T. Waterman Award, the United States PECASE Award, the Vannevar Bush Fellowship, the Simons Investigator award, and MIT's Junior Bose Award for Excellence in Teaching. ======================================== Refreshments will be served from 14:15 Lecture starts at 14:30