---
OA_place: repository
OA_type: green
_id: '18742'
abstract:
- lang: eng
text: Recent improved determinations of the mass density ρBH of supermassive black
holes (SMBHs) in the local universe have allowed accurate comparisons of ρBH with
the amount of light received from past quasar activity. These comparisons support
the notion that local SMBHs are "dead quasars" and yield a value epsilon ≳ 0.1
for the average radiative efficiency of cosmic SMBH accretion. BH coalescences
may represent an important component of the quasar mass assembly and yet not produce
any observable electromagnetic signature. Therefore, ignoring gravitational wave
(GW) emission during such coalescences, which reduces the amount of mass locked
into remnant BHs, results in an overestimate of epsilon. Here we put constraints
on the magnitude of this bias. We calculate the cumulative mass loss to GWs experienced
by a representative population of BHs during repeated cosmological mergers, using
loss prescriptions based on detailed general relativistic calculations. Despite
the possibly large number of mergers in the assembly history of each individual
SMBH, we find that near-equal mass mergers are rare; therefore, the cumulative
loss is likely to be modest, amounting at most to a 20% increase in the inferred
epsilon value. Thus, recent estimates of epsilon ≳ 0.1 appear robust. The space
interferometer LISA should provide empirical constraints on the dark side of quasar
evolution by measuring the masses and rates of coalescence of massive BHs to cosmological
distances.
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Kristen
full_name: Menou, Kristen
last_name: Menou
- first_name: Zoltán
full_name: Haiman, Zoltán
id: 7c006e8c-cc0d-11ee-8322-cb904ef76f36
last_name: Haiman
orcid: 0000-0003-3633-5403
citation:
ama: Menou K, Haiman Z. On the dark side of quasar evolution. The Astrophysical
Journal. 2004;615(1):130-134. doi:10.1086/423951
apa: Menou, K., & Haiman, Z. (2004). On the dark side of quasar evolution. The
Astrophysical Journal. American Astronomical Society. https://doi.org/10.1086/423951
chicago: Menou, Kristen, and Zoltán Haiman. “On the Dark Side of Quasar Evolution.”
The Astrophysical Journal. American Astronomical Society, 2004. https://doi.org/10.1086/423951.
ieee: K. Menou and Z. Haiman, “On the dark side of quasar evolution,” The Astrophysical
Journal, vol. 615, no. 1. American Astronomical Society, pp. 130–134, 2004.
ista: Menou K, Haiman Z. 2004. On the dark side of quasar evolution. The Astrophysical
Journal. 615(1), 130–134.
mla: Menou, Kristen, and Zoltán Haiman. “On the Dark Side of Quasar Evolution.”
The Astrophysical Journal, vol. 615, no. 1, American Astronomical Society,
2004, pp. 130–34, doi:10.1086/423951.
short: K. Menou, Z. Haiman, The Astrophysical Journal 615 (2004) 130–134.
date_created: 2025-01-03T12:34:57Z
date_published: 2004-11-01T00:00:00Z
date_updated: 2025-01-07T14:02:29Z
day: '01'
doi: 10.1086/423951
extern: '1'
external_id:
arxiv:
- astro-ph/0405335
intvolume: ' 615'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/astro-ph/0405335
month: '11'
oa: 1
oa_version: Preprint
page: 130-134
publication: The Astrophysical Journal
publication_identifier:
eissn:
- 1538-4357
issn:
- 0004-637X
publication_status: published
publisher: American Astronomical Society
quality_controlled: '1'
scopus_import: '1'
status: public
title: On the dark side of quasar evolution
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 615
year: '2004'
...
---
_id: '1963'
abstract:
- lang: eng
text: The mechanism coupling electron transfer and proton pumping in respiratory
complex I (NADH-ubiquinone oxidoreductase) has not been established, but it has
been suggested that it involves conformational changes. Here, the influence of
substrates on the conformation of purified complex I from Escherichia coli was
studied by cross-linking and electron microscopy. When a zero-length cross-linking
reagent was used, the presence of NAD(P)H, in contrast to that of NAD+, prevented
the formation of cross-links between the hydrophilic subunits of the complex,
including NuoB, NuoI, and NuoCD. Comparisons using different cross-linkers suggested
that NuoB, which is likely to coordinate the key iron-sulfur cluster N2, is the
most mobile subunit. The presence of NAD(P)H led also to enhanced proteolysis
of subunit NuoG. These data indicate that upon NAD(P)H binding, the peripheral
arm of the complex adopts a more open conformation, with increased distances between
subunits. Single particle analysis showed the nature of this conformational change.
The enzyme retains its L-shape in the presence of NADH, but exhibits a significantly
more open or expanded structure both in the peripheral arm and, unexpectedly,
in the membrane domain also.
acknowledgement: This work was supported by the Medical Research Council and by a
Royal Society/North Atlantic Treaty Organization postdoctoral fellowship (to A.
A. M.)
author:
- first_name: Aygun
full_name: Mamedova, Aygun A
last_name: Mamedova
- first_name: Peter
full_name: Holt, Peter J
last_name: Holt
- first_name: Joe
full_name: Carroll, Joe D
last_name: Carroll
- first_name: Leonid A
full_name: Leonid Sazanov
id: 338D39FE-F248-11E8-B48F-1D18A9856A87
last_name: Sazanov
orcid: 0000-0002-0977-7989
citation:
ama: Mamedova A, Holt P, Carroll J, Sazanov LA. Substrate-induced conformational
change in bacterial complex I. Journal of Biological Chemistry. 2004;279(22):23830-23836.
doi:10.1074/jbc.M401539200
apa: Mamedova, A., Holt, P., Carroll, J., & Sazanov, L. A. (2004). Substrate-induced
conformational change in bacterial complex I. Journal of Biological Chemistry.
American Society for Biochemistry and Molecular Biology. https://doi.org/10.1074/jbc.M401539200
chicago: Mamedova, Aygun, Peter Holt, Joe Carroll, and Leonid A Sazanov. “Substrate-Induced
Conformational Change in Bacterial Complex I.” Journal of Biological Chemistry.
American Society for Biochemistry and Molecular Biology, 2004. https://doi.org/10.1074/jbc.M401539200.
ieee: A. Mamedova, P. Holt, J. Carroll, and L. A. Sazanov, “Substrate-induced conformational
change in bacterial complex I,” Journal of Biological Chemistry, vol. 279,
no. 22. American Society for Biochemistry and Molecular Biology, pp. 23830–23836,
2004.
ista: Mamedova A, Holt P, Carroll J, Sazanov LA. 2004. Substrate-induced conformational
change in bacterial complex I. Journal of Biological Chemistry. 279(22), 23830–23836.
mla: Mamedova, Aygun, et al. “Substrate-Induced Conformational Change in Bacterial
Complex I.” Journal of Biological Chemistry, vol. 279, no. 22, American
Society for Biochemistry and Molecular Biology, 2004, pp. 23830–36, doi:10.1074/jbc.M401539200.
short: A. Mamedova, P. Holt, J. Carroll, L.A. Sazanov, Journal of Biological Chemistry
279 (2004) 23830–23836.
date_created: 2018-12-11T11:54:56Z
date_published: 2004-05-28T00:00:00Z
date_updated: 2021-01-12T06:54:22Z
day: '28'
doi: 10.1074/jbc.M401539200
extern: 1
intvolume: ' 279'
issue: '22'
month: '05'
page: 23830 - 23836
publication: Journal of Biological Chemistry
publication_status: published
publisher: American Society for Biochemistry and Molecular Biology
publist_id: '5123'
quality_controlled: 0
status: public
title: Substrate-induced conformational change in bacterial complex I
type: journal_article
volume: 279
year: '2004'
...
---
_id: '4372'
acknowledgement: This work was partially supported by the EC projects IST-2001-33520
CC (Control and Computation), IST-2001-35302 AMETIST (Advanced Methods for Timed
Systems) and IST-2003-507219 PROSYD (Property-Based System Design).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Maler O, Nickovic D. Monitoring Temporal Properties of Continuous Signals.
In: Springer; 2004:152-166. doi:10.1007/978-3-540-30206-3_12'
apa: 'Maler, O., & Nickovic, D. (2004). Monitoring Temporal Properties of Continuous
Signals (pp. 152–166). Presented at the FORMATS: Formal Modeling and Analysis
of Timed Systems, Springer. https://doi.org/10.1007/978-3-540-30206-3_12'
chicago: Maler, Oded, and Dejan Nickovic. “Monitoring Temporal Properties of Continuous
Signals,” 152–66. Springer, 2004. https://doi.org/10.1007/978-3-540-30206-3_12.
ieee: 'O. Maler and D. Nickovic, “Monitoring Temporal Properties of Continuous Signals,”
presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2004,
pp. 152–166.'
ista: 'Maler O, Nickovic D. 2004. Monitoring Temporal Properties of Continuous Signals.
FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 152–166.'
mla: Maler, Oded, and Dejan Nickovic. Monitoring Temporal Properties of Continuous
Signals. Springer, 2004, pp. 152–66, doi:10.1007/978-3-540-30206-3_12.
short: O. Maler, D. Nickovic, in:, Springer, 2004, pp. 152–166.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:31Z
date_published: 2004-12-14T00:00:00Z
date_updated: 2025-06-26T09:05:17Z
day: '14'
doi: 10.1007/978-3-540-30206-3_12
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 152 - 166
publication_status: published
publisher: Springer
publist_id: '1088'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring Temporal Properties of Continuous Signals
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2004'
...
---
_id: '4424'
abstract:
- lang: eng
text: "The enormous cost and ubiquity of software errors necessitates the need for
techniques and tools that can precisely analyze large systems and prove that they
meet given specifications, or if they don't, return counterexample behaviors showing
how the system fails. Recent advances in model checking, decision procedures,
program analysis and type systems, and a shift of focus to partial specifications
common to several systems (e.g., memory safety and race freedom) have resulted
in several practical verification methods. However, these methods are either precise
or they are scalable, depending on whether they track the values of variables
or only a fixed small set of dataflow facts (e.g., types), and are usually insufficient
for precisely verifying large programs.\r\n\r\nWe describe a new technique called
Lazy Abstraction (LA) which achieves both precision and scalability by localizing
the use of precise information. LA automatically builds, explores and refines
a single abstract model of the program in a way that different parts of the model
exhibit different degrees of precision, namely just enough to verify the desired
property. The algorithm automatically mines the information required by partitioning
mechanical proofs of unsatisfiability of spurious counterexamples into Craig Interpolants.
For multithreaded systems, we give a new technique based on analyzing the behavior
of a single thread executing in a context which is an abstraction of the other
(arbitrarily many) threads. We define novel context models and show how to automatically
infer them and analyze the full system (thread + context) using LA.\r\n\r\nLA
is implemented in BLAST. We have run BLAST on Windows and Linux Device Drivers
to verify API conformance properties, and have used it to find (or guarantee the
absence of) data races in multithreaded Networked Embedded Systems (NESC) applications.
BLAST is able to prove the absence of races in several cases where earlier methods,
which depend on lock-based synchronization, fail."
article_processing_charge: No
author:
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
citation:
ama: Jhala R. Program verification by lazy abstraction. 2004:1-165.
apa: Jhala, R. (2004). Program verification by lazy abstraction. University
of California, Berkeley.
chicago: Jhala, Ranjit. “Program Verification by Lazy Abstraction.” University of
California, Berkeley, 2004.
ieee: R. Jhala, “Program verification by lazy abstraction,” University of California,
Berkeley, 2004.
ista: Jhala R. 2004. Program verification by lazy abstraction. University of California,
Berkeley.
mla: Jhala, Ranjit. Program Verification by Lazy Abstraction. University
of California, Berkeley, 2004, pp. 1–165.
short: R. Jhala, Program Verification by Lazy Abstraction, University of California,
Berkeley, 2004.
date_created: 2018-12-11T12:08:47Z
date_published: 2004-12-01T00:00:00Z
date_updated: 2021-01-12T07:56:52Z
day: '01'
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 1 - 165
publication_status: published
publisher: University of California, Berkeley
publist_id: '307'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Program verification by lazy abstraction
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2004'
...
---
OA_type: closed access
_id: '4445'
abstract:
- lang: eng
text: We present a type system for E code, which is an assembly language that manages
the release, interaction, and termination of real-time tasks. E code specifies
a deadline for each task, and the type system ensures that the deadlines are path-insensitive.
We show that typed E programs allow, for given worst-case execution times of tasks,
a simple schedulability analysis. Moreover, the real-time programming language
Giotto can be compiled into typed E~code. This shows that typed E~code identifies
an easily schedulable yet expressive class of real-time programs. We have extended
the Giotto compiler to generate typed E code, and enabled the run-time system
for E code to perform a type and schedulability check before executing the code.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327
and by the NSF grants CCR- 0208875 and CCR-0225610.
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
citation:
ama: 'Henzinger TA, Kirsch C. A typed assembly language for real-time programs.
In: Proceedings of the 4th ACM International Conference on Embedded Software.
Association for Computing Machinery; 2004:104-113. doi:10.1145/1017753.1017774'
apa: 'Henzinger, T. A., & Kirsch, C. (2004). A typed assembly language for real-time
programs. In Proceedings of the 4th ACM international conference on Embedded
software (pp. 104–113). Pisa, Italy: Association for Computing Machinery.
https://doi.org/10.1145/1017753.1017774'
chicago: Henzinger, Thomas A, and Christoph Kirsch. “A Typed Assembly Language for
Real-Time Programs.” In Proceedings of the 4th ACM International Conference
on Embedded Software, 104–13. Association for Computing Machinery, 2004. https://doi.org/10.1145/1017753.1017774.
ieee: T. A. Henzinger and C. Kirsch, “A typed assembly language for real-time programs,”
in Proceedings of the 4th ACM international conference on Embedded software,
Pisa, Italy, 2004, pp. 104–113.
ista: 'Henzinger TA, Kirsch C. 2004. A typed assembly language for real-time programs.
Proceedings of the 4th ACM international conference on Embedded software. EMSOFT:
Embedded Software , 104–113.'
mla: Henzinger, Thomas A., and Christoph Kirsch. “A Typed Assembly Language for
Real-Time Programs.” Proceedings of the 4th ACM International Conference on
Embedded Software, Association for Computing Machinery, 2004, pp. 104–13,
doi:10.1145/1017753.1017774.
short: T.A. Henzinger, C. Kirsch, in:, Proceedings of the 4th ACM International
Conference on Embedded Software, Association for Computing Machinery, 2004, pp.
104–113.
conference:
end_date: 2004-09-29
location: Pisa, Italy
name: 'EMSOFT: Embedded Software '
start_date: 2004-09-27
date_created: 2018-12-11T12:08:53Z
date_published: 2004-09-27T00:00:00Z
date_updated: 2026-05-29T09:45:12Z
day: '27'
doi: 10.1145/1017753.1017774
extern: '1'
language:
- iso: eng
month: '09'
oa_version: None
page: 104 - 113
publication: Proceedings of the 4th ACM international conference on Embedded software
publication_identifier:
isbn:
- '9781581138603'
publication_status: published
publisher: Association for Computing Machinery
publist_id: '285'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A typed assembly language for real-time programs
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...
---
OA_type: closed access
_id: '4458'
abstract:
- lang: eng
text: 'The success of model checking for large programs depends crucially on the
ability to efficiently construct parsimonious abstractions. A predicate abstraction
is parsimonious if at each control location, it specifies only relationships between
current values of variables, and only those which are required for proving correctness.
Previous methods for automatically refining predicate abstractions until sufficient
precision is obtained do not systematically construct parsimonious abstractions:
predicates usually contain symbolic variables, and are added heuristically and
often uniformly to many or all control locations at once. We use Craig interpolation
to efficiently construct, from a given abstract error trace which cannot be concretized,
a parsominous abstraction that removes the trace. At each location of the trace,
we infer the relevant predicates as an interpolant between the two formulas that
define the past and the future segment of the trace. Each interpolant is a relationship
between current values of program variables, and is relevant only at that particular
program location. It can be found by a linear scan of the proof of infeasibility
of the trace.We develop our method for programs with arithmetic and pointer expressions,
and call-by-value function calls. For function calls, Craig interpolation offers
a systematic way of generating relevant predicates that contain only the local
variables of the function and the values of the formal parameters when the function
was called. We have extended our model checker Blast with predicate discovery
by Craig interpolation, and applied it successfully to C programs with more than
130,000 lines of code, which was not possible with approaches that build less
parsimonious abstractions.'
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Kenneth
full_name: Mcmillan, Kenneth
last_name: Mcmillan
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Mcmillan K. Abstractions from proofs. In:
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages. Association for Computing Machinery; 2004:232-244. doi:10.1145/964001.964021'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Mcmillan, K. (2004). Abstractions
from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles
of programming languages (pp. 232–244). Venice, Italy: Association for Computing
Machinery. https://doi.org/10.1145/964001.964021'
chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Kenneth Mcmillan.
“Abstractions from Proofs.” In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, 232–44. Association for Computing
Machinery, 2004. https://doi.org/10.1145/964001.964021.
ieee: T. A. Henzinger, R. Jhala, R. Majumdar, and K. Mcmillan, “Abstractions from
proofs,” in Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles
of programming languages, Venice, Italy, 2004, pp. 232–244.
ista: 'Henzinger TA, Jhala R, Majumdar R, Mcmillan K. 2004. Abstractions from proofs.
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming
languages. POPL: Principles of Programming Languages, 232–244.'
mla: Henzinger, Thomas A., et al. “Abstractions from Proofs.” Proceedings of
the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
Association for Computing Machinery, 2004, pp. 232–44, doi:10.1145/964001.964021.
short: T.A. Henzinger, R. Jhala, R. Majumdar, K. Mcmillan, in:, Proceedings of the
31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association
for Computing Machinery, 2004, pp. 232–244.
conference:
end_date: 2004-01-16
location: Venice, Italy
name: 'POPL: Principles of Programming Languages'
start_date: 2004-01-14
date_created: 2018-12-11T12:08:57Z
date_published: 2004-04-01T00:00:00Z
date_updated: 2026-05-29T09:32:36Z
day: '01'
doi: 10.1145/964001.964021
extern: '1'
language:
- iso: eng
month: '04'
oa_version: None
page: 232 - 244
publication: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of
programming languages
publication_identifier:
isbn:
- '9781581137293'
publication_status: published
publisher: Association for Computing Machinery
publist_id: '270'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstractions from proofs
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...
---
OA_type: closed access
_id: '4459'
abstract:
- lang: eng
text: Software model checking has been successful for sequential programs, where
predicate abstraction offers suitable models, and counterexample-guided abstraction
refinement permits the automatic inference of models. When checking concurrent
programs, we need to abstract threads as well as the contexts in which they execute.
Stateless context models, such as predicates on global variables, prove insufficient
for showing the absence of race conditions in many examples. We therefore use
richer context models, which combine (1) predicates for abstracting data state,
(2) control flow quotients for abstracting control state, and (3) counters for
abstracting an unbounded number of threads. We infer suitable context models automatically
by a combination of counterexample-guided abstraction refinement, bisimulation
minimization, circular assume-guarantee reasoning, and parametric reasoning about
an unbounded number of threads. This algorithm, called CIRC, has been implemented
in BLAST and succeeds in checking many examples of NESC code for data races. In
particular, BLAST proves the absence of races in several cases where previous
race checkers give false positives.
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In:
Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design
and Implementation. Association for Computing Machinery; 2004:1-13. doi:10.1145/996841.996844'
apa: 'Henzinger, T. A., Jhala, R., & Majumdar, R. (2004). Race checking by context
inference. In Proceedings of the ACM SIGPLAN 2004 conference on Programming
language design and implementation (pp. 1–13). Washington, DC, United States:
Association for Computing Machinery. https://doi.org/10.1145/996841.996844'
chicago: Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Race Checking
by Context Inference.” In Proceedings of the ACM SIGPLAN 2004 Conference on
Programming Language Design and Implementation, 1–13. Association for Computing
Machinery, 2004. https://doi.org/10.1145/996841.996844.
ieee: T. A. Henzinger, R. Jhala, and R. Majumdar, “Race checking by context inference,”
in Proceedings of the ACM SIGPLAN 2004 conference on Programming language design
and implementation, Washington, DC, United States, 2004, pp. 1–13.
ista: 'Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference.
Proceedings of the ACM SIGPLAN 2004 conference on Programming language design
and implementation. PLDI: Programming Languages Design and Implementation, 1–13.'
mla: Henzinger, Thomas A., et al. “Race Checking by Context Inference.” Proceedings
of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation,
Association for Computing Machinery, 2004, pp. 1–13, doi:10.1145/996841.996844.
short: T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the ACM SIGPLAN
2004 Conference on Programming Language Design and Implementation, Association
for Computing Machinery, 2004, pp. 1–13.
conference:
end_date: 2004-06-11
location: Washington, DC, United States
name: 'PLDI: Programming Languages Design and Implementation'
start_date: 2004-06-09
date_created: 2018-12-11T12:08:57Z
date_published: 2004-06-09T00:00:00Z
date_updated: 2026-05-29T09:37:45Z
day: '09'
doi: 10.1145/996841.996844
extern: '1'
language:
- iso: eng
month: '06'
oa_version: None
page: 1 - 13
publication: Proceedings of the ACM SIGPLAN 2004 conference on Programming language
design and implementation
publication_identifier:
isbn:
- '1581138075'
publication_status: published
publisher: Association for Computing Machinery
publist_id: '271'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Race checking by context inference
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...
---
OA_place: repository
OA_type: green
_id: '4461'
abstract:
- lang: eng
text: One of the central axioms of extreme programming is the disciplined use of
regression testing during stepwise software development. Due to recent progress
in software model checking, it has become possible to supplement this process
with automatic checks for behavioral safety properties of programs, such as conformance
with locking idioms and other programming protocols and patterns. For efficiency
reasons, all checks must be incremental, i.e., they must reuse partial results
from previous checks in order to avoid all unnecessary repetition of expensive
verification tasks. We show that the lazy-abstraction algorithm, and its implementation
in Blast, can be extended to support the fully automatic and incremental checking
of temporal safety properties during software development.
acknowledgement: 'This work was supported in part by the NSF grants CCR-9988172, CCR-0085949,
and CCR-0234690, the ONR grant N00014-02-1-0671, the DARPA grant F33615-00-C-1693,
and the MARCO grant 98-DT-660. '
alternative_title:
- Lecture Notes in Computer Science
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Marco
full_name: Sanvido, Marco
last_name: Sanvido
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Sanvido M. Extreme Model Checking. In:
Verification: Theory and Practice. Vol 2772. Lecture Notes in Computer
Science. Berlin: Springer Nature; 2004:332-358. doi:10.1007/978-3-540-39910-0_16'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Sanvido, M. (2004). Extreme
Model Checking. In Verification: Theory and Practice (Vol. 2772, pp. 332–358).
Berlin: Springer Nature. https://doi.org/10.1007/978-3-540-39910-0_16'
chicago: 'Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Marco Sanvido.
“Extreme Model Checking.” In Verification: Theory and Practice, 2772:332–58.
Lecture Notes in Computer Science. Berlin: Springer Nature, 2004. https://doi.org/10.1007/978-3-540-39910-0_16.'
ieee: 'T. A. Henzinger, R. Jhala, R. Majumdar, and M. Sanvido, “Extreme Model Checking,”
in Verification: Theory and Practice, vol. 2772, Berlin: Springer Nature,
2004, pp. 332–358.'
ista: 'Henzinger TA, Jhala R, Majumdar R, Sanvido M. 2004.Extreme Model Checking.
In: Verification: Theory and Practice. Lecture Notes in Computer Science, vol.
2772, 332–358.'
mla: 'Henzinger, Thomas A., et al. “Extreme Model Checking.” Verification: Theory
and Practice, vol. 2772, Springer Nature, 2004, pp. 332–58, doi:10.1007/978-3-540-39910-0_16.'
short: 'T.A. Henzinger, R. Jhala, R. Majumdar, M. Sanvido, in:, Verification: Theory
and Practice, Springer Nature, Berlin, 2004, pp. 332–358.'
date_created: 2018-12-11T12:08:58Z
date_published: 2004-02-24T00:00:00Z
date_updated: 2026-05-29T09:24:17Z
day: '24'
doi: 10.1007/978-3-540-39910-0_16
extern: '1'
intvolume: ' 2772'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://progsys.ucsd.edu/~rjhala/papers/extreme_model_checking.pdf
month: '02'
oa: 1
oa_version: Preprint
page: 332 - 358
place: Berlin
publication: 'Verification: Theory and Practice'
publication_identifier:
eisbn:
- '9783540399100'
isbn:
- '9783540210023'
publication_status: published
publisher: Springer Nature
publist_id: '269'
quality_controlled: '1'
series_title: Lecture Notes in Computer Science
status: public
title: Extreme Model Checking
type: book_chapter
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 2772
year: '2004'
...
---
OA_place: repository
OA_type: green
_id: '4525'
abstract:
- lang: eng
text: 'We present a new high-level programming language, called xGiotto, for programming
applications with hard real-time constraints. Like its predecessor, xGiotto is
based on the LET (logical execution time) assumption: the programmer specifies
when the outputs of a task become available, and the compiler checks if the specification
can be implemented on a given platform. However, while the predecessor language
xGiotto was purely time-triggered, xGiotto accommodates also asynchronous events.
Indeed, through a mechanism called event scoping, events are the main structuring
principle of the new language. The xGiotto compiler and run-time system implement
event scoping through a tree-based event filter. The compiler also checks programs
for determinism (absence of race conditions).'
acknowledgement: This research is supported by the AFOSR MURI grant F49620-00-1-0327,
the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, and the NSF
grants CCR-0208875 and CCR-0225610.
alternative_title:
- Lecture Notes in Computer Science
article_processing_charge: No
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Marco
full_name: Sanvido, Marco
last_name: Sanvido
citation:
ama: 'Ghosal A, Henzinger TA, Kirsch C, Sanvido M. Event-driven programming with
logical execution times. In: Springer Nature; 2004:357-371. doi:10.1007/978-3-540-24743-2_24'
apa: 'Ghosal, A., Henzinger, T. A., Kirsch, C., & Sanvido, M. (2004). Event-driven
programming with logical execution times (pp. 357–371). Presented at the HSCC:
Hybrid Systems - Computation and Control, Philadelphia, PA, United States: Springer
Nature. https://doi.org/10.1007/978-3-540-24743-2_24'
chicago: Ghosal, Arkadeb, Thomas A Henzinger, Christoph Kirsch, and Marco Sanvido.
“Event-Driven Programming with Logical Execution Times,” 357–71. Springer Nature,
2004. https://doi.org/10.1007/978-3-540-24743-2_24.
ieee: 'A. Ghosal, T. A. Henzinger, C. Kirsch, and M. Sanvido, “Event-driven programming
with logical execution times,” presented at the HSCC: Hybrid Systems - Computation
and Control, Philadelphia, PA, United States, 2004, pp. 357–371.'
ista: 'Ghosal A, Henzinger TA, Kirsch C, Sanvido M. 2004. Event-driven programming
with logical execution times. HSCC: Hybrid Systems - Computation and Control,
Lecture Notes in Computer Science, , 357–371.'
mla: Ghosal, Arkadeb, et al. Event-Driven Programming with Logical Execution
Times. Springer Nature, 2004, pp. 357–71, doi:10.1007/978-3-540-24743-2_24.
short: A. Ghosal, T.A. Henzinger, C. Kirsch, M. Sanvido, in:, Springer Nature, 2004,
pp. 357–371.
conference:
end_date: 2004-03-27
location: Philadelphia, PA, United States
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2004-03-25
date_created: 2018-12-11T12:09:18Z
date_published: 2004-03-12T00:00:00Z
date_updated: 2026-05-29T09:15:20Z
day: '12'
doi: 10.1007/978-3-540-24743-2_24
extern: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.cs.uni-salzburg.at/~ck/content/publications/conferences/HSCC04-EventDrivenProgramming.pdf
month: '03'
oa: 1
oa_version: Preprint
page: 357-371
publication_identifier:
eisbn:
- '9783540247432'
isbn:
- '9783540212591'
publication_status: published
publisher: Springer Nature
publist_id: '200'
quality_controlled: '1'
status: public
title: Event-driven programming with logical execution times
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...
---
OA_type: closed access
_id: '4555'
abstract:
- lang: eng
text: Strategies in repeated games can be classified as to whether or not they use
memory and/or randomization. We consider Markov decision processes and 2-player
graph games, both of the deterministic and probabilistic varieties. We characterize
when memory and/or randomization are required for winning with respect to various
classes of w-regular objectives, noting particularly when the use of memory can
be traded for the use of randomization. In particular, we show that Markov decision
processes allow randomized memoryless optimal strategies for all M?ller objectives.
Furthermore, we show that 2-player probabilistic graph games allow randomized
memoryless strategies for winning with probability 1 those M?ller objectives which
are upward-closed. Upward-closure means that if a set α of infinitely repeating
vertices is winning, then all supersets of α are also winning.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, De Alfaro L, Henzinger TA. Trading memory for randomness. In:
IEEE; 2004:206-217. doi:10.1109/QEST.2004.10051'
apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2004). Trading memory
for randomness (pp. 206–217). Presented at the QEST: Quantitative Evaluation of
Systems, Enschede, Netherlands: IEEE. https://doi.org/10.1109/QEST.2004.10051'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Trading
Memory for Randomness,” 206–17. IEEE, 2004. https://doi.org/10.1109/QEST.2004.10051.
ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Trading memory for randomness,”
presented at the QEST: Quantitative Evaluation of Systems, Enschede, Netherlands,
2004, pp. 206–217.'
ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2004. Trading memory for randomness.
QEST: Quantitative Evaluation of Systems, 206–217.'
mla: Chatterjee, Krishnendu, et al. Trading Memory for Randomness. IEEE,
2004, pp. 206–17, doi:10.1109/QEST.2004.10051.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2004, pp. 206–217.
conference:
end_date: 2004-09-30
location: Enschede, Netherlands
name: 'QEST: Quantitative Evaluation of Systems'
start_date: 2004-09-27
date_created: 2018-12-11T12:09:27Z
date_published: 2004-09-30T00:00:00Z
date_updated: 2026-05-29T09:05:35Z
day: '30'
doi: 10.1109/QEST.2004.10051
extern: '1'
language:
- iso: eng
month: '09'
oa_version: None
page: 206 - 217
publication_identifier:
isbn:
- '0769521851'
publication_status: published
publisher: IEEE
publist_id: '155'
quality_controlled: '1'
status: public
title: Trading memory for randomness
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...
---
OA_place: publisher
OA_type: free access
_id: '4556'
abstract:
- lang: eng
text: We study the problem of determining stack boundedness and the exact maximum
stack size for three classes of interrupt-driven programs. Interrupt-driven programs
are used in many real-time applications that require responsive interrupt handling.
In order to ensure responsiveness, programmers often enable interrupt processing
in the body of lower-priority interrupt handlers. In such programs a programming
error can allow interrupt handlers to be interrupted in a cyclic fashion to lead
to an unbounded stack, causing the system to crash. For a restricted class of
interrupt-driven programs, we show that there is a polynomial-time procedure to
check stack boundedness, while determining the exact maximum stack size is PSPACE-complete.
For a larger class of programs, the two problems are both PSPACE-complete, and
for the largest class of programs we consider, the two problems are PSPACE-hard
and can be solved in exponential time. While the complexities are high, our algorithms
are exponential only in the number of handlers, and polynomial in the size of
the program.
article_processing_charge: No
article_type: original
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Di
full_name: Ma, Di
last_name: Ma
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Tian
full_name: Zhao, Tian
last_name: Zhao
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jens
full_name: Palsberg, Jens
last_name: Palsberg
citation:
ama: Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. Stack size
analysis for interrupt-driven programs. Information and Computation. 2004;194(2):144-174.
doi:10.1016/j.ic.2004.06.001
apa: Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., & Palsberg,
J. (2004). Stack size analysis for interrupt-driven programs. Information and
Computation. Elsevier. https://doi.org/10.1016/j.ic.2004.06.001
chicago: Chatterjee, Krishnendu, Di Ma, Ritankar Majumdar, Tian Zhao, Thomas A Henzinger,
and Jens Palsberg. “Stack Size Analysis for Interrupt-Driven Programs.” Information
and Computation. Elsevier, 2004. https://doi.org/10.1016/j.ic.2004.06.001.
ieee: K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T. A. Henzinger, and J. Palsberg,
“Stack size analysis for interrupt-driven programs,” Information and Computation,
vol. 194, no. 2. Elsevier, pp. 144–174, 2004.
ista: Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. 2004. Stack
size analysis for interrupt-driven programs. Information and Computation. 194(2),
144–174.
mla: Chatterjee, Krishnendu, et al. “Stack Size Analysis for Interrupt-Driven Programs.”
Information and Computation, vol. 194, no. 2, Elsevier, 2004, pp. 144–74,
doi:10.1016/j.ic.2004.06.001.
short: K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T.A. Henzinger, J. Palsberg,
Information and Computation 194 (2004) 144–174.
date_created: 2018-12-11T12:09:28Z
date_published: 2004-11-01T00:00:00Z
date_updated: 2026-05-29T09:10:28Z
day: '01'
doi: 10.1016/j.ic.2004.06.001
extern: '1'
intvolume: ' 194'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.ic.2004.06.001
month: '11'
oa: 1
oa_version: Accepted Version
page: 144 - 174
publication: Information and Computation
publication_identifier:
eissn:
- 1090-2651
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '156'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Stack size analysis for interrupt-driven programs
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 194
year: '2004'
...
---
OA_place: repository
OA_type: green
_id: '4558'
abstract:
- lang: eng
text: We study perfect-information stochastic parity games. These are two-player
nonterminating games which are played on a graph with turn-based probabilistic
transitions. A play results in an infinite path and the conflicting goals of the
two players are ω-regular path properties, formalized as parity winning conditions.
The qualitative solution of such a game amounts to computing the set of vertices
from which a player has a strategy to win with probability 1 (or with positive
probability). The quantitative solution amounts to computing the value of the
game in every vertex, i.e., the highest probability with which a player can guarantee
satisfaction of his own objective in a play that starts from the vertex.For the
important special case of one-player stochastic parity games (parity Markov decision
processes) we give polynomial-time algorithms both for the qualitative and the
quantitative solution. The running time of the qualitative solution is O(d · m3/2)
for graphs with m edges and d priorities. The quantitative solution is based on
a linear-programming formulation.For the two-player case, we establish the existence
of optimal pure memoryless strategies. This has several important ramifications.
First, it implies that the values of the games are rational. This is in contrast
to the concurrent stochastic parity games of de Alfaro et al.; there, values are
in general algebraic numbers, optimal strategies do not exist, and ε-optimal strategies
have to be mixed and with infinite memory. Second, the existence of optimal pure
memoryless strategies together with the polynomial-time solution forone-player
case implies that the quantitative two-player stochastic parity game problem is
in NP ∩ co-NP. This generalizes a result of Condon for stochastic games with reachability
objectives. It also constitutes an exponential improvement over the best previous
algorithm, which is based on a doubly exponential procedure of de Alfaro and Majumdar
for concurrent stochastic parity games and provides only ε-approximations of the
values.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Jurdziński M, Henzinger TA. Quantitative stochastic parity games.
In: Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms.
Association for Computing Machinery; 2004:121-130. doi:10.5555/982792.982808'
apa: 'Chatterjee, K., Jurdziński, M., & Henzinger, T. A. (2004). Quantitative
stochastic parity games. In Proceedings of the 15th annual ACM-SIAM symposium
on Discrete algorithms (pp. 121–130). New Orleans, LA, United States: Association
for Computing Machinery. https://doi.org/10.5555/982792.982808'
chicago: Chatterjee, Krishnendu, Marcin Jurdziński, and Thomas A Henzinger. “Quantitative
Stochastic Parity Games.” In Proceedings of the 15th Annual ACM-SIAM Symposium
on Discrete Algorithms, 121–30. Association for Computing Machinery, 2004.
https://doi.org/10.5555/982792.982808.
ieee: K. Chatterjee, M. Jurdziński, and T. A. Henzinger, “Quantitative stochastic
parity games,” in Proceedings of the 15th annual ACM-SIAM symposium on Discrete
algorithms, New Orleans, LA, United States, 2004, pp. 121–130.
ista: 'Chatterjee K, Jurdziński M, Henzinger TA. 2004. Quantitative stochastic parity
games. Proceedings of the 15th annual ACM-SIAM symposium on Discrete algorithms.
SODA: Symposium on Discrete Algorithms, 121–130.'
mla: Chatterjee, Krishnendu, et al. “Quantitative Stochastic Parity Games.” Proceedings
of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms, Association
for Computing Machinery, 2004, pp. 121–30, doi:10.5555/982792.982808.
short: K. Chatterjee, M. Jurdziński, T.A. Henzinger, in:, Proceedings of the 15th
Annual ACM-SIAM Symposium on Discrete Algorithms, Association for Computing Machinery,
2004, pp. 121–130.
conference:
end_date: 2004-01-14
location: New Orleans, LA, United States
name: 'SODA: Symposium on Discrete Algorithms'
start_date: 2004-01-11
date_created: 2018-12-11T12:09:28Z
date_published: 2004-02-01T00:00:00Z
date_updated: 2026-05-29T08:40:03Z
day: '01'
doi: 10.5555/982792.982808
extern: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.dcs.warwick.ac.uk/people/academic/Marcin.Jurdzinski/Papers/CJH04-SODA.pdf
month: '02'
oa: 1
oa_version: Preprint
page: 121 - 130
publication: Proceedings of the 15th annual ACM-SIAM symposium on Discrete algorithms
publication_identifier:
isbn:
- 089871558X
publication_status: published
publisher: Association for Computing Machinery
publist_id: '153'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative stochastic parity games
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...
---
OA_type: closed access
_id: '4577'
abstract:
- lang: eng
text: While model checking has been successful in uncovering subtle bugs in code,
its adoption in software engineering practice has been hampered by the absence
of a simple interface to the programmer in an integrated development environment.
We describe an integration of the software model checker BLAST into the Eclipse
development environment. We provide a verification interface for practical solutions
for some typical program analysis problems - assertion checking, reachability
analysis, dead code analysis, and test generation - directly on the source code.
The analysis is completely automatic, and assumes no knowledge of model checking
or formal notation. Moreover, the interface supports incremental program verification
to support incremental design and evolution of code.
acknowledgement: This research was supported in part by the NSF grants CCR-0085949,
CCR-0234690, and ITR-0326577.
article_processing_charge: No
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. An eclipse plug-in for model checking.
In: Proceedings of the 12th IEEE International Workshop on Program Comprehension.
IEEE; 2004:251-255. doi:10.1109/WPC.2004.1311069
'
apa: 'Beyer, D., Henzinger, T. A., Jhala, R., & Majumdar, R. (2004). An eclipse
plug-in for model checking. In Proceedings of the 12th IEEE International Workshop
on Program Comprehension (pp. 251–255). Bari, Italy: IEEE. https://doi.org/10.1109/WPC.2004.1311069 '
chicago: Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “An
Eclipse Plug-in for Model Checking.” In Proceedings of the 12th IEEE International
Workshop on Program Comprehension, 251–55. IEEE, 2004. https://doi.org/10.1109/WPC.2004.1311069 .
ieee: D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “An eclipse plug-in
for model checking,” in Proceedings of the 12th IEEE International Workshop
on Program Comprehension, Bari, Italy, 2004, pp. 251–255.
ista: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. 2004. An eclipse plug-in for
model checking. Proceedings of the 12th IEEE International Workshop on Program
Comprehension. IWPC: Program Comprehension, 251–255.'
mla: Beyer, Dirk, et al. “An Eclipse Plug-in for Model Checking.” Proceedings
of the 12th IEEE International Workshop on Program Comprehension, IEEE, 2004,
pp. 251–55, doi:10.1109/WPC.2004.1311069
.
short: D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the
12th IEEE International Workshop on Program Comprehension, IEEE, 2004, pp. 251–255.
conference:
end_date: 2004-06-26
location: Bari, Italy
name: 'IWPC: Program Comprehension'
start_date: 2004-06-26
date_created: 2018-12-11T12:09:34Z
date_published: 2004-07-12T00:00:00Z
date_updated: 2026-05-29T08:23:32Z
day: '12'
doi: '10.1109/WPC.2004.1311069 '
extern: '1'
language:
- iso: eng
month: '07'
oa_version: None
page: 251 - 255
publication: Proceedings of the 12th IEEE International Workshop on Program Comprehension
publication_identifier:
isbn:
- '0769521495'
issn:
- 1092-8138
publication_status: published
publisher: IEEE
publist_id: '129'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An eclipse plug-in for model checking
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...
---
OA_type: closed access
_id: '4578'
abstract:
- lang: eng
text: 'BLAST is an automatic verification tool for checking temporal safety properties
of C programs. Blast is based on lazy predicate abstraction driven by interpolation-based
predicate discovery. In this paper, we present the Blast specification language.
The language specifies program properties at two levels of precision. At the lower
level, monitor automata are used to specify temporal safety properties of program
executions (traces). At the higher level, relational reachability queries over
program locations are used to combine lower-level trace properties. The two-level
specification language can be used to break down a verification task into several
independent calls of the model-checking engine. In this way, each call to the
model checker may have to analyze only part of the program, or part of the specification,
and may thus succeed in a reduction of the number of predicates needed for the
analysis. In addition, the two-level specification language provides a means for
structuring and maintaining specifications. '
acknowledgement: This research was supported in part by the NSF grants CCR-0085949,
CCR-0234690, and ITR-0326577.
alternative_title:
- Lecture Notes in Computer Science
article_processing_charge: No
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Adam
full_name: Chlipala, Adam
last_name: Chlipala
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. The BLAST query language
for software verification. In: Vol 3148. Springer; 2004:2-18. doi:10.1007/978-3-540-27864-1_2'
apa: 'Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., & Majumdar, R. (2004).
The BLAST query language for software verification (Vol. 3148, pp. 2–18). Presented
at the SAS: Static Analysis Symposium, Verona, Italy: Springer. https://doi.org/10.1007/978-3-540-27864-1_2'
chicago: Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar
Majumdar. “The BLAST Query Language for Software Verification,” 3148:2–18. Springer,
2004. https://doi.org/10.1007/978-3-540-27864-1_2.
ieee: 'D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “The BLAST
query language for software verification,” presented at the SAS: Static Analysis
Symposium, Verona, Italy, 2004, vol. 3148, pp. 2–18.'
ista: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. The BLAST query
language for software verification. SAS: Static Analysis Symposium, Lecture Notes
in Computer Science, vol. 3148, 2–18.'
mla: Beyer, Dirk, et al. The BLAST Query Language for Software Verification.
Vol. 3148, Springer, 2004, pp. 2–18, doi:10.1007/978-3-540-27864-1_2.
short: D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Springer,
2004, pp. 2–18.
conference:
end_date: 2004-08-28
location: Verona, Italy
name: 'SAS: Static Analysis Symposium'
start_date: 2004-08-26
date_created: 2018-12-11T12:09:34Z
date_published: 2004-08-17T00:00:00Z
date_updated: 2026-05-29T08:31:41Z
day: '17'
doi: 10.1007/978-3-540-27864-1_2
extern: '1'
intvolume: ' 3148'
language:
- iso: eng
month: '08'
oa_version: None
page: 2 - 18
publication_identifier:
eisbn:
- '9783540278641'
isbn:
- '9783540227915'
issn:
- 0302-9743
publication_status: published
publisher: Springer
publist_id: '130'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The BLAST query language for software verification
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 3148
year: '2004'
...
---
OA_type: closed access
_id: '4581'
abstract:
- lang: eng
text: We have extended the software model checker BLAST to automatically generate
test suites that guarantee full coverage with respect to a given predicate. More
precisely, given a C program and a target predicate p, BLAST determines the set
L of program locations which program execution can reach with p true, and automatically
generates a set of test vectors that exhibit the truth of p at all locations in
L. We have used BLAST to generate test suites and to detect dead code in C programs
with up to 30 K lines of code. The analysis and test vector generation is fully
automatic (no user intervention) and exact (no false positives).
article_processing_charge: No
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Adam
full_name: Chlipala, Adam
last_name: Chlipala
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. Generating tests from
counterexamples. In: Proceedings of the 26th International Conference on Software
Engineering. IEEE; 2004:326-335. doi:10.1109/ICSE.2004.1317455'
apa: 'Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., & Majumdar, R. (2004).
Generating tests from counterexamples. In Proceedings of the 26th International
Conference on Software Engineering (pp. 326–335). Edinburgh, United Kingdom:
IEEE. https://doi.org/10.1109/ICSE.2004.1317455'
chicago: Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar
Majumdar. “Generating Tests from Counterexamples.” In Proceedings of the 26th
International Conference on Software Engineering, 326–35. IEEE, 2004. https://doi.org/10.1109/ICSE.2004.1317455.
ieee: D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “Generating
tests from counterexamples,” in Proceedings of the 26th International Conference
on Software Engineering, Edinburgh, United Kingdom, 2004, pp. 326–335.
ista: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. Generating
tests from counterexamples. Proceedings of the 26th International Conference on
Software Engineering. ICSE: Software Engineering, 326–335.'
mla: Beyer, Dirk, et al. “Generating Tests from Counterexamples.” Proceedings
of the 26th International Conference on Software Engineering, IEEE, 2004,
pp. 326–35, doi:10.1109/ICSE.2004.1317455.
short: D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings
of the 26th International Conference on Software Engineering, IEEE, 2004, pp.
326–335.
conference:
end_date: 2004-05-28
location: Edinburgh, United Kingdom
name: 'ICSE: Software Engineering'
start_date: 2004-05-23
date_created: 2018-12-11T12:09:35Z
date_published: 2004-07-26T00:00:00Z
date_updated: 2026-05-29T07:46:59Z
day: '26'
doi: 10.1109/ICSE.2004.1317455
extern: '1'
language:
- iso: eng
month: '07'
oa_version: None
page: 326 - 335
publication: Proceedings of the 26th International Conference on Software Engineering
publication_identifier:
isbn:
- '0769521630'
issn:
- 0270-5257
publication_status: published
publisher: IEEE
publist_id: '128'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Generating tests from counterexamples
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...
---
OA_type: closed access
_id: '4629'
abstract:
- lang: eng
text: 'Temporal logic is two-valued: a property is either true or false. When applied
to the analysis of stochastic systems, or systems with imprecise formal models,
temporal logic is therefore fragile: even small changes in the model can lead
to opposite truth values for a specification. We present a generalization of the
branching-time logic Ctl which achieves robustness with respect to model perturbations
by giving a quantitative interpretation to predicates and logical operators, and
by discounting the importance of events according to how late they occur. In every
state, the value of a formula is a real number in the interval [0,1], where 1
corresponds to truth and 0 to falsehood. The boolean operators and and or are
replaced by min and max, the path quantifiers ∃ and ∀ determine sup and inf over
all paths from a given state, and the temporal operators and □ specify sup and
inf over a given path; a new operator averages all values along a path. Furthermore,
all path operators are discounted by a parameter that can be chosen to give more
weight to states that are closer to the beginning of the path. We interpret the
resulting logic Dctl over transition systems, Markov chains, and Markov decision
processes. We present two semantics for Dctl: a path semantics, inspired by the
standard interpretation of state and path formulas in CTL, and a fixpoint semantics,
inspired by the μ-calculus evaluation of CTL formulas. We show that, while these
semantics coincide for CTL, they differ for Dctl, and we provide model-checking
algorithms for both semantics.'
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
the ONR grant N00014-02-1-0671, and the NSF grants CCR-0132780, CCR-9988172, CCR-0225610,
and CCR-0234690.
alternative_title:
- Lecture Notes in Computer Science
article_processing_charge: No
author:
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- first_name: Marco
full_name: Faella, Marco
last_name: Faella
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Mariëlle
full_name: Stoelinga, Mariëlle
last_name: Stoelinga
citation:
ama: 'De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Model checking
discounted temporal properties. In: Vol 2988. Springer Nature; 2004:77-92. doi:10.1007/978-3-540-24730-2_6'
apa: 'De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., & Stoelinga,
M. (2004). Model checking discounted temporal properties (Vol. 2988, pp. 77–92).
Presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, Barcelona, Spain: Springer Nature. https://doi.org/10.1007/978-3-540-24730-2_6'
chicago: De Alfaro, Luca, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and
Mariëlle Stoelinga. “Model Checking Discounted Temporal Properties,” 2988:77–92.
Springer Nature, 2004. https://doi.org/10.1007/978-3-540-24730-2_6.
ieee: 'L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga,
“Model checking discounted temporal properties,” presented at the TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain,
2004, vol. 2988, pp. 77–92.'
ista: 'De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2004. Model
checking discounted temporal properties. TACAS: Tools and Algorithms for the Construction
and Analysis of Systems, Lecture Notes in Computer Science, vol. 2988, 77–92.'
mla: De Alfaro, Luca, et al. Model Checking Discounted Temporal Properties.
Vol. 2988, Springer Nature, 2004, pp. 77–92, doi:10.1007/978-3-540-24730-2_6.
short: L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, in:,
Springer Nature, 2004, pp. 77–92.
conference:
end_date: 2004-04-02
location: Barcelona, Spain
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2004-03-29
date_created: 2018-12-11T12:09:50Z
date_published: 2004-04-03T00:00:00Z
date_updated: 2026-05-29T07:32:26Z
day: '03'
doi: 10.1007/978-3-540-24730-2_6
extern: '1'
intvolume: ' 2988'
language:
- iso: eng
month: '04'
oa_version: None
page: 77 - 92
publication_identifier:
eisbn:
- '9783540247302'
isbn:
- '9783540212997'
publication_status: published
publisher: Springer Nature
publist_id: '79'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model checking discounted temporal properties
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 2988
year: '2004'
...
---
_id: '6155'
abstract:
- lang: eng
text: 'The genome of the nematode Caenorhabditis elegans encodes seven soluble guanylate
cyclases (sGCs) [1]. In mammals, sGCs function as α/β heterodimers activated by
gaseous ligands binding to a haem prosthetic group 2, 3. The principal activator
is nitric oxide, which acts through sGCs to regulate diverse cellular events.
In C. elegans the function of sGCs is mysterious: the worm genome does not appear
to encode nitric oxide synthase, and all C. elegans sGC subunits are more closely
related to mammalian β than α subunits [1]. Here, we show that two of the seven
C. elegans sGCs, GCY-35 and GCY-36, promote aggregation behavior. gcy-35 and gcy-36
are expressed in a small number of neurons. These include the body cavity neurons
AQR, PQR, and URX, which are directly exposed to the blood equivalent of C. elegans
and regulate aggregation behavior [4]. We show that GCY-35 and GCY-36 act as α-like
and β-like sGC subunits and that their function in the URX sensory neurons is
sufficient for strong nematode aggregation. Neither GCY-35 nor GCY-36 is absolutely
required for C. elegans to aggregate. Instead, these molecules may transduce one
of several pathways that induce C. elegans to aggregate or may modulate aggregation
by responding to cues in C. elegans body fluid.'
author:
- first_name: Benny H.H
full_name: Cheung, Benny H.H
last_name: Cheung
- first_name: Fausto
full_name: Arellano-Carbajal, Fausto
last_name: Arellano-Carbajal
- first_name: Irene
full_name: Rybicki, Irene
last_name: Rybicki
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
citation:
ama: Cheung BH., Arellano-Carbajal F, Rybicki I, de Bono M. Soluble guanylate cyclases
act in neurons exposed to the body fluid to promote C. elegans aggregation behavior.
Current Biology. 2004;14(12):1105-1111. doi:10.1016/j.cub.2004.06.027
apa: Cheung, B. H. ., Arellano-Carbajal, F., Rybicki, I., & de Bono, M. (2004).
Soluble guanylate cyclases act in neurons exposed to the body fluid to promote
C. elegans aggregation behavior. Current Biology. Elsevier. https://doi.org/10.1016/j.cub.2004.06.027
chicago: Cheung, Benny H.H, Fausto Arellano-Carbajal, Irene Rybicki, and Mario de
Bono. “Soluble Guanylate Cyclases Act in Neurons Exposed to the Body Fluid to
Promote C. Elegans Aggregation Behavior.” Current Biology. Elsevier, 2004.
https://doi.org/10.1016/j.cub.2004.06.027.
ieee: B. H. . Cheung, F. Arellano-Carbajal, I. Rybicki, and M. de Bono, “Soluble
guanylate cyclases act in neurons exposed to the body fluid to promote C. elegans
aggregation behavior,” Current Biology, vol. 14, no. 12. Elsevier, pp.
1105–1111, 2004.
ista: Cheung BH., Arellano-Carbajal F, Rybicki I, de Bono M. 2004. Soluble guanylate
cyclases act in neurons exposed to the body fluid to promote C. elegans aggregation
behavior. Current Biology. 14(12), 1105–1111.
mla: Cheung, Benny H. .., et al. “Soluble Guanylate Cyclases Act in Neurons Exposed
to the Body Fluid to Promote C. Elegans Aggregation Behavior.” Current Biology,
vol. 14, no. 12, Elsevier, 2004, pp. 1105–11, doi:10.1016/j.cub.2004.06.027.
short: B.H.. Cheung, F. Arellano-Carbajal, I. Rybicki, M. de Bono, Current Biology
14 (2004) 1105–1111.
date_created: 2019-03-21T09:42:01Z
date_published: 2004-06-22T00:00:00Z
date_updated: 2021-01-12T08:06:25Z
day: '22'
doi: 10.1016/j.cub.2004.06.027
extern: '1'
external_id:
pmid:
- '15203005'
intvolume: ' 14'
issue: '12'
language:
- iso: eng
month: '06'
oa_version: None
page: 1105-1111
pmid: 1
publication: Current Biology
publication_identifier:
issn:
- 0960-9822
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Soluble guanylate cyclases act in neurons exposed to the body fluid to promote
C. elegans aggregation behavior
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 14
year: '2004'
...
---
_id: '7706'
abstract:
- lang: eng
text: 'The Sir2 deacetylase modulates organismal life-span in various species. However,
the molecular mechanisms by which Sir2 increases longevity are largely unknown.
We show that in mammalian cells, the Sir2 homolog SIRT1 appears to control the
cellular response to stress by regulating the FOXO family of Forkhead transcription
factors, a family of proteins that function as sensors of the insulin signaling
pathway and as regulators of organismal longevity. SIRT1 and the FOXO transcription
factor FOXO3 formed a complex in cells in response to oxidative stress, and SIRT1
deacetylated FOXO3 in vitro and within cells. SIRT1 had a dual effect on FOXO3
function: SIRT1 increased FOXO3''s ability to induce cell cycle arrest and resistance
to oxidative stress but inhibited FOXO3''s ability to induce cell death. Thus,
one way in which members of the Sir2 family of proteins may increase organismal
longevity is by tipping FOXO-dependent responses away from apoptosis and toward
stress resistance.'
article_processing_charge: No
article_type: original
author:
- first_name: Anne
full_name: Brunet, Anne
last_name: Brunet
- first_name: Lora Beatrice Jaeger
full_name: Sweeney, Lora Beatrice Jaeger
id: 56BE8254-C4F0-11E9-8E45-0B23E6697425
last_name: Sweeney
orcid: 0000-0001-9242-5601
- first_name: 'J Fitzhugh '
full_name: 'Sturgill, J Fitzhugh '
last_name: Sturgill
- first_name: Katrin
full_name: Chua, Katrin
last_name: Chua
- first_name: Paul
full_name: Greer, Paul
last_name: Greer
- first_name: Yingxi
full_name: Lin, Yingxi
last_name: Lin
- first_name: Hien
full_name: Tran, Hien
last_name: Tran
- first_name: Sarah
full_name: Ross, Sarah
last_name: Ross
- first_name: Raul
full_name: Mostoslavsky, Raul
last_name: Mostoslavsky
- first_name: Haim
full_name: Cohen, Haim
last_name: Cohen
- first_name: Linda
full_name: Hu, Linda
last_name: Hu
- first_name: Hwei-Ling
full_name: Chen, Hwei-Ling
last_name: Chen
- first_name: Mark
full_name: Jedrychowski, Mark
last_name: Jedrychowski
- first_name: Steven
full_name: Gygi, Steven
last_name: Gygi
- first_name: David
full_name: Sinclair, David
last_name: Sinclair
- first_name: Frederick
full_name: Alt, Frederick
last_name: Alt
- first_name: Michael
full_name: Greenberg, Michael
last_name: Greenberg
citation:
ama: Brunet A, Sweeney LB, Sturgill JF, et al. Stress-dependent regulation of FOXO
transcription factors by the SIRT1 deacetylase. Science. 2004;303(5666):2011-2015.
doi:10.1126/science.1094637
apa: Brunet, A., Sweeney, L. B., Sturgill, J. F., Chua, K., Greer, P., Lin, Y.,
… Greenberg, M. (2004). Stress-dependent regulation of FOXO transcription factors
by the SIRT1 deacetylase. Science. American Association for the Advancement
of Science. https://doi.org/10.1126/science.1094637
chicago: Brunet, Anne, Lora B. Sweeney, J Fitzhugh Sturgill, Katrin Chua, Paul
Greer, Yingxi Lin, Hien Tran, et al. “Stress-Dependent Regulation of FOXO Transcription
Factors by the SIRT1 Deacetylase.” Science. American Association for the
Advancement of Science, 2004. https://doi.org/10.1126/science.1094637.
ieee: A. Brunet et al., “Stress-dependent regulation of FOXO transcription
factors by the SIRT1 deacetylase,” Science, vol. 303, no. 5666. American
Association for the Advancement of Science, pp. 2011–2015, 2004.
ista: Brunet A, Sweeney LB, Sturgill JF, Chua K, Greer P, Lin Y, Tran H, Ross S,
Mostoslavsky R, Cohen H, Hu L, Chen H-L, Jedrychowski M, Gygi S, Sinclair D, Alt
F, Greenberg M. 2004. Stress-dependent regulation of FOXO transcription factors
by the SIRT1 deacetylase. Science. 303(5666), 2011–2015.
mla: Brunet, Anne, et al. “Stress-Dependent Regulation of FOXO Transcription Factors
by the SIRT1 Deacetylase.” Science, vol. 303, no. 5666, American Association
for the Advancement of Science, 2004, pp. 2011–15, doi:10.1126/science.1094637.
short: A. Brunet, L.B. Sweeney, J.F. Sturgill, K. Chua, P. Greer, Y. Lin, H. Tran,
S. Ross, R. Mostoslavsky, H. Cohen, L. Hu, H.-L. Chen, M. Jedrychowski, S. Gygi,
D. Sinclair, F. Alt, M. Greenberg, Science 303 (2004) 2011–2015.
date_created: 2020-04-30T10:37:41Z
date_published: 2004-03-26T00:00:00Z
date_updated: 2024-01-31T10:14:17Z
day: '26'
doi: 10.1126/science.1094637
extern: '1'
intvolume: ' 303'
issue: '5666'
language:
- iso: eng
month: '03'
oa_version: None
page: 2011-2015
publication: Science
publication_identifier:
issn:
- 0036-8075
- 1095-9203
publication_status: published
publisher: American Association for the Advancement of Science
quality_controlled: '1'
status: public
title: Stress-dependent regulation of FOXO transcription factors by the SIRT1 deacetylase
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 303
year: '2004'
...
---
_id: '8517'
abstract:
- lang: eng
text: We consider the evolution of a connected set on the plane carried by a space
periodic incompressible stochastic flow. While for almost every realization of
the stochastic flow at time t most of the particles are at a distance of order
equation image away from the origin, there is a measure zero set of points that
escape to infinity at the linear rate. We study the set of points visited by the
original set by time t and show that such a set, when scaled down by the factor
of t, has a limiting nonrandom shape.
article_processing_charge: No
article_type: original
author:
- first_name: Dmitry
full_name: Dolgopyat, Dmitry
last_name: Dolgopyat
- first_name: Vadim
full_name: Kaloshin, Vadim
id: FE553552-CDE8-11E9-B324-C0EBE5697425
last_name: Kaloshin
orcid: 0000-0002-6051-2628
- first_name: Leonid
full_name: Koralov, Leonid
last_name: Koralov
citation:
ama: Dolgopyat D, Kaloshin V, Koralov L. A limit shape theorem for periodic stochastic
dispersion. Communications on Pure and Applied Mathematics. 2004;57(9):1127-1158.
doi:10.1002/cpa.20032
apa: Dolgopyat, D., Kaloshin, V., & Koralov, L. (2004). A limit shape theorem
for periodic stochastic dispersion. Communications on Pure and Applied Mathematics.
Wiley. https://doi.org/10.1002/cpa.20032
chicago: Dolgopyat, Dmitry, Vadim Kaloshin, and Leonid Koralov. “A Limit Shape Theorem
for Periodic Stochastic Dispersion.” Communications on Pure and Applied Mathematics.
Wiley, 2004. https://doi.org/10.1002/cpa.20032.
ieee: D. Dolgopyat, V. Kaloshin, and L. Koralov, “A limit shape theorem for periodic
stochastic dispersion,” Communications on Pure and Applied Mathematics,
vol. 57, no. 9. Wiley, pp. 1127–1158, 2004.
ista: Dolgopyat D, Kaloshin V, Koralov L. 2004. A limit shape theorem for periodic
stochastic dispersion. Communications on Pure and Applied Mathematics. 57(9),
1127–1158.
mla: Dolgopyat, Dmitry, et al. “A Limit Shape Theorem for Periodic Stochastic Dispersion.”
Communications on Pure and Applied Mathematics, vol. 57, no. 9, Wiley,
2004, pp. 1127–58, doi:10.1002/cpa.20032.
short: D. Dolgopyat, V. Kaloshin, L. Koralov, Communications on Pure and Applied
Mathematics 57 (2004) 1127–1158.
date_created: 2020-09-18T10:49:12Z
date_published: 2004-09-01T00:00:00Z
date_updated: 2021-01-12T08:19:50Z
day: '01'
doi: 10.1002/cpa.20032
extern: '1'
intvolume: ' 57'
issue: '9'
keyword:
- Applied Mathematics
- General Mathematics
language:
- iso: eng
month: '09'
oa_version: None
page: 1127-1158
publication: Communications on Pure and Applied Mathematics
publication_identifier:
issn:
- 0010-3640
- 1097-0312
publication_status: published
publisher: Wiley
quality_controlled: '1'
status: public
title: A limit shape theorem for periodic stochastic dispersion
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 57
year: '2004'
...
---
_id: '8518'
article_processing_charge: No
article_type: original
author:
- first_name: Leonid
full_name: Koralov, Leonid
last_name: Koralov
- first_name: Vadim
full_name: Kaloshin, Vadim
id: FE553552-CDE8-11E9-B324-C0EBE5697425
last_name: Kaloshin
orcid: 0000-0002-6051-2628
- first_name: Dmitry
full_name: Dolgopyat, Dmitry
last_name: Dolgopyat
citation:
ama: Koralov L, Kaloshin V, Dolgopyat D. Sample path properties of the stochastic
flows. The Annals of Probability. 2004;32(1A):1-27. doi:10.1214/aop/1078415827
apa: Koralov, L., Kaloshin, V., & Dolgopyat, D. (2004). Sample path properties
of the stochastic flows. The Annals of Probability. Institute of Mathematical
Statistics. https://doi.org/10.1214/aop/1078415827
chicago: Koralov, Leonid, Vadim Kaloshin, and Dmitry Dolgopyat. “Sample Path Properties
of the Stochastic Flows.” The Annals of Probability. Institute of Mathematical
Statistics, 2004. https://doi.org/10.1214/aop/1078415827.
ieee: L. Koralov, V. Kaloshin, and D. Dolgopyat, “Sample path properties of the
stochastic flows,” The Annals of Probability, vol. 32, no. 1A. Institute
of Mathematical Statistics, pp. 1–27, 2004.
ista: Koralov L, Kaloshin V, Dolgopyat D. 2004. Sample path properties of the stochastic
flows. The Annals of Probability. 32(1A), 1–27.
mla: Koralov, Leonid, et al. “Sample Path Properties of the Stochastic Flows.” The
Annals of Probability, vol. 32, no. 1A, Institute of Mathematical Statistics,
2004, pp. 1–27, doi:10.1214/aop/1078415827.
short: L. Koralov, V. Kaloshin, D. Dolgopyat, The Annals of Probability 32 (2004)
1–27.
date_created: 2020-09-18T10:49:19Z
date_published: 2004-03-04T00:00:00Z
date_updated: 2021-01-12T08:19:50Z
day: '04'
doi: 10.1214/aop/1078415827
extern: '1'
intvolume: ' 32'
issue: 1A
language:
- iso: eng
month: '03'
oa_version: None
page: 1-27
publication: The Annals of Probability
publication_identifier:
issn:
- 0091-1798
publication_status: published
publisher: Institute of Mathematical Statistics
quality_controlled: '1'
status: public
title: Sample path properties of the stochastic flows
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 32
year: '2004'
...