---
_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.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
citation:
ama: 'Henzinger TA, Kirsch C. A typed assembly language for real-time programs.
In: ACM; 2004:104-113. doi:10.1145/1017753.1017774'
apa: 'Henzinger, T. A., & Kirsch, C. (2004). A typed assembly language for real-time
programs (pp. 104–113). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1017753.1017774'
chicago: Henzinger, Thomas A, and Christoph Kirsch. “A Typed Assembly Language for
Real-Time Programs,” 104–13. ACM, 2004. https://doi.org/10.1145/1017753.1017774.
ieee: 'T. A. Henzinger and C. Kirsch, “A typed assembly language for real-time programs,”
presented at the EMSOFT: Embedded Software , 2004, pp. 104–113.'
ista: 'Henzinger TA, Kirsch C. 2004. A typed assembly language for real-time programs.
EMSOFT: Embedded Software , 104–113.'
mla: Henzinger, Thomas A., and Christoph Kirsch. A Typed Assembly Language for
Real-Time Programs. ACM, 2004, pp. 104–13, doi:10.1145/1017753.1017774.
short: T.A. Henzinger, C. Kirsch, in:, ACM, 2004, pp. 104–113.
conference:
name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:08:53Z
date_published: 2004-09-01T00:00:00Z
date_updated: 2021-01-12T07:57:01Z
day: '01'
doi: 10.1145/1017753.1017774
extern: 1
month: '09'
page: 104 - 113
publication_status: published
publisher: ACM
publist_id: '285'
quality_controlled: 0
status: public
title: A typed assembly language for real-time programs
type: conference
year: '2004'
...
---
_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.'
author:
- first_name: Thomas A
full_name: Thomas Henzinger
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 S
last_name: Majumdar
- first_name: Kenneth
full_name: McMillan, Kenneth L
last_name: Mcmillan
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Mcmillan K. Abstractions from proofs. In:
ACM; 2004:232-244. doi:10.1145/964001.964021'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Mcmillan, K. (2004). Abstractions
from proofs (pp. 232–244). Presented at the POPL: Principles of Programming Languages,
ACM. https://doi.org/10.1145/964001.964021'
chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Kenneth Mcmillan.
“Abstractions from Proofs,” 232–44. ACM, 2004. https://doi.org/10.1145/964001.964021.
ieee: 'T. A. Henzinger, R. Jhala, R. Majumdar, and K. Mcmillan, “Abstractions from
proofs,” presented at the POPL: Principles of Programming Languages, 2004, pp.
232–244.'
ista: 'Henzinger TA, Jhala R, Majumdar R, Mcmillan K. 2004. Abstractions from proofs.
POPL: Principles of Programming Languages, 232–244.'
mla: Henzinger, Thomas A., et al. Abstractions from Proofs. ACM, 2004, pp.
232–44, doi:10.1145/964001.964021.
short: T.A. Henzinger, R. Jhala, R. Majumdar, K. Mcmillan, in:, ACM, 2004, pp. 232–244.
conference:
name: 'POPL: Principles of Programming Languages'
date_created: 2018-12-11T12:08:57Z
date_published: 2004-04-01T00:00:00Z
date_updated: 2021-01-12T07:57:06Z
day: '01'
doi: 10.1145/964001.964021
extern: 1
month: '04'
page: 232 - 244
publication_status: published
publisher: ACM
publist_id: '270'
quality_controlled: 0
status: public
title: Abstractions from proofs
type: conference
year: '2004'
...
---
_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:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
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 S
last_name: Majumdar
- first_name: Marco
full_name: Sanvido, Marco A
last_name: Sanvido
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Sanvido M. Extreme model checking. In:
Verification: Theory and Practice. Vol 2772. Springer; 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).
Springer. 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.
Springer, 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, Springer, 2004, pp. 332–358.'
ista: 'Henzinger TA, Jhala R, Majumdar R, Sanvido M. 2004.Extreme model checking.
In: Verification: Theory and Practice. LNCS, vol. 2772, 332–358.'
mla: 'Henzinger, Thomas A., et al. “Extreme Model Checking.” Verification: Theory
and Practice, vol. 2772, Springer, 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, 2004, pp. 332–358.'
date_created: 2018-12-11T12:08:58Z
date_published: 2004-02-24T00:00:00Z
date_updated: 2021-01-12T07:57:08Z
day: '24'
doi: 10.1007/978-3-540-39910-0_16
extern: 1
intvolume: ' 2772'
month: '02'
page: 332 - 358
publication: 'Verification: Theory and Practice'
publication_status: published
publisher: Springer
publist_id: '269'
quality_controlled: 0
status: public
title: Extreme model checking
type: book_chapter
volume: 2772
year: '2004'
...
---
_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.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
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 S
last_name: Majumdar
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In:
ACM; 2004:1-13. doi:10.1145/996841.996844'
apa: 'Henzinger, T. A., Jhala, R., & Majumdar, R. (2004). Race checking by context
inference (pp. 1–13). Presented at the PLDI: Programming Languages Design and
Implementation, ACM. https://doi.org/10.1145/996841.996844'
chicago: Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Race Checking
by Context Inference,” 1–13. ACM, 2004. https://doi.org/10.1145/996841.996844.
ieee: 'T. A. Henzinger, R. Jhala, and R. Majumdar, “Race checking by context inference,”
presented at the PLDI: Programming Languages Design and Implementation, 2004,
pp. 1–13.'
ista: 'Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference.
PLDI: Programming Languages Design and Implementation, 1–13.'
mla: Henzinger, Thomas A., et al. Race Checking by Context Inference. ACM,
2004, pp. 1–13, doi:10.1145/996841.996844.
short: T.A. Henzinger, R. Jhala, R. Majumdar, in:, ACM, 2004, pp. 1–13.
conference:
name: 'PLDI: Programming Languages Design and Implementation'
date_created: 2018-12-11T12:08:57Z
date_published: 2004-06-01T00:00:00Z
date_updated: 2021-01-12T07:57:07Z
day: '01'
doi: 10.1145/996841.996844
extern: 1
month: '06'
page: 1 - 13
publication_status: published
publisher: ACM
publist_id: '271'
quality_controlled: 0
status: public
title: Race checking by context inference
type: conference
year: '2004'
...
---
_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:
- LNCS
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Marco
full_name: Sanvido, Marco A
last_name: Sanvido
citation:
ama: 'Ghosal A, Henzinger TA, Kirsch C, Sanvido M. Event-driven programming with
logical execution times. In: Vol 2993. Springer; 2004:167-170. 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 (Vol. 2993, pp. 167–170). Presented at
the HSCC: Hybrid Systems - Computation and Control, Springer. 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,” 2993:167–70. Springer,
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, 2004, vol. 2993, pp. 167–170.'
ista: 'Ghosal A, Henzinger TA, Kirsch C, Sanvido M. 2004. Event-driven programming
with logical execution times. HSCC: Hybrid Systems - Computation and Control,
LNCS, vol. 2993, 167–170.'
mla: Ghosal, Arkadeb, et al. Event-Driven Programming with Logical Execution
Times. Vol. 2993, Springer, 2004, pp. 167–70, doi:10.1007/978-3-540-24743-2_24.
short: A. Ghosal, T.A. Henzinger, C. Kirsch, M. Sanvido, in:, Springer, 2004, pp.
167–170.
conference:
name: 'HSCC: Hybrid Systems - Computation and Control'
date_created: 2018-12-11T12:09:18Z
date_published: 2004-03-12T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '12'
doi: 10.1007/978-3-540-24743-2_24
extern: 1
intvolume: ' 2993'
month: '03'
page: 167 - 170
publication_status: published
publisher: Springer
publist_id: '200'
quality_controlled: 0
status: public
title: Event-driven programming with logical execution times
type: conference
volume: 2993
year: '2004'
...
---
_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.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
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: Thomas Henzinger
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, 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, 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:
name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:27Z
date_published: 2004-09-30T00:00:00Z
date_updated: 2021-01-12T07:59:40Z
day: '30'
doi: 10.1109/QEST.2004.10051
extern: 1
month: '09'
page: 206 - 217
publication_status: published
publisher: IEEE
publist_id: '155'
quality_controlled: 0
status: public
title: Trading memory for randomness
type: conference
year: '2004'
...
---
_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.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
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: Thomas Henzinger
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: SIAM; 2004:121-130.'
apa: 'Chatterjee, K., Jurdziński, M., & Henzinger, T. A. (2004). Quantitative
stochastic parity games (pp. 121–130). Presented at the SODA: Symposium on Discrete
Algorithms, SIAM.'
chicago: Chatterjee, Krishnendu, Marcin Jurdziński, and Thomas A Henzinger. “Quantitative
Stochastic Parity Games,” 121–30. SIAM, 2004.
ieee: 'K. Chatterjee, M. Jurdziński, and T. A. Henzinger, “Quantitative stochastic
parity games,” presented at the SODA: Symposium on Discrete Algorithms, 2004,
pp. 121–130.'
ista: 'Chatterjee K, Jurdziński M, Henzinger TA. 2004. Quantitative stochastic parity
games. SODA: Symposium on Discrete Algorithms, 121–130.'
mla: Chatterjee, Krishnendu, et al. Quantitative Stochastic Parity Games.
SIAM, 2004, pp. 121–30.
short: K. Chatterjee, M. Jurdziński, T.A. Henzinger, in:, SIAM, 2004, pp. 121–130.
conference:
name: 'SODA: Symposium on Discrete Algorithms'
date_created: 2018-12-11T12:09:28Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:41Z
day: '01'
extern: 1
month: '01'
page: 121 - 130
publication_status: published
publisher: SIAM
publist_id: '153'
quality_controlled: 0
status: public
title: Quantitative stochastic parity games
type: conference
year: '2004'
...
---
_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.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
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 S
last_name: Majumdar
- first_name: Tian
full_name: Zhao, Tian
last_name: Zhao
- first_name: Thomas A
full_name: Thomas Henzinger
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-08-11T00:00:00Z
date_updated: 2021-01-12T07:59:40Z
day: '11'
doi: 10.1016/j.ic.2004.06.001
extern: 1
intvolume: ' 194'
issue: '2'
month: '08'
page: 144 - 174
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '156'
quality_controlled: 0
status: public
title: Stack size analysis for interrupt-driven programs
type: journal_article
volume: 194
year: '2004'
...
---
_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:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Adam
full_name: Chlipala, Adam J
last_name: Chlipala
- first_name: Thomas A
full_name: Thomas Henzinger
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 S
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, 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, 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, LNCS, 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:
name: 'SAS: Static Analysis Symposium'
date_created: 2018-12-11T12:09:34Z
date_published: 2004-08-17T00:00:00Z
date_updated: 2021-01-12T07:59:50Z
day: '17'
doi: 10.1007/978-3-540-27864-1_2
extern: 1
intvolume: ' 3148'
month: '08'
page: 2 - 18
publication_status: published
publisher: Springer
publist_id: '130'
quality_controlled: 0
status: public
title: The BLAST query language for software verification
type: conference
volume: 3148
year: '2004'
...
---
_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.
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
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 S
last_name: Majumdar
citation:
ama: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. An eclipse plug-in for model checking.
In: 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 (pp. 251–255). Presented at the IWPC: Program Comprehension,
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,” 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,” presented at the IWPC: Program Comprehension, 2004, pp. 251–255.'
ista: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. 2004. An eclipse plug-in for
model checking. IWPC: Program Comprehension, 251–255.'
mla: Beyer, Dirk, et al. An Eclipse Plug-in for Model Checking. IEEE, 2004,
pp. 251–55, doi:10.1109/WPC.2004.1311069
.
short: D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, IEEE, 2004, pp. 251–255.
conference:
name: 'IWPC: Program Comprehension'
date_created: 2018-12-11T12:09:34Z
date_published: 2004-07-12T00:00:00Z
date_updated: 2021-01-12T07:59:50Z
day: '12'
doi: '10.1109/WPC.2004.1311069 '
extern: 1
month: '07'
page: 251 - 255
publication_status: published
publisher: IEEE
publist_id: '129'
quality_controlled: 0
status: public
title: An eclipse plug-in for model checking
type: conference
year: '2004'
...
---
_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).
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Adam
full_name: Chlipala, Adam J
last_name: Chlipala
- first_name: Thomas A
full_name: Thomas Henzinger
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 S
last_name: Majumdar
citation:
ama: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. Generating tests from
counterexamples. In: 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 (pp. 326–335). Presented at the ICSE: Software
Engineering, 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,” 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,” presented at the ICSE: Software Engineering, 2004,
pp. 326–335.'
ista: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. Generating
tests from counterexamples. ICSE: Software Engineering, 326–335.'
mla: Beyer, Dirk, et al. Generating Tests from Counterexamples. IEEE, 2004,
pp. 326–35, doi:10.1109/ICSE.2004.1317455.
short: D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, IEEE,
2004, pp. 326–335.
conference:
name: 'ICSE: Software Engineering'
date_created: 2018-12-11T12:09:35Z
date_published: 2004-07-26T00:00:00Z
date_updated: 2021-01-12T07:59:52Z
day: '26'
doi: 10.1109/ICSE.2004.1317455
extern: 1
month: '07'
page: 326 - 335
publication_status: published
publisher: IEEE
publist_id: '128'
quality_controlled: 0
status: public
title: Generating tests from counterexamples
type: conference
year: '2004'
...
---
_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:
- LNCS
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: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar S
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; 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, Springer. 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, 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, 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, LNCS, vol. 2988, 77–92.'
mla: De Alfaro, Luca, et al. Model Checking Discounted Temporal Properties.
Vol. 2988, Springer, 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, 2004, pp. 77–92.
conference:
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:09:50Z
date_published: 2004-03-18T00:00:00Z
date_updated: 2021-01-12T08:00:38Z
day: '18'
doi: 10.1007/978-3-540-24730-2_6
extern: 1
intvolume: ' 2988'
month: '03'
page: 77 - 92
publication_status: published
publisher: Springer
publist_id: '79'
quality_controlled: 0
status: public
title: Model checking discounted temporal properties
type: conference
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: '7334'
abstract:
- lang: eng
text: 'Fundamental and phenomenological models for cells, stacks, and complete systems
of PEFC and SOFC are reviewed and their predictive power is assessed by comparing
model simulations against experiments. Computationally efficient models suited
for engineering design include the (1+1) dimensionality approach, which decouples
the membrane in-plane and through-plane processes, and the volume-averaged-method
(VAM) that considers only the lumped effect of pre-selected system components.
The former model was shown to capture the measured lateral current density inhomogeneities
in a PEFC and the latter was used for the optimization of commercial SOFC systems.
State Space Modeling (SSM) was used to identify the main reaction pathways in
SOFC and, in conjunction with the implementation of geometrically well-defined
electrodes, has opened a new direction for the understanding of electrochemical
reactions. Furthermore, SSM has advanced the understanding of the COpoisoning-induced
anode impedance in PEFC. Detailed numerical models such as the Lattice Boltzmann
(LB) method for transport in porous media and the full 3-D Computational Fluid
Dynamics (CFD) Navier-Stokes simulations are addressed. These models contain all
components of the relevant physics and they can improve the understanding of the
related phenomena, a necessary condition for the development of both appropriate
simplified models as well as reliable technologies. Within the LB framework, a
technique for the characterization and computer-reconstruction of the porous electrode
structure was developed using advanced pattern recognition algorithms. In CFD
modeling, 3-D simulations were used to investigate SOFC with internal methane
steam reforming and have exemplified the significance of porous and novel fractal
channel distributors for the fuel and oxidant delivery, as well as for the cooling
of PEFC. As importantly, the novel concept has been put forth of functionally
designed, fractal-shaped fuel cells, showing promise of significant performance
improvements over the conventional rectangular shaped units. Thermo-economic modeling
for the optimization of PEFC is finally addressed. '
article_processing_charge: No
article_type: original
author:
- first_name: John
full_name: Mantzaras, John
last_name: Mantzaras
- first_name: Stefan Alexander
full_name: Freunberger, Stefan Alexander
id: A8CA28E6-CE23-11E9-AD2D-EC27E6697425
last_name: Freunberger
orcid: 0000-0003-2902-5319
- first_name: Felix N.
full_name: Büchi, Felix N.
last_name: Büchi
- first_name: Markus
full_name: Roos, Markus
last_name: Roos
- first_name: Wilhelm
full_name: Brandstätter, Wilhelm
last_name: Brandstätter
- first_name: Michel
full_name: Prestat, Michel
last_name: Prestat
- first_name: Ludwig J.
full_name: Gauckler, Ludwig J.
last_name: Gauckler
- first_name: Bernhard
full_name: Andreaus, Bernhard
last_name: Andreaus
- first_name: Faegheh
full_name: Hajbolouri, Faegheh
last_name: Hajbolouri
- first_name: Stephan M.
full_name: Senn, Stephan M.
last_name: Senn
- first_name: Dimos
full_name: Poulikakos, Dimos
last_name: Poulikakos
- first_name: Andreas K.
full_name: Chaniotis, Andreas K.
last_name: Chaniotis
- first_name: Diego
full_name: Larrain, Diego
last_name: Larrain
- first_name: Nordahl
full_name: Autissier, Nordahl
last_name: Autissier
- first_name: François
full_name: Maréchal, François
last_name: Maréchal
citation:
ama: Mantzaras J, Freunberger SA, Büchi FN, et al. Fuel cell modeling and simulations.
CHIMIA International Journal for Chemistry. 2004;58(12):857-868. doi:10.2533/000942904777677029
apa: Mantzaras, J., Freunberger, S. A., Büchi, F. N., Roos, M., Brandstätter, W.,
Prestat, M., … Maréchal, F. (2004). Fuel cell modeling and simulations. CHIMIA
International Journal for Chemistry. Swiss Chemical Society. https://doi.org/10.2533/000942904777677029
chicago: Mantzaras, John, Stefan Alexander Freunberger, Felix N. Büchi, Markus Roos,
Wilhelm Brandstätter, Michel Prestat, Ludwig J. Gauckler, et al. “Fuel Cell Modeling
and Simulations.” CHIMIA International Journal for Chemistry. Swiss Chemical
Society, 2004. https://doi.org/10.2533/000942904777677029.
ieee: J. Mantzaras et al., “Fuel cell modeling and simulations,” CHIMIA
International Journal for Chemistry, vol. 58, no. 12. Swiss Chemical Society,
pp. 857–868, 2004.
ista: Mantzaras J, Freunberger SA, Büchi FN, Roos M, Brandstätter W, Prestat M,
Gauckler LJ, Andreaus B, Hajbolouri F, Senn SM, Poulikakos D, Chaniotis AK, Larrain
D, Autissier N, Maréchal F. 2004. Fuel cell modeling and simulations. CHIMIA International
Journal for Chemistry. 58(12), 857–868.
mla: Mantzaras, John, et al. “Fuel Cell Modeling and Simulations.” CHIMIA International
Journal for Chemistry, vol. 58, no. 12, Swiss Chemical Society, 2004, pp.
857–68, doi:10.2533/000942904777677029.
short: J. Mantzaras, S.A. Freunberger, F.N. Büchi, M. Roos, W. Brandstätter, M.
Prestat, L.J. Gauckler, B. Andreaus, F. Hajbolouri, S.M. Senn, D. Poulikakos,
A.K. Chaniotis, D. Larrain, N. Autissier, F. Maréchal, CHIMIA International Journal
for Chemistry 58 (2004) 857–868.
date_created: 2020-01-15T12:24:23Z
date_published: 2004-12-01T00:00:00Z
date_updated: 2021-01-12T08:13:09Z
day: '01'
doi: 10.2533/000942904777677029
extern: '1'
intvolume: ' 58'
issue: '12'
language:
- iso: eng
month: '12'
oa_version: None
page: 857-868
publication: CHIMIA International Journal for Chemistry
publication_identifier:
issn:
- 0009-4293
publication_status: published
publisher: Swiss Chemical Society
quality_controlled: '1'
status: public
title: Fuel cell modeling and simulations
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 58
year: '2004'
...
---
_id: '7333'
abstract:
- lang: eng
text: The analysis of the complete H2/air polymer electrolyte fuel cell system shows
that process air humidification is one of the biggest obstacles for a high performance
portable system in the kW range. Therefore, a new concept, with passive process
air humidification integrated into the stack, has been developed. Humidification
in each cell makes the process independent from the number of cells and the operation
mode, thus making the concept fully scalable. Without external humidification
the system is simpler, smaller, and cheaper. The humidification of the process
air is achieved by transfer of product water from the exhaust air, through part
of the membrane, to the dry intake air. Tests have shown that cells using the
concept of internal humidification and operated with dry air at 70 ° have almost
the same performance as when operated with external humidification. A 42‐cell
stack with this internal humidification concept was built and integrated into
a portable 1 kW power generator system.
article_processing_charge: No
article_type: original
author:
- first_name: M.
full_name: Santis, M.
last_name: Santis
- first_name: D.
full_name: Schmid, D.
last_name: Schmid
- first_name: M.
full_name: Ruge, M.
last_name: Ruge
- first_name: Stefan Alexander
full_name: Freunberger, Stefan Alexander
id: A8CA28E6-CE23-11E9-AD2D-EC27E6697425
last_name: Freunberger
orcid: 0000-0003-2902-5319
- first_name: F.N.
full_name: Büchi, F.N.
last_name: Büchi
citation:
ama: Santis M, Schmid D, Ruge M, Freunberger SA, Büchi FN. Modular stack-internal
air humidification concept-verification in a 1 kW stack. Fuel Cells. 2004;4(3):214-218.
doi:10.1002/fuce.200400028
apa: Santis, M., Schmid, D., Ruge, M., Freunberger, S. A., & Büchi, F. N. (2004).
Modular stack-internal air humidification concept-verification in a 1 kW stack.
Fuel Cells. Wiley. https://doi.org/10.1002/fuce.200400028
chicago: Santis, M., D. Schmid, M. Ruge, Stefan Alexander Freunberger, and F.N.
Büchi. “Modular Stack-Internal Air Humidification Concept-Verification in a 1 KW
Stack.” Fuel Cells. Wiley, 2004. https://doi.org/10.1002/fuce.200400028.
ieee: M. Santis, D. Schmid, M. Ruge, S. A. Freunberger, and F. N. Büchi, “Modular
stack-internal air humidification concept-verification in a 1 kW stack,” Fuel
Cells, vol. 4, no. 3. Wiley, pp. 214–218, 2004.
ista: Santis M, Schmid D, Ruge M, Freunberger SA, Büchi FN. 2004. Modular stack-internal
air humidification concept-verification in a 1 kW stack. Fuel Cells. 4(3), 214–218.
mla: Santis, M., et al. “Modular Stack-Internal Air Humidification Concept-Verification
in a 1 KW Stack.” Fuel Cells, vol. 4, no. 3, Wiley, 2004, pp. 214–18, doi:10.1002/fuce.200400028.
short: M. Santis, D. Schmid, M. Ruge, S.A. Freunberger, F.N. Büchi, Fuel Cells 4
(2004) 214–218.
date_created: 2020-01-15T12:24:14Z
date_published: 2004-08-01T00:00:00Z
date_updated: 2021-01-12T08:13:08Z
day: '01'
doi: 10.1002/fuce.200400028
extern: '1'
intvolume: ' 4'
issue: '3'
language:
- iso: eng
month: '08'
oa_version: None
page: 214-218
publication: Fuel Cells
publication_identifier:
issn:
- 1615-6846
- 1615-6854
publication_status: published
publisher: Wiley
quality_controlled: '1'
status: public
title: Modular stack-internal air humidification concept-verification in a 1 kW stack
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4
year: '2004'
...
---
_id: '864'
abstract:
- lang: eng
text: 'We present a method for prediction of functional sites in a set of aligned
protein sequences. The method selects sites which are both well conserved and
clustered together in space, as inferred from the 3D structures of proteins included
in the alignment. We tested the method using 86 alignments from the NCBI CDD database,
where the sites of experimentally determined ligand and/or macromolecular interactions
are annotated. In agreement with earlier investigations, we found that functional
site predictions are most successful when overall background sequence conservation
is low, such that sites under evolutionary constraint become apparent. In addition,
we found that averaging of conservation values across spatially clustered sites
improves predictions under certain conditions: that is, when overall conservation
is relatively high and when the site in question involves a large macromolecular
binding interface. Under these conditions it is better to look for clusters of
conserved sites than to look for particular conserved sites.'
acknowledgement: We thank John Spouge, Ben Shoemaker, and Michael Galperin forhelpful
suggestions, and the NIH Intramural Research Program forsupport.
author:
- first_name: Anna
full_name: Panchenko, Anna R
last_name: Panchenko
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Stephen
full_name: Bryant, Stephen H
last_name: Bryant
citation:
ama: Panchenko A, Kondrashov F, Bryant S. Prediction of functional sites by analysis
of sequence and structure conservation. Protein Science. 2004;13(4):884-892.
doi:10.1110/ps.03465504
apa: Panchenko, A., Kondrashov, F., & Bryant, S. (2004). Prediction of functional
sites by analysis of sequence and structure conservation. Protein Science.
Wiley-Blackwell. https://doi.org/10.1110/ps.03465504
chicago: Panchenko, Anna, Fyodor Kondrashov, and Stephen Bryant. “Prediction of
Functional Sites by Analysis of Sequence and Structure Conservation.” Protein
Science. Wiley-Blackwell, 2004. https://doi.org/10.1110/ps.03465504.
ieee: A. Panchenko, F. Kondrashov, and S. Bryant, “Prediction of functional sites
by analysis of sequence and structure conservation,” Protein Science, vol.
13, no. 4. Wiley-Blackwell, pp. 884–892, 2004.
ista: Panchenko A, Kondrashov F, Bryant S. 2004. Prediction of functional sites
by analysis of sequence and structure conservation. Protein Science. 13(4), 884–892.
mla: Panchenko, Anna, et al. “Prediction of Functional Sites by Analysis of Sequence
and Structure Conservation.” Protein Science, vol. 13, no. 4, Wiley-Blackwell,
2004, pp. 884–92, doi:10.1110/ps.03465504.
short: A. Panchenko, F. Kondrashov, S. Bryant, Protein Science 13 (2004) 884–892.
date_created: 2018-12-11T11:48:55Z
date_published: 2004-04-01T00:00:00Z
date_updated: 2021-01-12T08:20:22Z
day: '01'
doi: 10.1110/ps.03465504
extern: 1
intvolume: ' 13'
issue: '4'
month: '04'
page: 884 - 892
publication: Protein Science
publication_status: published
publisher: Wiley-Blackwell
publist_id: '6786'
quality_controlled: 0
status: public
title: Prediction of functional sites by analysis of sequence and structure conservation
type: journal_article
volume: 13
year: '2004'
...
---
_id: '870'
abstract:
- lang: eng
text: Only a fraction of eukaryotic genes affect the phenotype drastically. We compared
18 parameters in 1273 human morbid genes, known to cause diseases, and in the
remaining 16 580 unambiguous human genes. Morbid genes evolve more slowly, have
wider phylogenetic distributions, are more similar to essential genes of Drosophila
melanogaster, code for longer proteins containing more alanine and glycine and
less histidine, lysine and methionine, possess larger numbers of longer introns
with more accurate splicing signals and have higher and broader expressions. These
differences make it possible to classify as non-morbid 34% of human genes with
unknown morbidity, when only 5% of known morbid genes are incorrectly classified
as non-morbid. This classification can help to identify disease-causing genes
among multiple candidates.
author:
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Aleksey
full_name: Ogurtsov, Aleksey Yu
last_name: Ogurtsov
- first_name: Alexey
full_name: Kondrashov, Alexey S
last_name: Kondrashov
citation:
ama: Kondrashov F, Ogurtsov A, Kondrashov A. Bioinformatical assay of human gene
morbidity. Nucleic Acids Research. 2004;32(5):1731-1737. doi:10.1093/nar/gkh330
apa: Kondrashov, F., Ogurtsov, A., & Kondrashov, A. (2004). Bioinformatical
assay of human gene morbidity. Nucleic Acids Research. Oxford University
Press. https://doi.org/10.1093/nar/gkh330
chicago: Kondrashov, Fyodor, Aleksey Ogurtsov, and Alexey Kondrashov. “Bioinformatical
Assay of Human Gene Morbidity.” Nucleic Acids Research. Oxford University
Press, 2004. https://doi.org/10.1093/nar/gkh330.
ieee: F. Kondrashov, A. Ogurtsov, and A. Kondrashov, “Bioinformatical assay of human
gene morbidity,” Nucleic Acids Research, vol. 32, no. 5. Oxford University
Press, pp. 1731–1737, 2004.
ista: Kondrashov F, Ogurtsov A, Kondrashov A. 2004. Bioinformatical assay of human
gene morbidity. Nucleic Acids Research. 32(5), 1731–1737.
mla: Kondrashov, Fyodor, et al. “Bioinformatical Assay of Human Gene Morbidity.”
Nucleic Acids Research, vol. 32, no. 5, Oxford University Press, 2004,
pp. 1731–37, doi:10.1093/nar/gkh330.
short: F. Kondrashov, A. Ogurtsov, A. Kondrashov, Nucleic Acids Research 32 (2004)
1731–1737.
date_created: 2018-12-11T11:48:56Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T08:20:37Z
day: '01'
doi: 10.1093/nar/gkh330
extern: 1
intvolume: ' 32'
issue: '5'
month: '01'
page: 1731 - 1737
publication: Nucleic Acids Research
publication_status: published
publisher: Oxford University Press
publist_id: '6780'
quality_controlled: 0
status: public
title: Bioinformatical assay of human gene morbidity
type: journal_article
volume: 32
year: '2004'
...
---
_id: '875'
abstract:
- lang: eng
text: The dominance of wild-type alleles and the concomitant recessivity of deleterious
mutant alleles might have evolved by natural selection or could be a by-product
of the molecular and physiological mechanisms of gene action. We compared the
properties of human haplosufficient genes, whose wild-type alleles are dominant
over loss-of-function alleles, with haploinsufficient (recessive wild-type) genes,
which produce an abnormal phenotype when heterozygous for a loss-of-function allele.
The fraction of haplosufficient genes is the highest among the genes that encode
enzymes, which is best compatible with the physiological theory. Haploinsufficient
genes, on average, have more paralogs than haplosufficient genes, supporting the
idea that gene dosage could be important for the initial fixation of duplications.
Thus, haplo(in)sufficiency of a gene and its propensity for duplication might
have a common evolutionary basis.
author:
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Eugene
full_name: Koonin, Eugene V
last_name: Koonin
citation:
ama: Kondrashov F, Koonin E. A common framework for understanding the origin of
genetic dominance and evolutionary fates of gene duplications. Trends in Genetics.
2004;20(7):287-291. doi:10.1016/j.tig.2004.05.001
apa: Kondrashov, F., & Koonin, E. (2004). A common framework for understanding
the origin of genetic dominance and evolutionary fates of gene duplications. Trends
in Genetics. Elsevier. https://doi.org/10.1016/j.tig.2004.05.001
chicago: Kondrashov, Fyodor, and Eugene Koonin. “A Common Framework for Understanding
the Origin of Genetic Dominance and Evolutionary Fates of Gene Duplications.”
Trends in Genetics. Elsevier, 2004. https://doi.org/10.1016/j.tig.2004.05.001.
ieee: F. Kondrashov and E. Koonin, “A common framework for understanding the origin
of genetic dominance and evolutionary fates of gene duplications,” Trends in
Genetics, vol. 20, no. 7. Elsevier, pp. 287–291, 2004.
ista: Kondrashov F, Koonin E. 2004. A common framework for understanding the origin
of genetic dominance and evolutionary fates of gene duplications. Trends in Genetics.
20(7), 287–291.
mla: Kondrashov, Fyodor, and Eugene Koonin. “A Common Framework for Understanding
the Origin of Genetic Dominance and Evolutionary Fates of Gene Duplications.”
Trends in Genetics, vol. 20, no. 7, Elsevier, 2004, pp. 287–91, doi:10.1016/j.tig.2004.05.001.
short: F. Kondrashov, E. Koonin, Trends in Genetics 20 (2004) 287–291.
date_created: 2018-12-11T11:48:58Z
date_published: 2004-07-01T00:00:00Z
date_updated: 2021-01-12T08:20:54Z
day: '01'
doi: 10.1016/j.tig.2004.05.001
extern: 1
intvolume: ' 20'
issue: '7'
month: '07'
page: 287 - 291
publication: Trends in Genetics
publication_status: published
publisher: Elsevier
publist_id: '6775'
quality_controlled: 0
status: public
title: A common framework for understanding the origin of genetic dominance and evolutionary
fates of gene duplications
type: journal_article
volume: 20
year: '2004'
...
---
_id: '889'
abstract:
- lang: eng
text: 'The function of protein and RNA molecules depends on complex epistatic interactions
between sites. Therefore, the deleterious effect of a mutation can be suppressed
by a compensatory second-site substitution. In relating a list of 86 pathogenic
mutations in human IRNAs encoded by mitochondrial genes to the sequences of their
mammalian orthologs, we noted that 52 pathogenic mutations were present in normal
tRNAs of one or several nonhuman mammals. We found at least five mechanisms of
compensation for 32 pathogenic mutations that destroyed a Watson-Crick pair in
one of the four tRNA stems: restoration of the affected Watson-Crick interaction
(25 cases), strengthening of another pair (4 cases), creation of a new pair (8
cases), changes of multiple interactions in the affected stem (11 cases) and changes
involving the interaction between the loop and stem structures (3 cases). A pathogenic
mutation and its compensating substitution are fixed in a lineage in rapid succession,
and often a compensatory interaction evolves convergently in different clades.
At least 10%, and perhaps as many as 50%, of all nucleotide substitutions in evolving
mammalian (RNAs participate in such interactions, indicating that the evolution
of tRNAs proceeds along highly epistatic fitness ridges.'
acknowledgement: We thank J. Gillespie, M. Hahn, L. Horth, A. Kondrashov, A. Kopp,
S. Nuzhdin, M. Turelli and D. Weinreich for their contributions. The authors were
supported by a grant from the US National Institutes of Health to S. Nuzhdin, and
A.D.K. is a Howard Hughes
author:
- first_name: Andrew
full_name: Kern, Andrew D
last_name: Kern
- first_name: Fyodor
full_name: Fyodor Kondrashov
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
citation:
ama: Kern A, Kondrashov F. Mechanisms and convergence of compensatory evolution
in mammalian mitochondrial tRNAs. Nature Genetics. 2004;36(11):1207-1212.
doi:10.1038/ng1451
apa: Kern, A., & Kondrashov, F. (2004). Mechanisms and convergence of compensatory
evolution in mammalian mitochondrial tRNAs. Nature Genetics. Nature Publishing
Group. https://doi.org/10.1038/ng1451
chicago: Kern, Andrew, and Fyodor Kondrashov. “Mechanisms and Convergence of Compensatory
Evolution in Mammalian Mitochondrial TRNAs.” Nature Genetics. Nature Publishing
Group, 2004. https://doi.org/10.1038/ng1451.
ieee: A. Kern and F. Kondrashov, “Mechanisms and convergence of compensatory evolution
in mammalian mitochondrial tRNAs,” Nature Genetics, vol. 36, no. 11. Nature
Publishing Group, pp. 1207–1212, 2004.
ista: Kern A, Kondrashov F. 2004. Mechanisms and convergence of compensatory evolution
in mammalian mitochondrial tRNAs. Nature Genetics. 36(11), 1207–1212.
mla: Kern, Andrew, and Fyodor Kondrashov. “Mechanisms and Convergence of Compensatory
Evolution in Mammalian Mitochondrial TRNAs.” Nature Genetics, vol. 36,
no. 11, Nature Publishing Group, 2004, pp. 1207–12, doi:10.1038/ng1451.
short: A. Kern, F. Kondrashov, Nature Genetics 36 (2004) 1207–1212.
date_created: 2018-12-11T11:49:02Z
date_published: 2004-11-01T00:00:00Z
date_updated: 2021-01-12T08:21:17Z
day: '01'
doi: 10.1038/ng1451
extern: 1
intvolume: ' 36'
issue: '11'
month: '11'
page: 1207 - 1212
publication: Nature Genetics
publication_status: published
publisher: Nature Publishing Group
publist_id: '6759'
quality_controlled: 0
status: public
title: Mechanisms and convergence of compensatory evolution in mammalian mitochondrial
tRNAs
type: journal_article
volume: 36
year: '2004'
...
---
_id: '9493'
abstract:
- lang: eng
text: In a number of organisms, transgenes containing transcribed inverted repeats
(IRs) that produce hairpin RNA can trigger RNA-mediated silencing, which is associated
with 21-24 nucleotide small interfering RNAs (siRNAs). In plants, IR-driven RNA
silencing also causes extensive cytosine methylation of homologous DNA in both
the transgene "trigger" and any other homologous DNA sequences--"targets". Endogenous
genomic sequences, including transposable elements and repeated elements, are
also subject to RNA-mediated silencing. The RNA silencing gene ARGONAUTE4 (AGO4)
is required for maintenance of DNA methylation at several endogenous loci and
for the establishment of methylation at the FWA gene. Here, we show that mutation
of AGO4 substantially reduces the maintenance of DNA methylation triggered by
IR transgenes, but AGO4 loss-of-function does not block the initiation of DNA
methylation by IRs. AGO4 primarily affects non-CG methylation of the target sequences,
while the IR trigger sequences lose methylation in all sequence contexts. Finally,
we find that AGO4 and the DRM methyltransferase genes are required for maintenance
of siRNAs at a subset of endogenous sequences, but AGO4 is not required for the
accumulation of IR-induced siRNAs or a number of endogenous siRNAs, suggesting
that AGO4 may function downstream of siRNA production.
article_processing_charge: No
article_type: original
author:
- first_name: Daniel
full_name: Zilberman, Daniel
id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
last_name: Zilberman
orcid: 0000-0002-0123-8649
- first_name: Xiaofeng
full_name: Cao, Xiaofeng
last_name: Cao
- first_name: Lisa K.
full_name: Johansen, Lisa K.
last_name: Johansen
- first_name: Zhixin
full_name: Xie, Zhixin
last_name: Xie
- first_name: James C.
full_name: Carrington, James C.
last_name: Carrington
- first_name: Steven E.
full_name: Jacobsen, Steven E.
last_name: Jacobsen
citation:
ama: Zilberman D, Cao X, Johansen LK, Xie Z, Carrington JC, Jacobsen SE. Role of
Arabidopsis ARGONAUTE4 in RNA-directed DNA methylation triggered by inverted repeats.
Current Biology. 2004;14(13):1214-1220. doi:10.1016/j.cub.2004.06.055
apa: Zilberman, D., Cao, X., Johansen, L. K., Xie, Z., Carrington, J. C., &
Jacobsen, S. E. (2004). Role of Arabidopsis ARGONAUTE4 in RNA-directed DNA methylation
triggered by inverted repeats. Current Biology. Elsevier. https://doi.org/10.1016/j.cub.2004.06.055
chicago: Zilberman, Daniel, Xiaofeng Cao, Lisa K. Johansen, Zhixin Xie, James C.
Carrington, and Steven E. Jacobsen. “Role of Arabidopsis ARGONAUTE4 in RNA-Directed
DNA Methylation Triggered by Inverted Repeats.” Current Biology. Elsevier,
2004. https://doi.org/10.1016/j.cub.2004.06.055.
ieee: D. Zilberman, X. Cao, L. K. Johansen, Z. Xie, J. C. Carrington, and S. E.
Jacobsen, “Role of Arabidopsis ARGONAUTE4 in RNA-directed DNA methylation triggered
by inverted repeats,” Current Biology, vol. 14, no. 13. Elsevier, pp. 1214–1220,
2004.
ista: Zilberman D, Cao X, Johansen LK, Xie Z, Carrington JC, Jacobsen SE. 2004.
Role of Arabidopsis ARGONAUTE4 in RNA-directed DNA methylation triggered by inverted
repeats. Current Biology. 14(13), 1214–1220.
mla: Zilberman, Daniel, et al. “Role of Arabidopsis ARGONAUTE4 in RNA-Directed DNA
Methylation Triggered by Inverted Repeats.” Current Biology, vol. 14, no.
13, Elsevier, 2004, pp. 1214–20, doi:10.1016/j.cub.2004.06.055.
short: D. Zilberman, X. Cao, L.K. Johansen, Z. Xie, J.C. Carrington, S.E. Jacobsen,
Current Biology 14 (2004) 1214–1220.
date_created: 2021-06-07T10:33:00Z
date_published: 2004-07-13T00:00:00Z
date_updated: 2021-12-14T08:52:00Z
day: '13'
department:
- _id: DaZi
doi: 10.1016/j.cub.2004.06.055
extern: '1'
external_id:
pmid:
- '15242620 '
intvolume: ' 14'
issue: '13'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1016/j.cub.2004.06.055
month: '07'
oa: 1
oa_version: Published Version
page: 1214-1220
pmid: 1
publication: Current Biology
publication_identifier:
eissn:
- 1879-0445
issn:
- 0960-9822
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Role of Arabidopsis ARGONAUTE4 in RNA-directed DNA methylation triggered by
inverted repeats
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 14
year: '2004'
...