• 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
    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
    Introduces fundamental programming concepts with engineering applications using C at a lower level of abstraction and MATLAB at a higher, application-focused level. Teaches the use of pointers, control flow, and data types. Example engineering applications include signal processing and the numerical computations. 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 / Fall 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 2703 - Discrete Mathematics for Computer Engineers
    Primary Instructor - Spring 2019
    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
    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.

Background

International Activities