What comes after today's large language models and deep neural networks? Join the Computing Community Consortium (CCC) for a virtual 30-min community chat led by David Jensen, CCC Council Member and lead author of the new CCC whitepaper, Envisioning Possible Futures for AI Research. Jensen will explore paradigm-shifting AI Research Futures like Neuro-Symbolic, Embodied, Multi-Agent, and Quantum AI, and then open the floor to the audience for an engaging Q&A discussion.

Register here.

Topic: AI Seminar: Stanley Bak
Time: Monday Nov 1, 2021 12:00 PM Eastern Time (US and Canada)

Join Zoom Meeting
https://stonybrook.zoom.us/j/91227496273?pwd=M3EyUDlzK3Vzd2pDOGpDU1ZjN0k1UT09

Abstract: The field of formal verification has traditionally looked at proving properties about finite state machines or software programs. The surge in deep learning has been accompanied by a surge of progress in trying to apply mathematical and algorithmic techniques to prove things about the function being computed by a neural network.

This talk formalizes the neural network verification problem and describes technical methods for neural network verification based on reachability analysis. Improvements to analysis efficiency will be given, as well as research directions for further exploration. We also include an objective comparison performed this last summer trying to evaluate the best existing verification methods in terms of speed and network size. The competition was performed on common hardware and involved the participation of twelve international teams (the tool authors) on a common set of benchmarks. 

Biography: Stanley Bak is an assistant professor in the Department of Computer Science at Stony Brook University investigating the verification of autonomy, cyber-physical systems, and neural networks. He strives to develop practical formal methods that are both scalable and useful, which demands developing new theory, programming efficient tools and building experimental systems.
Stanley Bak received a Bachelor's degree in Computer Science from Rensselaer Polytechnic Institute (RPI) in 2007 (summa cum laude), and a Master's degree in Computer Science from the University of Illinois at Urbana-Champaign (UIUC) in 2009. He completed his PhD from the Department of Computer Science at UIUC in 2013. He received the Founders Award of Excellence for his undergraduate research at RPI in 2004, the Debra and Ira Cohen Graduate Fellowship from UIUC twice, in 2008 and 2009, and was awarded the Science, Mathematics and Research for Transformation (SMART) Scholarship from 2009 to 2013. From 2013 to 2018, Stanley was a Research Computer Scientist at the US Air Force Research Lab (AFRL), both in the Information Directorate in Rome, NY, and in the Aerospace Systems Directorate in Dayton, OH. He helped run Safe Sky Analytics, a research consulting company investigating verification and autonomous systems, and performed teaching at Georgetown University before joining Stony Brook University as an assistant professor in Fall 2020.
Join librarian Christine Fena for an interactive workshop that invites you to explore AI tools firsthand, not just as users, but as critical investigators. Through playful experimentation and collaborative discovery, you'll uncover inherent biases, probe algorithmic flaws, and gain a deeper understanding of AI's limitations and societal impacts.

Location: Melville Library, Central Reading Room, Lab B

https://library.stonybrook.edu/library-events/critiquing-ai/

Join the Department of Biomedical Informatics for an exclusive fall semester programming bootcamp. Discover essential programming, data analytics, and machine learning skills crucial for biomedical informatics. Special topics such as Bioinformatics and NLP will be briefly covered.

Gain hands-on programming experience and discover diverse career opportunities in biomedical informatics.

Don't miss this chance to excel in healthcare data analytics and shape the future of the industry.

https://bmi.stonybrookmedicine.edu/Bootcamp/Bootcamp-Fall-2025

Location: NCS 120

The Art Department is hosting a guest artist exhibition, featuring the work of Young Maeng. The Opening Reception will be held on October 10th at 5 PM. Additionally, Young Maeng will be giving a talk on 'AI and Painting' on Oct 9 at 4:30 PM at the Future Histories Studio. Exhibition Location: Gallery Unbound, 3rd Floor, Staller Center, Stony Brook University

Stony Brook University Libraries invites students, faculty, & staff to join a conversation about how AI is transforming the private sector workforce. As AI tools move from experimentation to everyday business use, companies are rethinking roles, skill sets, leadership, and long-term strategy. This discussion-based event will focus on the fast-paced changes and directions at tech companies and their possible impact. This event will be particularly relevant for students preparing for an AI influenced job market and how to position themselves for opportunities in a rapidly evolving professional landscape.

The discussion will be led by Tariq Khan, Senior Director of Private Cloud Solutions at Hewlett Packard Enterprise. Tariq is a technology leader and architect with experience across private cloud, hybrid cloud, and data center platforms. He is responsible for shaping the technology architecture and strategic direction of HPE's Private Cloud offerings across on premises and cloud integrated environments.

Light refreshments will be served.


Location: Melville Library, NRR, Learning Lab
Hyperscale Verification in Microsoft Azure talk by Nikolaj Bjorner

Abstract: Cloud providers are increasingly embracing network verification for managing complex datacenter network infrastructure. Microsoft's Azure cloud infrastructure integrates the SecGuru tool, which leverages the Z3 Satisfiability Modulo Theories solver, for checking network access
control lists. It also integrates a verifier that uses both custom verification algorithms and Z3 that checks correctness of forwarding tables in Azure data-centers. These tools assure that the network is configured to preserve desired intent over hundreds of thousands of network devices. We describe our experiences building and running SecGuru for network verification in Azure.

Finally we mention recent advances in Z3, including a distributed version of Z3 that scales with Azure's elastic cloud. It integrates recent advances in lookahead and distributed SAT solving for Z3's
engines for SMT. A different recent advance includes integration of DNNs to learn variable branching strategies for high-performance SAT solvers, including MiniSAT, Glucose and Z3's SAT solver.

Bio: Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS in 2014, and test of time award at ETAPS 2018. Together with Leonardo de Moura received the CADE 2019 Herbrand award for contributions to SMT and applications. Previously, he developed the DFSR, Distributed File System - Replication, and Remote Differential
Compression protocols, RDC, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup, and program synthesis and transformation systems at the Kestrel Institute. He received his Master's and PhD degrees in computer science from Stanford University.