87,172 research outputs found
Come studiare l'italiano parlato? Parlato spontaneo e corpora di parlato
No full text1. Priorità della lingua parlata nella storia della linguistica e prospettiva grafocentrica della ricerca linguistica
2. Cosa è il 'parlato'?
2a. Il parlato come modalità fisica di trasmissione (dalle macchine parlanti del 600 e 700 alla linguistica applicata all’insegnamento delle lingue straniere e alla riabilitazione degli handicaps sensoriali)
2b. Il parlato come modalità semiotica di emissione (la produzione dei 'semicolti': la Confessione di Bellezze)
2c. Il parlato come modalità d'uso di una lingua, insieme di usi linguistici (corpora di parlato)
3. I corpora di parlato
I corpora di parlato, acquisiti in varie condizioni, sono di fondamentale importanza per la descrizione e la conoscenza del funzionamento della lingua parlata in tutte le sue tipologie di impiego così come per la predisposizione di strumenti applicativi utili alla realizzazione di sistemi di riconoscimento del parlato e di produzione di voce sintetica
3.a. I corpora di parlato italiano (AVIP-API - CLIPS)
4. La variabilità fonica del parlato e il ruolo del contesto
5. Le difficoltà nello studio del parlato: l'ipoarticolazione. Importanza della prosodia.
6. Nella comunicazione parlata i complessi processi della significazione non si svolgono tutti ed esclusivamente nel testo (inteso in senso tradizionale come successione lineare di unità linguistiche) ma sono spesso esterni al testo, affidati a componenti extralinguistici o paralinguistici (come la prosodia e qualità della voce, la mimica facciale e la gestualità, le modalità dell’interazione dialogica, i rinvii e le allusioni al mondo circostante, il gioco delle inferenze, delle presupposizioni e delle intenzioni). Tutti questi aspetti, che nella comunicazione parlata agiscono in modi variabili e poco prevedibili, sono invece assenti nella comunicazione scritta oppure, se presenti, sono prevedibili (in quanto canonizzati dalla tradizione). Le aree di ricerca intorno alla lingua parlata sono pertanto molteplici:
5.a. parlato e fonetica segmentale
5.b. parlato e prosodia
5.c. parlato, morfologia e sintassi
5.d. parlato e lessico
5.e. parlato e varietà regionali
5.f. parlato e testualità
5.g. parlato e dinamiche comunicative
5.h. parlato e didattica dell'italiano
5.i. parlato e sordità e patologie in genere
5.l. parlato, emozioni, sentimenti e atteggiamenti
5.m. strumenti per lo studio, la codifica e la rappresentazione del parlat
Verifying concurrent programs by memory unwinding
No full textWe describe a new sequentialization-based approach to the symbolic verification of multi-threaded programs with shared memory and dynamic thread creation. Its main novelty is the idea of memory unwinding, i.e., an explicit representation of the sequence of write operations into the shared memory. For the verification, we nondeterministically guess this unwinding and then simulate the behavior of the program according to any scheduling that respects this guess. This approach is complementary to other sequentializations and explores an orthogonal dimension, i.e., the number of write operations. It also simplifies the implementation of several important optimizations, in particular the targeted exposure of individual writes. We implemented this approach as code-to-code transformation from multi-threaded into nondeterministic sequential programs, which allows the reuse of sequential verification tools. Experiments show that our approach is very promising: it found all errors in the concurrency category of SV-COMP15
Osservatorio dell'Italiano Contemporaneo: esempi di continuum linguistico tra scritto e parlato
No full textPresentazione di alcuni risultati del gruppo di ricerca "Osservatorio linguistico dell'italiano contemporaneo", con particolare riguardo al problema della norma e della risalita nell'italiano scritto di fenomeni tipici del parlato
Bounded model checking of multi-threaded c programs via lazy sequentialization
No full textBounded model checking (BMC) has successfully been used for many practical program verification problems, but concurrency still poses a challenge. Here we describe a new approach to BMC of sequentially consistent C programs using POSIX threads. Our approach first translates a multi-threaded C program into a nondeterministic sequential C program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. It then re-uses existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so that it produces tight SAT/SMT formulae, and is thus very effective in practice: our prototype won the concurrency category of SV-COMP14. It solved all verification tasks successfully and was 30x faster than the best tool with native concurrency handling.<br/
The tree width of auxiliary storage
No full textWe propose a generalization of results on the decidability of emptiness for several restricted classes of sequential and distributed automata with auxiliary storage (stacks, queues) that have recently been proved. Our generalization relies on reducing emptiness of these automata to finite-state graph automata (without storage) restricted to monadic second-order (MSO) definable graphs of bounded tree-width, where the graph structure encodes the mechanism provided by the auxiliary storage. Our results outline a uniform mechanism to derive emptiness algorithms for automata, explaining and simplifying several existing results, as well as proving new decidability results
Looking at Computations from a Different Angle
No full textWe present a novel framework to reason about programs based on encodings of computations as graphs. The main insight here is to rearrange the programs such that given a bound k, each computation can be explored according to any tree decomposition of width k of the corresponding behaviour graph. This produces under-approximations parameterized on k, which result in a complete method when we restrict to classes of behaviour graphs of bounded tree-width. As an additional feature, the transformation of the input program can be targeted to existing tools for the analysis, and thus, off-the-shelf tools based on fixed-point, or capable of analyzing sequential programs with scalar variables and nondeterminism, can be used.To illustrate our approach, we develop this framework for sequential programs and discuss how to extend it to handle concurrency. For the case of sequential programs, we develop a compositional approach to generate on-the-fly tree decompositions of nested words, which is based on graph-summaries. To illustrate our technique, we also implement our algorithms for C programs
Scritto e parlato: tracce di un’antinomia nella trattatistica retorica di età ellenistica
No full textNel presente contributo metteremo in evidenza che, andando alla ricerca di tracce dell’antitesi scritto-parlato nella storia del pensiero, l’indagine sull’epoca ellenistica (323 a.C. – 31 a.C.) ci restituisce una tendenza piuttosto chiara: tali tracce non le troviamo nella riflessione filosofica riconducibile alle tre principali scuole dell’epoca (Epicureismo, Stoicismo e Scetticismo), quanto piuttosto nella trattatistica retorica la quale, ovviamente, si nutre anche della riflessione filosofica precedente, ma ha tuttavia una sua specificità di metodo ed oggetto di indagine
Sequentializing parameterized programs
No full textWe exhibit assertion-preserving (reachability-preserving) transformations from parameterized concurrent shared-memory programs, under a k-round scheduling of processes, to sequential programs. The salient feature of the sequential program is that it tracks the local variables of only one thread at any point, and uses only O(k) copies of shared variables (it does not use extra counters, not even one counter to keep track of the number of threads). Sequentialization is achieved using the concept of a linear interface that captures the effect an unbounded block of processes have on the shared state in a k-round schedule. Linear interfaces in fact serve as summaries for parallel processes, and the sequentialization compiles these linear interfaces to procedural summaries in the sequential program. Our transformation utilizes linear interfaces to sequentialize the program, and to ensure the sequential program explores only reachable states and preserves local invariants
Getting rid of store-buffers in TSO analysis
No full textWe propose an approach for reducing the TSO reachability analysis of concurrent programs to their SC reachability analysis, under some conditions on the explored behaviors. First, we propose a linear code-to-code translation that takes as input a concurrent program P and produces a concurrent program P? such that, running P? under SC yields the same set of reachable (shared) states as running P under TSO with at most k context-switches for each thread, for a fixed k. Basically, we show that it is possible to use only O(k) additional copies of the shared variables of P as local variables to simulate the store buffers, even if they are unbounded. Furthermore, we show that our translation can be extended so that an unbounded number of context-switches is possible, under the condition that each write operation sent to the store buffer stays there for at most k context-switches of the thread. Experimental results show that bugs due to TSO can be detected with small bounds, using off-the-shelf SC analysis tools
- …
