Convergence

Regular Expressions from Axioms

Induction

Propositional Encodings

SAT Certificates

Contracts

Dynamic Logic

DPLL

Blasting & Quantifiers

Data structure

Compositional Reasoning

Predicate transformer semantics

Sound Transformations

Temporal logic

Ghosts

Loops

Sequent Calculus

Satisfiability Modulo Theories (SMT)

Semantics

Array (data structure)

Resolution

Equality and Arrays

15-414 Bug Catching: Automated Program Verification Carnegie Mellon University Spring 2022 This course is about software verification, with the goal of writing bug-free code. Students will learn to formalize program correctness, write verified code, and use automated tools for verification. It explores the principles behind verification tools, logical specifications, and deductive reasoning. Previous knowledge in program correctness reasoning is beneficial. High-profile bugs continue to plague the software industry, leading to major problems in the reliability, safety, and security of systems. This course teaches students how to write bug-free code through the process of software verification, which aims to prove the correctness of a program with respect to a mathematical specification. Along the way, students will learn how to:

- Specify correct program behavior
- Prove the correctness of their code
- Use formal semantics to reason about the soundness of proof rules
- Write practical and efficient verified code
- Use decision procedures and model checkers to reduce verification effort

Students will learn the principles and algorithms behind automated verification tools, and understand their practical limitations while gaining experience writing verified, machine-checked code that solves real problems. **Identify and formalize program correctness.** In order to reason about the existence of bugs in code, and ultimately justify their absence, we need to state what it means for the code to be correct. Students will learn how to formalize correctness using logical specifications that give precise meaning to the program's intended behavior.

**Understand how to write correct software from the ground up.** Writing good specifications of program correctness is essential to showing that there aren't any bugs in the code, but it is also useful for writing good code from the start. Students will develop experience reasoning about correctness as they implement functionality, learning how to write code that establishes and preserves properties and invariants needed to meet a target specification.

**Apply rigorous reasoning to program correctness.** Program verification is the process of mathematically proving that all possible behaviors of a given program adhere to its specification. Students will learn how to use deductive reasoning and state space exploration to realize this goal, and gain experience verifying their own code against logical correctness specifications.

**Learn to use automated tools to aid in verification.** Formally verifying real code is challenging, but given the scale of modern software, can also be tedious and labor-intensive. A number of tools exist for automating key parts of the verification process, notably deductive verification tools and model checkers. Students will learn how to use these tools when developing correct software, and gain experience applying them to non-trivial implementations.

**Understand how verification tools work.** Verification tools are not perfect, and will never be able to scale universally to all software development needs. Understanding the principles and techniques that these tools use is necessary for evaluating when it is appropriate to use a particular tool, and for addressing a tool's limitations when they arise in practice.  There is no textbook for this class, and detailed lecture notes will be posted to the website within a few days after each class. Keep in mind that lecture notes may not contain everything we cover in class. Comments and corrections are welcome, please give them to the course staff on Piazza.

15-414 Bug Catching: Automated Program Verification

Software Engineering

Connectionist Machines

McCullough and Pitt model

Hebb’s learning rule

Rosenblatt’s perceptron

Universal Approximator

Neural network

Perceptron learning rule

Empirical risk minimization

Optimization

Gradient descent

Back-propagation

Momentum

Nestorov

Learning Rates

Optimization Algorithms

RMSProp

Stochastic gradient descent (SGD)

Acceleration

Overfitting

Regularization (mathematics)

Convolutional neural network (CNN)

Translation Invariance

Cascade Correlation Filters

Recurrent neural network (RNN)

Bidirectional RNNs

Sequence Prediction

Long Short-Term Memory (LSTM)

Connectionist Temporal Classification (CTC)

Representations

Autoencoders

Hopfield Networks

Boltzmann Machines

Normalizing Flows

Variational autoencoder (VAE)

Generative adversarial network (GAN)

Reinforcement learning (RL)

Multi-layer Perceptron

Sequence-to-sequence (Seq2Seq)

AdaGrad

11-785 Introduction to Deep Learning Carnegie Mellon University Spring 2020 This course provides a comprehensive introduction to deep learning, starting from foundational concepts and moving towards complex topics such as sequence-to-sequence models. Students gain hands-on experience with PyTorch and can fine-tune models through practical assignments. A basic understanding of calculus, linear algebra, and Python programming is required. “Deep Learning” systems, typified by deep neural networks, are increasingly taking over all AI tasks, ranging from language understanding, and speech and image recognition, to machine translation, planning, and even game playing and autonomous driving. As a result, expertise in deep learning is fast changing from an esoteric desirable to a mandatory prerequisite in many advanced academic settings, and a large advantage in the industrial job market.

In this course we will learn about the basics of deep neural networks, and their applications to various AI tasks. By the end of the course, it is expected that students will have significant familiarity with the subject, and be able to apply Deep Learning to a variety of tasks. They will also be positioned to understand much of the current literature on the topic and extend their knowledge through further study.

If you are only interested in the lectures, you can watch them on the YouTube channel listed below.

### Course description from student point of view

The course is well rounded in terms of concepts. It helps us understand the fundamentals of Deep Learning. The course starts off gradually with MLPs and it progresses into the more complicated concepts such as attention and sequence-to-sequence models. We get a complete hands on with PyTorch which is very important to implement Deep Learning models. As a student, you will learn the tools required for building Deep Learning models. The homeworks usually have 2 components which is Autolab and Kaggle. The Kaggle components allow us to explore multiple architectures and understand how to fine-tune and continuously improve models. The task for all the homeworks were similar and it was interesting to learn how the same task can be solved using multiple Deep Learning approaches. Overall, at the end of this course you will be confident enough to build and tune Deep Learning models.  1. We will be using one of several toolkits (the primary toolkit for recitations/instruction is PyTorch). The toolkits are largely programmed in Python. You will need to be able to program in at least one of these languages. Alternately, you will be responsible for finding and learning a toolkit that requires programming in a language you are comfortable with,
1. You will need familiarity with basic calculus (differentiation, chain rule), linear algebra and basic probability. ### Course description from student point of view

The course is well rounded in terms of concepts. It helps us understand the fundamentals of Deep Learning. The course starts off gradually with MLPs and it progresses into the more complicated concepts such as attention and sequence-to-sequence models. We get a complete hands on with PyTorch which is very important to implement Deep Learning models. As a student, you will learn the tools required for building Deep Learning models. The homeworks usually have 2 components which is Autolab and Kaggle. The Kaggle components allow us to explore multiple architectures and understand how to fine-tune and continuously improve models. The task for all the homeworks were similar and it was interesting to learn how the same task can be solved using multiple Deep Learning approaches. Overall, at the end of this course you will be confident enough to build and tune Deep Learning models.

11-785 Introduction to Deep Learning

Deep Learning

Convergence

2 courses cover this concept

15-414 Bug Catching: Automated Program Verification

11-785 Introduction to Deep Learning