scholarly journals Formal Verification of a State-of-the-Art Integer Square Root

2019 ◽  
Author(s):  
Guillaume Melquiond ◽  
Raphael Rieu-Helft
Keyword(s):  
Formal Verification ◽  
State Of The Art ◽  
Square Root

scholarly journals Fusion of Elliptical Extended Object Estimates Parameterized with Orientation and Axes Lengths

2020 ◽  
Author(s):  
Kolja Thormann ◽  
Marcus Baum
Keyword(s):  
Monte Carlo ◽  
Monte Carlo Methods ◽  
Euclidean Distance ◽  
State Of The Art ◽  
Optimal Estimation ◽  
Square Root ◽  
Multiple Sensors ◽  
Practical Algorithms ◽  
Extended Object ◽  
Wasserstein Distances

This article considers the fusion of target estimates stemming from multiple sensors, where the spatial extent of the targets is incorporated. The target estimates are represented as ellipses parameterized with center orientation and semi-axis lengths and width. Here, the fusion faces challenges such as ambiguous parameterization and an unclear meaning of the Euclidean distance between such estimates. We introduce a novel Bayesian framework for random ellipses based on the concept of a Minimum Mean Gaussian Wasserstein (MMGW) estimator. The MMGW estimate is optimal with respect to the Gaussian Wasserstein (GW) distance, which is a suitable distance metric for ellipses. We develop practical algorithms to approximate the MMGW estimate of the fusion result. The key idea is to approximate the GW distance with a modified version of the Square Root (SR) distance. By this means, optimal estimation and fusion can be performed based on the square root of the elliptic shape matrices. We analyze different implementations using, e.g., Monte Carlo methods, and evaluate them in simulated scenarios. An extensive comparison with state-of-the-art methods highlights the benefits of estimators tailored to the Gaussian Wasserstein distances.

scholarly journals Fusion of Elliptical Extended Object Estimates Parameterized with Orientation and Axes Lengths

2020 ◽  
Author(s):  
Kolja Thormann ◽  
Marcus Baum
Keyword(s):  
Monte Carlo ◽  
Monte Carlo Methods ◽  
Euclidean Distance ◽  
State Of The Art ◽  
Optimal Estimation ◽  
Square Root ◽  
Multiple Sensors ◽  
Practical Algorithms ◽  
Extended Object ◽  
Wasserstein Distances

This article considers the fusion of target estimates stemming from multiple sensors, where the spatial extent of the targets is incorporated. The target estimates are represented as ellipses parameterized with center orientation and semi-axis lengths and width. Here, the fusion faces challenges such as ambiguous parameterization and an unclear meaning of the Euclidean distance between such estimates. We introduce a novel Bayesian framework for random ellipses based on the concept of a Minimum Mean Gaussian Wasserstein (MMGW) estimator. The MMGW estimate is optimal with respect to the Gaussian Wasserstein (GW) distance, which is a suitable distance metric for ellipses. We develop practical algorithms to approximate the MMGW estimate of the fusion result. The key idea is to approximate the GW distance with a modified version of the Square Root (SR) distance. By this means, optimal estimation and fusion can be performed based on the square root of the elliptic shape matrices. We analyze different implementations using, e.g., Monte Carlo methods, and evaluate them in simulated scenarios. An extensive comparison with state-of-the-art methods highlights the benefits of estimators tailored to the Gaussian Wasserstein distances.

scholarly journals Model-Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification

Electronics ◽  
2019 ◽  
Vol 8 (9) ◽  
pp. 1057
Author(s):  
Gianpiero Cabodi ◽  
Paolo Camurati ◽  
Fabrizio Finocchiaro ◽  
Danilo Vendraminetto
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
High Performance ◽  
State Of The Art ◽  
Realistic Model ◽  
Bounded Model Checking ◽  
Sensitive Information ◽  
Model Checker ◽  
Verification Process ◽  
Verification Techniques

Spectre and Meltdown attacks in modern microprocessors represent a new class of attacks that have been difficult to deal with. They underline vulnerabilities in hardware design that have been going unnoticed for years. This shows the weakness of the state-of-the-art verification process and design practices. These attacks are OS-independent, and they do not exploit any software vulnerabilities. Moreover, they violate all security assumptions ensured by standard security procedures, (e.g., address space isolation), and, as a result, every security mechanism built upon these guarantees. These vulnerabilities allow the attacker to retrieve leaked data without accessing the secret directly. Indeed, they make use of covert channels, which are mechanisms of hidden communication that convey sensitive information without any visible information flow between the malicious party and the victim. The root cause of this type of side-channel attacks lies within the speculative and out-of-order execution of modern high-performance microarchitectures. Since modern processors are hard to verify with standard formal verification techniques, we present a methodology that shows how to transform a realistic model of a speculative and out-of-order processor into an abstract one. Following related formal verification approaches, we simplify the model under consideration by abstraction and refinement steps. We also present an approach to formally verify the abstract model using a standard model checker. The theoretical flow, reliant on established formal verification results, is introduced and a sketch of proof is provided for soundness and correctness. Finally, we demonstrate the feasibility of our approach, by applying it on a pipelined DLX RISC-inspired processor architecture. We show preliminary experimental results to support our claim, performing Bounded Model-Checking with a state-of-the-art model checker.

Formal verification of division and square root implementations, an Oracle report

2016 ◽  
Author(s):  
David L. Rager ◽  
Jo Ebergen ◽  
Dmitry Nadezhin ◽  
Austin Lee ◽  
Cuong Kim Chau ◽  
...  
Keyword(s):  
Formal Verification ◽  
Square Root

scholarly journals State of the Art in the Research of Formal Verification

2014 ◽  
Vol 15 (4) ◽  
pp. 615-623 ◽  
Author(s):  
Serna-M. Edgar ◽  
Morales-V. David
Keyword(s):  
Formal Verification ◽  
State Of The Art
Sign in / Sign up

Export Citation Format

Share Document