Tutorial
Zeller A. Mining Programs ....................................... 1

Invited Talks
Best E., Darondeau Ph. Petri Net Distributability ............... 2
Bruni R., Melgratti H., Montanari U. Connector Algebras and 
   Petri Nets ................................................... 3
Bunernan P. Models of Provenance ................................ 8
Majumdar R. End-to-End Guarantees in Embedded Control Systems ... 9
Zeller A. Mining Precise Specifications ........................ 10

Regular Papers
Baar Th., Kumar Ph. Detecting Entry Points in Java Libraries ... 11
Beyer M., Glesner S. Static Analysis of Run-Time Modes in 
   Synchronous Process Network ................................. 20
Demm A., Ponomaryov D., Vityaev E. Probabilistic Concepts in
   Formal Contexts ............................................. 29
Fried M.A.H., Fensel A., Facca F.M., Fensel D. An Extensible
   System for Enhancing Social Conference Experience ........... 39
Garanina N.O. Exponential Acceleration of Model Checking for
   Perfect Recall Systems ...................................... 50
Glück R. Bootstrapping Compiler Generators from Partial
   Evaluators .................................................. 59
Hamilton G.W., Jones N.D. Proving the Correctness of Unfold/
   Fold Program Transformations Using Bisimulation ............. 69
Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. 
   Towards an Open Framework for С Verification Tools 
   Benchmarking ................................................ 82
Klimov A.V. Coverability Problem for Monotonie Counter 
   Systems by Supercompilation ................................. 92
Klyuchnikov I., Romanenko S. Multi-Result Supercompilation as
   Branching Growth of the Penultimate Level in Metasystem
   Transitions ................................................ 104
Knoop J., Kovács L., Zwirchmayr J. Symbolic Loop Bound 
   Computation for WCET Analysis .............................. 116
Korovin K., Tsiskaridze N., Voronkov A. Implementing
   Conflict Resolution ........................................ 127
Korovina M., Vorobjov N. Reachability in One-Dimensional 
   Controlled Polynomial Dynamical Systems .................... 137
Mardare R. Decidability of Modular Logics for Concurrency ..... 144
Mogensen Т.Æ. Partial Evaluation of Janus Part 2: Assertions 
   and Procedures ............................................. 155
Sharma A.. Katoen J.-P. Weighted Lumpability on Markov 
   Chains ..................................................... 164
Studer Th. Justified Terminological Reasoning ................. 177
Veanes M., Bjørner N. Symbolic Tree Transducers ............... 186

Short Papers
Bozhenkova E.N. Compositional Methods in Characterization of
   Timed Event Structures ..................................... 198
Caballero R., García-Ruiz Y., Sáenz-Pérez F. Algorithmic 
   Debugging of SQL Views ..................................... 204
Dubtsov R. Timed Transition Systems with Independence and
   Marked Scott Domains: an Adjunction ........................ 210
Gribovskaya N.S. A Logic Characteristic For Timed Extensions
   of Partial Order Based Equivalences ........................ 216
Jaskelioff M., Russo A. Secure Multi-Execution in Haskell ..... 223
Korovin K., Voronkov A. GoRRiLA and Hard Reality .............. 229
Letichevsky A.A., Letychevskyi O.A., Peschanenko V.S. 
  Insertion Modeling System ................................... 234
Petrov E. Scalable Parallel Interval Propagation 
   for Sparse Constraint Satisfaction Problems ................ 242
Ponomarenko A., Rubanov V. A Combined Technique for 
   Automatic Detection of Backward Binary 
   Compatibility Problems ..................................... 249
Shilov N.V., Akinin A.A., Zubkov A.V., Idrisov R.I.
   Development of the Computer Language 
   Classification Knowledge Portal ............................ 255

Posters 
Anureev I, Maryasov I., Nepomniaschy V. The Mixed Axiomatic 
   Semantics Method for C-program Verification ................ 261
Baranov S., Kotlyarov V., Weigert Th. Test Automation
   with Verifiable Coverage Criteria .......................... 267
Klimov A. Transforming Affine Nested Loop Programs to 
   Dataflow Computation Model ................................. 274
Polo Usaola M., Reales Mateo P., Pérez Lamancha B. Reduction 
   of Test Suites Using Mutation .............................. 286
Promsky A.V. Verification Condition Understanding ............. 295
Shelekhov V. Rules of Correctness Proof for Programs with
   Simple Logic ............................................... 301
Tarasyuk I.V. Performance Analysis of the Dining 
   Philosophers System in dtsPBC .............................. 309
Zagorulko Yu., Zagorulko G. Open Extensible Tools for 
   Development of Intelligent DSS: Towards an Architecture .... 322