Programme
Programme |
|
| Tutorials by Invited Speakers (October 3, 2012) | |
| 08:00 - 09:00 | Registration |
| 09:00 - 10:30 | SAT Based Design Debugging - Sharad Malik |
| 10:30 - 11:00 | Tea/Coffee break |
| 11:00 - 12:30 | Software Model Checking - Andreas Podelski |
| 12:30 - 14:00 | Lunch break |
| 14:00 - 15:30 | Discretizations based approaches to quantitative verification - P. S. Thiagarajan |
| 15:30 - 16:00 | Tea/Coffee break |
| 16:00 - 18:00 | Industry Session |
| Day 1 (October 4, 2012) | |
| 08:00 - 09:00 | Registration |
| 09:00 - 10:00 | Invited Talk - Sharad Malik Verification of Computer Switching Networks: An Overview (Chair: Supratik Chakraborty) |
| 10:00 - 10:30 | Tea/Coffee break |
| Session I: Automata Theory (Chair: K. Narayan Kumar) |
|
| 10:30 - 11:00 | Shulamit Halamish and Orna Kupferman Approximating Deterministic Lattice Automata |
| 11:00 - 11:30 | Sven Schewe and Thomas Varghese Tight Bounds for the Determinisation and Complementation of Generalised Buchi Automata |
| 11:30 - 12:00 | Sofia Cassel, Bengt Jonsson, Falk Howar and Bernhard Steffen A Succinct Canonical Register Automaton Model for Data Domains with Binary Relations |
| 12:00 - 12:20 | [Tool Paper] Andreas Gaiser, Jan Kretinsky and Javier Esparza Rabinizer: Small Deterministic Automata for LTL(F,G) |
| 12:20 - 14:00 | Lunch break |
| Session II: Logics and Proofs (Chair: S. P. Suresh) |
|
| 14:00 - 14:30 | Simoni Shah and Paritosh Pandya The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints |
| 14:30 - 15:00 | Alexandre Donzé, Oded Maler, Ezio Bartocci, Dejan Nickovic, Radu Grosu and Scott Smolka On Temporal Logic and Signal Processing |
| 15:00 - 15:30 | Ashutosh Gupta Improved Single Pass Algorithms for Resolution Proof Reduction |
| 15:30 - 16:00 | Tea/Coffee break |
| Session III: Model Checking (Chair: Madhavan Mukund) |
|
| 16:00 - 16:30 | Sarai Sheinvald, Orna Grumberg and Orna Kupferman Model Checking Systems and Specifications with Parameterized Atomic Propositions |
| 16:30 - 17:00 | Mohamed Amin Ben Sassi, Romain Testylier, Thao Dang and Antoine Girard Reachability Analysis of Polynomial Systems using Linear Programming Relaxations |
| 17:00 - 17:30 | Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar and Prakash Saivasan Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding |
| Banquet dinner (7 PM onwards) Venue:Vivanta by Taj, Trivandrum | |
| Day 2 (October 5, 2012) | |
| 09:00 - 10:00 | Invited Talk - Andreas Podelski Interpolant Automata (Chair: R Venkatesh) |
| 10:00 - 10:30 | Tea/Coffee break |
| Session I: Software Verification (Chair: Nishant Sinha) |
|
| 10:30 - 11:00 | Ahmed Bouajjani, Cezara Dragoi, Constantin Enea and Mihaela Sighireanu Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data |
| 11:00 - 11:20 | [Tool Paper] Carlo Alberto Furia A Verifier for Functional Properties of Sequence-Manipulating Programs |
| 11:20 - 11:50 | Hossein Hojjat, Radu Iosif, Filip Konecny, Viktor Kuncak and Philipp Ruemmer Accelerating Interpolants |
| 11:50 - 12:10 | [Tool Paper] Ondrej Sery, Grigory Fedyukovich and Natasha Sharygina FunFrog: Bounded Model Checking with Interpolation-based Function Summarization |
| 12:10 - 14:00 | Lunch break |
| Session II: Synthesis (Chair: Paritosh Pandya) |
|
| 14:00 - 14:30 | John Fearnley, Doron Peled and Sven Schewe Synthesis of Succinct Systems |
| 14:30 - 15:00 | Peter Bulychev, Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Jean-Francois Raskin and Pierre-Alain Reynier Controllers with Minimal Observation Power (Application to Timed Systems) |
| 15:00 - 15:30 | Matthias Guedemann, Gwen Salaün and Meriem Ouederni Counterexample Guided Synthesis of Monitors for Realizability Enforcement |
| 15:30 - 16:00 | Tea/Coffee break |
| Session III: Verification and Parallelism (Chair: Madhavan Mukund) |
|
| 16:00 - 16:30 | Daniel Schwartz-Narbonne, Georg Weissenbacher and Sharad Malik Parallel Assertions for Architectures with Weak Memory Models |
| 16:30 - 17:00 | Sami Evangelista, Alfons Laarman, Laure Petrucci and Jaco Van De Pol Improved Multi-Core Nested Depth-First Search |
| 17:00 - 17:30 | Rodrigo T. Saad, Silvano Dal Zilio and Bernard Berthomieu An Experiment on Parallel Model Checking of a CTL Fragment |
| Day 3 (October 6, 2012) | |
| 09:00 - 10:00 | Invited Talk - P S Thiagarajan Dynamic Bayesian Networks: A Factored Model of Probabilistic Dynamics (Chair: Madhavan Mukund) |
| 10:00 - 10:30 | Tea/Coffee break |
| Session I: Probabilistic Verification (Chair: Supratik Chakraborty) |
|
| 10:30 - 11:00 | Luis María Ferrer Fioriti, Ernst Moritz Hahn, Holger Hermanns and Björn Wachter Variable Probabilistic Abstraction Refinement |
| 11:00 - 11:30 | Vojtech Forejt, Marta Kwiatkowska and David Parker Pareto Curves for Probabilistic Model Checking |
| 11:30 - 12:00 | Sergio Giro and Markus N. Rabe Verification of partial-information probabilistic systems using counterexample-guided refinements |
| 12:00 - 12:20 | [Tool Paper] Nils Jansen, Erika Abraham, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen and Bernd Becker The COMICS Tool - Computing Minimal Counterexamples for DTMCs |
| 12:20 - 14:00 | Lunch break |
| Session II: Constraint Solving and Applications (Chair: Mandayam Srivas) |
|
| 14:00 - 14:30 | Daniel Neider Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers |
| 14:30 - 15:00 | Bernd Becker, Rüdiger Ehlers, Matthew Lewis and Paolo Marin ALLQBF Solving by Computational Learning |
| 15:00 - 15:30 | Tea/Coffee break |
| Session III: Probabilistic Systems (Chair: K. Narayan Kumar) |
|
| 15:30 - 16:00 | Krishnendu Chatterjee, Martin Chmelík and Rupak Majumdar Equivalence of Games with Probabilistic Uncertainty and Partial-observation Games |
| 16:00 - 16:30 | Benedikt Bollig, Paul Gastin, Benjamin Monmege and Marc Zeitoun A Probabilistic Kleene Theorem |
| 16:30 - 17:00 | Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate Higher-Order Approximations for Verification of Stochastic Hybrid Systems |