| Authors | Title | Paper | Talk |
|---|
| Somesh Jha | Semantic Adversarial Deep Learning |  | Jul 16 11:00 |
| Eran Yahav | From Programs to Interpretable Deep Models and Back | | Jul 14 14:00 |
| Byron Cook | Formal reasoning about the security of AWS | | |
| Ilya Grishchenko, Matteo Maffei and Clara Schneidewind | Foundations and Tools for the Static Analysis of Ethereum smart contracts | | |
| Bernhard Kragl and Shaz Qadeer | Layered Concurrent Programs | | |
| Yuki Satake and Hiroshi Unno | Propositional Dynamic Logic for Higher-Order Functional Programs | | Jul 14 11:00 |
| Grigory Fedyukovich, Yueling Zhang and Aarti Gupta | Syntax-Guided Termination Analysis | | Jul 14 11:15 |
| Hazem Torfah, Bernd Finkbeiner and Christopher Hahn | Model Checking Quantitative Hyperproperties | | Jul 14 11:30 |
| Lauren Pick, Grigory Fedyukovich and Aarti Gupta | Exploiting Synchrony and Symmetry in Relational Verification | | Jul 14 11:45 |
| Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel and Marek Trtik | JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode | | Jul 14 12:00 |
| Kenneth McMillan | Eager Abstraction for Symbolic Model Checking | | Jul 14 12:15 |
| Gagandeep Singh, Markus Püschel and Martin Vechev | Fast Numerical Program Analysis with Reinforcement Learning | | Jul 14 15:00 |
| Anna Becchi and Enea Zaffanella | A Direct Encoding for NNC Polyhedra | | Jul 14 15:15 |
| S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal and Shetal Shah | What’s hard about Boolean Functional Synthesis? | | Jul 14 16:00 |
| Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening and Elizabeth Polgreen | Counterexample Guided Inductive Synthesis Modulo Theories | | Jul 14 16:15 |
| Bernd Finkbeiner, Leander Tentrup, Marvin Stenger, Philip Lukert and Christopher Hahn | Synthesizing Reactive Systems from Hyperproperties | | Jul 14 16:30 |
| Daniel J. Fremont and Sanjit A. Seshia | Reactive Control Improvisation | | Jul 14 16:45 |
| Aws Albarghouthi and Justin Hsu | Constraint-Based Synthesis of Coupling Proofs | | Jul 14 17:00 |
| Chuchu Fan, Umang Mathur, Sayan Mitra and Mahesh Viswanathan | Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics | | Jul 14 17:15 |
| Suguman Bansal, Kedar Namjoshi and Yaniv Sa'Ar | Synthesis Of Asynchronous Reactive Programs From Temporal Specifications | | Jul 14 17:30 |
| Qinheping Hu and Loris D'Antoni | Syntax Guided Synthesis with Quantitative Syntactic Objectives | | Jul 14 17:45 |
| Xinyu Wang, Greg Anderson, Isil Dillig and Ken McMillan | Learning Abstractions for Program Synthesis | | Jul 15 10:00 |
| George Argyros and Loris D'Antoni | The Learnability of Symbolic Automata | | Jul 15 10:15 |
| Hui Kong, Ezio Bartocci and Tom Henzinger | Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes | | Jul 15 11:00 |
| Goran Frehse, Mirco Giacobbe and Thomas Henzinger | Space-time Interpolants | | Jul 15 11:15 |
| Michael Emmi and Constantin Enea | Monitoring Weak Consistency | | Jul 15 11:30 |
| Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia and Naijun Zhan | Monitoring CTMCs By Multi-Clock Timed Automata | | Jul 15 11:45 |
| Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz and Jiri Srba | Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems | | Jul 15 12:00 |
| Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Franz Roeck | A Counting Semantics for Monitoring LTL Specifications over Finite Traces | | Jul 15 12:15 |
| Jan Kretinsky, Tobias Meggendorfer, Salomon Sickert and Christopher Ziegler | Rabinizer 4: From LTL to Your Favourite Deterministic Automaton | | Jul 15 14:00 |
| Philipp J. Meyer, Salomon Sickert and Michael Luttenberger | Strix: Explicit Reactive Synthesis Strikes Back! | | Jul 15 14:15 |
| Aina Niemetz, Mathias Preiner, Clifford Wolf and Armin Biere | BTOR2, BtorMC and Boolector 3.0 | | Jul 15 14:30 |
| Marco Eilers and Peter Müller | Nagini: A Static Verifier for Python | | Jul 15 14:45 |
| Michael Blondin, Javier Esparza and Stefan Jaax | Peregrine: A Tool for the Analysis of Population Protocols | | Jul 15 15:00 |
| Milan Ceska, Jiri Matyas, Vojtech Mrazek, Lukas Sekanina, Zdenek Vasicek and Tomas Vojnar | ADAC: Automated Design of Approximate Circuits | | Jul 15 15:15 |
| Edon Kelmendi, Julia Krämer, Jan Kretinsky and Maximilian Weininger | Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm | | Jul 15 16:00 |
| Tim Quatmann and Joost-Pieter Katoen | Sound Value Iteration | | Jul 15 16:15 |
| Weichao Zhou and Wenchao Li | Safety-Aware Apprenticeship Learning | | Jul 15 16:30 |
| Qiyi Tang and Franck van Breugel | Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains | | Jul 15 16:45 |
| Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja and Thomas Noll | Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs | | Jul 16 09:00 |
| Mostafa Hassan, Caterina Urban, Marco Eilers and Peter Müller | MaxSMT-Based Type Inference for Python 3 | | Jul 16 09:15 |
| Andrew Gacek, John Backes, Michael Whalen, Lucas Wagner and Elaheh Ghassabani | The JKind Model Checker | | Jul 16 09:30 |
| Vincent Cheval, Steve Kremer and Itsaka Rakotonirina | The DEEPSEC prover | | Jul 16 09:45 |
| Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier and Moshe Vardi | SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability | | Jul 16 10:00 |
| Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir and Vijay Ganesh | StringFuzz: A Fuzzer for String Solvers | | Jul 16 10:15 |
| Jérôme Dohrau, Alexander J Summers, Caterina Urban, Severin Münger and Peter Müller | Permission Inference for Array Programs | | Jul 16 12:00 |
| Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato | Program Analysis is Harder than Verification: A Computability Perspective | | Jul 16 12:15 |
| Suguman Bansal, Swarat Chaudhuri and Moshe Vardi | Automata vs Linear-Programming Discounted-Sum Inclusion | | Jul 17 09:00 |
| Matthew Bauer, Rohit Chadha, Mahesh Viswanathan and Prasad Sistla | Model checking indistinguishability of randomized security protocols | | Jul 17 09:15 |
| Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta and Sharad Malik | Lazy Self-Composition for Security Verification | | Jul 17 09:30 |
| Jun Zhang, Pengfei Gao, Fu Song and Chao Wang | SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks | | Jul 17 09:45 |
| Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee and Viktor Toman | Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives | | Jul 17 10:00 |
| Tom van Dijk | Attracting Tangles to Solve Parity Games | | Jul 17 10:15 |
| Soonho Kong, Armando Solar-Lezama and Sicun Gao | Delta-Decision Procedures for Exists-Forall Problems over the Reals | | Jul 17 11:00 |
| Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli | Solving Quantified Bit-Vectors using Invertibility Conditions | | Jul 17 11:15 |
| Markus N. Rabe, Leander Tentrup, Cameron Rasmussen and Sanjit A. Seshia | Understanding and Extending Incremental Determinization for 2QBF | | Jul 17 11:30 |
| Robert Robere, Antonina Kolokolova and Vijay Ganesh | The Proof Complexity of SMT Solvers | | Jul 17 11:45 |
| Benjamin Farinier, Sebastien Bardin, Richard Bonichon and Marie-Laure Potet | Model Generation for Quantified Formulas: A Taint-Based Approach | | Jul 17 12:00 |
| Xinhao Yuan, Junfeng Yang and Ronghui Gu | Partial Order Aware Concurrency Sampling | | Jul 17 14:00 |
| Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil and Serdar Tasiran | Reasoning About TSO Programs Using Reduction and Abstraction | | Jul 17 14:15 |
| Huyen T.T. Nguyen, Cesar Rodriguez, Marcelo Sousa, Camille Coti and Laure Petrucci | Quasi-Optimal Partial Order Reduction | | Jul 17 14:30 |
| Ahmed Bouajjani, Constantin Enea, Kailiang Ji and Shaz Qadeer | On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony | | Jul 17 14:45 |
| Elvira Albert, Miguel Gomez-Zamalloa, Miguel Isabel and Albert Rubio | Constrained Dynamic Partial Order Reduction | | Jul 17 15:00 |
| Mark Tullsen, Lee Pike, Nathan Collins and Aaron Tomb | Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System | | Jul 17 16:00 |
| Andrey Chudnov, Nathan Collins, Byron Cook, Josiah Dodds, Brian Huffman, Colm MacCarthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb and Edwin Westbrook | Continuous formal verification of Amazon s2n | | Jul 17 16:15 |
| Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll and Klaus Wehrle | Symbolic Liveness Analysis of Real-World Software | | Jul 17 16:30 |
| Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig and Mark R. Tuttle | Model Checking Boot Code from AWS Data Centers | | Jul 17 16:45 |
| Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu and Jun Yan | Android Stack Machine | | Jul 17 17:00 |
| Christoph Walther | Formally Verified Montgomery Multiplication | | Jul 17 17:15 |
| Eric Goubault, Sylvie Putot and Lorenz Sahlman | Inner and Outer Approximating Flowpipes for Delay Differential Equations | | Jul 17 17:30 |