Search result: Catalogue data in Spring Semester 2018
|Computer Science Master|
|Focus Courses in Software Engineering|
|Focus Elective Courses Software Engineering|
|263-2812-00L||Program Verification |
Number of participants limited to 30.
|W||5 credits||2V + 1U + 1A||A. J. Summers|
|Abstract||A 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.|
|Objective||Students 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.
|Content||The 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 build small tools on top 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 mini-projects (each worth 10% of the final grade) spread throughout the course, which count towards the final grade. An oral examination (worth 70% of the final grade) will cover the technical content covered.
|Lecture notes||Slides and other materials will be available online.|
|Literature||Background reading material and links to tools will be published on the course website.|
|Prerequisites / Notice||Some 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-2300-00L||How To Write Fast Numerical Code |
Does not take place this semester.
Number of participants limited to 84.
Prerequisite: Master student, solid C programming skills.
|W||6 credits||3V + 2U||M. Püschel|
|Abstract||This course introduces the student to the foundations and state-of-the-art techniques in developing high performance software for numerical functionality such as linear algebra and others. The focus is on optimizing for the memory hierarchy and for special instruction sets. Finally, the course will introduce the recent field of automatic performance tuning.|
|Objective||Software performance (i.e., runtime) arises through the interaction of algorithm, its implementation, and the microarchitecture the program is run on. The first goal of the course is to provide the student with an understanding of this interaction, and hence software performance, focusing on numerical or mathematical functionality. The second goal is to teach a general systematic strategy how to use this knowledge to write fast software for numerical problems. This strategy will be trained in a few homeworks and semester-long group projects.|
|Content||The 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 software development using important functionality such as linear algebra functionality, transforms, filters, and others as examples. The course will explain how to optimize for the memory hierarchy, take advantage of special instruction sets, and, if time permits, how to write multithreaded code for multicore platforms. Much of the material is based on state-of-the-art research.
Further, a general strategy for performance analysis and optimization is introduced that the students will apply in group projects that accompany the course. Finally, the course will introduce the students to the recent field of automatic performance tuning.
- Page 1 of 1