(User-friendly) formal requirements verification in the context of ISO26262 by Denis Makartetskiy, Guido Marchetto, Riccardo Sisto, Fulvio Valenza, Matteo Virgilio, Denise Leri, Paolo Denti, Roberto Finizio

“…This paper proposes an approach for requirements formal verification where formal methods, languages, and tools are only minimally exposed to the user, and are integrated into one of the commonly used system modeling environments based on SysML. …”
Get full text

P3 problem and Magnolia language: Specializing array computations for emerging architectures by Benjamin Chetioui, Marius Kleppe Larnøy, Jaakko Järvi, Magne Haveraaen, Lenore Mullin

“…Axioms can be used to produce tests for concrete implementations of specifications, for formal verification, or to perform semantics-preserving program transformations. …”
Get full text

PROLEAD_SW by Jannik Zeitschner, Nicolai Müller, Amir Moradi

“…These include (1) evaluation of larger designs compared to the state of the art, e.g. a full Advanced Encryption Standard (AES) masked implementation, and (2) formal verification under our new generic leakage model for CPUs. …”
Get full text

On Reconfiguration Theory of Discrete-Event Systems: From Initial Specification Until Final Deployment by Mohamed Khalgui, Olfa Mosbahi, Zhiwu Li

“…Since the development of distributed RDESs under functional and extra-functional constraints is required by experts, we propose a complete methodology that deals first with their initial design with a new general profile named R-UML extending unified modeling language (UML) or also with new specific technology-oriented profiles, the validation of the related models with a new language R-OCL extending object constraint language (OCL), before their transformation to formal formalisms, such as Petri nets, timed automata, or B method for simulation or also formal verification of different properties. The checked models are transformed into OS reconfigurable tasks in the operational level, before applying a co-design methodology under functional, real-time, memory, and energy constraints for minimizing redundancies in tasks and for optimizing the composition of software and hardware parts together. …”
Get full text

A Systematic Mapping Study on Software Quality Control Techniques for Assessing Privacy in Information Systems by Danny S. Guaman, Jose M. Del Alamo, Julio C. Caiza

“…The maturity of the techniques varies between the type of technique: Formal verification techniques exhibit the lowest level of maturity while the combination of techniques has demonstrated its successful application in real-world scenarios. …”
Get full text

Temporal Logic for Programmable Logic Controllers by Natalia Olegovna Garanina, Igor Sergeevich Anureev, Vladimir Evgenyevich Zyubin, Sergey Mikhailovich Staroletov, Tatiana Victorovna Liakh, Andrey Sergeevich Rozov, Sergei Petrovich Gorlatch

“…We address the formal verification of the control software of critical systems, i.e., ensuring the absence of design errors in a system with respect to requirements. …”
Get full text

Operational Semantics of Annotated Reflex Programs by Igor S. Anureev

“…Currently, the main goal of the Reflex language project is to develop formal verification methods for Reflex programs in order to guarantee increased reliability of the software created on its basis. …”
Get full text

Security Analysis of a Digital Twin Framework Using Probabilistic Model Checking by Eman Shaikh, A. R. Al-Ali, Shahabuddin Muhammad, Nazeeruddin Mohammad, F. Aloul

“…This paper presents a framework in which the security of a DT can be analyzed with the help of a formal verification technique. The framework captures the defense of the system at different layers and considers various attacks at each layer. …”
Get full text

BCmECC: A Lightweight Blockchain-Based Authentication and Key Agreement Protocol for Internet of Things by Jan Lansky, Amir Masoud Rahmani, Saqib Ali, Nasour Bagheri, Masoumeh Safkhani, Omed Hassan Ahmed, Mehdi Hosseinzadeh

“…We evaluate the security of the proposed protocol heuristically and validate it formally, which demonstratse the high level of the security. For the formal verification we used the widely accepted formal methods, i.e., BAN logic and the Scyther tool. …”
Get full text

Smooth Passage with the Guards: Second-Order Hardware Masking of the AES with Low Randomness and Low Latency by Barbara Gigerl, Franz Klug, Stefan Mangard, Florian Mendel, Robert Primas

“…We assess the security of our design in the probing model using a formal verification tool. Furthermore, we evaluate the practical side-channel resistance on an FPGA. …”
Get full text

Collision Tests in Human-Robot Collaboration: Experiments on the Influence of Additional Impact Parameters on Safety by Clara Fischer, Michael Neuhold, Martin Steiner, Thomas Haspl, Michael Rathmair, Sebastian Schlund

“…This analysis requires highly elaborate physical crash tests of potential impact scenarios. Formal verification will save considerable amounts of time and effort. …”
Get full text

A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits by Burlyaev, Dmitry, Fradet, Pascal, Girault, Alain

“…We address scalability issues arising from formal verification with approximations and assess their efficiency and precision.…”
Get full text

Kronos : verifying leak-free reset for a system-on-chip with multiple clock domains by Moroze, Noah(Noah F.)

Get full text

The analysis of cryptographic APIs using the theorem prover Otter by Youn, Paul, 1981-

Get full text

Secure and efficient authentication schemes for 5G heterogeneous networks by Ozhelvaci, Alican

“…All designed schemes are verified by security verification methods, we used the SPAN-AVISPA tool to simulate and analyze our proposed scheme and to provide a formal verification, and BAN Logic is used for logical correctness. …”
Get full text

Automated quantitative software verification by Kattenbelt, M

“…This can be done with a formal verification technique called <em>model checking</em>, which establishes <em>properties</em> of systems by algorithmically considering all execution scenarios. …”

Precise abstract interpretation of hardware designs by Mukherjee, R

“…We then present the application of native software analyzers based on SAT/SMT-based decision procedures as well as abstraction-based techniques such as abstract interpretation for the formal verification of the software netlist design generated from the hardware RTL. …”

An architectural approach for reasoning about trust properties by Namiluko, C

“…An <em>abstraction model</em> based on formal verification is developed to reason about the impact of the system's construction and configuration on its trustworthiness. …”

An efficient authentication and key agreement protocol for 4G (LTE) networks by Alezabi, Kamal Ali, Hashim, Fazirulhisyam, Hashim, Shaiful Jahari, Mohd Ali, Borhanuddin

“…The automated validation of internet security protocols and applications (AVISPA) tool is used to provide a formal verification. Results show that the proposed EEPS-AKA is efficient and secure against active and passive attacks.…”
Get full text

Synthesizing Signaling Pathways from Temporal Phosphoproteomic Data by Ali Sinan Köksal, Kirsten Beck, Dylan R. Cronin, Aaron McKenna, Nathan D. Camp, Saurabh Srivastava, Matthew E. MacGilvray, Rastislav Bodík, Alejandro Wolf-Yadlin, Ernest Fraenkel, Jasmin Fisher, Anthony Gitter

“…The Temporal Pathway Synthesizer (TPS) algorithm uses constraint-solving techniques first developed in the context of formal verification to explore paths in an interaction network. …”
Get full text