This special issue contains extended versions of papers presented at FoSSaCS 2007, the international conference Foundations of Software Science and Computations Structures (FOSSACS) 2007, held in Braga, Portugal, March 26-28, 2007, as part of the Joint European Conferences on Theory and Practice of Software (ETAPS) 2007.

The 11 papers collected in this special issue have been invited by the guest editor. The selection was made on the basis of the ranking of the papers by the Program Committee and the opinion of the expert reviewers who assisted the Program Committee. The papers reect the high level of the conference and represent a wide range of topics including separation logic, process calculi, probabilistic systems, higher-order pushdowns, verification of functional programs with state and model-checking. We are grateful to the authors for their excellent submissions.

All papers were refereed in accordance with the usual high standards of LMCS. We also thank the members of the Program Committee of FoSSaCS 2007 and their subreferees as well as to all those who have served as reviewers of the papers submitted to this special issue. We would also like to thank Jiri Adámek, Executive Editor of LMCS for his assistance and guidance.