Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userProperty Directed Self Composition
47
0
0.0
(
0
)
Added by
Ron Shemer
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self composition. In this approach, the problem of checking k-safety over the original program is reduced to checking an ordinary safety property over a program that executes k copies of the original program in some order. The way in which the copies are composed determines how complicated it is to verify the composed program. We view this composition as provided by a semantic self composition function that maps each state of the composed program to the copies that make a move. Since the quality of a self composition function is measured by the ability to verify the safety of the composed program, we formulate the problem of inferring a self composition function together with the inductive invariant needed to verify safety of the composed program, where both are restricted to a given language. We develop a property-directed inference algorithm that, given a set of predicates, infers composition-invariant pairs expressed by Boolean combinations of the given predicates, or determines that no such pair exists. We implemented our algorithm and demonstrate that it is able to find self compositions that are beyond reach of existing tools.
rate research
Read More
IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our main focus is to develop the theory underlying PrIC3. Alongside, we present a first implementation of PrIC3 including the key ingredients from IC3 such as generalization, repushing, and propagation.
ABX3 perovskites have attracted intensive research interest in recent years due to their versatile composition and superior optoelectronic properties. Their counterparts, antiperovskites (X3BA), can be viewed as electronically inverted perovskite derivatives, but they have not been extensively studied for solar applications. Therefore, understanding their composition-property relationships is crucial for future photovoltaic application. Here, taking six antiperovskite nitrides X3NA (X2+ = Mg, Ca, Sr; A3- = P, As, Sb, Bi) as an example, we investigate the effect of X- and A-sites on the electronic, dielectric, and mechanical properties from the viewpoint of the first-principles calculations. Our calculation results show that the X-site dominates the conduction band, and the A-site has a non-negligible contribution to the band edge. These findings are completely different from traditional halide perovskites. Interestingly, when changing X- or A-site elements, a linear relationship between the tolerance factor and physical quantities, such as electronic parameters, dielectric constants, and Youngs modulus, is observed. By designing the Mg3NAs1-xBix alloys, we further verify this power of the linear relationship, which provides a predictive guidance for experimental preparation of antiperovskite alloys. Finally, we make a comprehensive comparison between the antiperovskite nitrides and conventional halide perovskites for pointing out the future device applications.
The use of annotations, referred to as assertions or contracts, to describe program properties for which run-time tests are to be generated, has become frequent in dynamic programing languages. However, the frameworks proposed to support such run-time testing generally incur high time and/or space overheads over standard program execution. We present an approach for reducing this overhead that is based on the use of memoization to cache intermediate results of check evaluation, avoiding repeated checking of previously verified properties. Compared to approaches that reduce checking frequency, our proposal has the advantage of being exhaustive (i.e., all tests are checked at all points) while still being much more efficient than standard run-time checking. Compared to the limited previous work on memoization, it performs the task without requiring modifications to data structure representation or checking code. While the approach is general and system-independent, we present it for concreteness in the context of the Ciao run-time checking framework, which allows us to provide an operational semantics with checks and caching. We also report on a prototype implementation and provide some experimental results that support that using a relatively small cache leads to significant decreases in run-time checking overhead.
Directed assembly of block polymers is rapidly becoming a viable strategy for lithographic patterning of nanoscopic features. One of the key attributes of directed assembly is that an underlying chemical or topographic substrate pattern used to direct assembly need not exhibit a direct correspondence with the sought after block polymer morphology, and past work has largely relied on trial-and-error approaches to design appropriate patterns. In this work, a computational evolutionary strategy is proposed to solve this optimization problem. By combining the Cahn-Hilliard equation, which is used to find the equilibrium morphology, and the covariance-matrix evolutionary strategy, which is used to optimize the combined outcome of particular substrate-copolymer combinations, we arrive at an efficient method for design of substrates leading to non-trivial, desirable outcomes.
Common programming tools, like compilers, debuggers, and IDEs, crucially rely on the ability to analyse program code to reason about its behaviour and properties. There has been a great deal of work on verifying compilers and static analyses, but far less on verifying dynamic analyses such as program slicing. Recently, a new mathematical framework for slicing was introduced in which forward and backward slicing are dual in the sense that they constitute a Galois connection. This paper formalises forward and backward dynamic slicing algorithms for a simple imperative programming language, and formally verifies their duality using the Coq proof assistant.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
