Teaching
CIS 301: Logical Foundations of Programming
This course teaches the basic elements found in a formal logic including syntax for claims and rules for making deductions, as well as on how to judge if the rules are suitable in the sense that they only lead to claims that match the reality of the domain that are being reasoned. The focus will be on formal logics for reasoning about program behavior.
CIS 855: High Assurance Systems
This course is about model-based development of high-assurance systems. It covers the AADL modeling language, the SAnToS Lab HAMR tool, and extended examples of high-assurance systems including an infant incubator and Patient-Controlled Analgesia (PCA) pump.
CIS 771: Software Specifications
The course teaches a collection of techniques that lie at the foundation of an approach to software development that can enable the construction of large highly reliable software. That foundation is specification of the precise meaning of the execution behavior of software. The techniques covered span the development process ranging from high-level semantic modeling, to system architecture design, and to coding and debugging.
CIS 842: Specification and Verification of Reactive Systems
This course studies various model-checking techniques with the goal of applying those techniques to real concurrent software systems.