Programme

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