scholarly journals Property-Directed Inference of Relational Invariants

2019 ◽  
Vol 26 (4) ◽  
pp. 550-571
Author(s):  
Dmitry A. Mordvinov
Keyword(s):  
Experimental Evaluation ◽  
Horn Clauses ◽  
Non Linear ◽  
Symbolic Constraints ◽  
Novel Algorithm

Property Directed Reachability (PDR) is an efficient and scalable approach to solving systems of symbolic constraints also known as Constrained Horn Clauses (CHC). In the case of non-linear CHCs, which may arise, e.g., from relational verification tasks, PDR aims to infer an inductive invariant for each uninterpreted predicate. However, in many practical cases this reasoning is not successful, as invariants should be derived for groups of predicates instead of individual predicates. The article describes a novel algorithm that identifies these groups automatically and complements the existing PDR technique. The key feature of the algorithm is that it does not require a possibly expensive synchronization transformation over the system of CHCs. We have implemented the algorithm on top of a up-to-date CHC solver Spacer. Our experimental evaluation shows that for some CHC systems, on which existing solvers diverge, our tool is able to discover relational invariants.

scholarly journals Experimental Evaluation of Distortion in Amplitude Modulation Techniques for Parametric Loudspeakers

2020 ◽  
Vol 10 (6) ◽  
pp. 2070
Author(s):  
Ricardo San Martín ◽  
Pablo Tello ◽  
Ana Valencia ◽  
Asier Marzo
Keyword(s):  
Frequency Response ◽  
Amplitude Modulation ◽  
Experimental Evaluation ◽  
Harmonic Distortion ◽  
Intermodulation Distortion ◽  
Simple Method ◽  
Modulation Techniques ◽  
Audible Sound ◽  
Non Linear

Parametric loudspeakers can generate a highly directional beam of sound, having applications in targeted audio delivery. Audible sound modulated into an ultrasonic carrier will get self-demodulated along the highly directive beam due to the non-linearity of air. This non-linear demodularization should be compensated to reduce audio distortion, different amplitude modulation techniques have been developed during the last years. However, some studies are only theoretical whereas others do not analyze the audio distortion in depth. Here, we present a detailed experimental evaluation of the frequency response, harmonic distortion and intermodulation distortion for various amplitude modulation techniques applied with different indices of modulation. We used a simple method to measure the audible signal that prevents the saturation of the microphones when the high levels of the ultrasonic carrier are present. This work could be useful for selecting predistortion techniques and indices of modulation for regular parametric arrays.

Experimental evaluation of ultrasound higher-order harmonic imaging with Filtered-Delay Multiply And Sum (F-DMAS) non-linear beamforming

Ultrasonics ◽  
2018 ◽  
Vol 86 ◽  
pp. 59-68 ◽  
Author(s):  
Giulia Matrone ◽  
Alessandro Ramalli ◽  
Piero Tortoli ◽  
Giovanni Magenes
Keyword(s):  
Experimental Evaluation ◽  
Higher Order ◽  
Harmonic Imaging ◽  
Non Linear

scholarly journals Solving Horn Clauses on Inductive Data Types Without Induction

2018 ◽  
Vol 18 (3-4) ◽  
pp. 452-469 ◽  
Author(s):  
EMANUELE DE ANGELIS ◽  
FABIO FIORAVANTI ◽  
ALBERTO PETTOROSSI ◽  
MAURIZIO PROIETTI
Keyword(s):  
Data Structures ◽  
Experimental Evaluation ◽  
Satisfiability Problem ◽  
Data Types ◽  
Transformation Technique ◽  
Horn Clauses ◽  
Transformation Algorithm ◽  
Integer Constraints

AbstractWe address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction.

scholarly journals Tree dimension in verification of constrained Horn clauses

2018 ◽  
Vol 18 (2) ◽  
pp. 224-251 ◽  
Author(s):  
BISHOKSAN KAFLE ◽  
JOHN P. GALLAGHER ◽  
PIERRE GANTY
Keyword(s):  
Experimental Results ◽  
Horn Clause ◽  
Higher Dimension ◽  
Dimension Zero ◽  
Horn Clauses ◽  
Verification Problem ◽  
Non Linear

AbstractIn this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCsP, we define a transformation ofPyielding adimension-boundedset of CHCsP≤k. The set of derivations forP≤kconsists of the derivations forPthat have dimension at mostk. We also show how to construct a set of clauses denotedP>kwhose derivations have dimension exceedingk. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.

scholarly journals Synchronizing Constrained Horn Clauses

10.29007/gr5c ◽  
2018 ◽  
Author(s):  
Dmitry Mordvinov ◽  
Grigory Fedyukovich
Keyword(s):  
Iterative Algorithm ◽  
Recurrence Relations ◽  
Multiple Recurrence ◽  
Integer Arithmetic ◽  
Horn Clauses ◽  
Constraint Language ◽  
Non Linear

Simultaneous occurrences of multiple recurrence relations in a system of non-linear constrained Horn clauses are crucial for proving its satis ability. A solution of such system is often inexpressible in the constraint language. We propose to synchronize recurrent computations, thus increasing the chances for a solution to be found. We introduce a notion of CHC product allowing to formulate a lightweight iterative algorithm of merging recurrent computations into groups and prove its soundness. The evaluation over a set of systems handling lists and linear integer arithmetic confirms that the transformed systems are drastically more simple to solve than the original ones.

scholarly journals Solving non-linear Horn clauses using a linear Horn clause solver

2016 ◽  
Vol 219 ◽  
pp. 33-48 ◽  
Author(s):  
Bishoksan Kafle ◽  
John P. Gallagher ◽  
Pierre Ganty
Keyword(s):  
Horn Clause ◽  
Horn Clauses ◽  
Non Linear
Sign in / Sign up

Export Citation Format

Share Document