ATVA 2015

13th International Symposium on Automated Technology for Verification and Analysis

October 12–15, 2015, Shanghai, China

ATVA 2015 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