Accepted papers | TASE 2017

Sebastian Küpper, Barbara König, Alexandra Silva and Harsh Beohar. Conditional Transition Systems with Upgrades.
Yueling Zhang, Jianwen Li, Min Zhang, Geguang Pu and Fu Song. Optimizing Backbone Filtering.
Claudio Antares Mezzina and Vasileios Koutavas. A Safety and Liveness Theory for Total Reversibility.
Shichao Liu and Ying Jiang. Modeling and Reasoning About Wireless Networks: A Graph-based Calculus Approach.
Bingqing Xu and Qin Li. A Bounded Multi-dimensional Modal Logic for Autonomous Cars Based on Local Traffic and Estimation.
Messaoud Rahim, Malika Ioualalen and Ahmed Hammad. Slicing Based Verification Approach for the Validation of SysML Activity Diagrams. (short)
Pattaravut Maleehuan, Yuki Chiba and Toshiaki Aoki. Assembly Program Verification for Multiprocessors with Relaxed Memory Model using SMT Solver.
Jacques Julliand, Olga Kouchnarenko, Pierre-Alain Masson and Guillaume Voiron. Two Under-Approximation Techniques for 3-Modal Abstraction Coverage of Event Systems: Joint Effort?
Chunyan Mu and Shengchao Qin. Time-sensitive Information Flow Control in Timed Event-B.
Tian-Ming Bu, Hengyang Wu and Yixiang Chen. Computing Behavioural Distance for Fuzzy Transition Systems.
Diego Marmsoler. On the Semantics of Temporal Specifications of Component-Behavior for Dynamic Architectures. (short)
Jian Liu, Ying Jiang and Yanyun Chen. VMDV: A 3D Visualization Tool for Modeling, Demonstration, and Verification. (tool)
Juliana Küster Filipe Bowles, Marco B. Caminati and Suhyun Cha. An Integrated Framework for Verifying Multiple Care Pathways.
Haiyang Liu, Tingting Hu and Zongyan Qiu. Automatic Fine-grain Locking Generation for Shared Data Structures.
Ning Ge, Arnaud Dieumegard, Eric Jenn, Bruno D’ausbourg and Yamine Aït-Ameur. Formal Development Process of Safety-Critical Embedded Human Machine Interface Systems.
Zeineb Zhioua, Yves Roudier and Rabea Boulifa Ameur. Formal Specification of Security Guidelines for Program Certification.
Ning Ge, Marc Pantel and Silvano Dal Zilio. Formal Verification of User-Level Real-Time Property Patterns. (slides)
Yan Ma, Zining Cao and Yang Liu. PSO-based refinement for CEGAR in stochastic model checking.
Yuxin Deng and Yuan Feng. Bisimulations for Probabilistic Lambda Calculi.