Program
Monday, October 23th (VSTTE)
The program is available here: VSTTE Program
Tuesday, October 24th
| Session | Time | Authors | Title |
|---|---|---|---|
| Tuesday, October 24th | |||
| Registration | 8:15 AM - 9:00 AM | ||
| Tutorial - Katherine Kosaian |
9:00 AM - 10:30 AM | Peter J. Stuckey | MiniZinc for Formal Methods |
| break | 10:30 AM - 11:00 AM | ||
| Tutorial - Karem Sakallah |
11:00 AM - 12:30 PM | Shaowei Cai | Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT |
| lunch | 12:30 PM - 2:00 PM | ||
| Tutorial - Christopher Johannsen |
2:00 PM - 3:30 PM | The NSF:CCRI Project Investigators (Rozier, Shankar, Tinelli, Vardi) | Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community |
| break | 3:30 PM - 4:00 PM | ||
| Tutorial - Kristin Y. Rozier |
4:00 PM - 5:30 PM | David Swartwout | NASA’s core Flight System Framework Overview / Tutorial |
| Evening Reception | 5:30 PM - | ||
Welcome Reception at Alluvial Brewery:
- 5:45 PM: First Bus Leave from Reiman Gardens*
- 6:00 PM: Fisrt Bus Arrival to Alluvial
- 6:00 – 8:00 PM: Food
- 9:00 PM: Last Bus Leave from Alluvial*
- 9:25 PM: Last Bus Arrival to Reiman Gardens
- 9:35 PM: Last Bus Arrival to Gateway Hotel
*The Bus will make loops back and forth to make sure everyone can get to Alluvial or come back from Reception
Wednesday, October 25th
| Session | Time | Authors | Title |
|---|---|---|---|
| Wednesday, October 25th | |||
| Keynote | 9:00 AM - 10:00 AM | Bettina Könighofer | Formal Methods for Trusted AI |
| break | 10:00 AM - 10:30 AM | ||
| 10:30 AM - 10:55 AM | Bassan, Shahaf; Amir, Guy; Corsi, Davide; Refaeli, Idan; Katz, Guy | Formally Explaining Neural Networks within Reactive Systems | |
| NN/ML - Clark Barrett |
10:55 AM - 11:20 AM | Wu, Haoze; Hahn, Christopher; Lonsing, Florian; Mann, Makai; Ramanujan, Raghuram; Barrett, Clark | Lightweight Online Learning for Sets of Related Problems in Automated Reasoning |
| 11:20 AM - 11:45 AM | Elsaleh, Raya; Katz, Guy | Delta-Debugging Neural Network Verifiers | |
| Student Forum Lightning Talks - Andrew Wu & Andy Reynolds |
11:45 AM - 12:30 PM | ||
| lunch | 12:30 AM - 1:15 PM | ||
| 1:15 PM - 1:40 PM | Yu, Emily; Froleyks, Nils; Biere, Armin; Heljanko, Keijo | Towards Compositional Hardware Model Checking Certification | |
| 1:40 PM - 2:05 PM | Tafese, Joseph; Gurfinkel, Arie; Garcia-Contreras, Isabel | Btor2MLIR: A Format for Hardware Verification | |
| MC - Christoph Sticksel |
2:05 PM - 2:30 PM | Thakkar, Arkesh H; D’Souza, Deepak | Data-Driven Learning of Strong Conjunctive Invariants |
| 2:30 PM - 2:55 PM | Bhat, Shreesha G.; Nagar, Kartik | Automating Cutoff-based Verification of Distributed Protocols | |
| 2:55 PM - 3:10 PM | Marmanis, Iason; Vafeiadis, Viktor | Optimal Bounded Partial Order Reduction | |
| break | 3:10 PM - 3:40 PM | ||
| 3:40 PM - 4:05 PM | Coward, Samuel; Morini, Emiliano; Tan, Bryan; Drane, Theo; Constantinides, George | Datapath Verification via Word-Level E-Graph Rewriting | |
| Hardware - Georg Weissenbacher |
4:05 PM - 4:30 PM | Tollec, Simon; Asavoae, Mihail; Couroussé, Damien; Heydemann, Karine; Jan, Mathieu | µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections |
| 4:30 PM - 4:55 PM | Ryan, Kaki; Sturton, Cynthia | Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs | |
| 4:55 PM - 5:20 PM | Pastva, Samuel; Henzinger, Thomas | Binary decision diagrams on modern hardware | |
| Business Meeting | 5:30 PM - 6:30 PM | ||
| Dinner at Aunt Maude’s (invitation only) |
6:30 PM - | ||
Dinner at Aunt Maude’s (invitation only):
- 6:45 PM: Bus Leave from Reiman Gardens
- 7:00 PM: Bus Arrival to Aunt Maude’s
- 7:00 – 9:00 PM: Dinner
- 9:00 PM: Bus Leave from Aunt Maude’s
- 9:15 PM: Bus Arrival to Reiman Gardens
- 9:30 PM: Bus Arrival to Gateway Hotel
| Bus Shuttle | Departure Time | Arrival Time |
|---|---|---|
| Reiman Gardens | 6:45 PM | - |
| Aunt Maude’s | - | 7:00 PM |
| - | - | - |
| Aunt Maude’s | 9:00 PM | - |
| Reiman Gardens | - | 9:15 PM |
| Gateway Hotel | - | 9:30 PM |
Thursday, October 26th
| Session | Time | Authors | Title |
|---|---|---|---|
| Thursday, October 26th | |||
| Keynote - Natarajan Shankar |
9:00 AM - 10:00 AM | Maria Paola Bonacina | Reasoning about quantifiers in SMT: the QSMA algorithm |
| break | 10:00 AM - 10:30 AM | ||
| 10:30 AM - 10:55 AM | Kiesl-Reiter, Benjamin; Whalen, Michael W | Proofs for Incremental SAT with Inprocessing | |
| 10:55 AM - 11:20 AM | Codel, Cayden R; Avigad, Jeremy; Heule, Marijn J.H. | Verified Encodings for SAT Solvers | |
| SAT - Clark Barrett |
11:20 AM - 11:45 AM | Sakallah, Karem A; Fazekas, Katalin; Goel, Aman | SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols |
| 11:45 AM - 12:00 PM | Froleyks, Nils; Yu, Emily; Biere, Armin | BIG Backbones | |
| lunch | 12:00 PM - 12:45 PM | ||
| Poster Presentation | 12:45 PM - 1:30 PM | ||
| 1:30 PM - 1:55 PM | Li, Bohan; Cai, Shaowei | Local Search For SMT On Linear and Multilinear Real Arithmetic | |
| 1:55 PM - 2:20 PM | Zhou, Yi; Bosamiya, Jay; Takashima, Yoshiki; Li, Jessica G; Heule, Marijn J.H.; Parno, Bryan | Mariposa: Measuring SMT Instability in Automated Program Verification | |
| SMT - Christoph Sticksel |
2:20 PM - 2:45 PM | Mohamed, Abdalrhman M; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare | A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery |
| 2:45 PM - 3:10 PM | Wilson, Amalee D; Noetzli, Andres P; Reynolds, Andrew; Cook, Byron; Tinelli, Cesare; Barrett, Clark | Partitioning Strategies for Distributed SMT Solving | |
| break | 3:10 PM - 3:40 PM | ||
| 3:40 PM - 4:05 PM | Larraz, Daniel; Lorch, Robert M; Yahyazadeh, Moosa; Arif, M. Fareed; Chowdhury, Omar; Tinelli, Cesare | CRV: An Automated Resiliency Reasoner for System Design Models | |
| Avionics - Michael Whalen |
4:05 PM - 4:30 PM | Meng, Baoluo; Debnath, Joyanta; Varanasi, Sarat Chandra; Manolios, Emmanuel; Durling, Michael; Paul, Saswata; Prince, Daniel; Alsabbagh, Saif; Haadsma, Richard; McMillan, Craig; Zhang, Chi; Oates, Tim | Towards a Correct-by-Construction Design of Integrated Modular Avionics |
| 4:30 PM - 4:55 PM | Zhang, Changjian; Dardik, Ian; Meira-Góes, Rômulo; Garlan, David; Kang, Eunsuk | Fortis: A Tool for Analysis and Repair of Robust Software Systems | |
| 4:55 PM - 5:20 PM | Bernardes Fernandes Ferreira, Nikson; Moscato, Mariano M; Titolo, Laura; Ayala-Rincon, Mauricio | A provably correct floating-point implementation of Well Clear Avionics Concepts | |
| Salisbury House and Gardens | 5:30 PM - | ||
Salisbury House and Gardens:
- 5:30 PM: Bus Leave from Reiman Gardens (bus will depart as close to 5:30 as possible)
- 6:15 PM: Bus Arrival to Salisbury House & Gardens
- 6:15 PM: Self guided tours
- 7:00 – 8:00 PM: Dinner Service
- 9:00 PM: Bus Leave from Salisbury House & Gardens
- 10:00 PM: Bus Arrival to Gateway Hotel
- 10:15 PM: Bus Arrival to Reiman Gardens
| Bus Shuttle | Departure Time | Arrival Time |
|---|---|---|
| Reiman Gardens | 5:30 PM | - |
| Salisbury House & Gardens | - | 6:15 PM |
| - | - | - |
| Salisbury House & Gardens | 9:00 PM | - |
| Gateway Hotel | - | 10:00 PM |
| Reiman Gardens | - | 10:15 PM |
Friday, October 27th
| Session | Time | Authors | Title |
|---|---|---|---|
| Friday, October 27th | |||
| Keynote | 9:00 AM - 10:00 AM | Kuldeep Meel | Distribution Testing: The New Frontier for Formal Methods |
| break | 10:00 AM - 10:30 AM | ||
| 10:30 AM - 10:55 AM | Dong, Ning; Guanciale, Roberto; Dam, Mads; Lööw, Andreas | Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor | |
| Security & Synthesis - Georg Weissenbacher |
10:55 AM - 11:20 AM | Park, Kanghee; Johnson, Keith J C; D’Antoni, Loris; Reps, Thomas | Modular System Synthesis |
| 11:20 AM - 11:35 AM | Godbole, Adwait; Ye, Leiqi; Manerkar, Yatin A.; Seshia, Sanjit A. | Modelling and Verification of Security-Oriented Resource Partitioning Schemes | |
| Poster Presentation | 11:35 AM - 12:35 PM | ||
| short lunch | 12:35 PM - 1:45 PM | ||
| 1:45 PM - 2:10 PM | Lam, Kait; Coughlin, Nicholas | Lift-off: Trustworthy ARMv8 semantics from formal specifications | |
| 2:10 PM - 2:35 PM | Taylor, Landon J; Israelsen, Bryant; Zhang, Zhen | Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks | |
| CPS - Michael Whalen |
2:35 PM - 3:00 PM | Qin, Xin; Hashemi, Navid; Lindemann, Lars; Deshmukh, Jyotirmoy | Conformance Testing for Stochastic Cyber-Physical Systems |
| 3:00 PM - 3:25 PM | Saxena, Manasvi; Song, Shuang; Sha, Lui | MediK: Towards Safe Guideline-based Clinical Decision Support | |
| Walk to ISU Creamery* | 3:25 PM - 4:00 PM | ||
| ISU Creamery Tour | 4:00 PM - 5:00 PM | ||
| Walk back to Reiman Gardens | 5:00 PM - 5:30 PM | ||
*One small shuttle is available for those that are not able to walk. Guests may drive to campus and park in the Memorial Union ramp (parking fee)