Foundations of Software Science and Computational Structures: 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, ProceedingsHelmut Seidl Springer Science & Business Media, 2. jul. 2007 - 379 sider This book constitutes the refereed proceedings of the 10th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2007, held in Braga, Portugal in March/April 2007. The 25 revised full papers presented together with the abstract of one invited talk cover a broad spectrum on theories and methods to support analysis, synthesis, transformation and verification of programs and software systems. |
Indhold
| 17 | |
| 32 | |
The Complexity of Generalized Satisfiabilityfor Linear Temporal Logic | 48 |
Formalising the πCalculus Using Nominal Logic | 63 |
Relational Parametricity and Separation Logic | 93 |
ModelChecking OneClockPriced Timed Automata | 108 |
Approximating a Behavioural PseudometricWithout Discount for Probabilistic Systems | 123 |
Optimal Strategy Synthesis inStochastic M ̈uller Games | 138 |
A Distribution Law for CCS anda New Congruence Result for the πCalculus | 228 |
On the Expressiveness and Complexity of ATL | 243 |
Polynomial Constraints forSets with Cardinality Bounds | 258 |
A Lower Bound on Web Services Composition | 274 |
Logical Characterizations of Bisimulations forDiscrete Probabilistic Systems | 287 |
Semantic Barbs and Biorthogonality | 302 |
On the Stability by Union of ReducibilityCandidates | 317 |
An Effective Algorithm for the MembershipProblem for Extended Regular Expressions | 332 |
Generalized Parity Games | 153 |
Tree Automata with Memory Visibility andStructural Constraints | 168 |
Enriched μCalculi Module Checking | 183 |
PDL with Intersection and Converse Is 2EXPComplete | 198 |
Symbolic BackwardsReachability Analysis forHigherOrder Pushdown Systems | 213 |
Complexity Results on Balanced ContextFreeLanguages | 346 |
Logical Reasoning forHigherOrder Functions with Local State | 361 |
Author Index | 378 |
Andre udgaver - Se alle
Foundations of Software Science and Computational Structures: 10th ... Helmut Seidl Uddragsvisning - 2007 |
Almindelige termer og sætninger
A₁ abstract ai+1 algorithm automaton biorthogonal bisimilarity bisimulation Boolean bound names calculus checking complexity Computer Science configuration congruence consider constraints construct context corresponding datatype defined definition denote derivation encoding equivalence example exists EXPTIME finite set formula FOSSACS function game graph given higher-order history expressions ICPDL induction infinite input iter itree Kripke structure labeled language Lemma linear LNCS loop memory modal model-checking module node operational semantics operator p-calculus parity parity games path player probabilistic automata problem Proc process calculi processes proof Proposition pseudometric PSPACE PSPACE-complete pushdown reachability reduction regular expressions relation result rewrite rules satisfiability Section semantics separation logic sequence simulation Springer Streett subset symbol t₁ temporal Theorem transition relation tree automata TWAPTA variables VTAM WCTL winning condition winning strategy
Populære passager
Side 18 - The rest of this paper is structured as follows. In the next section we motivate the ideas and recall the necessary background material required for the rest of this paper.
Side 272 - References [1] A. Aiken, D. Kozen, M. Vardi and E. Wimmers. The complexity of set constraints.
Side 201 - The purpose of this section is to prove the following theorem. THEOREM 3.1.
Side 153 - This research was supported in part by the Swiss National Science Foundation and by the NSF grants CCR-0225610 and CCR-0234690.
Side 167 - Second International Joint Conference on Artificial Intelligence, pages 481489. The British Computer Society, London, 1971.
Side 93 - Separation logic [20, 18, 5, 14, 9, 4] is a Hoare-style program logic, and variants of it have been applied to prove correct interesting pointer algorithms such as copying a dag, disposing a graph, the Schorr- Waite graph algorithm, and Cheney's copying garbage collector. The main advantage of separation logic compared to ordinary Hoare logic is that it facilitates local reasoning, formalized via the so-called frame rule using a connective called separating conjunction. The development of separation...
Side 80 - A substitution is a mapping from the set of variables to the set of terms of L(C) such that variables of type t map to terms of type t.
Side 181 - ... gives the trees of Adelson-Velskii and Landis). Bayer [Ba72b] considers binary trees with two different kinds of branches, downward pointers, and horizontal pointers. The height constraint he imposes is that every path from the root to a leaf contains the same number of downward pointers, and that there may never be two horizontal pointers in succession. The trees of Adelson-Velskii and Landis can be represented in this way by assigning some branches on long paths to horizontal pointers. A new...
Side 136 - Colloquium on Automata. Languages and Programming, volume 2719 of Lecture Notes in Computer Science, pages 943-955.
Side 31 - ... Constrained quantification in polymorphic type analysis. Technical Report CSL-901, Xerox PARC, 1990. [8] Luis Damas and Robin Milner. Principal typeschemes for functional programs. In Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982. [9] Luis Manuel Martins Damas. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1985. [10] Bruce F. Duba, Robert Harper, and David MacQueen. Typing first-class continuations in ML. In Conference...