Program

14:00	Carl Kwan, Yutong Xin and William D. Young A Formal Y86 Simulator with CHERI Features (abstract) PRESENTER: William D. Young
14:30	Raven Beutner and Bernd Finkbeiner On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information (abstract)
15:00	Christopher Johannsen, Phillip Jones, Tichakorn Wongpiromsarn and Kristin Yvonne Rozier Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding (abstract) PRESENTER: Christopher Johannsen

15:30-16:00Coffee Break

16:00-17:50 Session 11: Neural Networks and Large Language Models

Chair:

Haoze Wu

16:00	Meghan Stuart and Parasara Sridhar Duggirala Quantifying Robustness of 3D BioMedical Image Segmentation Networks Using TensorStars (abstract)
16:30	Samuel Teuber, Debasmita Lohar and Bernhard Beckert Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision (abstract) PRESENTER: Samuel Teuber
17:00	Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch and André Platzer Can Large Language Models Autoformalize Kinematics? (abstract) PRESENTER: Aditi Kabra
17:20	Amirmohammad Nazari, Matin Amini and Mukund Raghothaman "How Does my Circuit Work?": Local Explanations for the Behavior of Sequential Circuits (abstract)

Thursday, October 9th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 12: Invited Talk

Chair:

Daniela Kaufmann

09:00

Nina Narodytska

Integrating Large Language Models in Automated Program Verification (abstract)

10:00-10:30Coffee Break

10:30-12:30 Session 13: SAT and SMT

Chair:

Nikolaj Bjørner

10:30	Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli and Clark Barrett Towards SMT Solver Stability via Input Normalization (abstract) PRESENTER: Daneshvar Amrollahi
11:00	Amalee Wilson, Nina Narodytska, Clark Barrett and Haoze Wu Per-Instance Subproblem Generation for Strategy Selection in SMT (abstract) PRESENTER: Amalee Wilson
11:30	Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Marsha Chechik Solving Set Constraints with Comprehensions and Bounded Quantifiers (abstract)
12:00	Amar Shah, Twain Byrnes, Joseph Reeves and Marijn J. H. Heule Learning Short Clauses via Conditional Autarkies (abstract) PRESENTER: Amar Shah

12:30-14:00Lunch Break

14:00-15:30 Session 14: Synthesis

Chair:

Christoph Scholl

14:00	Petra Hozzová and Nikolaj Bjørner Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols (abstract) PRESENTER: Nikolaj Bjørner
14:30	Yuan Xia, Aabha Shailesh Pingle, Deepayan Sur, Srivatsan Ravi, Mukund Raghothaman and Jyotirmoy V. Deshmukh Guiding Likely Invariant Synthesis on Distributed Systems with Large Language Models (abstract) PRESENTER: Yuan Xia
15:00	Leiqi Ye, Guy Frankel, Yixuan Li, Jianyi Cheng and Elizabeth Polgreen Unlocking Hardware Verification with Oracle Guided Synthesis (abstract)

15:30-16:00Coffee Break

16:00-17:30 Session 15: Case Studies and HWMCC

Chair:

Nestan Tsiskaridze

16:00	Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward Lee and Sanjit Seshia PolyVer: A Compositional Approach for Polyglot System Modeling and Verification (abstract) PRESENTER: Pei-Wei Chen
16:30	Yahya Sohail and Warren Hunt A Method for the Verification of Memory Management Software in the Presence of TLBs (abstract) PRESENTER: Yahya Sohail
17:00	Mathias Preiner, Armin Biere and Nils Froleyks Hardware Model Checking Competition PRESENTER: Mathias Preiner

17:30-18:30 Session 16: Business Meeting

19:00-22:00 Banquet

Banquet at Domenico Winery

Friday, October 10th

View this program: with abstracts session overview talk overview

09:00-10:50 Session 17: Verification Application

Chair:

Zhen Zhang

09:00	Sewon Park and Atsushi Igarashi Making Rabbit Run for Security Verification of Networked Systems with Unbounded Loops (abstract) PRESENTER: Sewon Park
09:30	Lee Barnett, Loris D'Antoni, Amit Goel, Rami Gökhan Kıcı, Neha Rungta, Mary Southern and Chungha Sung Modeling the AWS Authorization Engine (abstract) PRESENTER: Rami Gökhan Kıcı
10:00	Jackson Melchert, Caleb Terrill, Áron Ricardo Perez-Lopez, Clark Barrett and Priyanka Raina Automated Translation Validation of a Compiler for Statically Scheduled Accelerators (abstract) PRESENTER: Jackson Melchert
10:30	Ilo Chen, Che Cheng and Jie-Hong R. Jiang Unifying DQMax#SAT and DSSAT: Polynomial-Time Reduction and Applications (abstract) PRESENTER: Ilo Chen

10:50-11:20Coffee Break

11:20-12:50 Session 18: Tools

Chair:

Mathias Preiner

11:20	Mitja Kulczynski, Kevin Lotz and Dirk Nowotka s2s: An Eager SMT Solver for Strings (abstract)
11:40	Alexis Aurandt, Kristin Yvonne Rozier and Phillip H. Jones R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor (abstract) PRESENTER: Alexis Aurandt
12:00	Alexander Konrad and Christoph Scholl FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits (abstract) PRESENTER: Alexander Konrad
12:20	Oliver Markgraf, Anthony W. Lin, Matthew Hague, Philipp Rümmer, Zhilin Wu, Denghang Hu and Artur Jeż OSTRICH: Solver for Complex String Constraints (abstract)

12:50-14:00Lunch Break

14:00-15:20 Session 19: Software Verification

Chair:

Mitesh Jain

14:00	Matthew Sotoudeh and Zachary Yedidia Automated Formal Verification of a Software Fault Isolation System (abstract) PRESENTER: Matthew Sotoudeh
14:20	Aaron Tomb and Anjali Joshi Static Coverage in Deductive Software Verification (abstract) PRESENTER: Aaron Tomb
14:50	Joseph Tafese, Siddharth Priya, Giuliano Losa, Arie Gurfinkel and Graydon Hoare A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SeaBMC (abstract) PRESENTER: Joseph Tafese

15:20-15:25 Session 20: Closing