Abstract is missing.
- Probabilistic Programming: A True Verification ChallengeJoost-Pieter Katoen. 1-3 [doi]
- Machines Reasoning About Machines: 2015J. Strother Moore. 4-13 [doi]
- Using SMT for Solving Fragments of Parameterised Boolean Equation SystemsRuud P. J. Koolen, Tim A. C. Willemse, Hans Zantema. 14-30 [doi]
- Unfolding-Based Process DiscoveryHernán Ponce de León, César Rodríguez, Josep Carmona, Keijo Heljanko, Stefan Haar. 31-47 [doi]
- Improving Interpolants for Linear ArithmeticErnst Althaus, Björn Beber, Joschka Kupilas, Christoph Scholl. 48-63 [doi]
- A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic DifferencesThibaut Girka, David Mentré, Yann Régis-Gianas. 64-79 [doi]
- On Automated Lemma Generation for Separation Logic with Inductive DefinitionsConstantin Enea, Mihaela Sighireanu, Zhilin Wu. 80-96 [doi]
- Severity Levels of Inconsistent CodeMartin Schäf, Ashish Tiwari. 97-113 [doi]
- Learning the Language of ErrorMartin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, Michael Tautschnig. 114-130 [doi]
- Explicit Model Checking of Very Large MDP Using Partitioning and Secondary StorageArnd Hartmanns, Holger Hermanns. 131-147 [doi]
- Model Checking Failure-Prone Open Systems Using Probabilistic AutomataYue Ben, A. Prasad Sistla. 148-165 [doi]
- Optimal Continuous Time Markov DecisionsYuliya Butkova, Hassan Hatefi, Holger Hermanns, Jan Krcál. 166-182 [doi]
- Spanning the Spectrum from Safety to LivenessRachel Faran, Orna Kupferman. 183-200 [doi]
- Marimba: A Tool for Verifying Properties of Hidden Markov ModelsNoé Hernández, Kerstin Eder, Evgeni Magid, Jesús Savage, David A. Rosenblueth. 201-206 [doi]
- ParaVerifier: An Automatic Framework for Proving Parameterized Cache Coherence ProtocolsYongjian Li, Jun Pang, Yi Lv, Dongrui Fan, Shen Cao, Kaiqiang Duan. 207-213 [doi]
- ASSA-PBN: An Approximate Steady-State Analyser of Probabilistic Boolean NetworksAndrzej Mizera, Jun Pang, Qixia Yuan. 214-220 [doi]
- EviCheck: Digital Evidence for AndroidMohamed Nassim Seghir, David Aspinall. 221-227 [doi]
- Lazy-CSeq-SP: Boosting Sequentialization-Based Verification of Multi-threaded C Programs via Symbolic Pruning of Redundant SchedulesVladimir Herdt, Hoang M. Le, Daniel Große, Rolf Drechsler. 228-233 [doi]
- A Contextual Equivalence Checker for IMJ ∗Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos. 234-240 [doi]
- Trace Diagnostics Using Temporal ImplicantsThomas Ferrère, Oded Maler, Dejan Nickovic. 241-258 [doi]
- Test Case Generation of Actor SystemsElvira Albert, Puri Arenas, Miguel Gómez-Zamalloa. 259-275 [doi]
- Lattice-Based Semantics for Combinatorial Model EvolutionRachel Tzoref-Brill, Shahar Maoz. 276-292 [doi]
- Effective Verification of Replicated Data Types Using Later Appearance Records (LAR)Madhavan Mukund, Gautham Shenoy R., S. P. Suresh. 293-308 [doi]
- TSO-to-TSO Linearizability Is UndecidableChao Wang, Yi Lv, Peng Wu. 309-325 [doi]
- Formal Verification of Infinite-State BIP ModelsSimon Bliudze, Alessandro Cimatti, Mohamad Jaber, Sergio Mover, Marco Roveri, Wajeb Saab, Qiang Wang. 326-343 [doi]
- PBMC: Symbolic Slicing for the Verification of Concurrent ProgramsHabib Saissi, Péter Bokor, Neeraj Suri. 344-360 [doi]
- On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter SystemsSteen Vester. 361-377 [doi]
- Hierarchical Information Patterns and Distributed Strategy SynthesisDietmar Berwanger, Anup Basil Mathew, Marie van den Bogaard. 378-393 [doi]
- Cooperative Reactive SynthesisRoderick Bloem, Rüdiger Ehlers, Robert Könighofer. 394-410 [doi]
- Game Semantic Analysis of Equivalence in IMJAndrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos. 411-428 [doi]
- Looking at Mean-Payoff Through Foggy WindowsPaul Hunter, Guillermo A. Pérez, Jean-François Raskin. 429-445 [doi]
- Bounded Verification with On-the-Fly Discrepancy ComputationChuchu Fan, Sayan Mitra. 446-463 [doi]
- Formal Verification of Simulink/Stateflow DiagramsLiang Zou, Naijun Zhan, Shuling Wang, Martin Fränzle. 464-481 [doi]
- Decidability of the Reachability for a Family of Linear Vector FieldsTing Gan, Mingshuai Chen, Liyun Dai, Bican Xia, Naijun Zhan. 482-499 [doi]
- Stochastic Local Search for Falsification of Hybrid SystemsJyotirmoy V. Deshmukh, Xiaoqing Jin, James Kapinski, Oded Maler. 500-517 [doi]