| 1. |
|
|
| 2. |
- Borgström, Johannes, et al.
(författare)
-
A Chart Semantics for the Pi-Calculus
- 2008
-
Ingår i: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 194:2, s. 3-29
-
Tidskriftsartikel (refereegranskat)abstract
- We present a graphical semantics for the pi-calculus, that is easier to visualize and better suited to expressing causality and temporal properties than conventional relational semantics. A pi-chart is a finite directed acyclic graph recording a computation in the pi-calculus. Each node represents a process, and each edge either represents a computation step, or a message-passing interaction. Pi-charts enjoy a natural pictorial representation, akin to message sequence charts, in which vertical edges represent control flow and horizontal edges represent data flow based on message passing. A pi-chart represents a single computation starting from its top (the nodes with no ancestors) to its bottom (the nodes with no descendants). Unlike conventional reductions or transitions, the edges in a pi-chart induce ancestry and other causal relations on processes. We give both compositional and operational definitions of pi-charts, and illustrate the additional expressivity afforded by the chart semantics via a series of examples.
|
|
| 3. |
- Richards, Stephen, et al.
(författare)
-
The genome of the model beetle and pest Tribolium castaneum.
- 2008
-
Ingår i: Nature. - 1476-4687. ; 452:7190, s. 949-55
-
Tidskriftsartikel (refereegranskat)abstract
- Tribolium castaneum is a representative of earth’s most numerous eukaryotic order, a powerful model organism for the study of generalized insect development, and also an important pest of stored agricultural products. We describe its genome sequence here. This omnivorous beetle has evolved an ability to interact with a diverse chemical environment as evidenced by large expansions in odorant and gustatory receptors, as well as p450 and other detoxification enzymes. Developmental patterns in Tribolium are more representative of other arthropods than those found in Drosophila, a fact represented in gene content and function. For one, Tribolium has retained more ancestral genes involved in cell-cell communication than Drosophila, and some are expressed in the growth zone crucial for axial elongation in short germ development. Systemic RNAi in T. castaneum appears to use mechanisms distinct from those found in C. elegans, but nevertheless offers similar power for the elucidation of gene function and identification of targets for selective insect control.
|
|
| 4. |
- Bengtson, Jesper, 1977-, et al.
(författare)
-
Refinement Types for Secure Implementations
- 2008
-
Ingår i: Proc. 21st IEEE Computer Security Foundations Symposium. - Piscataway, NJ : IEEE. - 9780769531823 ; , s. 17-32
-
Konferensbidrag (refereegranskat)
|
|
| 5. |
- Borgström, Johannes, et al.
(författare)
-
A Compositional Theory for STM Haskell
- 2009
-
Ingår i: Proceedings of the 2nd ACM SIGPLAN symposium on Haskell. - New York, NY, USA : ACM Press. - 9781605585086 ; , s. 69-80
-
Konferensbidrag (refereegranskat)abstract
- We address the problem of reasoning about Haskell programs that use Software Transactional Memory (STM). As a motivating example, we consider Haskell code for a concurrent non-deterministic tree rewriting algorithm implementing the operational semantics of the ambient calculus. The core of our theory is a uniform model, in the spirit of process calculi, of the run-time state of multi-threaded STM Haskell programs. The model was designed to simplify both local and compositional reasoning about STM programs. A single reduction relation captures both pure functional computations and also effectful computations in the STM and I/O monads. We state and prove liveness, soundness, completeness, safety, and termination properties relating source processes and their Haskell implementation. Our proof exploits various ideas from concurrency theory, such as the bisimulation technique, but in the setting of a widely used programming language rather than an abstract process calculus. Additionally, we develop an equational theory for reasoning about STM Haskell programs, and establish for the first time equations conjectured by the designers of STM Haskell. We conclude that using a pure functional language extended with STM facilitates reasoning about concurrent implementation code.
|
|
| 6. |
- Borgström, Johannes
(författare)
-
Equivalences and Calculi for Formal Verification of Cryptographic Protocols
- 2008
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Security protocols are essential to the proper functioning of any distributed system running over an insecure network but often have flaws that can be exploited even without breaking the cryptography. Formal cryptography, the assumption that the cryptographic primitives are flawless, facilitates the construction of formal models and verification tools. Such models are often based on process calculi, small formal languages for modelling communicating systems. The spi calculus, a process calculus for the modelling and formal verification of cryptographic protocols, is an extension of the pi calculus with cryptography. In the spi calculus, security properties can be formulated as equations on process terms, so no external formalism is needed. Moreover, the contextual nature of observational process equivalences takes into account any attacker/environment that can be expressed in the calculus. We set out to address the problem of automatic verification of observational equivalence in an extension of the spi calculus: A channel-passing calculus with a more general expression language. As a first step, we study existing non-contextual proof techniques for a particular canonical contextual equivalence. In contrast to standard process calculi, reasoning on cryptographic processes must take into account the partial knowledge of the environment about transmitted messages. In the setting of the spi calculus, several notions of environment-sensitive bisimulation has been developed to treat this environment knowledge. We exhibit distinguishing examples between several of these notions, including ones previously believed to coincide. We then give a general framework for comparison of environment-sensitive relations, based on a comparison of the corresponding kinds of environment and notions of environment consistency. Within this framework we perform an exhaustive comparison of the different bisimulations, where every possible relation that is not proven is disproven. For the second step, we consider the question of which expression languages are suitable. Extending the expression language to account for more sophisticated cryptographic primitives or other kinds of data terms quickly leads to decidability issues. Two important problems in this area are the knowledge problem and an indistinguishability problem called static equivalence. It is known that decidability of static equivalence implies decidability of knowledge in many cases; we exhibit an expression language where knowledge is decidable but static equivalence is not. We then define a class of constructor-destructor expression languages and prove that environment consistency over any such language directly corresponds to static equivalence in a particular extension thereof. We proceed to place some loose constraints on deterministic expression evaluation, and redefine the spi calculus in this more general setting. Once we have chosen an expression language, we encounter a third problem, which is inherent in the operational semantics of message-passing process calculi: The possibility to receive arbitrary messages gives rise to infinite branching on process input. To mitigate this problem, we define a symbolic semantics, where the substitution of received messages for input variables never takes place. Instead, input variables are only subject to logical constraints. We then use this symbolic semantics to define a symbolic bisimulation that is sound and complete with respect to its concrete counterpart, extending the possibilities for automated bisimulation checkers.
|
|
| 7. |
- Wu, Xifeng, et al.
(författare)
-
Genetic variation in the prostate stem cell antigen gene PSCA confers susceptibility to urinary bladder cancer.
- 2009
-
Ingår i: Nature genetics. - : Springer Science and Business Media LLC. - 1546-1718 .- 1061-4036. ; 41:9, s. 991-5
-
Tidskriftsartikel (refereegranskat)abstract
- We conducted a genome-wide association study on 969 bladder cancer cases and 957 controls from Texas. For fast-track validation, we evaluated 60 SNPs in three additional US populations and validated the top SNP in nine European populations. A missense variant (rs2294008) in the PSCA gene showed consistent association with bladder cancer in US and European populations. Combining all subjects (6,667 cases, 39,590 controls), the overall P-value was 2.14 x 10(-10) and the allelic odds ratio was 1.15 (95% confidence interval 1.10-1.20). rs2294008 alters the start codon and is predicted to cause truncation of nine amino acids from the N-terminal signal sequence of the primary PSCA translation product. In vitro reporter gene assay showed that the variant allele significantly reduced promoter activity. Resequencing of the PSCA genomic region showed that rs2294008 is the only common missense SNP in PSCA. Our data identify rs2294008 as a new bladder cancer susceptibility locus.
|
|
