| 2014 | Formal Throughput and Response Time Analysis of MARTE Models. | Gaogao Yan, Xueyang Zhu, Rongjie Yan, Guangyuan Li |
| 2014 | GPU Accelerated Counterexample Generation in LTL Model Checking. | Zhimin Wu, Yang Liu, Yun Liang, Jun Sun |
| 2014 | Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code. | Jonatan Wiik, Pontus Bostrm |
| 2014 | Fast Translation from LTL to Bchi Automata via Non-transition-based Automata. | Shohei Mochizuki, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki |
| 2014 | Bounded Model Checking High Level Petri Nets in PIPE+Verifier. | Su Liu, Reng Zeng, Zhuo Sun, Xudong He |
| 2014 | Formal Modeling and Analysis of Cassandra in Maude. | Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta, Jos Meseguer |
| 2014 | On the Formal Analysis of HMM Using Theorem Proving. | Liya Liu, Vincent Aravantinos, Osman Hasan, Sofine Tahar |
| 2014 | TAuth: Verifying Timed Security Protocols. | Li Li, Jun Sun, Yang Liu, Jin Song Dong |
| 2014 | Practical Analysis Framework for Software-Based Attestation Scheme. | Li Li, Hong Hu, Jun Sun, Yang Liu, Jin Song Dong |
| 2014 | A Resource-Based Logic for Termination and Non-termination Proofs. | Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin |
| 2014 | A Formula-Based Approach for Automatic Fault Localization of Imperative Programs. | Si-Mohamed Lamraoui, Shin Nakajima |
| 2014 | GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems. | Fatma Jebali, Frdric Lang, Radu Mateescu |
| 2014 | Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior. | Klaus Havelund, Rajeev Joshi |
| 2014 | A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators. | Mounira Kezadri Hamiaz, Marc Pantel, Benot Combemale, Xavier Thirioux |
| 2014 | SCC-Based Improved Reachability Analysis for Markov Decision Processes. | Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong |
| 2014 | An LTL Model Checking Approach for Biological Parameter Inference. | Emmanuelle Gallet, Matthieu Manceny, Pascale Le Gall, Paolo Ballarini |
| 2014 | Pointer Program Derivation Using Coq: Graphs and Schorr-Waite Algorithm. | Jean-Franois Dufourd |
| 2014 | Modal Characterisations of Probabilistic and Fuzzy Bisimulations. | Yuxin Deng, Hengyang Wu |
| 2014 | Approximations for Stochastic Graph Rewriting. | Vincent Danos, Tobias Heindel, Ricardo Honorato-Zimmer, Sandro Stucki |
| 2014 | PHASE: A Stochastic Formalism for Phase-Type Distributions. | Gabriel Ciobanu, Armand Stefan Rotaru |
| 2014 | A Language-Independent Proof System for Mutual Program Equivalence. | Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu |
| 2014 | A Hybrid Model of Connectors in Cyber-Physical Systems. | Xiaohong Chen, Jun Sun, Meng Sun |
| 2014 | A Formal Model for Natural-Language Timed Requirements of Reactive Systems. | Gustavo Carvalho, Ana Carvalho, Eduardo Rocha, Ana Cavalcanti, Augusto Sampaio |
| 2014 | Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints. | Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi |
| 2014 | Complete Model-Based Equivalence Class Testing for the ETCS Ceiling Speed Monitor. | Ccile Braunstein, Anne E. Haxthausen, Wen-ling Huang, Felix Hbner, Jan Peleska, Uwe Schulze, Linh Vu Hong |