Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(7)
Functional Equivalence
Functional Programming
Left To Right
Linear Time
Satisfiability
Software Verification
Input Output
Subscribe
Academic
Publications
Streaming transducers for algorithmic verification of singlepass listprocessing programs
Streaming transducers for algorithmic verification of singlepass listprocessing programs,10.1145/1925844.1926454,Sigplan Notices,Rajeev Alur,Pavol Č
Edit
Streaming transducers for algorithmic verification of singlepass listprocessing programs
(
Citations: 5
)
BibTex

RIS

RefWorks
Download
Rajeev Alur
,
Pavol Černý
We introduce streaming data string transducers that map input data strings to output data strings in a single lefttoright pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data domain that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next input symbol, updating its state, remembering the input data value in its data variables, and updating datastring variables by concatenating datastring variables and new symbols formed from data variables, while avoiding duplication. We establish PSPACE bounds for the problems of checking
functional equivalence
of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over input/output datastrings. We identify a class of imperative and a class of functional programs, manipulating lists of data items, which can be effectively translated to streaming datastring transducers. The imperative programs dynamically modify a singlylinked heap by changing nextpointers of heapnodes and by adding new nodes. The main restriction specifies how the nextpointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking
functional equivalence
of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.
Journal:
Sigplan Notices  SIGPLAN
, pp. 599610, 2011
DOI:
10.1145/1925844.1926454
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
dl.acm.org
)
(
portal.acm.org
)
(
portal.acm.org
)
Citation Context
(5)
...For example, to pairwise add the numbers in two sequences we could use zipwith(+; [0;
1
; 2]; [3; 4; 5]) = [3; 5; 7],Streaming transducers [
1
] provide another recent symbolic extension of nite transducers where the label theories are restricted to be total orders, in order to maintain decidability of equivalence...
Margus Veanes
,
et al.
DataParallel StringManipulating Programs
...Streaming transducers [
1
] provide another recent symbolic extension of finite transducers where the label theories are restricted to be total orders...
Margus Veanes
,
et al.
Symbolic Tree Transducers
...Streaming transducers [
1
] provide another recent symbolic extension of finite transducers where the label theories are restricted to be total orders, in order to maintain decidability of equivalence...
Margus Veanes
,
et al.
Generating Fast String Manipulating Code Through Transducer Exploratio...
...This talk is based on results reported in [
2
] and [1]...
Rajeev Alur
.
Streaming String Transducers
...Deterministic streaming string transducers (dssts), first introduced in [
1
,2], in addition to all transductions implemented by deterministic finite transducers, can implement transductions such as reversing a string and swapping substrings...
...Deterministic streaming string transducers (dsst) have been proposed as an effective machine model for MSOdefinable string transductions [2,
1
]...
...Let T1 be a( Σ1 ,Σ 2)dsst, with the set of states Q1, and the set of string variables X1, and let T2 be a (Σ2 ,Σ 3)dsst with the set of states Q2 and the set of string variables X2. We review the construction from [
1
] to construct the (Σ1 ,Σ 3)dsst Ts = T1 ◦ T2, i.e., Ts is the sequential composition of T1 and T2 .L et the set of states and the set of string variables of Ts be Qs and Xs respectively...
...The following relationships are known: dmsos = 2dgsm [6], dmsos = dsst [
1
], nmsos � 2ngsm and 2ngsm � nmsos [6]...
...We first show that for every nsst T we can define a nmsos transduction W such that T = W .I n [
1
], the authors shows how a sequence of states and copyless assignments of a dsst can be encoded in the copy set of a dmsostransduction...
...The construction for part (a) is as discussed, for details see [
1
]...
...state q, one string variable x ,a nd for alla ∈ Σ, its transitions are of the form (q, a, x := x.γ, q), where γ is a finite string in Γ ∗ .F rom [
1
], we know that for...
Rajeev Alur
,
et al.
Nondeterministic Streaming String Transducers
References
(18)
Algorithmic Analysis of ArrayAccessing Programs
(
Citations: 2
)
Rajeev Alur
,
Pavol Cerný
,
Scott Weinstein
Conference:
Computer Science Logic  CSL
, pp. 86101, 2009
TwoVariable Logic on Words with Data
(
Citations: 87
)
Mikolaj Bojanczyk
,
Anca Muscholl
,
Thomas Schwentick
,
Luc Segoufin
,
Claire David
Conference:
Logic in Computer Science  LICS
, pp. 716, 2006
Regular Model Checking
(
Citations: 152
)
Ahmed Bouajjani
,
Bengt Jonsson
,
Marcus Nilsson
,
Tayssir Touili
Conference:
Computer Aided Verification  CAV
, pp. 403418, 2000
Verifying Programs with Dynamic 1SelectorLinked Structures in Regular Model Checking
(
Citations: 46
)
Ahmed Bouajjani
,
Peter Habermehl
,
Pierre Moro
,
Tomás Vojnar
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 1329, 2005
Programs with Lists Are Counter Automata
(
Citations: 44
)
Ahmed Bouajjani
,
Marius Bozga
,
Peter Habermehl
,
Radu Iosif
,
Pierre Moro
,
Tomás Vojnar
Conference:
Computer Aided Verification  CAV
, pp. 517531, 2006
Sort by:
Citations
(5)
DataParallel StringManipulating Programs
Margus Veanes
,
David Molnar
,
Todd Mytkowicz
,
Benjamin Livshits
Published in 2012.
Symbolic Tree Transducers
(
Citations: 1
)
Margus Veanes
,
Nikolaj Bjorner
Published in 2011.
Generating Fast String Manipulating Code Through Transducer Exploration and SIMD Integration
Margus Veanes
,
David Molnar
,
Benjamin Livshits
,
Lubomir Litchev
Published in 2011.
Streaming String Transducers
Rajeev Alur
Conference:
Workshop on Logic, Language, Information and Computation  WOLLIC
, 2011
Nondeterministic Streaming String Transducers
Rajeev Alur
,
Jyotirmoy V. Deshmukh