This book constitutes the refereed proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2009, held in York, UK, in March 2009, as part of ETAPS 2009, the European Joint Conferences on Theory and Practice of Software.
The 30 revised full papers presented together with two invited talks were carefully reviewed and selected from 102 full paper submissions. The topics addressed are semantics, logics and automata, algebras, automata theory, processes and models, security, probabilistic and quantitative models, synthesis, and program analysis and semantics.
Author(s): Wolfgang Thomas (auth.), Luca de Alfaro (eds.)
Series: Lecture Notes in Computer Science 5504 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 471
Tags: Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering; Programming Languages, Compilers, Interpreters; Computation by Abstract Devices; Theory of Computation
Front Matter....Pages -
Facets of Synthesis: Revisiting Church’s Problem....Pages 1-14
Temporal Reasoning about Program Executions....Pages 15-15
Least and Greatest Fixpoints in Game Semantics....Pages 16-31
Full Abstraction for Reduced ML....Pages 32-47
Logics and Bisimulation Games for Concurrency, Causality and Conflict....Pages 48-62
Separating Graph Logic from MSO....Pages 63-77
On the Completeness of Dynamic Logic....Pages 78-91
Dependency Tree Automata....Pages 92-106
On Global Model Checking Trees Generated by Higher-Order Recursion Schemes....Pages 107-121
A Kleene Theorem for Polynomial Coalgebras....Pages 122-136
Coalgebraic Hybrid Logic....Pages 137-151
A Description of Iterative Reflections of Monads (Extended Abstract)....Pages 152-166
Tighter Bounds for the Determinisation of Büchi Automata....Pages 167-181
Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata....Pages 182-196
Interrupt Timed Automata....Pages 197-211
Parameter Reduction in Grammar-Compressed Trees....Pages 212-226
The Calculus of Handshake Configurations....Pages 227-241
On the Expressive Power of Restriction and Priorities in CCS with Replication....Pages 242-256
Normal Bisimulations in Calculi with Passivation....Pages 257-271
Reactive Systems, Barbed Semantics, and the Mobile Ambients....Pages 272-287
On the Foundations of Quantitative Information Flow....Pages 288-302
Cryptographic Protocol Composition via the Authentication Tests....Pages 303-317
Bisimulation for Demonic Schedulers....Pages 318-332
On Omega-Languages Defined by Mean-Payoff Conditions....Pages 333-347
Minimal Cost Reachability/Coverability in Priced Timed Petri Nets....Pages 348-363
Delayed Nondeterminism in Continuous-Time Markov Decision Processes....Pages 364-379
Concurrency, σ -Algebras, and Probabilistic Fairness....Pages 380-394
Synthesis from Component Libraries....Pages 395-409
Realizability of Concurrent Recursive Programs....Pages 410-424
Beyond Shapes: Lists with Ordered Data....Pages 425-439
Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains....Pages 440-455
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types....Pages 456-470
Back Matter....Pages -
