Automated Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography by M. . Anikeev, F. . Madlener, A. . Schlosser, S. A. Huss, C. . Walther

“…The correctness proof of the projective coordinate system transformation has practically been performed with the help of the an interactive formal verification system XeriFun.…”
Get full text

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic by Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani

“…The problem of computing Craig interpolants in SAT and SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for interpolant generation have been presented for some theories of interest ---including that of equality and uninterpreted functions, linear arithmetic over the rationals, and their combination--- and they are successfully used within model checking tools. …”
Get full text

Formalizing Calculus without Limit Theory in Coq by Yaoshun Fu, Wensheng Yu

“…Formal verification of mathematical theory has received widespread concern and grown rapidly. …”
Get full text

Jolie Static Type Checker: a Prototype by Daniel de Carvalho, Manuel Mazzara, Bogdan Mingela, Larisa Safina, Alexander Tchitchigin, Nikolay Troshkov

“…Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. …”
Get full text

A Situation-Aware Scheme for Efficient Device Authentication in Smart Grid-Enabled Home Area Networks by Anhao Xiang, Jun Zheng

“…The security of the design is verified by using both formal verification and informal security analysis. Our performance analysis demonstrates that the proposed scheme is efficient in terms of computational and communication costs.…”
Get full text

A Faithful Semantics for Generalised Symbolic Trajectory Evaluation by Koen Claessen, Jan-Willem Roorda

“…Generalised Symbolic Trajectory Evaluation (GSTE) is a high-capacity formal verification technique for hardware. GSTE uses abstraction, meaning that details of the circuit behaviour are removed from the circuit model. …”
Get full text

Power of Randomization in Automata on Infinite Strings by Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

“…We present results on the decidability and precise complexity of the emptiness, universality and language containment problems for such machines, thus answering questions central to the use of these models in formal verification. Next, we characterize the languages recognized by PBAs topologically, demonstrating that though general PBAs can recognize languages that are not regular, topologically the languages are as simple as \omega-regular languages. …”
Get full text

A security enhanced authentication and key distribution protocol for wireless networks by Lv, Chao, Ma, Maode, Li, Hui, Ma, Jianfeng, Niu, Ben

“…Security analysis and formal verification mainly using Automated Validation of Internet Security Protocols and Applications toolkit show that the proposed protocol is secure against those attacks.…”
Get full text
Get full text

A Refinement Approach to Design and Verification of On-Chip Communication Protocols by Boehm, P, Melham, T

“…To meet performance requirements these protocols have become highly complex, which usually makes their formal verification infeasible with reasonable time and effort. …”

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. by Brillout, A, Kroening, D, Rümmer, P, Wahl, T

“…Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. …”

Probabilistic model checking of complex biological pathways by Heath, J, Kwiatkowska, M, Norman, G, Parker, D, Tymchyshyn, O

“…Probabilistic model checking is a formal verification technique that has been successfully applied to the analysis of systems from a broad range of domains, including security and communication protocols, distributed algorithms and power management. …”

ANALYSING UML-BASED SOFTWARE MODELLING LANGUAGES by Mert Ozkaya

“…The model analysis is essentially enabled by those languages whose formal semantics are defined in terms of the translations into some formal verification languages that are supported with exhaustive model checkers. …”
Get full text

Relational $\star$-Liftings for Differential Privacy by Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub

“…Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. …”
Get full text

On the specification and verification of the PCR parallel programming pattern in TLA+ by José Solsona

“…In this way, we contribute to the state of the art in formal verification of parallel programs by leveraging TLA+-related tools to proving properties about high-level PCR-based algorithms such as their functional correctness and refinement. …”
Get full text

Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review by Angela Pappagallo, Annalisa Massini, Enrico Tronci

“…The ever-increasing deployment of autonomous Cyber-Physical Systems (CPSs) (e.g., autonomous cars, UAV) exacerbates the need for efficient formal verification methods. In this setting, the main obstacle to overcome is the huge number of scenarios to be evaluated. …”
Get full text

The Complexity of Reachability in Affine Vector Addition Systems with States by Michael Blondin, Mikhail Raskin

“…Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. …”
Get full text

Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents by Wiktor B. Daszczuk

“…Formal verification of distributed systems is essential, especially in mission-critical systems that cannot be restarted. …”
Get full text

Using SPIN for Verification of Multi-agent Data Analysis by N. O. Garanina, E. V. Bodin, E. A. Sidorova

“…The paper presents an approach to formal verification of multi-agent data analysis algorithms for ontology population. …”
Get full text

Robust Financial Fraud Alerting System Based in the Cloud Environment by Branka Stojanović, Josip Božić

“…Therefore, a systematic risk assessment was conducted in this context, and exploitation probabilities were inferred for multiple attack scenarios. In addition, formal verification was accomplished in order to determine the effects of successful vulnerability exploits. …”
Get full text

Security Analysis and Enhancement of INTERBUS Protocol in ICS Based on Colored Petri Net by Tao Feng, Chengfan Liu, Xiang Gong, Ye Lu

“…Our approach leverages the theory of colored Petri nets (CPN) for modeling, enabling a comprehensive analysis of the protocol’s security. Rigorous formal verification and analysis of the security protocol are conducted by employing the Dolev–Yao adversary model. …”
Get full text