Das Frühjahrssemester 2021 findet grundsätzlich online statt. Neue Präsenzelemente ab 26. April werden von den Dozierenden mitgeteilt.

Suchergebnis: Katalogdaten im Frühjahrssemester 2019

Informatik Master Information
Vertiefungsfächer
Vertiefung in Information Security
Wahlfächer der Vertiefung in Information Security
NummerTitelTypECTSUmfangDozierende
252-0408-00LCryptographic Protocols Information W5 KP2V + 2UM. Hirt, U. Maurer
KurzbeschreibungThe course presents a selection of hot research topics in cryptography. The choice of topics varies and may include provable security, interactive proofs, zero-knowledge protocols, secret sharing, secure multi-party computation, e-voting, etc.
LernzielIndroduction to a very active research area with many gems and paradoxical
results. Spark interest in fundamental problems.
InhaltThe course presents a selection of hot research topics in cryptography. The choice of topics varies and may include provable security, interactive proofs, zero-knowledge protocols, secret sharing, secure multi-party computation, e-voting, etc.
Skriptthe lecture notes are in German, but they are not required as the entire
course material is documented also in other course material (in english).
Voraussetzungen / BesonderesA basic understanding of fundamental cryptographic concepts
(as taught for example in the course Information Security or
in the course Cryptography Foundations) is useful, but not required.
263-2925-00LProgram Analysis for System Security and Reliability Information W5 KP2V + 1U + 1AM. Vechev
KurzbeschreibungSecurity breaches in modern systems (blockchains, datacenters, AI, etc.) result in billions of losses. We will cover key security issues and how the latest automated techniques can be used to prevent these. The course has a practical focus, also covering systems built by successful ETH Spin-offs (ChainSecurity.com and DeepCode.ai).

More info: https://www.sri.inf.ethz.ch/teaching/pass2019
Lernziel* Learn about security issues in modern systems -- blockchains, smart contracts, AI-based systems (e.g., autonomous cars), data centers -- and why they are challenging to address.

* Understand how the latest automated analysis techniques work, both discrete and probabilistic.

* Understand how these techniques combine with machine-learning methods, both supervised and unsupervised.

* Understand how to use these methods to build reliable and secure modern systems.

* Learn about new open problems that if solved can lead to research and commercial impact.
InhaltPart I: Security of Blockchains

- We will cover existing blockchains (e.g., Ethereum, Bitcoin), how they work, what the core security issues are, and how these have led to massive financial losses.
- We will show how to extract useful information about smart contracts and transactions using interactive analysis frameworks for querying blockchains (e.g. Google's Ethereum BigQuery).
- We will discuss the state-of-the-art security tools (e.g., https://securify.ch) for ensuring that smart contracts are free of security vulnerabilities.
- We will study the latest automated reasoning systems (e.g., Dagger) for checking custom (temporal) properties of smart contracts and illustrate their operation on real-world use cases.
- We will study the underlying methods for automated reasoning and testing (e.g., abstract interpretation, symbolic execution, fuzzing) are used to build such tools.

Part II: Machine Learning for Security

- We will discuss how machine learning models for structured prediction are used to address security tasks, including de-obfuscation of binaries (Debin: https://debin.ai), Android APKs (DeGuard: http://apk-deguard.com) and JavaScript (JSNice: http://jsnice.org).
- We will study to leverage program abstractions in combination with clustering techniques to learn security rules for cryptography APIs from large codebases.
- We will study how to automatically learn to identify security vulnerabilities related to the handling of untrusted inputs (cross-Site scripting, SQL injection, path traversal, remote code execution) from large codebases.

Part III: Security of Datacenters and Networks

- We will show how to ensure that datacenters and ISPs are secured using declarative reasoning methods (e.g., Datalog). We will also see how to automatically synthesize secure configurations (e.g. using SyNET and NetComplete) which lead to desirable behaviors, thus automating the job of the network operator and avoiding critical errors.
- We will discuss how to apply modern discrete probabilistic inference (e.g., PSI and Bayonet) so to reason about probabilistic network properties (e.g., the probability of a packet reaching a destination if links fail).

Part IV: Security of AI-based Systems

- We will look into the security issues related to modern systems that combine machine learning models (e.g., neural networks) within traditional systems such as cars, airplanes, and medical systems.
- We will learn state-of-the-art techniques for security testing and certifying entire AI-based systems, such as autonomous driving systems.

To gain a deeper understanding, the course will involve a hands-on programming project where the methods studied in the class will be applied.
263-4600-00LFormal Methods for Information Security Information W4 KP2V + 1UR. Sasse, C. Sprenger
KurzbeschreibungThe course focuses on formal methods for the modelling and analysis of security protocols for critical systems, ranging from authentication protocols for network security to electronic voting protocols and online banking.
LernzielThe students will learn the key ideas and theoretical foundations of formal modelling and analysis of security protocols. The students will complement their theoretical knowledge by solving practical exercises, completing a small project, and using state-of-the-art tools.
InhaltThe course treats formal methods mainly for the modelling and analysis of security protocols. Cryptographic protocols (such as SSL/TLS, SSH, Kerberos, SAML single-sign on, and IPSec) form the basis for secure communication and business processes. Numerous attacks on published protocols show that the design of cryptographic protocols is extremely error-prone. A rigorous analysis of these protocols is therefore indispensable, and manual analysis is insufficient. The lectures cover the theoretical basis for the (tool-supported) formal modeling and analysis of such protocols. Specifically, we discuss their operational semantics, the formalization of security properties, and techniques and algorithms for their verification.

In addition to the classical security properties for confidentiality and authentication, we will study strong secrecy and privacy properties. We will discuss electronic voting protocols, and RFID protocols (a staple of the Internet of Things), where these properties are central. The accompanying tutorials provide an opportunity to apply the theory and tools to concrete protocols. Moreover, we will discuss methods to abstract and refine security protocols and the link between symbolic protocol models and cryptographic models.

Furthermore, we will also present a security notion for general systems based on non-interference as well as language-based information flow security where non-interference is enforced via a type system.
263-4630-00LComputer-Aided Modelling and Reasoning Information
In the Master Programme max. 10 credits can be accounted by Labs on top of the Interfocus Courses. Additional Labs will be listed on the Addendum.
W8 KP7PC. Sprenger, D. Traytel
KurzbeschreibungThe "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The lab has two parts: The first introduces various modelling and proof techniques. The second part consists of a project in which the students apply these techniques
LernzielThe students learn to effectively use a theorem prover to create unambiguous models and rigorously analyse them. They learn how to write precise and concise specifications, to exploit the theorem prover as a tool for checking and analysing such models and for taming their complexity, and to extract certified executable implementations from such specifications.
InhaltThe "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems supported by a theorem prover. The course will demonstrate the challenges of formal rigor, but also the benefits of machine support in modelling, proving and validating.

The lab will have two parts: The first part introduces basic and advanced modelling techniques (functional programs, inductive definitions, modules), the associated proof techniques (term rewriting, resolution, induction, proof automation), and compilation of the models to certified executable code. In the second part, the students work in teams of two on a project assignment in which they apply these techniques: they build a formal model and prove its desired properties. The project lies in the area of programming languages, model checking, or information security.
LiteraturTextbook: Tobias Nipkow, Gerwin Klein. Concrete Semantics, part 1 (www.concrete-semantics.org)
Seminar in Information Security
NummerTitelTypECTSUmfangDozierende
263-2930-00LBlockchain Security Seminar Information Belegung eingeschränkt - Details anzeigen
Number of participants limited to 22.

The deadline for deregistering expires at the end of the second week of the semester. Students who are still registered after that date, but do not attend the seminar, will officially fail the seminar.
W2 KP2SM. Vechev, D. Drachsler Cohen, P. Tsankov
KurzbeschreibungThis seminar introduces students to the latest research trends in the field of blockchains.
LernzielThe objectives of this seminar are twofold: (1) learning about the blockchain platform, a prominent technology receiving a lot of attention in computer Science and economy and (2) learning to convey and present complex and technical concepts in simple terms, and in particular identifying the core idea underlying the technicalities.
InhaltThis seminar introduces students to the latest research trends in the field of blockchains. The seminar covers the basics of blockchain technology, including motivation for decentralized currency, establishing trust between multiple parties using consensus algorithms, and smart contracts as a means to establish decentralized computation. It also covers security issues arising in blockchains and smart contracts as well as automated techniques for detecting vulnerabilities using programming language techniques.
Vertiefung in Information Systems
Kernfächer der Vertiefung in Information Systems
NummerTitelTypECTSUmfangDozierende
263-2925-00LProgram Analysis for System Security and Reliability Information W5 KP2V + 1U + 1AM. Vechev
KurzbeschreibungSecurity breaches in modern systems (blockchains, datacenters, AI, etc.) result in billions of losses. We will cover key security issues and how the latest automated techniques can be used to prevent these. The course has a practical focus, also covering systems built by successful ETH Spin-offs (ChainSecurity.com and DeepCode.ai).

More info: https://www.sri.inf.ethz.ch/teaching/pass2019
Lernziel* Learn about security issues in modern systems -- blockchains, smart contracts, AI-based systems (e.g., autonomous cars), data centers -- and why they are challenging to address.

* Understand how the latest automated analysis techniques work, both discrete and probabilistic.

* Understand how these techniques combine with machine-learning methods, both supervised and unsupervised.

* Understand how to use these methods to build reliable and secure modern systems.

* Learn about new open problems that if solved can lead to research and commercial impact.
InhaltPart I: Security of Blockchains

- We will cover existing blockchains (e.g., Ethereum, Bitcoin), how they work, what the core security issues are, and how these have led to massive financial losses.
- We will show how to extract useful information about smart contracts and transactions using interactive analysis frameworks for querying blockchains (e.g. Google's Ethereum BigQuery).
- We will discuss the state-of-the-art security tools (e.g., https://securify.ch) for ensuring that smart contracts are free of security vulnerabilities.
- We will study the latest automated reasoning systems (e.g., Dagger) for checking custom (temporal) properties of smart contracts and illustrate their operation on real-world use cases.
- We will study the underlying methods for automated reasoning and testing (e.g., abstract interpretation, symbolic execution, fuzzing) are used to build such tools.

Part II: Machine Learning for Security

- We will discuss how machine learning models for structured prediction are used to address security tasks, including de-obfuscation of binaries (Debin: https://debin.ai), Android APKs (DeGuard: http://apk-deguard.com) and JavaScript (JSNice: http://jsnice.org).
- We will study to leverage program abstractions in combination with clustering techniques to learn security rules for cryptography APIs from large codebases.
- We will study how to automatically learn to identify security vulnerabilities related to the handling of untrusted inputs (cross-Site scripting, SQL injection, path traversal, remote code execution) from large codebases.

Part III: Security of Datacenters and Networks

- We will show how to ensure that datacenters and ISPs are secured using declarative reasoning methods (e.g., Datalog). We will also see how to automatically synthesize secure configurations (e.g. using SyNET and NetComplete) which lead to desirable behaviors, thus automating the job of the network operator and avoiding critical errors.
- We will discuss how to apply modern discrete probabilistic inference (e.g., PSI and Bayonet) so to reason about probabilistic network properties (e.g., the probability of a packet reaching a destination if links fail).

Part IV: Security of AI-based Systems

- We will look into the security issues related to modern systems that combine machine learning models (e.g., neural networks) within traditional systems such as cars, airplanes, and medical systems.
- We will learn state-of-the-art techniques for security testing and certifying entire AI-based systems, such as autonomous driving systems.

To gain a deeper understanding, the course will involve a hands-on programming project where the methods studied in the class will be applied.
Wahlfächer der Vertiefung in Information Systems
NummerTitelTypECTSUmfangDozierende
252-0312-00LUbiquitous Computing Information W3 KP2VF. Mattern, S. Mayer
KurzbeschreibungUbiquitous computing integrates tiny wirelessly connected computers and sensors into the environment and everyday objects. Main topics: The vision of ubiquitous computing, trends in technology, smart cards, RFID, Personal Area Networks (Bluetooth), sensor networks, location awareness, privacy and security, application areas, economic and social impact.
LernzielThe vision of ubiquitous computing, trends in technology, smart cards, RFID, Personal Area Networks (Bluetooth), sensor networks, location awareness, privacy and security, application areas, economic and social impact.
SkriptCopies of slides will be made available
LiteraturWill be provided in the lecture. To put you in the mood:
Mark Weiser: The Computer for the 21st Century. Scientific American, September 1991, pp. 94-104
252-3005-00LNatural Language Understanding Information Belegung eingeschränkt - Details anzeigen
Number of participants limited to 200.
W4 KP2V + 1UM. Ciaramita, T. Hofmann
KurzbeschreibungThis course presents topics in natural language processing with an emphasis on modern techniques, primarily focusing on statistical and deep learning approaches. The course provides an overview of the primary areas of research in language processing as well as a detailed exploration of the models and techniques used both in research and in commercial natural language systems.
LernzielThe objective of the course is to learn the basic concepts in the statistical processing of natural languages. The course will be project-oriented so that the students can also gain hands-on experience with state-of-the-art tools and techniques.
InhaltThis course presents an introduction to general topics and techniques used in natural language processing today, primarily focusing on statistical approaches. The course provides an overview of the primary areas of research in language processing as well as a detailed exploration of the models and techniques used both in research and in commercial natural language systems.
LiteraturLectures will make use of textbooks such as the one by Jurafsky and Martin where appropriate, but will also make use of original research and survey papers.
263-5215-00LFairness, Explainability, and Accountability for Machine Learning Information Belegung eingeschränkt - Details anzeigen
Number of participants limited to 40.

The deadline for deregistering expires at the end of the second week of the semester. Students who are still registered after that date, but do not attend the course, will officially fail the course.
W4 KP1V + 2PH. Heidari
Kurzbeschreibung
Lernziel- Familiarize students with the ethical implications of applying Big Data and ML tools to socially-sensitive domains; teach them to think critically about these issues.
- Overview the long-established philosophical, sociological, and economic literature on these subjects.
- Provide students with a tool-box of technical solutions for addressing - at least partially - the ethical and societal issues of ML and Big data.
InhaltAs ML continues to advance and make its way into different aspects of modern life, both the designers and users of the technology need to think seriously about its impact on individuals and society. We will study some of the ethical implications of applying ML tools to socially sensitive domains, such as employment, education, credit ledning, and criminal justice. We will discuss at length what it means for an algorithm to be fair; who should be held responsible when algorithmic decisions negatively impacts certain demographic groups or individuals; and last but not least, how algorithmic decisions can be explained to a non-technical audience. Throughout the course, we will focus on technical solutions that have been recently proposed by the ML community to tackle the above issues. We will critically discuss the advantages and shortcomings of these proposals in comparison with non-technical alternatives.
Voraussetzungen / BesonderesStudents are expected to sufficient knowledge of ML (i.e. they must have taken the "Introduction to Machine Learning" or an equivalent course).
Seminar in Information Systems
NummerTitelTypECTSUmfangDozierende
252-3002-00LAlgorithms for Database Systems Information
Limited number of participants.

The deadline for deregistering expires at the end of the second week of the semester. Students who are still registered after that date, but do not attend the seminar, will officially fail the seminar.
W2 KP2SP. Penna
KurzbeschreibungQuery processing, optimization, stream-based systems, distributed and parallel databases, non-standard databases.
LernzielDevelop an understanding of selected problems of current interest in the area of algorithms for database systems.
263-3840-00LHardware Architectures for Machine Learning Information
The deadline for deregistering expires at the end of the second week of the semester. Students who are still registered after that date, but do not attend the seminar, will officially fail the seminar.
W2 KP2SG. Alonso, T. Hoefler, C. Zhang
KurzbeschreibungThe seminar covers recent results in the increasingly important field of hardware acceleration for data science and machine learning, both in dedicated machines or in data centers.
LernzielThe seminar aims at students interested in the system aspects of machine learning, who are willing to bridge the gap across traditional disciplines: machine learning, databases, systems, and computer architecture.
InhaltThe seminar is intended to cover recent results in the increasingly important field of hardware acceleration for data science and machine learning, both in dedicated machines or in data centers.
Voraussetzungen / BesonderesThe seminar should be of special interest to students intending to complete a master's thesis or a doctoral dissertation in related topics.
Vertiefung in Software Engineering
Kernfächer der Vertiefung in Software Engineering
NummerTitelTypECTSUmfangDozierende
263-2925-00LProgram Analysis for System Security and Reliability Information W5 KP2V + 1U + 1AM. Vechev
KurzbeschreibungSecurity breaches in modern systems (blockchains, datacenters, AI, etc.) result in billions of losses. We will cover key security issues and how the latest automated techniques can be used to prevent these. The course has a practical focus, also covering systems built by successful ETH Spin-offs (ChainSecurity.com and DeepCode.ai).

More info: https://www.sri.inf.ethz.ch/teaching/pass2019
Lernziel* Learn about security issues in modern systems -- blockchains, smart contracts, AI-based systems (e.g., autonomous cars), data centers -- and why they are challenging to address.

* Understand how the latest automated analysis techniques work, both discrete and probabilistic.

* Understand how these techniques combine with machine-learning methods, both supervised and unsupervised.

* Understand how to use these methods to build reliable and secure modern systems.

* Learn about new open problems that if solved can lead to research and commercial impact.
InhaltPart I: Security of Blockchains

- We will cover existing blockchains (e.g., Ethereum, Bitcoin), how they work, what the core security issues are, and how these have led to massive financial losses.
- We will show how to extract useful information about smart contracts and transactions using interactive analysis frameworks for querying blockchains (e.g. Google's Ethereum BigQuery).
- We will discuss the state-of-the-art security tools (e.g., https://securify.ch) for ensuring that smart contracts are free of security vulnerabilities.
- We will study the latest automated reasoning systems (e.g., Dagger) for checking custom (temporal) properties of smart contracts and illustrate their operation on real-world use cases.
- We will study the underlying methods for automated reasoning and testing (e.g., abstract interpretation, symbolic execution, fuzzing) are used to build such tools.

Part II: Machine Learning for Security

- We will discuss how machine learning models for structured prediction are used to address security tasks, including de-obfuscation of binaries (Debin: https://debin.ai), Android APKs (DeGuard: http://apk-deguard.com) and JavaScript (JSNice: http://jsnice.org).
- We will study to leverage program abstractions in combination with clustering techniques to learn security rules for cryptography APIs from large codebases.
- We will study how to automatically learn to identify security vulnerabilities related to the handling of untrusted inputs (cross-Site scripting, SQL injection, path traversal, remote code execution) from large codebases.

Part III: Security of Datacenters and Networks

- We will show how to ensure that datacenters and ISPs are secured using declarative reasoning methods (e.g., Datalog). We will also see how to automatically synthesize secure configurations (e.g. using SyNET and NetComplete) which lead to desirable behaviors, thus automating the job of the network operator and avoiding critical errors.
- We will discuss how to apply modern discrete probabilistic inference (e.g., PSI and Bayonet) so to reason about probabilistic network properties (e.g., the probability of a packet reaching a destination if links fail).

Part IV: Security of AI-based Systems

- We will look into the security issues related to modern systems that combine machine learning models (e.g., neural networks) within traditional systems such as cars, airplanes, and medical systems.
- We will learn state-of-the-art techniques for security testing and certifying entire AI-based systems, such as autonomous driving systems.

To gain a deeper understanding, the course will involve a hands-on programming project where the methods studied in the class will be applied.
Wahlfächer der Vertiefung in Software Engineering
NummerTitelTypECTSUmfangDozierende
263-2300-00LHow To Write Fast Numerical Code Information Belegung eingeschränkt - Details anzeigen
Number of participants limited to 84.

Prerequisite: Master student, solid C programming skills.

Takes place the last time in this form.
W6 KP3V + 2UM. Püschel
KurzbeschreibungThis course introduces the student to the foundations and state-of-the-art techniques in developing high performance software for mathematical functionality such as matrix operations, transforms, and others. The focus is on optimizing for a single core. This includes optimizing for the memory hierarchy, for special instruction sets, and the possible use of automatic performance tuning.
LernzielSoftware performance (i.e., runtime) arises through the complex interaction of algorithm, its implementation, the compiler used, and the microarchitecture the program is run on. The first goal of the course is to provide the student with an understanding of this "vertical" interaction, and hence software performance, for mathematical functionality. The second goal is to teach a systematic strategy how to use this knowledge to write fast software for numerical problems. This strategy will be trained in several homeworks and a semester-long group project.
InhaltThe fast evolution and increasing complexity of computing platforms pose a major challenge for developers of high performance software for engineering, science, and consumer applications: it becomes increasingly harder to harness the available computing power. Straightforward implementations may lose as much as one or two orders of magnitude in performance. On the other hand, creating optimal implementations requires the developer to have an understanding of algorithms, capabilities and limitations of compilers, and the target platform's architecture and microarchitecture.

This interdisciplinary course introduces the student to the foundations and state-of-the-art techniques in high performance mathematical software development using important functionality such as matrix operations, transforms, filters, and others as examples. The course will explain how to optimize for the memory hierarchy, take advantage of special instruction sets, and other details of current processors that require optimization. The concept of automatic performance tuning is introduced. The focus is on optimization for a single core; thus, the course complements others on parallel and distributed computing.

Finally a general strategy for performance analysis and optimization is introduced that the students will apply in group projects that accompany the course.
263-2812-00LProgram Verification Information Belegung eingeschränkt - Details anzeigen
Maximale Teilnehmerzahl: 30.
W5 KP2V + 1U + 1AA. J. Summers
KurzbeschreibungA hands-on introduction to the theory and construction of deductive software verifiers, covering both cutting-edge methodologies for formal program reasoning, and a perspective over the broad tool stacks making up modern verification tools.
LernzielStudents will earn the necessary skills for designing and developing deductive verification tools which can be applied to modularly analyse complex software, including features challenging for reasoning such as heap-based mutable data and concurrency. Students will learn both a variety of fundamental reasoning principles, and how these reasoning ideas can be made practical via automatic tools.

Students will be gain practical experience with reasoning tools at various levels of abstraction, from SAT and SMT solvers at the lowest level, up through intermediate verification languages and tools, to verifiers which target front-end code in executable languages.

By the end of the course, students should have a good working understanding and experience of the issues and decisions involved with designing and building practical verification tools, and the theoretical techniques which underpin them.
InhaltThe course will be organized around building up a "tool stack", starting at the lowest-level with background on SAT and SMT solving techniques, and working upwards through tools at progressively-higher levels of abstraction. The notion of intermediate verification languages will be explored, and the Boogie (Microsoft Research) and Viper (ETH) languages will be used in depth to tackle increasingly ambitious verification tasks.

The course will intermix technical content with hands-on experience; at each level of abstraction, we will understand who to build and use tools which can tackle specific program correctness problems, starting from simple puzzle solvers (Soduko) at the SAT level, and working upwards to full functional correctness of application-level code. This practical work will include three projects (typically worked on in pairs) spread throughout the course, which count towards the final grade. The graded projects are worth 40% in total, individually weighted at 14%, 13% and 13% respectively. The projects are a compulsory performance assessment; in this case, they need not be passed on their own, but will count 40% in all cases towards the final grading. An oral examination (worth the remaining 60% of the final grade) will examine the full technical content covered in the course.
SkriptHandouts (complementing the lecture material) and other materials will be available online.
LiteraturBackground reading material and links to tools will be published on the course website.
Voraussetzungen / BesonderesSome programming experience is essential, as the course contains several practical assignments. A basic familiarity with propositional and first-order logic will be assumed.

Courses with an emphasis on formal reasoning about programs (such as Formal Methods and Functional Programming) are advantageous background, but are not a requirement.
263-4630-00LComputer-Aided Modelling and Reasoning Information
In the Master Programme max. 10 credits can be accounted by Labs on top of the Interfocus Courses. Additional Labs will be listed on the Addendum.
W8 KP7PC. Sprenger, D. Traytel
KurzbeschreibungThe "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The lab has two parts: The first introduces various modelling and proof techniques. The second part consists of a project in which the students apply these techniques
LernzielThe students learn to effectively use a theorem prover to create unambiguous models and rigorously analyse them. They learn how to write precise and concise specifications, to exploit the theorem prover as a tool for checking and analysing such models and for taming their complexity, and to extract certified executable implementations from such specifications.
InhaltThe "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems supported by a theorem prover. The course will demonstrate the challenges of formal rigor, but also the benefits of machine support in modelling, proving and validating.

The lab will have two parts: The first part introduces basic and advanced modelling techniques (functional programs, inductive definitions, modules), the associated proof techniques (term rewriting, resolution, induction, proof automation), and compilation of the models to certified executable code. In the second part, the students work in teams of two on a project assignment in which they apply these techniques: they build a formal model and prove its desired properties. The project lies in the area of programming languages, model checking, or information security.
LiteraturTextbook: Tobias Nipkow, Gerwin Klein. Concrete Semantics, part 1 (www.concrete-semantics.org)
Seminar in Software Engineering
NummerTitelTypECTSUmfangDozierende
263-2100-00LResearch Topics in Software Engineering Information Belegung eingeschränkt - Details anzeigen
Number of participants limited to 22.

The deadline for deregistering expires at the end of the second week of the semester. Students who are still registered after that date, but do not attend the seminar, will officially fail the seminar.
W2 KP2ST. Gross
KurzbeschreibungThis seminar introduces students to the latest research trends that help to improve various aspects of software quality.

Topics cover the following areas of research: Compilers, domain-specific languages, concurrency, formal methods, performance optimization, program analysis, program generation, program synthesis, testing, tools, verification
LernzielAt the end of the course, the students should be:

- familiar with a broad range of key research results in the area as well as their applications.

- know how to read and assess high quality research papers

- be able to highlight practical examples/applications, limitations of existing work, and outline potential improvements.
InhaltThe course will be structured as a sequence of presentations of high-quality research papers, spanning both theory and practice. These papers will have typically appeared in top conferences spanning several areas such as POPL, PLDI, OOPSLA, OSDI, ASPLOS, SOSP, AAAI, ICML and others.
LiteraturThe publications to be presented will be announced on the seminar home page at least one week before the first session.
Voraussetzungen / BesonderesPapers will be distributed during the first lecture.
263-2926-00LDeep Learning for Big Code Information Belegung eingeschränkt - Details anzeigen
Number of participants limited to 24.

The deadline for deregistering expires at the end of the second week of the semester. Students who are still registered after that date, but do not attend the seminar, will officially fail the seminar.
W2 KP2SV. Raychev
KurzbeschreibungThe seminar covers some of the latest and most exciting developments (industrial and research) in the field of Deep Learning for Code, including new methods and latest systems, as well as open challenges and opportunities.
LernzielThe objective of the seminar is to:

- Introduce students to the field of Deep Learning for Big Code.

- Learn how machine learning models can be used to solve practical challenges in software engineering and programming beyond traditional methods.

- Highlight the latest research and work opportunities in industry and academia available on this topic.
InhaltThe last 5 years have seen increased interest in applying advanced machine learning techniques such as deep learning to new kind of data: program code. As the size of open source code increases dramatically (over 980 billion lines of code written by humans), so comes the opportunity for new kind of deep probabilistic methods and commercial systems that leverage this data to revolutionize software creation and address hard problems not previously possible. Examples include: machines writing code, program de-obfuscation for security, code search, and many more.

Interestingly, this new type of data, unlike natural language and images, introduces technical challenges not typically encountered when working with standard datasets (e.g., images, videos, natural language), for instance, finding the right representation over which deep learning operates. This in turn has the potential to drive new kinds of machine learning models with broad applicability.

Because of this, there has been substantial interest over the last few years in both industry (e.g., companies such as Facebook starting, various start-ups in the space such as http://deepcode.ai), academia (e.g., http://plml.ethz.ch) and government agencies (e.g., DARPA) on using machine learning to automate various programming tasks.

In this seminar, we will cover some of the latest and most exciting developments in the field of Deep Learning for Code, including new methods and latest systems, as well as open challenges and opportunities.

The seminar is carried out as a set of presentations chosen from a list of available papers. The grade is determined as a function of the presentation, handling questions and answers, and participation.
Voraussetzungen / BesonderesThe seminar is carried out as a set of presentations chosen from a list of available papers. The grade is determined as a function of the presentation, handling questions and answers, and participation.

The seminar is ideally suited for M.Sc. students in Computer Science.
263-2930-00LBlockchain Security Seminar Information Belegung eingeschränkt - Details anzeigen
Number of participants limited to 22.

The deadline for deregistering expires at the end of the second week of the semester. Students who are still registered after that date, but do not attend the seminar, will officially fail the seminar.
W2 KP2SM. Vechev, D. Drachsler Cohen, P. Tsankov
KurzbeschreibungThis seminar introduces students to the latest research trends in the field of blockchains.
LernzielThe objectives of this seminar are twofold: (1) learning about the blockchain platform, a prominent technology receiving a lot of attention in computer Science and economy and (2) learning to convey and present complex and technical concepts in simple terms, and in particular identifying the core idea underlying the technicalities.
InhaltThis seminar introduces students to the latest research trends in the field of blockchains. The seminar covers the basics of blockchain technology, including motivation for decentralized currency, establishing trust between multiple parties using consensus algorithms, and smart contracts as a means to establish decentralized computation. It also covers security issues arising in blockchains and smart contracts as well as automated techniques for detecting vulnerabilities using programming language techniques.
Vertiefung in Theoretical Computer Science
Kernfächer der Vertiefung in Theoretical Computer Science
NummerTitelTypECTSUmfangDozierende
252-0407-00LCryptography Foundations Information
Takes place the last time in this form.
W7 KP3V + 2U + 1AU. Maurer
KurzbeschreibungFundamentals and applications of cryptography. Cryptography as a mathematical discipline: reductions, constructive cryptography paradigm, security proofs. The discussed primitives include cryptographic functions, pseudo-randomness, symmetric encryption and authentication, public-key encryption, key agreement, and digital signature schemes. Selected cryptanalytic techniques.
LernzielThe goals are:
(1) understand the basic theoretical concepts and scientific thinking in cryptography;
(2) understand and apply some core cryptographic techniques and security proof methods;
(3) be prepared and motivated to access the scientific literature and attend specialized courses in cryptography.
InhaltSee course description.
Skriptyes.
Voraussetzungen / BesonderesFamiliarity with the basic cryptographic concepts as treated for
example in the course "Information Security" is required but can
in principle also be acquired in parallel to attending the course.
261-5110-00LOptimization for Data Science Information W8 KP3V + 2U + 2AB. Gärtner, D. Steurer
KurzbeschreibungThis course teaches an overview of modern optimization methods, with applications in particular for machine learning and data science.
LernzielUnderstanding the theoretical and practical aspects of relevant optimization methods used in data science. Learning general paradigms to deal with optimization problems arising in data science.
InhaltThis course teaches an overview of modern optimization methods, with applications in particular for machine learning and data science.

In the first part of the course, we will discuss how classical first and second order methods such as gradient descent and Newton's method can be adapated to scale to large datasets, in theory and in practice. We also cover some new algorithms and paradigms that have been developed specifically in the context of data science. The emphasis is not so much on the application of these methods (many of which are covered in other courses), but on understanding and analyzing the methods themselves.

In the second part, we discuss convex programming relaxations as a powerful and versatile paradigm for designing efficient algorithms to solve computational problems arising in data science. We will learn about this paradigm and develop a unified perspective on it through the lens of the sum-of-squares semidefinite programming hierarchy. As applications, we are discussing non-negative matrix factorization, compressed sensing and sparse linear regression, matrix completion and phase retrieval, as well as robust estimation.
Voraussetzungen / BesonderesAs background, we require material taught in the course "252-0209-00L Algorithms, Probability, and Computing". It is not necessary that participants have actually taken the course, but they should be prepared to catch up if necessary.
  • Erste Seite Vorherige Seite Seite  2  von  7 Nächste Seite Letzte Seite     Alle