Abstract is missing.
- A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety CaseValentin Cassano, Thomas S. E. Maibaum, Silviya Grigorova. 1-17 [doi]
- Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa's Case (Extended Abstract)Keijiro Araki, Taro Kurita. 18-25 [doi]
- Automated Requirements Validation for ATP Software via Specification Review and TestingWeikai Miao, Geguang Pu, Yinbo Yao, Ting Su, Danzhu Bao, Yang Liu 0003, Shuohao Chen, Kunpeng Xiong. 26-40 [doi]
- Automatic Generation of Potentially Pathological Instances for Validating Alloy ModelsTakaya Saeki, Fuyuki Ishikawa, Shinichi Honiden. 41-56 [doi]
- A General Lattice Model for Merging Symbolic Execution BranchesDominic Scheurer, Reiner Hähnle, Richard Bubel. 57-73 [doi]
- A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid AutomataRyo Yanase, Tatsunori Sakai, Makoto Sakai, Satoshi Yamane. 74-89 [doi]
- Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water TanksRichard Banach, Michael J. Butler. 90-105 [doi]
- A System Substitution Mechanism for Hybrid Systems in Event-BGuillaume Babin, Yamine Aït Ameur, Neeraj Kumar Singh, Marc Pantel. 106-121 [doi]
- Service Adaptation with Probabilistic Partial ModelsManman Chen, Tian Huat Tan, Jun Sun, Jingyi Wang, Yang Liu, Jing Sun 0002, Jin Song Dong. 122-140 [doi]
- A Formal Approach to Identifying Security Vulnerabilities in Telecommunication NetworksLinas Laibinis, Elena Troubitsyna, Inna Pereverzeva, Ian Oliver, Silke Holtmanns. 141-158 [doi]
- Multi-threaded On-the-Fly Model Generation of Malware with Hash CompactionNguyen Minh Hai, Quan Thanh Tho, Le Duc Anh. 159-174 [doi]
- CPDY: Extending the Dolev-Yao Attacker with Physical-Layer InteractionsMarco Rocchetto, Nils Ole Tippenhauer. 175-192 [doi]
- Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal LogicFrancesco Marconi, Marcello M. Bersani, Madalina Erascu, Matteo Rossi. 193-209 [doi]
- Proving Event-B Models with Reusable Generic LemmasAlexei Iliasov, Paulius Stankaitis, Alexander Romanovsky. 210-225 [doi]
- Formal Availability Analysis Using Theorem ProvingWaqar Ahmed, Osman Hasan. 226-242 [doi]
- Formal Verification of the rank Algorithm for Succinct Data StructuresAkira Tanaka, Reynald Affeldt, Jacques Garrigue. 243-260 [doi]
- Contextual Trace Refinement for Concurrent Objects: Safety and ProgressBrijesh Dongol, Lindsay Groves. 261-278 [doi]
- Local Livelock Analysis of Component-Based ModelsMadiel S. Conserva Filho, Marcel Vinicius Medeiros Oliveira, Augusto Sampaio, Ana Cavalcanti. 279-295 [doi]
- Session-Based Compositional Analysis for Actor-Based Languages Using FuturesEduard Kamburjan, Crystal Chang Din, Tzu-Chun Chen. 296-312 [doi]
- An Event-B Development Process for the Distributed BIP FrameworkBadr Siala, Mohamed Tahar Bhiri, Jean-Paul Bodeveix, Mamoun Filali. 313-328 [doi]
- Partial Order Reduction for State/Event SystemsShuanglong Kan, Zhiqiu Huang, Zhe Chen. 329-345 [doi]
- Concolic Unbounded-Thread Reachability via Loop SummariesPeizun Liu, Thomas Wahl. 346-362 [doi]
- Scaling BDD-based Timed Verification with Simulation ReductionTruong Khanh Nguyen, Tian Huat Tan, Jun Sun, Jiaying Li, Yang Liu, Manman Chen, Jin Song Dong. 363-382 [doi]
- Model Checking Real-Time Properties on the Functional Layer of Autonomous RobotsMohammed Foughali, Bernard Berthomieu, Silvano Dal-Zilio, Félix Ingrand, Anthony Mallet. 383-399 [doi]
- Decision Problems for Parametric Timed AutomataÉtienne André, Didier Lime, Olivier H. Roux. 400-416 [doi]
- Verifying Nested Lock Priority Inheritance in RTEMS with Java PathfinderSaurabh Gadia, Cyrille Artho, Gedare Bloom. 417-432 [doi]
- An SMT-Based Approach to the Formal Analysis of MARTE/CCSLMin Zhang, Frédéric Mallet, Huibiao Zhu. 433-449 [doi]
- Checking SysML Models for Co-simulationNuno Amálio, Richard Payne, Ana Cavalcanti, Jim Woodcock. 450-465 [doi]
- A CEGAR Scheme for Information Flow AnalysisManuel Töws, Heike Wehrheim. 466-483 [doi]