Programme

PDF
Tutorials (Oct. 3) Day 1 (Oct. 4) Day 2 (Oct. 5) Day 3 (Oct. 6) All days
Tutorials by Invited Speakers (October 3, 2017)
08:00 - 08:45 Registration
08:45 - 09:00 Opening Remarks
09:00 - 10:30 Generic Fixpoint Engines for Interprocedural Analyses with Widening and Narrowing - Helmut Seidl

(Chair: Deepak D'Souza)

10:30 - 11:00 Tea/Coffee break
11:00 - 12:30 Data types, tools, and techniques for building available and correct distributed applications - Carla Ferreira

(Chair: S P Suresh)

12:30 - 14:00 Lunch break
14:00 - 15:30 Isabelle Tutorial - Gerwin Klein

(Chair: Mandayam Srivas)

15:30 - 16:00 Tea/Coffee break
Industry Session

(Chair: R Venkatesh)

16:00 - 16:20 Sponsor's Presentation - Ravindra Metta (Tata Consultancy Services)
16:20 - 16:40 Sponsor's Presentation - Manoj Dixit Gangadhar (MathWorks)
16:40 - 16:55 [Industry Presentation] Amol Wakankar, Paritosh K. Pandya, and Raj Mohan Matteplackel
DCSynth: Guided Reactive Synthesis with Soft Requirements and Performance Measurement
16:55 - 17:10 [Industry Presentation] Venkat M, and Sanjeev Kumar
Regression Test Automation of Embedded QT based GUI Application
Conference, Day 1 (October 4, 2017)
08:00 - 09:00 Registration
09:00 - 10:00 Invited Talk - Gerwin Klein
From Trustworthy Kernels to Trustworthy Systems

(Chair: Deepak D'Souza)

10:00 - 10:30 Tea/Coffee break
Session I: Model Checking

(Chair: Sanjiva Prasad)

10:30 - 10:55 Mohammad Torabi Dashti and David Basin
Tests and Refutation
10:55 - 11:20 Kumar Madhukar, Peter Schrammel and Mandayam Srivas
Compositional Safety Refutation Techniques
11:20 - 11:45 Elvio Gilberto Amparore, Marco Beccuti and Susanna Donatelli
Gradient-based variable ordering of Decision Diagrams for systems with structural units
11:45 - 12:05 [Tool Paper] Sumanth Prabhu, Peter Schrammel, Mandayam Srivas, Michael Tautschnig and Anand Yeolekar
Concurrent Program Verification With Invariant-guided Underapproximation
12:05 - 13:35 Lunch break
Session II: Model Checking: Tools

(Chair: Ravindra Metta)

13:35 - 13:55 [Tool Paper] Antonio Bruto Da Costa and Pallab Dasgupta
ForFET: A Formal Feature Evaluation Tool for Hybrid Systems
13:55 - 14:15 [Tool Paper] Fabrizio Biondi, Yusuke Kawamoto, Axel Legay and Louis-Marie Traonouez
HyLeak: Hybrid Analysis Tool for Information Leakage
14:15 - 14:35 [Tool Paper] Zuzana Baranová, Jiri Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai and Vladimír Štill
Model Checking of C and C++ with DIVINE 4
14:35 - 14:55 [Tool Paper] Kunal Banerjee, Chittaranjan Mandal and Dipankar Sarkar
An Equivalence Checking Framework for Array-Intensive Programs
14:55 - 15:15 [Tool Paper] Soumyadip Bandyopadhyay, Santonu Sarkar, Dipankar Sarkar and Chittaranjan Mandal
SamaTulyata: An Efficient Path Based Equivalence Checking Tool
15:15 - 15:45 Tea/Coffee break
Session III: Neural Networks

(Chair: Susanna Donatelli)

15:45 - 16:10 Chih-Hong Cheng, Georg Nührenberg and Harald Ruess
Maximum Resilience of Artificial Neural Networks
16:10 - 16:35 Rüdiger Ehlers
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
Conference, Day 2 (October 5, 2017)
09:00 - 10:00 Invited Talk - Carla Ferreira
Consistency made easy: Towards building correct by design cloud applications

(Chair: Madhavan Mukund)

10:00 - 10:30 Tea/Coffee break
Session I: Temporal Logic/Automata

(Chair: David Basin)

10:30 - 10:55 Bernd Finkbeiner and Hazem Torfah
The Density of Linear-time Properties
10:55 - 11:20 Graeme Gange, Pierre Ganty and Peter J. Stuckey
Fixing the State Budget: Approximation of Regular Languages with Small DFAs
11:20 - 11:45 Marcio Diaz and Tayssir Touili
Dealing with priorities and locks for concurrent programs
11:45 - 12:10 Pierre Ganty, Boris Köpf and Pedro Valero
A Language-theoretic View on Network Protocols
12:10 - 13:40 Lunch break
Session II: Probabilistic Systems/Learning

(Chair: B Srivathsan)

13:40 - 14:05 Jan Kretinsky and Tobias Meggendorfer
Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes
14:05 - 14:30 Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan and Bican Xia
Finding Polynomial Loop Invariants for Probabilistic Programs
14:30 - 14:55 Christel Baier, Clemens Dubslaff, Lubos Korenciak, Antonin Kucera and Vojtech Rehak
Synthesis of Optimal Resilient Control Strategies
14:55 - 15:20 Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening and Tom Melham
Lifting CDCL to Template-based Abstract Domains for Program Verification
15:20 - 16:20 Tea/Coffee break + Tool Demonstrations (Informal)
16:25 - 16:55 Business Meeting
17:00 - 18:30 Cultural Programme
Banquet Dinner (07:00 PM onwards)
Venue: Radisson Blu, Hinjewadi
Conference, Day 3 (October 6, 2017)
09:00 - 10:00 Invited Talk - Helmut Seidl
Proving Absence of Starvation by Means of Abstract Interpretation and Model-checking

(Chair: K Narayan Kumar)

10:00 - 10:30 Tea/Coffee break
Session I: Program Analysis

(Chair: Ashutosh Gupta)

10:30 - 10:55 Ankush Das and Akash Lal
Precise Null Pointer Analysis Through Global Value Numbering
10:55 - 11:20 Jean-Yves Moyen, Thomas Rubiano and Thomas Seiller
Loop Quasi-Invariant Chunk Detection
11:20 - 11:45 Elvira Albert, Samir Genaim and Pablo Gordillo
May-Happen-in-Parallel Analysis with Returned Futures
11:45 - 12:05 [Tool Paper] Krishnendu Chatterjee, Amir Kafshdar Goharshady and Andreas Pavlogiannis
JTDec: A Tool for Tree Decompositions in Soot
12:05 - 13:35 Lunch break
Session II: Invariant Synthesis

(Chair: Peter Schrammel)

13:35 - 14:00 Manuel Montenegro, Susana Nieva, Ricardo Peña and Clara Segura
Liquid Types for Array Invariant Synthesis
14:00 - 14:25 Steven De Oliveira, Saddek Bensalem and Virgile Prevosto
Synthesizing invariants by solving solvable loops
14:25 - 14:50 Nuno Macedo, Alcino Cunha and Eduardo Pessoa
Exploiting Partial Knowledge for Efficient Model Analysis
14:50 - 15:20 Tea/Coffee break
Session III: Hybrid Systems/Security

(Chair: S Akshay)

15:20 - 15:45 Abdullah Abdul Khadir, Madhavan Mukund and S P Suresh
Knowledge transfer and information leakage in protocols
15:45 - 16:10 Ashish Tiwari, Scott A. Smolka, Lukas Esterle, Anna Lukina, Junxing Yang and Radu Grosu
Attacking the V: On the Resiliency of Adaptive-Horizon MPC
16:10 - 16:35 Krishna S., Ashutosh Trivedi, Aviral Kumar, Fabio Somenzi and Behrouz Touri
The Reach-Avoid Problem for Constant-Rate Multi-Mode Systems
16:35 - 16:45 Closing Remarks