Quantitative Analysis of Software: Challenges and Recent Advances
Even with impressive advances in formal methods over the last few decades, some problems in automatic verification remain challenging. Central amongst these is the verification of quantitative properties of software such as execution time or energy usage. In this talk, I will discuss the main challenges for quantitative analysis of software in cyber-physical systems. I will also present some recent advances based on the combination of inductive inference with deductive reasoning.
Sanjit A. Seshia is an assistant professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. His research interests are in dependable computing and computational logic, with a current focus on applying automated formal methods to problems in embedded systems, electronic design automation, computer security, and program analysis. He has received a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, and the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University.
Analysis of Service Oriented Software Systems
We overview perspectives on the general concept of service-based computing, and present some of our recently proposed techniques, based on process algebras, type theory and logic, to reason about key properties of service-based software systems. We will also discuss how our basic framework may be extended to cover several interesting security properties, such as separation of duties in multiple partner protocols. (talk based in joint work with Hugo. T. Vieira)
Luis Cares is an Associate Professor (with Habilitation) at the Department of Informatics of FCT/UNL (Universidade Nova de Lisboa). He is also the Director of CITI (Center of Informatics and Information Technology). Member of EATSC, ACM, ICTI (CMU|Portugal) and IFIP TC-2 WG 2.2 (on Formal Description of Programming Concepts), his research interests span from concurrency models and logics to program languages, calculi and types. His work on spatial logic, with Luca Cardelli and others, is widely recognized as a landmark in the area.