Prof. Somenzi's research is concerned with the design and verification of digital and cyberphysical systems. Deciding whether an artifact satisfies a specification is computationally hard. Yet, it is vital, given society's reliance on electronic systems. Model checking is an algorithmic approach to verification. Prof. Somenzi's group has developed model checkers that have pioneered many techniques and have been widely adopted. They have developed software for decision diagrams that is adopted in fields that go from electronic design automation to compilers to computer algebra. Decision procedures for propositional logic are used by computers to perform various forms of reasoning. Prof. Somenzi and his group have found ways to increase their deductive power. Game theory and machine learning can be applied to synthesize hardware or programs. Prof. Somenzi's group has developed efficient techniques used for this task.
keywords
Formal methods for the verification of digital systems, model checking, efficient decision procedures for propositional and first-order logic, binary decision diagrams, automata theory, temporal logic, game theory, synthesis of reactive systems from logical specifications, cyberphysical systems, reinforcement learning
CSCI 5135 - Computer-Aided Verification
Primary Instructor
-
Fall 2019 / Fall 2020 / Fall 2021 / Fall 2022 / Fall 2023 / Fall 2024
Covers two-level and multilevel minimization, optimization via expert systems, algebraic and Boolean decomposition, layout methodologies, state assignment, encoding and minimization, silicon compilation. Recommended prerequisites: ECEN 2703 and general proficiency in discrete mathematics and programming. Same as ECEN 5139.
ECEN 1310 - Introduction to C Programming
Primary Instructor
-
Fall 2018 / Fall 2020
This introductory programming course teaches fundamental concepts using the C programming language. The class generally meets programming requirements for majors within the engineering school and assumes no prior programming experience. Includes a weekly computer lab session. Covered topics include pointers, control flow, dynamic memory, and abstract data types. Recommended co-requisite: APPM 1350 or equivalent. Degree credit not granted for this course and CSCI 1300 or CSPB 1300.
ECEN 2310 - Programming with Mathematical Software
Primary Instructor
-
Fall 2018 / Spring 2019
Applies mathematical software to the solution of engineering applications, using numerical and symbolic techniques. Typical applications include the manipulation of acoustic signals and the study of the dynamics of simple continuous and discrete systems.
ECEN 2350 - Digital Logic
Primary Instructor
-
Fall 2021
Covers the design and applications of digital logic circuits, including both combinational and sequential logic circuits. Introduces hardware descriptive language, simulating and synthesis software, and programming of field programmable arrays (FPGAs). This course is 3 lectures and 1 lab per week.
ECEN 2703 - Discrete Mathematics for Computer Engineers
Primary Instructor
-
Spring 2019 / Fall 2019 / Spring 2020 / Spring 2021 / Spring 2022 / Fall 2022 / Spring 2023 / Fall 2023 / Spring 2024 / Fall 2024
Emphasizes elements of discrete mathematics appropriate for computer engineering. Topics: logic, proof techniques, algorithms, complexity, relations, and graph theory.
ECEN 5139 - Computer-Aided Verification
Primary Instructor
-
Fall 2019 / Fall 2020 / Fall 2021 / Fall 2022 / Fall 2023 / Fall 2024
Covers theoretical and practical aspects of verification of finite-state systems (hardware) and infinite-state systems (programs). Model checking: temporal logics, explicit-state and symbolic search, BDDs. Constraint solvers: SAT solvers, decision procedures. Program verification: invariants, partial vs. total correctness, abstraction. Recommended prerequisite: CSCI 2824. Department enforced requisite: general proficiency in discrete mathematics and programming. Same as CSCI 5135.
