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 and to combine them with natural language processing techniques to improve AI explainability. 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, neurosymbolic approaches to explainable artificial intelligence.
Assume-Guarantee Reinforcement Learning.
Proceedings of the ... AAAI Conference on Artificial Intelligence. AAAI Conference on Artificial Intelligence.
21223-21231.
2024
Omega-Regular Decision Processes.
Proceedings of the ... AAAI Conference on Artificial Intelligence. AAAI Conference on Artificial Intelligence.
21125-21133.
2024
Reinforcement Learning and Formal Requirements.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
26-41.
2019
A hybrid algorithm for LTL games.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
309-+.
2008
GrCUs: A hybrid satistiability solver.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
211-223.
2005
Minimal assignments for bounded model checking.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
31-45.
2004
On complementing nondeterministic Buchi automata.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
96-110.
2003
The charme of abstract entities.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
2-2.
2003
Analysis of symbolic SCC Hull algorithms.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
88-105.
2002
Fate and free will in error traces.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
445-459.
2002
Hints to accelerate symbolic traversal.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
250-264.
1999
Modular verification of multipliers.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
49-63.
1996
