| 2015 | TSO-to-TSO Linearizability Is Undecidable. | Chao Wang, Yi Lv, Peng Wu |
| 2015 | On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems. | Steen Vester |
| 2015 | Lattice-Based Semantics for Combinatorial Model Evolution. | Rachel Tzoref-Brill, Shahar Maoz |
| 2015 | EviCheck: Digital Evidence for Android. | Mohamed Nassim Seghir, David Aspinall |
| 2015 | Severity Levels of Inconsistent Code. | Martin Schf, Ashish Tiwari |
| 2015 | PBMC: Symbolic Slicing for the Verification of Concurrent Programs. | Habib Saissi, Pter Bokor, Neeraj Suri |
| 2015 | Game Semantic Analysis of Equivalence in IMJ. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2015 | A Contextual Equivalence Checker for IMJ ∗. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2015 | Effective Verification of Replicated Data Types Using Later Appearance Records (LAR). | Madhavan Mukund, Ranjal Gautham Shenoy, S. P. Suresh |
| 2015 | Machines Reasoning About Machines: 2015. | J Strother Moore |
| 2015 | ASSA-PBN: An Approximate Steady-State Analyser of Probabilistic Boolean Networks. | Andrzej Mizera, Jun Pang, Qixia Yuan |
| 2015 | ParaVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols. | Yongjian Li, Jun Pang, Yi Lv, Dongrui Fan, Shen Cao, Kaiqiang Duan |
| 2015 | Unfolding-Based Process Discovery. | Hernn Ponce de Len, Csar Rodrguez, Josep Carmona, Keijo Heljanko, Stefan Haar |
| 2015 | Using SMT for Solving Fragments of Parameterised Boolean Equation Systems. | Ruud P. J. Koolen, Tim A. C. Willemse, Hans Zantema |
| 2015 | Probabilistic Programming: A True Verification Challenge. | Joost-Pieter Katoen |
| 2015 | Looking at Mean-Payoff Through Foggy Windows. | Paul Hunter, Guillermo A. Prez, Jean-Franois Raskin |
| 2015 | Marimba: A Tool for Verifying Properties of Hidden Markov Models. | No Hernndez, Kerstin Eder, Evgeni Magid, Jess Savage, David A. Rosenblueth |
| 2015 | Lazy-CSeq-SP: Boosting Sequentialization-Based Verification of Multi-threaded C Programs via Symbolic Pruning of Redundant Schedules. | Vladimir Herdt, Hoang Minh Le, Daniel Groe, Rolf Drechsler |
| 2015 | Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage. | Arnd Hartmanns, Holger Hermanns |
| 2015 | A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences. | Thibaut Girka, David Mentr, Yann Rgis-Gianas |
| 2015 | Decidability of the Reachability for a Family of Linear Vector Fields. | Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, Naijun Zhan |
| 2015 | Trace Diagnostics Using Temporal Implicants. | Thomas Ferrre, Oded Maler, Dejan Nickovic |
| 2015 | Spanning the Spectrum from Safety to Liveness. | Rachel Faran, Orna Kupferman |
| 2015 | Bounded Verification with On-the-Fly Discrepancy Computation. | Chuchu Fan, Sayan Mitra |
| 2015 | On Automated Lemma Generation for Separation Logic with Inductive Definitions. | Constantin Enea, Mihaela Sighireanu, Zhilin Wu |