Ensuring the correctness of software is both difficult and important. While the problem is undecidable in general, there is a wide range of algorithms and techniques for solving it in many practical cases. In this course we will learn how the correctness of software can be mathematically proven using automated tools called solvers. We will explore some of the algorithms these tools rely on, and also gain hands-on experience in using them. We will focus on: Boolean satisfiability (SAT) solvers, Satisfiability Modulo Theories (SMT) solvers, and Linear Programming (LP) solvers, and their applications in analyzing software through deductive reasoning, symbolic execution, and model checking. We will also learn about applying these techniques, both theoretically and practically, to ensure the correctness of software generated through machine learning.
A first-year introductory course to data structures, which covers the following topics: 1. Sorting: insertion-sort, merge-sort and quick-sort. Lower bound for comparison sorting. 2. Asymptotic analysis of running time 3. Recurrence relations, and the divide and conquer paradigm 4. Dynamic data structures 5. Heaps: implementation with an array. Heapsort algorithm 6. Binary Search Trees, AVL trees 7. Huffman Coding 7. Hashing algorithms. 8. Graph algorithms: breadth first search, depth first search (BFS, DFS), minimum spanning tree (MST), strongly connected components (SCC), topological ordering.
Formal Verification of Deep Learning Seminar (67695)
A seminar in which the students present papers that survey the field of formal verification of deep learning, including different verification methods based on constraint solving, abstract interpretation, complete and incomplete methods, and more.