Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. ProceedingsBarbara Jobstmann, K. Rustan M. Leino 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, abstractinterpretation and abstract domains, program synthesis, static analysis,type systems, deductive methods, program certification, debugging techniques,program transformation, optimization, hybrid and cyber-physical systems. |
Contents
Abstract Interpretation | 63 |
Abstraction | 124 |
Hybrid and Timed Systems | 226 |
Dynamic and Static Verification | 289 |
Probabilistic Systems | 348 |
Concurrent Programs | 391 |
Parameterized and ComponentBased Systems | 453 |
Solver Improvements | 514 |
| 557 | |
Other editions - View all
Verification, Model Checking, and Abstract Interpretation: 17th ... Barbara Jobstmann,K. Rustan M. Leino No preview available - 2015 |
Common terms and phrases
abstract domain abstract interpretation abstract transformers algorithm approach array elements automatic benchmarks bisimulation bound Bounding Lemma cartesian trace component compute concolic testing concrete configuration constraints construction corresponding counter machine data structures deadlocked defined Definition denote disjunctive dynamic encoding example finite fixpoint formula function Galois connection given heap Heidelberg hybrid analysis ic3par IMDP implementation initial input intervals invariant iteration K-robustness language Lemma linear LNCS logic loop Manhattan distance Markov Chains method model checking output over-approximation parameter valuations parameterised path pointer race polyhedra polynomial postcondition predicates problem procedure proof propagation properties PSpace-complete reachability refinement relation SAT solver Sect semantics sequence specification Springer static analysis symmetry patterns template Theorem thread choices tion tool transducer transition transition relation tuple updates UwMDP variables verification Viper VMCAI