| Authors | Title | Paper | Talk |
|---|
| David Monniaux | How do we get Inductive Invariants? |  | Jul 18 08:45 |
| Fabio Somenzi | Hardware Model Checking | | Jul 18 14:30 |
| Erik Winfree | Designing and Verifying Molecular Circuits and Systems Made of DNA | | Jul 19 17:10 |
| Rance Cleaveland | Automated Testing | | Jul 20 17:10 |
| Rajeev Alur, Dana Fisman, Rishab Singh and Armando Solar-Lezama | The First Syntax-Guided Synthesis Competition (SyGuS-COMP 2014) | | Jul 19 12:55 |
| Armin Biere and Keijo Heljanko | Hardware Model Checking Competition CAV 2014 Edition | | Jul 20 14:30 |
| Roderick Bloem, Rüdiger Ehlers and Swen Jacobs | SYNTCOMP - Synthesis Competition for Reactive Systems | | Jul 21 12:55 |
| Jean-Christophe Filliatre, Léon Gondelman and Andrei Paskevich | The Spirit of Ghost Code | | Jul 19 10:45 |
| Anvesh Komuravelli, Arie Gurfinkel and Sagar Chaki | SMT-based Model Checking for Recursive Programs | | Jul 19 11:05 |
| Shachar Itzhaky, Nikolaj Bjorner, Thomas Reps, Mooly Sagiv and Aditya Thakur | Property-Directed Shape Analysis | | Jul 19 11:25 |
| Quang Loc Le, Cristian Gherghina, Shengchao Qin and Wei-Ngan Chin | Shape Analysis via Second-Order Bi-Abduction | | Jul 19 11:45 |
| Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider | ICE: A Robust Learning Framework for Synthesizing Invariants | | Jul 19 12:05 |
| Rahul Sharma and Alex Aiken | From Invariant Checking to Invariant Inference Using Randomized Search | | Jul 19 12:25 |
| Zvonimir Rakamaric and Michael Emmi | SMACK: Decoupling Source Language Details from Verifier Implementations | | Jul 19 12:45 |
| Hassan Eldib and Chao Wang | Synthesis of Masking Countermeasures against Side Channel Attacks | | Jul 19 14:30 |
| Omar Chowdhury, Limin Jia, Deepak Garg and Anupam Datta | Temporal Mode-Checking for Runtime Monitoring of Privacy Policies | | Jul 19 14:50 |
| Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp Reummer and Jari Stenman | String Constraints for Verification | | Jul 19 15:10 |
| Sudeep Kanav, Peter Lammich and Andrei Popescu | A Conference Management System with Verified Document Confidentiality | | Jul 19 15:30 |
| Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen and Gennaro Parlato | VAC - Verifier of Administrative Role-based Access Control Policies | | Jul 19 15:50 |
| Javier Esparza and Jan Kretinsky | From LTL to Deterministic Automata: A Safraless Compositional Approach | | Jul 19 16:30 |
| Loris D'Antoni and Rajeev Alur | Symbolic Visibly Pushdown Automata | | Jul 19 16:50 |
| Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair Donaldson, Jeroen Ketema, Dan Liew and Shaz Qadeer | Engineering a Static Verification Tool for GPU Kernels | | Jul 20 10:45 |
| Kenneth McMillan | Lazy Annotation Revisited | | Jul 20 11:05 |
| Yakir Vizel and Arie Gurfinkel | Interpolating Property Directed Reachability | | Jul 20 11:25 |
| Jesse Bingham and Joe Leslie-Hurd | Verifying Relative Error Bounds using Symbolic Simulation | | Jul 20 11:45 |
| Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi and Darko Marinov | Regression Test Selection for Distributed Software Histories | | Jul 20 12:05 |
| Anton Wijs, Joost-Pieter Katoen and Dragan Bosnacki | GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components | | Jul 20 12:25 |
| Dirk Beyer, Georg Dresler and Philipp Wendler | Software Verification in the Google App-Engine Cloud | | Jul 20 12:45 |
| Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri and Stefano Tonetta | The nuXmv Symbolic Model Checker | | Jul 20 12:55 |
| Hillel Kugler, Nicola Paoletti, Boyan Yordanov, Youssef Hamadi and Christoph M. Wintersteiger | Analyzing and Synthesizing Genomic Logic Functions | | Jul 20 14:40 |
| Byron Cook, Jasmin Fisher, Benjamin Hall, Samin Ishtiaq, Garvit Juniwal and Nir Piterman | Finding instability in biological models | | Jul 20 15:00 |
| Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra and Marta Kwiatkowska | Invariant verification of nonlinear hybrid automata networks of cardiac cells | | Jul 20 15:20 |
| Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen and Jun Sun | Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions | | Jul 20 15:40 |
| Willem Hagemann | Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections | | Jul 20 16:30 |
| Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta | Verifying LTL properties of hybrid systems with K-liveness | | Jul 20 16:50 |
| Rodica Bozianu, Catalin Dima and Emmanuel Filiot | Safraless Synthesis for Epistemic Temporal Specifications | | Jul 21 10:45 |
| Tomas Brazdil, David Klaska, Antonin Kucera and Petr Novotný | Minimizing Running Costs in Consumption Systems | | Jul 21 11:05 |
| Krishnendu Chatterjee, Martin Chmelík and Przemyslaw Daca | CEGAR for Qualitative Analysis of Probabilistic Systems | | Jul 21 11:25 |
| Thomas Dillig, Isil Dillig and Swarat Chaudhuri | Optimal Guard Synthesis for Memory Safety | | Jul 21 11:45 |
| Jade Alglave, Daniel Kroening, Vincent Nimal and Daniel Poetzl | Don't sit on the fence: A static analysis approach to automatic fence insertion | | Jul 21 12:05 |
| Petr Čermák, Alessio Lomuscio, Fabio Mogavero and Aniello Murano | MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications | | Jul 21 12:25 |
| Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Walker | Solving Games without Controllable Predecessor | | Jul 21 12:35 |
| Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess and Stefan Stattelmann | G4LTL-ST: Automatic Generation of PLC Programs | | Jul 21 12:45 |
| Mohsen Lesani, Todd Millstein and Jens Palsberg | Automatic Atomicity Verification for Clients of Concurrent Data Structures | | Jul 21 14:30 |
| Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach | Regression-free Synthesis for Concurrency | | Jul 21 14:50 |
| Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre and Gennaro Parlato | Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization | | Jul 21 15:10 |
| Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp Meyer and Filip Niksic | An SMT-based Approach to Coverability Analysis | | Jul 21 15:30 |
| Alejandro Sanchez and Cesar Sanchez | LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes | | Jul 21 15:50 |
| Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg | Monadic Decomposition | | Jul 22 10:45 |
| Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Morgan Deters | A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions | | Jul 22 11:05 |
| Alexander Nadel | Bit-Vector Rewriting with Automatic Rule Generation | | Jul 22 11:25 |
| Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli and Kshitij Bansal | A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors | | Jul 22 11:45 |
| Andrei Voronkov | AVATAR: The New Architecture for First-Order Theorem Provers | | Jul 22 12:05 |
| Ruzica Piskac, Thomas Wies and Damien Zufferey | Automating Separation Logic with Trees and Data | | Jul 22 12:25 |
| Ashish Tiwari and Patrick Lincoln | A Nonlinear Real Arithmetic Fragment | | Jul 22 12:45 |
| Bruno Dutertre | Yices 2.2 | | Jul 22 12:55 |
| Moritz Sinn, Florian Zuleger and Helmut Veith | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis | | Jul 22 14:30 |
| Ravichandhran Madhavan and Viktor Kuncak | Symbolic Resource Bound Inference for Functional Programs | | Jul 22 14:50 |
| Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio | Proving Non-termination Using Max-SMT | | Jul 22 15:10 |
| Matthias Heizmann, Jochen Hoenicke and Andreas Podelski | Termination Analysis by Learning Terminating Programs | | Jul 22 15:30 |
| Andrey Kupriyanov and Bernd Finkbeiner | Causal Termination of Multi-threaded Programs | | Jul 22 15:50 |
| Johannes Birgmeier, Aaron R. Bradley and Georg Weissenbacher | Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) | | Jul 22 16:40 |
| Suho Lee and Karem A. Sakallah | Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction | | Jul 22 17:00 |
| Arlen Cox, Bor-Yuh Evan Chang and Sriram Sankaranarayanan | QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers | | Jul 22 17:20 |