scholarly journals SMT-Based System Verification with DVF

10.29007/59rn ◽  
2018 ◽  
Author(s):  
Amit Goel ◽  
Sava Krstic ◽  
Rebekah Leslie ◽  
Mark Tuttle
Keyword(s):  
Thin Layer ◽  
Type System ◽  
Transition Systems ◽  
First Order ◽  
Verification Conditions ◽  
Logic Verification ◽  
System Verification ◽  
Selected Subset ◽  
Parametric Specification

We introduce the <i>Deductive Verificaton Framework</i> (DVF), a language and a tool for verifying properties of transition systems. The language is procedural and the system transitions are a selected subset of procedures. The type system and built-in operations are consistent with SMT-LIB, as are the multisorted first-order logical formulas that may occur in DVF programs as pre- and post-conditions, assumptions, assertions, and goals. A template mechanism allows parametric specification of complex types within the confines of this logic. Verification conditions are generated from specified goals and passed to SMT engine(s). A general assume-guarantee scheme supports a thin layer of interactive proving.

Some logical and syntactical observations concerning the first-order dependent type system λP

1999 ◽  
Vol 9 (4) ◽  
pp. 335-359 ◽  
Author(s):  
HERMAN GEUVERS ◽  
ERIK BARENDSEN
Keyword(s):  
Predicate Logic ◽  
Type System ◽  
Logical Framework ◽  
First Order ◽  
Logical Derivation ◽  
Dependent Type ◽  
First Order Predicate Logic

We look at two different ways of interpreting logic in the dependent type system λP. The first is by a direct formulas-as-types interpretation à la Howard where the logical derivation rules are mapped to derivation rules in the type system. The second is by viewing λP as a Logical Framework, following Harper et al. (1987) and Harper et al. (1993). The type system is then used as the meta-language in which various logics can be coded.We give a (brief) overview of known (syntactical) results about λP. Then we discuss two issues in some more detail. The first is the completeness of the formulas-as-types embedding of minimal first-order predicate logic into λP. This is a remarkably complicated issue, a first proof of which appeared in Geuvers (1993), following ideas in Barendsen and Geuvers (1989) and Swaen (1989). The second issue is the minimality of λP as a logical framework. We will show that some of the rules are actually superfluous (even though they contribute nicely to the generality of the presentation of λP).At the same time we will attempt to provide a gentle introduction to λP and its various aspects and we will try to use little inside knowledge.

scholarly journals Deep Network Guided Proof Search

10.29007/8mwc ◽  
2018 ◽  
Author(s):  
Sarah Loos ◽  
Geoffrey Irving ◽  
Christian Szegedy ◽  
Cezary Kaliszyk
Keyword(s):  
Deep Learning ◽  
Program Analysis ◽  
Network Models ◽  
Theorem Prover ◽  
Neural Network Models ◽  
Two Phase ◽  
First Order ◽  
Proof Search ◽  
System Verification ◽  
Theory Reasoning

Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playing the game of Go.Automated first-order theorem provers can aid in the formalization and verification of mathematical theorems and play a crucial role in program analysis, theory reasoning, security, interpolation, and system verification.Here we suggest deep learning based guidance in the proof search of the theorem prover E. We train and compare several deep neural network models on the traces of existing ATP proofs of Mizar statements and use them to select processed clauses during proof search. We give experimental evidence that with a hybrid, two-phase approach, deep learning based guidance can significantly reduce the average number of proof search steps while increasing the number of theorems proved.Using a few proof guidance strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.

The effect of normal blowing on the flow near a rotating disk of infinite extent

1971 ◽  
Vol 47 (4) ◽  
pp. 789-798 ◽  
Author(s):  
H. K. Kuiken
Keyword(s):  
Asymptotic Analysis ◽  
Thin Layer ◽  
Rotating Disk ◽  
Complete Agreement ◽  
Viscous Effects ◽  
First Order ◽  
Numerical Integrations ◽  
Infinite Extent

The effect of blowing through a porous rotating disk on the flow induced by this disk is studied. For strong blowing the flow is almost wholly inviscid. First-order viscous effects are encountered only in a thin layer at some distance from the disk. The results of an asymptotic analysis are compared with numerical integrations of the full equations and complete agreement is found.

scholarly journals Generalized impedance boundary conditions and shape derivatives for 3D Helmholtz problems

2016 ◽  
Vol 26 (10) ◽  
pp. 1995-2033 ◽  
Author(s):  
Djalil Kateb ◽  
Frédérique Le Louër
Keyword(s):  
Thin Layer ◽  
Three Dimensional ◽  
Transmission Problem ◽  
Impedance Boundary Condition ◽  
Constant Thickness ◽  
Laplacian Operator ◽  
Shape Sensitivity ◽  
Impedance Boundary ◽  
First Order ◽  
Exterior Boundary

This paper is concerned with the shape sensitivity analysis of the solution to the Helmholtz transmission problem for three-dimensional sound-soft or sound-hard obstacles coated by a thin layer. This problem can be asymptotically approached by exterior problems with an improved condition on the exterior boundary of the coated obstacle, called generalized impedance boundary condition (GIBC). Using a series expansion of the Laplacian operator in the neighborhood of the exterior boundary, we retrieve the first-order GIBCs characterizing the presence of an interior thin layer with a constant thickness. The first shape derivative of the solution to the original Helmholtz transmission problem solves a new thin layer transmission problem with non-vanishing jumps across the exterior and the interior boundary of the thin layer. We show that we can interchange the first-order differentiation with respect to the shape of the exterior boundary and the asymptotic approximation of the solution. Numerical experiments are presented to highlight the various theoretical results.

scholarly journals Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs

10.29007/pmmz ◽  
2018 ◽  
Author(s):  
Sylvia Grewe ◽  
André Pacak ◽  
Mira Mezini
Keyword(s):  
Type System ◽  
Type Systems ◽  
First Order ◽  
Domain Specific ◽  
The Past ◽  
Finite Term ◽  
The Individual ◽  
Input Format ◽  
Ongoing Project ◽  
Superposition Calculus

In our ongoing project VeriTaS, we aim at automating soundness proofs for type sys- tems of domain-specific languages. In the past, we successfully used previous Vampire versions for automatically discharging many intermediate proof obligations arising within standard soundness proofs for small type systems. With older Vampire versions, encoding the individual proof problems required manual encoding of algebraic datatypes via the theory of finite term algebras. One of the new Vampire versions now supports the direct specification of algebraic datatypes and integrates reasoning about term algebras into the internally used superposition calculus.In this work, we investigate how many proof problems that typically arise within type soundness proofs different Vampire 4.1 versions can prove. Our test set consists of proof problems from a progress proof of a type system for a subset of SQL. We compare running Vampire 4.1 with our own encodings of algebraic datatypes (in untyped as well as in typed first-order logic) to running Vampire 4.1 with support for algebraic datatypes, which uses SMTLIB as input format. We observe that with our own encodings, Vampire 4.1 still proves more of our input problems. We discuss the differences between our own encoding of algebraic datatypes and the ones used within Vampire 4.1 with support for algebraic datatypes.

scholarly journals Classification of bi-Hamiltonian pairs extended by isometries

2021 ◽  
Vol 477 (2251) ◽  
pp. 20210185
Author(s):  
Maxim V. Pavlov ◽  
Pierandrea Vergallo ◽  
Raffaele Vitolo
Keyword(s):  
Type System ◽  
Local Part ◽  
First Order ◽  
Hydrodynamic Type System ◽  
Dependent Variables ◽  
Particular Solution ◽  
Non Local ◽  
Hamiltonian Operators ◽  
Hamiltonian Pair

The aim of this article is to classify pairs of the first-order Hamiltonian operators of Dubrovin–Novikov type such that one of them has a non-local part defined by an isometry of its leading coefficient. An example of such a bi-Hamiltonian pair was recently found for the constant astigmatism equation. We obtain a classification in the case of two dependent variables, and a significant new example with three dependent variables that is an extension of a hydrodynamic-type system obtained from a particular solution of the Witten–Dijkgraaf–Verlinde–Verlinde equations.

scholarly journals Modular specification and verification of closures in Rust

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Fabian Wolff ◽  
Aurel Bílý ◽  
Christoph Matheja ◽  
Peter Müller ◽  
Alexander J. Summers
Keyword(s):  
Formal Verification ◽  
Functional Properties ◽  
Type System ◽  
Order Logic ◽  
First Order Logic ◽  
Formal Reasoning ◽  
First Order ◽  
Novel Technique ◽  
Smt Solvers ◽  
Specification And Verification

Closures are a language feature supported by many mainstream languages, combining the ability to package up references to code blocks with the possibility of capturing state from the environment of the closure's declaration. Closures are powerful, but complicate understanding and formal reasoning, especially when closure invocations may mutate objects reachable from the captured state or from closure arguments. This paper presents a novel technique for the modular specification and verification of closure-manipulating code in Rust. Our technique combines Rust's type system guarantees and novel specification features to enable formal verification of rich functional properties. It encodes higher-order concerns into a first-order logic, which enables automation via SMT solvers. Our technique is implemented as an extension of the deductive verifier Prusti, with which we have successfully verified many common idioms of closure usage.

scholarly journals On the Versatility of Open Logical Relations

2020 ◽  
pp. 56-83 ◽  
Author(s):  
Gilles Barthe ◽  
Raphaëlle Crubillé ◽  
Ugo Dal Lago ◽  
Francesco Gavazzo
Keyword(s):  
Programming Languages ◽  
Automatic Differentiation ◽  
Type System ◽  
Order Type ◽  
Higher Order ◽  
Base Case ◽  
Logical Relation ◽  
First Order ◽  
Differentiable Functions ◽  
The One

AbstractLogical relations are one among the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we study a generalization of the concept of a logical relation, called open logical relation, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed $$\lambda $$ λ -calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any collection of real-valued first-order functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations.

Distinguishing Lorenz and Chen Systems Based Upon Hamiltonian Energy Theory

2017 ◽  
Vol 27 (02) ◽  
pp. 1750024 ◽  
Author(s):  
Shijian Cang ◽  
Aiguo Wu ◽  
Zenghui Wang ◽  
Zengqiang Chen
Keyword(s):  
Energy Function ◽  
Lorenz System ◽  
Three Dimensional ◽  
Type System ◽  
Chen System ◽  
First Order ◽  
Dimensional Phase Space ◽  
Ellipsoidal Surface ◽  
Generalized Hamiltonian Realization ◽  
The Lorenz System

Solving the linear first-order Partial Differential Equations (PDEs) derived from the unified Lorenz system, it is found that there is a unified Hamiltonian (energy function) for the Lorenz and Chen systems, and the unified energy function shows a hyperboloid of one sheet for the Lorenz system and an ellipsoidal surface for the Chen system in three-dimensional phase space, which can be used to explain that the Lorenz system is not equivalent to the Chen system. Using the unified energy function, we obtain two generalized Hamiltonian realizations of these two chaotic systems, respectively. Moreover, the energy function and generalized Hamiltonian realization of the Lü system and a four-dimensional hyperchaotic Lorenz-type system are also discussed.

Phantom types and subtyping

2006 ◽  
Vol 16 (6) ◽  
pp. 751-791 ◽  
Author(s):  
MATTHEW FLUET ◽  
RICCARDO PUCELLA
Keyword(s):  
Type System ◽  
Type Systems ◽  
First Order ◽  
Standard Ml ◽  
Parametric Polymorphism ◽  
The One ◽  
Multiple Interface

We investigate a technique from the literature, called the phantom-types technique, that uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. Hindley-Milner type systems, such as the one found in Standard ML, can be used to enforce the subtyping relation, at least for first-order values. We show that this technique can be used to encode any finite subtyping hierarchy (including hierarchies arising from multiple interface inheritance). We formally demonstrate the suitability of the phantom-types technique for capturing first-order subtyping by exhibiting a type-preserving translation from a simple calculus with bounded polymorphism to a calculus embodying the type system of SML.

Sign in / Sign up

Export Citation Format

Share Document