Program

12:05	Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz and Clark Barrett Automating System Configuration (abstract)
12:20	Aman Goel and Karem A. Sakallah Towards an Automatic Proof of Lamport's Paxos (abstract)
12:35	Ning Dong, Roberto Guanciale and Mads Dam Refinement-Based Verification of Device-to-Device Information Flow (abstract) PRESENTER: Ning Dong
12:50	Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi and Akash Lal Celestial: A Framework for Verified Smart Contracts (abstract)
13:05	Bernhard Kragl and Shaz Qadeer The Civl Verifier (abstract)

13:40-14:55 Session 8

Model Checking and IC3

Chair:

Christoph Sticksel

13:40	Rohit Dureja, Arie Gurfinkel, Alexander Ivrii and Yakir Vizel IC3 with Internal Signals (abstract)
13:55	Nils Froleyks and Armin Biere Single Clause Assumption without Activation Literals to Speed-up IC3 (abstract)
14:10	Hari Govind Vediramana Krishnan, Sharon Shoham and Arie Gurfinkel Logical Characterization of Coherent Uninterpreted Programs (abstract)
14:25	Nham Le, Xujie Si and Arie Gurfinkel Data-driven Inductive Generalization (abstract)
14:40	Timothee Durand, Katalin Fazekas, Georg Weissenbacher and Jakob Zwirchmayr Model Checking AUTOSAR Components with CBMC (abstract)

15:15-16:15 Session 9

Student Forum and Sponsors' Night

Chair:

Mark Santolucito

Thursday, October 21st

View this program: with abstracts session overview talk overview

11:00-12:00 Session 10

Invited Talk

Chair:

Georg Weissenbacher

11:00

Seny Kamara

Algorithms for the People (abstract)

12:05-13:20 Session 11

SAT Solving

Chair:

Armin Biere

12:05	Alexander Ivrii and Ofer Strichman Exploiting Isomorphic Subgraphs in SAT (abstract)
12:20	Jaroslav Bendík On Decomposition of Maximal Satisfiable Subsets (abstract)
12:35	Priyanka Golia, Mate Soos, Sourav Chakraborty and Kuldeep S. Meel Designing Samplers is Easy: The Boon of Testers (abstract)
12:50	Petar Vukmirović, Jasmin Blanchette and Marijn Heule SAT-Inspired Eliminations for Superposition (abstract)
13:05	Alex Ozdemir, Haoze Wu and Clark Barrett SAT Solving in the Serverless Cloud (abstract)

13:40-14:55 Session 12

Applied Verification and Synthesis

Chair:

Elizabeth Polgreen

13:40	Ori Lahav and Guy Katz Pruning and Slicing Neural Networks using Formal Verification (abstract)
13:55	Guy Amir, Michael Schapira and Guy Katz Towards Scalable Verification of Deep Reinforcement Learning (abstract) PRESENTER: Guy Amir
14:10	Hazem Torfah, Shetal Shah, Supratik Chakraborty, S. Akshay and Sanjit A. Seshia Synthesizing Pareto-optimal Interpretations for Black-Box Models (abstract)
14:25	Michalis Kokologiannakis, Xiaowei Ren and Viktor Vafeiadis Dynamic Partial Order Reductions for Spinloops (abstract)
14:40	Soham Chakraborty Robustness between Weak Memory Models (abstract)

15:15-16:15 Session 13

Panel: 25 years of FMCAD

Chairs:

Ruzica Piskac and Michael Whalen

Friday, October 22nd

View this program: with abstracts session overview talk overview

11:00-12:15 Session 14

Hardware Verification

Chair:

Rebekah Leslie-Hurd

11:00	Dapeng Gao and Tom Melham End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers (abstract)
11:15	Neta Bar Kama and Roope Kaivola Hardware Security Leak Detection by Symbolic Simulation (abstract)
11:30	Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark Barrett and Subhasish Mitra Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition (abstract)
11:45	Mertcan Temel and Warren Hunt Sound and Automated Verification of Real-World RTL Multipliers (abstract)
12:00	Vedad Hadžić and Roderick Bloem Coco-Alma: A Versatile Masking Verifier (abstract)

12:35-13:35 Session 15

Invited Talk

Chair:

Michael Whalen

12:35

Peter Sewell

Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V (abstract)

13:40-14:55 Session 16

SMT and FOL

Chair:

Dejan Jovanović

13:40	Marton Hajdu, Petra Hozzová, Laura Kovacs and Andrei Voronkov Induction with Recursive Definitions in Superposition (abstract)
13:55	Mikolas Janota, Haniel Barbosa, Pascal Fontaine and Andrew Reynolds Fair and Adventurous Enumeration of Quantifier Instantiations (abstract)
14:10	Ankit Kumar and Panagiotis Manolios Mathematical Programming Modulo Strings (abstract)
14:25	Antti Hyvärinen, Matteo Marescotti and Natasha Sharygina Lookahead in Partitioning SMT (abstract)
14:40	Michael Rawson and Giles Reger A Multithreaded Vampire with Shared Persistent Grounding (abstract)

15:15-16:15 Session 17

FMCAD Business Meeting