Abstract is missing.
- General Lessons from a Rely/Guarantee DevelopmentCliff B. Jones, Andrius Velykis, Nisansala Yatapanage. 3-22 [doi]
- Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPsVahid Hashemi, Andrea Turrini, Ernst Moritz Hahn, Holger Hermanns, Khaled Elbassioni. 25-41 [doi]
- Better Automated Importance Splitting for Transient Rare EventsCarlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns. 42-58 [doi]
- On the Criticality of Probabilistic Worst-Case Execution Time ModelsLuca Santinelli, Zhishan Guo. 59-74 [doi]
- Nested Timed Automata with InvariantsYuwei Wang, Guoqiang Li 0001, Shoji Yuen. 77-93 [doi]
- Multi-core Cyclic Executives for Safety-Critical SystemsCalvin Deutschbein, Tom Fleming, Alan Burns, Sanjoy Baruah. 94-109 [doi]
- Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration CalculusDimitar P. Guelev, Shuling Wang, Naijun Zhan. 110-127 [doi]
- Termination of Semi-algebraic Loop ProgramsYi Li. 131-146 [doi]
- Computing Exact Loop Bounds for Bounded Program VerificationTianhai Liu, Shmuel S. Tyszberowicz, Bernhard Beckert, Mana Taghdiri. 147-163 [doi]
- AndroidLeaker: A Hybrid Checker for Collusive Leak in Android ApplicationsZipeng Zhang, Xinyu Feng. 164-180 [doi]
- Remark on Some \pi VariantsJianxin Xue, Huan Long, Yuxi Fu. 183-199 [doi]
- Reasoning About Periodicity on Infinite WordsWanwei Liu, Fu Song, Ge Zhou. 200-215 [doi]
- On Equivalence Checking of Nondeterministic Finite AutomataChen Fu, Yuxin Deng, David N. Jansen, Lijun Zhang 0001. 216-231 [doi]
- A New Decomposition Method for Attractor Detection in Large Synchronous Boolean NetworksAndrzej Mizera, Jun Pang, Hongyang Qu 0001, Qixia Yuan. 232-249 [doi]
- Construction of Abstract State Graphs for Understanding Event-B ModelsDaichi Morita, Fuyuki Ishikawa, Shinichi Honiden. 250-265 [doi]
- A Framework for Modeling and Verifying IoT Communication ProtocolsMaithily Diwan, Meenakshi D'Souza. 266-280 [doi]
- Formal Analysis of Information Flow in HOLGhassen Helali, Sofiène Tahar, Osman Hasan, Tsvetan Dunchev. 283-299 [doi]
- Formalizing SPARCv8 Instruction Set Architecture in CoqJiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng. 300-316 [doi]
- How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven ApproachStefano Schivo, Bugra M. Yildiz, Enno Ruijters, Christopher Gerking, Rajesh Kumar, Stefan Dziwok, Arend Rensink, Mariëlle Stoelinga. 319-336 [doi]
- PranCS: A Protocol and Discrete Controller Synthesis ToolIdress Husien, Sven Schewe, Nicolas Berthier. 337-349 [doi]