-
Incremental Bounded Model Checking of Artificial Neural Networks in CUDA
Authors:
Luiz H. Sena,
Iury V. Bessa,
Mikhail R. Gadelha,
Lucas C. Cordeiro,
Edjard Mota
Abstract:
Artificial Neural networks (ANNs) are powerful computing systems employed for various applications due to their versatility to generalize and to respond to unexpected inputs/patterns. However, implementations of ANNs for safety-critical systems might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are hardly interpretable. Here w…
▽ More
Artificial Neural networks (ANNs) are powerful computing systems employed for various applications due to their versatility to generalize and to respond to unexpected inputs/patterns. However, implementations of ANNs for safety-critical systems might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are hardly interpretable. Here we develop and evaluate a novel symbolic software verification framework based on incremental bounded model checking (BMC) to check for adversarial cases and coverage methods in multi-layer perceptron (MLP). In particular, we further develop the efficient SMT-based Context-Bounded Model Checker for Graphical Processing Units (ESBMC-GPU) in order to ensure the reliability of certain safety properties in which safety-critical systems can fail and make incorrect decisions, thereby leading to unwanted material damage or even put lives in danger. This paper marks the first symbolic verification framework to reason over ANNs implemented in CUDA. Our experimental results show that our approach implemented in ESBMC-GPU can successfully verify safety properties and covering methods in ANNs and correctly generate 28 adversarial cases in MLPs.
△ Less
Submitted 30 July, 2019;
originally announced July 2019.
-
Counterexample Guided Inductive Optimization Applied to Mobile Robots Path Planning (Extended Version)
Authors:
Rodrigo F. Araújo,
Alexandre Ribeiro,
Iury V. Bessa,
Lucas C. Cordeiro,
João E. C. Filho
Abstract:
We describe and evaluate a novel optimization-based off-line path planning algorithm for mobile robots based on the Counterexample-Guided Inductive Optimization (CEGIO) technique. CEGIO iteratively employs counterexamples generated from Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers, in order to guide the optimization process and to ensure global optimization. This p…
▽ More
We describe and evaluate a novel optimization-based off-line path planning algorithm for mobile robots based on the Counterexample-Guided Inductive Optimization (CEGIO) technique. CEGIO iteratively employs counterexamples generated from Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers, in order to guide the optimization process and to ensure global optimization. This paper marks the first application of CEGIO for planning mobile robot path. In particular, CEGIO has been successfully applied to obtain optimal two-dimensional paths for autonomous mobile robots using off-the-shelf SAT and SMT solvers.
△ Less
Submitted 14 August, 2017;
originally announced August 2017.
-
Verification of Magnitude and Phase Responses in Fixed-Point Digital Filters
Authors:
Daniel P. M. de Mello,
Mauro L. de Freitas,
Lucas C. Cordeiro,
Waldir S. S. Junior,
Iury V. de Bessa,
Eddie B. L. Filho,
Laurent Clavier
Abstract:
In the digital signal processing (DSP) area, one of the most important tasks is digital filter design. Currently, this procedure is performed with the aid of computational tools, which generally assume filter coefficients represented with floating-point arithmetic. Nonetheless, during the implementation phase, which is often done in digital signal processors or field programmable gate arrays, the…
▽ More
In the digital signal processing (DSP) area, one of the most important tasks is digital filter design. Currently, this procedure is performed with the aid of computational tools, which generally assume filter coefficients represented with floating-point arithmetic. Nonetheless, during the implementation phase, which is often done in digital signal processors or field programmable gate arrays, the representation of the obtained coefficients can be carried out through integer or fixed-point arithmetic, which often results in unexpected behavior or even unstable filters. The present work addresses this issue and proposes a verification methodology based on the digital-system verifier (DSVerifier), with the goal of checking fixed-point digital filters w.r.t. implementation aspects. In particular, DSVerifier checks whether the number of bits used in coefficient representation will result in a filter with the same features specified during the design phase. Experimental results show that errors regarding frequency response and overflow are likely to be identified with the proposed methodology, which thus improves overall system's reliability.
△ Less
Submitted 16 June, 2017;
originally announced June 2017.
-
Counterexample Guided Inductive Optimization
Authors:
Rodrigo F. Araujo,
Higo F. Albuquerque,
Iury V. de Bessa,
Lucas C. Cordeiro,
Joao Edgar C. Filho
Abstract:
This paper describes three variants of a counterexample guided inductive optimization (CEGIO) approach based on Satisfiability Modulo Theories (SMT) solvers. In particular, CEGIO relies on iterative executions to constrain a verification procedure, in order to perform inductive generalization, based on counterexamples extracted from SMT solvers. CEGIO is able to successfully optimize a wide range…
▽ More
This paper describes three variants of a counterexample guided inductive optimization (CEGIO) approach based on Satisfiability Modulo Theories (SMT) solvers. In particular, CEGIO relies on iterative executions to constrain a verification procedure, in order to perform inductive generalization, based on counterexamples extracted from SMT solvers. CEGIO is able to successfully optimize a wide range of functions, including non-linear and non-convex optimization problems based on SMT solvers, in which data provided by counterexamples are employed to guide the verification engine, thus reducing the optimization domain. The present algorithms are evaluated using a large set of benchmarks typically employed for evaluating optimization techniques. Experimental results show the efficiency and effectiveness of the proposed algorithms, which find the optimal solution in all evaluated benchmarks, while traditional techniques are usually trapped by local minima.
△ Less
Submitted 11 April, 2017;
originally announced April 2017.
-
Application of Global Route-Planning Algorithms with Geodesy
Authors:
William C. da Rosa,
Iury V. de Bessa,
Lucas C. Cordeiro
Abstract:
Global Route-Planning Algorithms (GRPA) are required to compute paths between several points located on Earth's surface. A geodesic algorithm is employed as an auxiliary tool, increasing the precision of distance calculations. This work presents a novel simulator for GRPA, which compares and evaluates three GRPAs implemented to solve the shortest path problem for points located at different cities…
▽ More
Global Route-Planning Algorithms (GRPA) are required to compute paths between several points located on Earth's surface. A geodesic algorithm is employed as an auxiliary tool, increasing the precision of distance calculations. This work presents a novel simulator for GRPA, which compares and evaluates three GRPAs implemented to solve the shortest path problem for points located at different cities: A*, LPA*, and D*Lite. The performance of each algorithm is investigated with a set of experiments, which are executed to check the answers provided by the algorithms and to compare their execution time. It is shown that GRPAs implementations with consistent heuristics lead to optimal paths. The noticeable differences among those algorithms are related to the time execution after successive executions.
△ Less
Submitted 14 October, 2016;
originally announced October 2016.
