Titlebook: Automated Technology for Verification and Analysis; 15th International S Deepak D‘Souza,K. Narayan Kumar Conference proceedings 2017 Spring

idiopathic

Fixing the State Budget: Approximation of Regular Languages with Small DFAse-automata. They are a well-understood formalism, and operations on them are decidable and well-known. But in practice these operations either blow up in size or in cost of operations. Hence the attractive automata representations become impractical. In this paper we propose reasoning about strings

Ornithologist

An Equivalence Checking Framework for Array-Intensive Programsn validation of array-intensive programs requires manipulation of intervals of integers (representing domains of array indices) and relations over such intervals to account for loop transformations and simplification of arithmetic expressions to handle arithmetic transformations. Translation validat

无底

Loop Quasi-Invariant Chunk Detectionto optimize generated code, or simply ease developers’ lives. In this paper, we introduce a new concept of dependency analysis borrowed from the field of Implicit Computational Complexity (ICC), allowing to work with composed statements called “Chunks” to detect more quasi-invariants. Based on an op

GUILE

柔软

ZEST

删除

SCORE

Compositional Safety Refutation Techniques, bounded model checking instances often exceed the limits of resources available. Generating such counterexamples in a modular way could speed up refutation, but it is challenging because of the inherently non-compositional nature of these counterexamples. We start from the monolithic safety verifi

Definitive

Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural Unitss. Gradient-. combines the structural informations of the Petri net (either the set of minimal P-semiflows or, when available, the structure of the net in terms of “Nested Units”) with a gradient-based greedy strategy inspired by methods for matrix bandwidth reduction. The value of the proposed heur

保存