Courses

EECS 662 - Programming Languages

EECS 662 - Programming Languages - This course is an undergraduate introduction to programming language concepts. It is taught by implementing a collection of interpreters that implement language features. Specific topics include structuring an interpreter, abstract syntax, early and late binding, laziness and strictness, function definition and application, static an dynamic scoping, and techniques for implementing these features.

EECS 742 - Static Analysis

EECS 742 - Static Analysis - Static analysis includes tecniques used to analyze softare prior to running it. Such techniques commonly include data flow analysis, control flow analysis, abstract interpretation, and type and effect systems. This course introduces basic static analysis techniques and their application to system verification and transformation. We will discuss the theoretical basis for various techniques and develop prototype analysis tool implementations.

EECS 762 - Programming Language Foundations I

EECS 762 - Programming Language Foundations I - Programming Language Fundamentals is an introduction to the semantics of programming languages. The course will present modern approaches for defining dynamic and static semantics as well as verifying definitions and implementing interpreters. We will start with dynamic semantics defining languages using operational, denotational, and axiomatic semantics. We will then overview domain theory and being looking at static semantics and types. The course concentrates on pragmatic issues and requires both specification and verification of semantics and implementation of interpreters.

EECS 755 - Software Requirements Modeling

EECS 755 - Software Requirements Modeling - Software Requirements Modeling is an advanced introduction to modern techniques for specification, verification and implementation of software systems. Topics covered are equally useful for hardware and software verification. We will learn to write formal specifications, refine specifications and verify that implementations meet their requirements. Specific topics include axiomatic specification, invariants, algebraic types and induction, constructive specification, assume-guarantees style specification, safety and liveness, and natural deduction. Currently we use the Coq verification tool, but techniques learned apply equally well to other verification systems.

EECS 843 - Programming Language Foundations II

EECS 843 - Programming Language Foundations II - Programming Language Foundation II is an advanced introduction to programming language concepts, primarily related to type systems. Topics covered vary from one offering to the next, but typically include recursive types, universally quantified types, System F, existentially quantified types, type operations and dependent types, System F-Omega and advanced subtyping techniques. We will learn to define and verify semantics for type systems and algorithms for deciding type judgments. Programming Language Foundations I or equivalent is a hard prerequisite for this course.

EECS 800 - Decision Procedures & Model Checking

EECS 800 - Decision Procedures & Model Checking - Decision Procedures & Model Checking is an advanced introduction to decision procedures and model checking. Decision procedures are programs that take a logic problem and terminate a ‘yes’ or ‘no’ answer. They are exceptionally common in software and hardware verification, compilation, theorem proving, and model checking. Model checkers are frequently implemented with decision procedures and introduce temporal logics useful for verifying stateful systems. In this course, we will examine both theoretical and implementation issues focusing on SAT techniques, Equality, Uninterpreted Functions, Quantified Formulas, Theory Combination, LTL and CTL, explicit state modeling techniques, BDD-based modeling techniques, k-induction, safety and liveness properties, abstraction and bisimulation, and theoretical foundations.

HNRS 190 - Honors Tutorial

HNRS 190 - Honors Tutorial - The Freshman Honors Tutorial is a one hour class introducing freshman honors program students to research and KU. My section looks at the early days of computing focusing on how computing came to be and why. We look at work by the major early computing scholars and put their work in the context of World War II. We also look a that the limitations of computing and what we know about what can and cannot be computed mechanically