Verification, Model Checking, and Abstract Interpretation

1. Front Matter

   Pages I-XIII

   PDF

2. Invited Talks

   1. Front Matter

      Pages 1-1

      PDF

   2. Automating Abstract Interpretation

      • Thomas Reps, Aditya Thakur

      Pages 3-40

   3. Viper: A Verification Infrastructure for Permission-Based Reasoning

      • Peter Müller, Malte Schwerhoff, Alexander J. Summers

      Pages 41-62

3. Abstract Interpretation

   1. Front Matter

      Pages 63-63

      PDF

   2. Predicate Abstraction for Linked Data Structures

      • Alexander Bakst, Ranjit Jhala

      Pages 65-84

   3. An Abstract Domain of Uninterpreted Functions

      • Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

      Pages 85-103

   4. Property Directed Abstract Interpretation

      • Noam Rinetzky, Sharon Shoham

      Pages 104-123

4. Abstraction

   1. Front Matter

      Pages 125-125

      PDF

   2. Program Analysis with Local Policy Iteration

      • Egor George Karpenkov, David Monniaux, Philipp Wendler

      Pages 127-146

   3. Lazy Constrained Monotonic Abstraction

      • Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng

      Pages 147-165

   4. Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem

      • Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michael Périn

      Pages 166-184

   5. \(D^3\): Data-Driven Disjunctive Abstraction

      • Hila Peleg, Sharon Shoham, Eran Yahav

      Pages 185-205

   6. Exact Heap Summaries for Symbolic Execution

      • Benjamin Hillery, Eric Mercer, Neha Rungta, Suzette Person

      Pages 206-225

5. Hybrid and Timed Systems

   1. Front Matter

      Pages 227-227

      PDF

   2. Abstract Interpretation with Infinitesimals

      • Kengo Kido, Swarat Chaudhuri, Ichiro Hasuo

      Pages 229-249

   3. Lipschitz Robustness of Timed I/O Systems

      • Thomas A. Henzinger, Jan Otop, Roopsha Samanta

      Pages 250-267

   4. A Method for Invariant Generation for Polynomial Continuous Systems

      • Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, André Platzer

      Pages 268-288

6. Dynamic and Static Verification

   1. Front Matter

      Pages 289-289

      PDF

   2. Hybrid Analysis for Partial Order Reduction of Programs with Arrays

      • Pavel Parízek

      Pages 291-310

This book constitutes the refereed proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2016, held in St. Petersburg, FL, USA, in January 2016. The  24 full papers together with 2 invited talks and 1 abstract presented were carefully reviewed and selected from 67 submissions. VMCAI provides topics including: program verification, model checking, abstract
interpretation and abstract domains, program synthesis, static analysis,
type systems, deductive methods, program certification, debugging techniques,
program transformation, optimization, hybrid and cyber-physical systems.

• cloud computing
• complexity
• distributed systems
• logic model checking
• timed automata
• concurrency
• constraint-based reasoning
• formal verification
• hybrid systems
• massive parallelism
• parallelism
• reactive synthesis
• robustness
• SAT-solvers
• simulations/bisimulations
• software testing
• software verification
• swarm verification
• symbolic execution
• weighted automata

• EPFL IC-DO, Lausanne, Switzerland

  Barbara Jobstmann

• Microsoft Research, Redmond, USA

  K. Rustan M. Leino

Policies and ethics