Accepted Papers

Ankush Das and Akash Lal. Precise Null Pointer Analysis Through Global Value Numbering
Kunal Banerjee, Chittaranjan Mandal and Dipankar Sarkar. An Equivalence Checking Framework for Array-Intensive Programs (Tool Paper)
Jean-Yves Moyen, Thomas Rubiano and Thomas Seiller. Loop Quasi-Invariant Chunk Detection
Mohammad Torabi Dashti and David Basin. Tests and Refutation
Chih-Hong Cheng, Georg Nührenberg and Harald Ruess. Maximum Resilience of Artificial Neural Networks
Manuel Montenegro, Susana Nieva, Ricardo Peña and Clara Segura. Liquid Types for Array Invariant Synthesis
Nuno Macedo, Alcino Cunha and Eduardo Pessoa. Exploiting Partial Knowledge for Efficient Model Analysis
Jan Kretinsky and Tobias Meggendorfer. Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes
Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening and Tom Melham. Lifting CDCL to Template-based Abstract Domains for Program Verification
Soumyadip Bandyopadhyay, Santonu Sarkar, Dipankar Sarkar and Chittaranjan Mandal. SamaTulyata: An Efficient Path Based Equivalence Checking Tool (Tool Paper)
Steven De Oliveira, Saddek Bensalem and Virgile Prevosto. Synthesizing invariants by solving solvable loops
Elvira Albert, Samir Genaim and Pablo Gordillo. May-Happen-in-Parallel Analysis with Returned Futures
Krishnendu Chatterjee, Amir Kafshdar Goharshady and Andreas Pavlogiannis. JTDec: A Tool for Tree Decompositions in Soot (Tool Paper)
Pierre Ganty, Boris Köpf and Pedro Valero. A Language-theoretic View on Network Protocols
Fabrizio Biondi, Yusuke Kawamoto, Axel Legay and Louis-Marie Traonouez. HyLeak: Hybrid Analysis Tool for Information Leakage (Tool Paper)
Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan and Bican Xia. Finding Polynomial Loop Invariants for Probabilistic Programs
Kumar Madhukar, Peter Schrammel and Mandayam Srivas. Compositional Safety Refutation Techniques
Elvio Gilberto Amparore, Marco Beccuti and Susanna Donatelli. Gradient-based variable ordering of Decision Diagrams for systems with structural units
Antonio Bruto Da Costa and Pallab Dasgupta. ForFET: A Formal Feature Evaluation Tool for Hybrid Systems (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 (Tool Paper)
Marcio Diaz and Tayssir Touili. Dealing with priorities and locks for concurrent programs
Rüdiger Ehlers. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
Ashish Tiwari, Scott A. Smolka, Lukas Esterle, Anna Lukina, Junxing Yang and Radu Grosu. Attacking the V: On the Resiliency of Adaptive-Horizon MPC
Graeme Gange, Pierre Ganty and Peter J. Stuckey. Fixing the State Budget: Approximation of Regular Languages with Small DFAs
Abdullah Abdul Khadir, Madhavan Mukund and S P Suresh. Knowledge transfer and information leakage in protocols
Sumanth Prabhu, Peter Schrammel, Mandayam Srivas, Michael Tautschnig and Anand Yeolekar. Concurrent Program Verification With Invariant-guided Underapproximation (Tool Paper)
Bernd Finkbeiner and Hazem Torfah. The Density of Linear-time Properties
Krishna S., Ashutosh Trivedi, Aviral Kumar, Fabio Somenzi and Behrouz Touri. The Reach-Avoid Problem for Constant-Rate Multi-Mode Systems
Christel Baier, Clemens Dubslaff, Lubos Korenciak, Antonin Kucera and Vojtech Rehak. Synthesis of Optimal Resilient Control Strategies