This book presents a comprehensive mathematical theory that explains precisely what information flow is, how it can be assessed quantitatively - so bringing precise meaning to the intuition that certain information leaks are small enough to be tolerated - and how systems can be constructed that achieve rigorous, quantitative information-flow guarantees in those terms. It addresses the fundamental challenge that functional and practical requirements frequently conflict with the goal of preserving confidentiality, making perfect security unattainable. Topics include: a systematic presentation of how unwanted information flow, i.e., "leaks", can be quantified in operationally significant ways and then bounded, both with respect to estimated benefit for an attacking adversary and by comparisons between alternative implementations; a detailed study of capacity, refinement, and Dalenius leakage, supporting robust leakage assessments; a unification of information-theoretic channels and information-leaking sequential programs within the same framework; and a collection of case studies, showing how the theory can be applied to interesting realistic scenarios. The text is unified, self-contained and comprehensive, accessible to students and researchers with some knowledge of discrete probability and undergraduate mathematics, and contains exercises to facilitate its use as a course textbook.

The book is a focused survey on probabilistic program semantics, conceived to tell a coherent story with a uniform notation. It is grouped into three themes: Part I is for 'users' of the techniques who will be developing actual programs; Part II gives mathematical foundations intended for those studying exactly how it was done and how to build semantic structures/models in their own work; and Part III describes a very 'hot' research direction, temporal logic and model checking. Topics and features: - introduces readers to very up-to-date research in the mathematics of rigorous development of randomized (probabilistic) algorithms- illustrates by example the typical steps necessary in computer science to build a mathematical model of any programming paradigm- presents results of a large and integrated body of research in the area of 'quantitative' program logics. An advanced research survey monograph, integrating three major topic areas.

This book constitutes the proceedings of the 15th International Conference on Quantitative Evaluation Systems, QEST 2018, held in Beijing, China, in September 2018. The 24 full papers presented were carefully reviewed and selected from 51 submissions. The papers cover topics in the field of quantitative evaluation and verification of computer systems and networks through stochastic models and measurements emphasizing two frontier topics in research: quantitative information flow for security and industrial formal methods.

This book constitutes the proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-20, held in November 2015, in Suva, Fiji. The 43 regular papers presented together with 1 invited talk included in this volume were carefully reviewed and selected from 92 submissions. The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, LPAR, is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world.

Illustrates by example the typical steps necessary in computer science to build a mathematical model of any programming paradigm .

Presents results of a large and integrated body of research in the area of 'quantitative' program logics.

This book constitutes the refereed proceedings of the 23rd Symposium on Formal Methods, FM 2019, held in Porto, Portugal, in the form of the Third World Congress on Formal Methods, in October 2019. The 44 full papers presented together with 3 invited presentations were carefully reviewed and selected from 129 submissions. The papers are organized in topical sections named: Invited Presentations; Verification; Synthesis Techniques; Concurrency; Model Checking Circus; Model Checking; Analysis Techniques; Specification Languages; Reasoning Techniques; Modelling Languages; Learning-Based Techniques and Applications; Refactoring and Reprogramming; I-Day Presentations.