1,721,018 research outputs found
Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving
No full textRewriting-based quantifier free interpolation for a theory of arrays
No full textThe use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general.
In this paper, we show that, with a minor extension to the theory of arrays, it is possible to obtain quantifier-free interpolants. We prove this by designing an interpolating procedure, based on solving equations between array updates. Rewriting techniques are used in the key steps of the solver and its proof of correctness. To the best of our knowledge, this is the first successful attempt of computing quantifier-free interpolants for a theory of arrays
Model Checking: Teoria ed Applicazioni
No full textIl model checking è una tecnica algoritmica per la verifica di proprietà temporali di sistemi dinamici, introdotto nella prima parte degli anni ’80. Le tecniche iniziali di model checking a stati finiti, basate sull’esplorazione esplicita dello spazio degli stati, sono state progressivamente sostituite, nel corso degli anni, da tecniche simboliche, ovvero basate su Diagrammi di Decisione Binaria (BDD), e sistemi per la soddisfacibilità proposizionale (SAT solvers). Ulteriori sviluppi nel model checking, orientati all’analisi di sistemi a stati infiniti, derivano dalla applicazione di tecniche per la soddisfacibilità modulo teorie (SMT). Si tratta di procedure di decisione per frammenti della logica del primo ordine, che possono essere viste come una integrazione di SAT con tecniche per la risoluzione di vincoli. Il model checking è applicato in molti ambiti a supporto della progettazione, debugging e certificazione di sistemi a stati finiti e infiniti. Obiettivo di questo lavoro è fornire una introduzione alla teoria del model checking, ed una panoramica delle sue applicazioni in vari ambiti della sicurezza
An extension of lazy abstraction with interpolation for programs with arrays
No full textLazy abstraction with interpolation-based refinement has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method suffers from an intrinsic limitation, due to the fact that invariants needed for verification usually contain universally quantified variables, which are not present in program specifications. In this work we present an extension of the interpolation-based lazy abstraction framework in which arrays of unknown length can be handled in a natural manner. In particular, we exploit the Model Checking Modulo Theories framework to derive a backward reachability version of lazy abstraction that supports reasoning about arrays. The new approach has been implemented in a tool, called safari, which has been validated on a wide range of benchmarks. We show by means of experiments that our approach can synthesize and prove universally quantified properties over arrays in a completely automatic fashion
- …
