13th International Symposium on Automated Technology for Verification and Analysis
October 12–15, 2015, Shanghai, China
| 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 |