Call for participation 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
October 12-15, 2015, Shanghai, China http://atva2015.ios.ac.cn/ *** Early registration deadline: August 15, 2015 *** ATVA promotes research on theoretical and practical aspects of automated analysis, verification and synthesis by providing a forum for interaction between the regional and the international research communities and industry in the field. The conference will be held at East China Normal University (old campus) in Shanghai. Shanghai is China’s largest economic comprehensive industrial base, and a famous historical and cultural city. KEYNOTES and TUTORIALS Dino Distefano (Facebook and Queen Mary University of London, UK) Martin Fränzle (Carl von Ossietzky Universität, Oldenburg, Germany) Joost-Pieter Katoen (RWTH Aachen University, Germany) J Strother Moore (University of Texas-Austin, USA) ACCOMODATION ATVA has arranged special rates at nearby hotels for conference participants. If you book early, you may also be able to take advantage of special offers available at many other nearby hotels in the range of 230-700 CNY per night. REGISTRATION Registration is open now. The early registration fee is 2500CNY, late is 3000CNY, and 3500CNY for author registration. The fee includes registration, lunches and coffee breaks on all conference days, the conference dinner and the welcome reception (including food). Early registration deadline: August 15, 2015 For details see http://atva2015.ios.ac.cn/participation.html#registration ACCEPTED PAPERS Steen Vester. On the Complexity of Model-checking Branching and Alternating-time Temporal Logics in One-counter systems Noe Hernandez, Kerstin Eder, Evgeni Magid, Jesus Savage and David Rosenblueth. Marimba: A Tool for Verifying Properties of Hidden Markov Models Arnd Hartmanns and Holger Hermanns. Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage Chuchu Fan and Sayan Mitra. Bounded Verification with On-the-Fly Discrepancy Computation Thomas Ferrere, Oded Maler and Dejan Nickovic. Trace Diagnostics using Temporal Implicants Puri Arenas, Elvira Albert and Miguel Gomez-Zamalloa. Test Case Generation of Actor Systems Yongjian Li, Jun Pang, Yi Lv, Dongrui Fan, Shen Cao and Kaiqiang Duan. paraVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols Chao Wang, Yi Lv and Peng Wu. TSO-to-TSO Linearizability is Undecidable Yue Ben and A. Prasad Sistla. Model Checking Failure Prone Open Systems Using Probabilistic Automata Ruud Koolen, Tim Willemse and Hans Zantema. Using SMT for Solving Fragments of Parameterised Boolean Equation Systems Andrzej Mizera, Jun Pang and Qixia Yuan. ASSA-PBN: An Approximate Steady-state Analyser of Probabilistic Boolean Networks Rachel Tzoref-Brill and Shahar Maoz. Lattice-Based Semantics for Combinatorial Model Evolution Paul Hunter, Guillermo Perez and Jean-Francois Raskin. Looking at Mean-Payoff through Foggy Windows Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman and Michael Tautschnig. Learning the Language of Error Rachel Faran and Orna Kupferman. Spanning the Spectrum from Safety to Liveness Liang Zou, Naijun Zhan, Shuling Wang and Martin Fränzle. Formal Verification of Simulink/Stateflow Diagrams Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia and Naijun Zhan. Decidability of the Reachability for a Family of Linear Vector Fields Thibaut Girka, David Mentré and Yann Régis-Gianas. A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences Hernan Ponce-De-Leon, César Rodríguez, Josep Carmona, Keijo Heljanko and Stefan Haar. Unfolding-Based Process Discovery Constantin Enea, Mihaela Sighireanu and Zhilin Wu. On Automated Lemma Generation for Separation Logic with Inductive Definitions Mohamed Nassim Seghir and David Aspinall. EviCheck: Digital Evidence for Android Simon Bliudze, Alessandro Cimatti, Mohamad Jaber, Sergio Mover, Marco Roveri, Wajeb Saab and Wang Qiang. Formal Verification of Infinite-sate BIP models Andrzej Murawski, Steven Ramsay and Nikos Tzevelekos. Game Semantic Analysis of Equivalence in IMJ Roderick Bloem, Rüdiger Ehlers and Robert Koenighofer. Cooperative Reactive Synthesis Habib Saissi, Peter Bokor and Neeraj Suri. PBMC: Symbolic Slicing for the Verification of Concurrent Programs Jyotirmoy Deshmukh, Xiaoqing Jin, James Kapinski and Oded Maler. Stochastic Local Search for Falsification of Hybrid Systems Martin Schaef and Ashish Tiwari. Severity Levels of Inconsistent Code Madhavan Mukund, Gautham Shenoy R and S P Suresh. Effective verification of Replicated Data Types using Later Appearance Records (LAR) Vladimir Herdt, Hoang M. Le, Daniel Grosse and Rolf Drechsler. Lazy-CSeq-SP: Boosting Sequentialization-based Verification of Multi-Threaded C Programs via Symbolic Pruning of Redundant Schedules Dietmar Berwanger, Anup Basil Mathew and Marie Van Den Bogaard. Hierarchical Information Patterns and Distributed Strategy Synthesis Andrzej Murawski, Steven Ramsay and Nikos Tzevelekos. A Contextual Equivalence Checker for IMJ* Yuliya Butkova, Hassan Hatefi, Holger Hermanns and Jan Krcal. Optimal Continuous Time Markov Decisions Ernst Althaus, Björn Beber, Joschka Kupilas and Christoph Scholl. Improving Interpolants for Linear Arithmetic GENERAL CHAIR Jifeng He (East China Normal University, China) PROGRAMME CHAIRS Bernd Finkbeiner (Saarland University, Germany) Geguang Pu (East China Normal University, China) Lijun Zhang (Institute of Software, Chinese Academy of Sciences) WORKSHOP CHAIR Jun Sun (Singapore University of Technology and Design, SG) PUBLICITY CHAIRS David N. Jansen (Radboud Universiteit, Netherlands) Huibiao Zhu (East China Normal University, China) PROGRAM COMMITTEE Alessandro Abate (University of Oxford, UK) Erika Ábrahám (RWTH Aachen University, Germany) Michael Backes (Saarland University, Germany) Christel Baier (Technical University of Dresden, Germany) Ahmed Bouajjani (University Paris Diderot, FR) Tevfik Bultan (University of California at Santa Barbara, USA) Franck Cassez (NICTA, Australia) Rance Cleaveland (University of Maryland, USA) Hung Dang-Van (UET, Vietnam National University, Vietnam) Bernd Finkbeiner (Saarland University, Germany) Mark Greenstreet (University of British Columbia, Canada) Holger Hermanns (Saarland University, Germany) Pao-Ann Hsiung (National Chung Cheng University, Taiwan) Alan Hu (University of British Columbia, Canada) Michael Huth (Imperial College London, UK) Jie-Hong Roland Jiang (National Taiwan University, Taiwan) Orna Kupferman (Hebrew University, Israel) Kim Guldstrand Larsen (Aalborg University, Denmark) Xuandong Li (Nanjing University, China) Annabelle McIver (Macquarie University, AU) Ken McMillan (Microsoft, USA) Madhavan Mukund (Chennai Mathematical Institute, India) Flemming Nielson (Technical University of Denmark, Denmark) Mizuhito Ogawa (Japan Advanced Institute of Science and Technology) Catuscia Palamidessi (INRIA Saclay and LIX, FR) Doron Peled (Bar Ilan University, Israel) Geguang Pu (East China Normal University, China) Jean-François Raskin (Université Libre de Bruxelles, Belgium) Kristin Y. Rozier (NASA's Ames Research Center, USA) Sven Schewe (Liverpool University, UK) Scott Smolka (Stony Brook University, USA) Farn Wang (National Taiwan University, Taiwan) Bow-Yaw Wang (Academia Sinica, Taiwan) Wang Yi (Uppsala University, Sweden) Naijun Zhan (Institute of Software, Chinese Academy of Sciences) Lijun Zhang (Institute of Software, Chinese Academy of Sciences) STEERING COMMITTEE E. Allen Emerson (University of Texas-Austin, USA) Teruo Higashino (Osaka University, Japan) Insup Lee (University of Pennsylvania, USA) Doron Peled (Bar Ilan University, Israel) Farn Wang (National Taiwan University, Taiwan) Hsu-Chun Yen (National Taiwan University, Taiwan)
_______________________________________________ Om-announce mailing list [email protected] http://openmath.org/mailman/listinfo/om-announce
