| 2017 | Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking. | Si Liu, Peter Csaba lveczky, Jatin Ganhotra, Indranil Gupta, Jos Meseguer |
| 2017 | An Improved Android Collusion Attack Detection Method Based on Program Slicing. | Yunhao Liu, Xiaohong Li, Zhiyong Feng, Jianye Hao |
| 2017 | Classification-Based Parameter Synthesis for Parametric Timed Automata. | Jiaying Li, Jun Sun, Bo Gao, tienne Andr |
| 2017 | A Sliding-Window Algorithm for On-The-Fly Interprocedural Program Analysis. | Xin Li, Mizuhito Ogawa |
| 2017 | A Verification Framework for Stateful Security Protocols. | Li Li, Naipeng Dong, Jun Pang, Jun Sun, Guangdong Bai, Yang Liu, Jin Song Dong |
| 2017 | A Certified Decision Procedure for Tree Shares. | Xuan Bach Le, Thanh-Toan Nguyen, Wei-Ngan Chin, Aquinas Hobor |
| 2017 | Detecting Energy Bugs in Android Apps Using Static Analysis. | Hao Jiang, Hongli Yang, Shengchao Qin, Zhendong Su, Jian Zhang, Jun Yan |
| 2017 | Refinement-Based Modelling and Verification of Design Patterns for Self-adaptive Systems. | Thomas Gthel, Nils Jhnig, Simon Seif |
| 2017 | Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability. | Marie Farrell, Rosemary Monahan, James F. Power |
| 2017 | Verifying Temporal Properties of C Programs via Lazy Abstraction. | Zhao Duan, Cong Tian, Zhenhua Duan |
| 2017 | Improving the Scalability of Automatic Linearizability Checking in SPIN. | Patrick Doolan, Graeme Smith, Chenyi Zhang, Padmanabhan Krishnan |
| 2017 | An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics. | Yuxin Deng, Min Zhang, Guoqing Lei |
| 2017 | Compiling Parameterized X86-TSO Concurrent Programs to Cubicle- | Sylvain Conchon, David Declerck, Fatiha Zadi |
| 2017 | A Framework for Multi-view Reconciliation and for Medical Devices Personalization. | Yihai Chen, Bofang Zhang, Ridha Khdri, Huaikou Miao |
| 2017 | Transforming Timing Requirements into CCSL Constraints to Verify Cyber-Physical Systems. | Xiaohong Chen, Ling Yin, Yijun Yu, Zhi Jin |
| 2017 | Model Checking Pushdown Epistemic Game Structures. | Taolue Chen, Fu Song, Zhilin Wu |
| 2017 | A Flexible Approach for Finding Optimal Paths with Minimal Conflicts. | Juliana Kster Filipe Bowles, Marco B. Caminati |
| 2017 | Modularization of Refinement Steps for Agile Formal Methods. | Fabian Benduhn, Thomas Thm, Ina Schaefer, Gunter Saake |
| 2016 | An SMT-Based Approach to the Formal Analysis of MARTE/CCSL. | Min Zhang, Frdric Mallet, Huibiao Zhu |
| 2016 | A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata. | Ryo Yanase, Tatsunori Sakai, Makoto Sakai, Satoshi Yamane |
| 2016 | A CEGAR Scheme for Information Flow Analysis. | Manuel Tws, Heike Wehrheim |
| 2016 | Formal Verification of the rank Algorithm for Succinct Data Structures. | Akira Tanaka, Reynald Affeldt, Jacques Garrigue |
| 2016 | An Event-B Development Process for the Distributed BIP Framework. | Badr Siala, Mohamed Tahar Bhiri, Jean-Paul Bodeveix, Mamoun Filali |
| 2016 | A General Lattice Model for Merging Symbolic Execution Branches. | Dominic Scheurer, Reiner Hhnle, Richard Bubel |
| 2016 | Automatic Generation of Potentially Pathological Instances for Validating Alloy Models. | Takaya Saeki, Fuyuki Ishikawa, Shinichi Honiden |