News 

4 papers from CENTAUR have been accepted to FMCAD 2024!

26 Sep 2024

Papers by Udayan Mandal, Ross Daly, and Rachel Cleaveland as well as a tool paper 'SMT-D: New Strategies for Portfolio-Based SMT Solving' have been accepted to FMCAD2024.

Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection
Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware

SMT tutorial paper has been selected as distinguished tutorial at FM 2024

26 Sep 2024

Satisfiability Modulo Theories: A Beginner's Tutorial by Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, and Yoni Zohar has been selected as a distinguished tutorial at the 26th International Symposium on Formal Methods located in Milan, Italy!

Satisfiability Modulo Theories: A Beginner’s Tutorial

Clark Barrett and David Dill received the CAV Award

29 Jul 2024

Clark Barrett received his second, and David Dill his third, CAV Award for developing the Reluplex algorithm!

2024 CAV award
Reluplex algorithm

Udayan Mandal received the Cristofer Stephensen Memorial Award

23 Jun 2024

Udayan Mandal has been awarded the Cristofer Stephensen Memorial Award for his master's thesis!


Ying Sheng joining UCLA

23 Jun 2024

Ying Sheng has accepted a faculty offer from UCLA!


Benjamin Przybocki received the Firestone Medal

14 Jun 2024

Benjamin Przybocki has been recognized with the Firestone Medal for his undergraduate thesis, Theoretical Aspects of Satisfiability Modulo Theories!

List of 2024 Firestone Medal winners

Benjamin Przybocki's paper accepted to FM 2024

10 Jun 2024

The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems by Benjamin Przybocki, Guilherme Toledo, Yoni Zohar, and Clark Barrett has been accepted to the 26th International Symposium on Formal Methods located in Milan, Italy!


Haoze Wu received the Centennial Teaching Assistant (CTA) Award

28 May 2024

Haoze (Andrew) Wu has been recognized with the Centennial Teaching Assistant (CTA) Award for his service as a teaching assistant (TA)!

List of 2024 CTA winners

SMT tutorial paper accepted to FM 2024

24 May 2024

Satisfiability Modulo Theories: A Beginner's Tutorial by Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds and Yoni Zohar has been accepted to the 26th International Symposium on Formal Methods located in Milan, Italy!


Nestan Tsiskaridze's paper accepted to IJCAR 2024

19 May 2024

Generalized Optimization Modulo Theories by Nestan Tsiskaridze, Clark Barrett and Cesare Tinelli has been accepted to the 12th International Joint Conference on Automated Reasoning located in Nancy, France!

Generalized Optimization Modulo Theories

Chuyue Sun and Ying Sheng's paper accepted to SAIV2024

19 May 2024

Clover: Closed-Loop Verifiable Code Generation by Chuyue Sun, Ying Sheng, Oded Padon and Clark Barrett has been accepted to the 7th International Symposium on AI Verification co-located with CAV in Montreal, Canada!

Clover: Closed-Loop Verifiable Code Generation

Pei Huang's paper accepted to SAIV2024

19 May 2024

Parallel Verification for δ-Equivalence of Neural Network Quantization by Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia and Clark Barrett has been accepted to the 7th International Symposium on AI Verification co-located with CAV in Montreal, Canada!


Haoze Wu's paper accepted to CAV2024

15 May 2024

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks by Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz and Clark Barrett has been accepted to the 36th International Conference on Computer Aided Verification located in Montreal, Canada!

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

Alex Ozdemir's paper accepted to CAV2024

15 May 2024

Split Gröbner Bases for Satisfiability Modulo Finite Fields by Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett and Işil Dillig has been accepted to the 36th International Conference on Computer Aided Verification located in Montreal, Canada!

Split Gröbner Bases for Satisfiability Modulo Finite Fields

Aina Niemetz and Mathias Preiner's paper accepted to CAV2024

15 May 2024

Scalable Bit-Blasting with Abstractions by Aina Niemetz, Mathias Preiner and Yoni Zohar has been accepted to the 36th International Conference on Computer Aided Verification located in Montreal, Canada!


Benjamin Przybocki awarded Churchill Scholarship

18 Jan 2024

Benjamin Przybocki was awarded the Churchill Scholarship for a year of independent research at Cambridge and selected as a runner-up for the Computing Research Association (CRA) Outstanding Undergraduate Research Award!

Stanford News on Churchill Scholarship
CRA Announcement

Haoze Wu joining Amherst College

04 Jan 2024

Haoze (Andrew) Wu will be joining Amherst College as an Assistant Professor in the Computer Science Department starting Fall 2024!