• Contact Info
Publications in VIVO
 

Somenzi, Fabio

Professor

Positions

Research Areas research areas

Research

research overview

  • 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

Publications

selected publications

Teaching

courses taught

  • CSCI 5135 - Computer-Aided Verification
    Primary Instructor - Fall 2019 / Fall 2020 / Fall 2021 / Fall 2022 / Fall 2023
    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 1030 - Special Topics
    Primary Instructor - Spring 2018
    Special topics class.
  • ECEN 1310 - C Programming for ECE
    Primary Instructor - Fall 2018 / Fall 2020
    Introduces fundamental programming concepts using the C language. Teaches the use of pointers, control flow, aggregate types, input/output, heap-allocated memory, and abstract data types. Includes a weekly computer lab session. Recommended prerequisite: APPM 1350. Degree credit not granted for this course and CSCI 1300 or CSPB 1300 or CSCI 1310 or CSCI 1320.
  • 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 ciruits. Introduces hardware descriptive language, simulating and synthesis software, and programming of field programmable arrays (FPGAs).
  • 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
    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
    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.

Background

International Activities

Other Profiles