Probabilistic Programming, Statistical Model Checking and Euclidean

Model Checking

 

Gul Agha

University of Illinois at Urbana-Champaign

http://osl.cs.illinois.edu

 

 

Large concurrent systems lead to an explosion of states that make it

hard to reason about all possible behaviors of a system.  However, in

many applications (such as biological systems or big data), we are

interested in probabilistic guarantees.  The talk will define a

probabilistic programming language, formalisms for specification of

properties, and methods for reasoning based on sampling the behavior

of a concurrent system.  In particular, I will describe concepts

behind statistical model checking for probabilistic properties based

on paths, and Euclidean model checking for quantitative properties of

systems.  I will illustrate the approach with applications such as

diversity of problems ranging from Pharmacokinetics to sensor

networks.

 

Short Bio

 

Gul Agha is Professor of Computer Science, and of Electrical and

Computer Engineering, at the University of Illinois at

Urbana-Champaign.  Dr. Agha's research is in the area of programming

models and languages for open distributed and embedded computation.

Dr. Agha is a Fellow of the IEEE and a Golden Core of the IEEE

Computer Society.  He served as Editor-in-Chief of IEEE Concurrency:

Parallel, Distributed and Mobile Computing (1994-98), and EIC of the

ACM Computing Surveys (1999-2007).  He has published over 200 research

articles and supervised 20 PhD dissertations.  His book on Actors,

published by MIT Press, is among the most widely cited works.  Besides

work on semantics and implementation of actor languages, Agha has done

pioneering research in concolic testing, predictive runtime monitoring,

computation learning for verification, statistical model checking and

Euclidean model checking.  His former students hold faculty positions

at UC Irvine, UC Berkeley, Saskatchewan, Illinois Institute of

Technology and RPI.