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.

Short Bio: Stanley Bak received his PhD from the the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC) in 2013 and then worked for several years at the Air Force Research Laboratory (AFRL) in the Verification and Validation (V&V) group of the Aerospace Systems Directorate. He received the AFOSR Young Investigator Research Program (YIP) award in 2020 and the NSF CAREER award in 2023. He is currently an assistant professor in the Department of Computer Science at Stony Brook University.

Longer Bio: 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 Verification and Validation (V&V) group 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 in 2019. He has been an assistant professor at Stony Brook University since Fall 2020, where he is affiliated with the AI institute. He received the US Air Force Office of Scientific Research (AFOSR) Young Investigator Research Program (YIP) award in 2020, and the National Science Foundation (NSF) CAREER Award in 2023.

Email: {{makeEmail()}}stonybrook.edu
CV: pdf
Google Scholar: link ({{gs_citations}} citations, h-index {{gs_hindex}} as of {{gs_date}})

Courses:
(Spring 2024) CSE 352 - Artificial Intelligence
(Fall 2023) CSE 510 - Hybrid Systems
(Fall 2021) CSE 510 - Hybrid Systems
(Fall 2021) CSE 643 - Cyber-Physical Systems Verification Seminar
(Spring 2021) CSE 510 - Hybrid Systems

---

Recent News
News by stanleybak

---

Publications
Conference Papers
Journal Articles
Other
Copyright Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

For certain papers (see notices inside): The U.S. government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. These papers were authored by an employee(s) of the United States Government and are in the public domain. Non-exclusive copying or redistribution is allowed, provided that the article citation is given and the authors and agency are clearly identified as its source.

For some of the above publications: The final publication is available at link.springer.com.

---

Program Committees

---

Grants

---

Awards

---

---

Projects

• Hylaa Reachability Tool: Hylaa is a verification tool for system models with linear ODEs, time-varying inputs, and possibly hybrid dynamics. Hylaa computes simulation-equivalent reachability, which is the set of states that can be reached by any fixed-step simulation from any initial start state (given a bounded set of start states) under any possible input (given a bounded set of possible inputs). Hylaa is able to generate counter-example traces when an error is found, and has been shown to be able to scale to systems with over 10000 dimensions.
  
  
• Hyst Model Transformation and Translation Tool: Hyst is a tool for converting hybrid automaton models from the SpaceEx input format into the formats of other tools such as Flow*, dReach, or Hylaa. Hyst can also optionally perform model transformations such as duplicatating components within a model, rescaling time, or simulation-guided hybridization. Hyst also includes the hypy python library which allows easy scripting of model transformations using Hyst and running various analysis tools.
  
  

---

Past Projects

• HyCreate Reachability Tool: Cyber-physical systems can be modeled as hybrid automata with discrete state and continuous state which interact. HyCreate is a tool for reasoning about the future behavior of systems modeled in such a fashion, which can facilitate formal reasoning.
  
  
• Verification of Complex Cyber-Physical Systems: Modern embedded and cyber-physical systems demand reliability in spite of complex behavior. Practical ways are needed to enable systems to be both complex and safe. The System-Level Simplex Architecture was developed to allow arbitrary controllers to control a plant without compromising safety.
  
  
• Network Simulator Scalability: To be feasible for simulating large networks, a network simulator must have a scalable design. The scalability of the NS2 network simulator is evaluated and contrasted to a new, FPGA-based network simulator design. The developed design is shown to scale O(log(N)) where N is number of routers.
  
  
• Verifiable VHDL Generation with VMaude: Behavior within a model checker, such as Maude, can be checked to meet some specification. Within this research, we created VMaude, a VHDL-structured Maude framework. This allows you to write Maude behavior in VMaude, perform model checking, and automatically generate the corresponding VHDL module encoding the behavior.