| Monday 13 April |
| 10h30 - 12h30 |
Hybrid systems (Chair: Cesare Tinelli)
- Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki and André Platzer. A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
- Fabian Immler. Verified Reachability Analysis of Continuous Systems
- Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta. HYCOMP - an SMT-based model checker for hybrid systems
- Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan and Matthew Potok. C2E2: A Verification Tool For Annotated Stateflow Models
|
| 14h00 - 16h00 |
Program analysis (Chair: Heike Wehrheim)
- Elvira Albert, Jesús Correas Fernández and Guillermo Román-Díez. Non-Cumulative Resource Analysis
- Shrawan Kumar, Amitabha Sanyal and Uday Khedker. Value Slice: A New Slicing Concept for Scalable Property Checking
- Reng Zeng, Zhuo Sun, Su Liu and Xudong He. A Method for Improving the Precision and Coverage of Atomicity Violation Predictions
- Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha and Bow-Yaw Wang. Commutativity of Reducers
|
| 16h30 - 17h30 |
Verification, abstraction (Chair: Marsha Chechik)
- Hiroshi Unno and Tachio Terauchi. Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling
- Kedar Namjoshi and Richard Trefler. Analysis of Dynamic Process Networks
|
| Tuesday 14 April |
| 14h00 - 16h15 |
Tool demonstrations (Chair: Jaco van de Pol)
- Tomas Brazdil, Krishnendu Chatterjee, Vojtech Forejt and Antonin Kucera. MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives
- Ramiro Demasi, Nicolas Ricci, Pablo Castro, Tom Maibaum and Nazareno Aguirre. syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications
- Nikolaj Bjorner, Anh-Dung Phan and Lars Fleckenstein. νZ - An Optimizing SMT Solver
- Soonho Kong, Sicun Gao, Wei Chen and Edmund Clarke. dReach: Delta-Reachability Analysis for Hybrid Systems
- Alexandre David, Peter G. Jensen, Kim G. Larsen, Marius Mikucionis and Jakob H. Taankvist. STRATEGO: Verification, Performance Analysis and Optimization of Timed Game Strategies
- Adel Djoudi and Sébastien Bardin. BINSEC: Binary-level analysis with Low-Level Regions
- Emmanuel Fleury, Olivier Ly, Gérald Point and Aymeric Vincent. Insight: An Open Binary Analysis Framework
- Gabriele Costa, Alessandro Armando, Alessio Merlo, Gabriele De Maglie, Gianluca Bocci, Giantonio Chiarelli and Rocco Mammoliti. SAM: the Static Analysis Module of the MAVERIC Mobile App Security Verification Platform
- Yann Thierry-Mieg. Symbolic model-checking using ITS-Tools
|
| 16h30 - 18h00 |
Tool demo market (Chair: Jaco van de Pol) |
| Wednesday 15 April |
| 9h00 - 10h00 |
Invited Talk (Chair: Christel Baier)
Wang Yi. |
| 10h30 - 12h00 |
Stochastic models (Chair: Arie Gurfunkel)
- Jeffery Hansen, Lutz Wrage, Sagar Chaki, Dionisio De Niz and Mark Klein. Semantic Importance Sampling for Statistical Model Checking
- Parosh Nicolas Basset, Marta Kwiatkowska, Ufuk Topcu and Clemens Wiltsche. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives
- Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts and Alessandro Abate. FAUST2: Formal Abstractions of Uncountable-STate STochastic processes
|
| 14h00 - 16h00 |
SAT and SMT (Chair: Tobias Nipkow)
- Jeroen Bransen, L. Thomas van Binsbergen, Koen Claessen and Atze Dijkstra. Linearly Ordered Attribute Grammar scheduling using SAT-solving
- Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia and Moshe Y. Vardi. On Parallel Scalable Uniform SAT Witness Generation
- Dmitry Chistikov, Rayna Dimitrova and Rupak Majumdar. Approximate Counting in SMT and Value Estimation for Probabilistic Programs
- Roberto Sebastiani and Patrick Trentin. Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
|
| 16h30 - 18h00 |
Partial order reduction, bisimulation and fairness (Chair: Leonore Zuck)
- Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson and Konstantinos Sagonas. Stateless Model Checking for TSO and PSO
- Anton Wijs. GPU Accelerated Strong and Branching Bisimulation Checking
- Byron Cook, Heidy Khlaaf and Nir Piterman. Fairness for Infinite-State Systems
|
| Thursday 16 April |
| 10h30 - 12h30 |
[SV-COMP talks] (Chair: Dirk Beyer) |
| 15h00 - 16h00 |
Parameter synthesis (Chair: Joost-Pieter Katoen)
- Mirco Giacobbe, Calin Guet, Ashutosh Gupta, Thomas Henzinger, Tiago Paixao and Tatjana Petrov. Model Checking Gene Regulatory Networks
- Ocan Sankur. Symbolic Quantitative Robustness Analysis of Timed Automata
|
| 16h30 - 18h00 |
Program synthesis (Chair: Tiziana Margaria)
- Rajeev Alur, Salar Moarref and Ufuk Topcu. Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
- Roderick Bloem, Krishnendu Chatterjee, Swen Jacobs and Robert Koenighofer. Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
- Roderick Bloem, Bettina Konighofer, Robert Konighofer and Chao Wang. Shield Synthesis: Runtime Enforcement for Reactive Systems
|
| Friday 17 April |
| 10h30 - 12h30 |
Program and runtime verification (Chair: Christel Baier)
- Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre and Gennaro Parlato. Verifying Concurrent Programs by Memory Unwinding
- Julian Tschannen, Carlo A. Furia, Martin Nordio and Nadia Polikarpova. AutoProof: Auto-active Functional Verification of Object-oriented Programs
- Adrian Francalanza and Clare Cini. An LTL Proof System for Runtime Verification
- Giles Reger, Helena Cuenca Cruz and David Rydeheard. MarQ: Monitoring At Runtime with QEA
|
| 14h00 - 16h00 |
Temporal logic and automata (Chair: Christel Baier)
- Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon and Denis Poitrenaud. Parallel Explicit Model Checking for Generalized Büchi Automata
- Dileep Kini and Mahesh Viswanathan. Probabilistic Büchi Automata for LTL\GU
- Vince Molnár, Dániel Darvas, András Vörös and Tamás Bartha. Saturation-based Incremental LTL Model Checking with Inductive Proofs
- Tomas Fiedor, Lukas Holik, Ondrej Lengal and Tomas Vojnar. Nested Antichains for WS1S
|
| 16h30 - 18h00 |
Model checking (Chair: Cesare Tinelli)
- Tom van Dijk and Jaco van de Pol. Sylvan: Multi-core Decision Diagrams
- Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom and Tom van Dijk. LTSmin: High-Performance Language-Independent Model Checking
- Abderahman Kriouile and Wendelin Serwe. Using a Formal Model to Improve Verification of a Cache Coherent System-on-Chip
|