| Diego Marmsoler |
A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL |
| Wanling Xie, Huibiao Zhu and Shengchao Qin |
UTP Semantics for BigrTiMo |
| Yuan Fei and Huibiao Zhu |
Modeling and Verifying NDN Access Control Using CSP |
| Teck Ping Khoo and Jun Sun |
The Miles before Formal Methods - a Case Study on Modeling a Passenger Lift System |
| Nils Berg, Thomas Göthel, Sabine Glesner and Armin Danziger |
Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages |
| Guohui Wang, Yong Guan, Zhiping Shi, Qianying Zhang, Xiaojuan Li and Yongdong Li |
Formalization of Symplectic Geometry in HOL-Light |
| Inna Vistbakka, Amin Majd and Elena Troubitsyna |
Deriving Mode Logic for Autonomous Resilient Systems |
| Matthieu Martel |
Strongly Typed Numerical Computations |
| Timm Liebrenz, Paula Herber and Sabine Glesner |
Deductive Verification of Hybrid Control Systems modeled in Simulink with KeYmaera X |
| Tsutomu Kobayashi and Fuyuki Ishikawa |
Analysis on Strategies of Superposition Refinement of Event-B Specifications |
| Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt and Michael Fisher |
The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators |
| Dileepa Fernando, Naipeng Dong, Cyrille Jegourel and Jin Song Dong |
Verification of Strong Nash-equilibrium for Probabilistic BAR Systems |
| Xi Wu, Yi Lu, Patrick Meiring, Ian Hayes and Larissa Meinicke |
Type Capabilities for Object-Oriented Programming Languages |
| Mihai Herda, Michael Kirsten, Marko Kleine Büning, Bernhard Beckert and Simon Bischof |
Using Theorem Provers to Improve the Precision of Dependency Analysis for Information Flow Control |
| Vladimír Štill and Jiří Barnat |
Model Checking of C++ Programs under the x86-TSO Memory Model |
| Colin Snook, Thai Son Hoang, Dana Dghaym, Michael Butler, Tomas Fischer, Rupert Schlick and Keming Wang |
Behaviour-driven formal model development |
| Aaron Craig, Alex Potanin, Lindsay Groves and Jonathan Aldrich |
Capabilities: Effects for Free |
| Michael Foster, Ramsay Taylor, Achim Brucker and John Derrick |
Formalising Extended Finite State Machine Transition Merging |
| Naipeng Dong and Tim Muller |
The Foul Adversary: Formal Models |
| Cunjing Ge, Jiwei Yan, Jun Yan and Jian Zhang |
Checking Activity Transition Systems with Back Transitions against Assertions |
| Jinyun Xue, Yujun Zheng, Qimin Hu, Zhen You, Wuping Xie and Zhuo Cheng |
PAR: A Practicable Formal Method and Its Supporting Platform |
| Zhiwu Xu, Kerong Ren, Shengchao Qin, and Florin Craciun |
CDGDroid: Android Malware Detection Based on Deep Learning using CFG and DFG |
