Invited Talks

Abstract: We present a technique to improve the performance of testing of concurrent programs by means of Model Checking. The key insight to obtain scalability is to apply the Model Checker only to small partitions of the model. The benchmarks are modelled using SystemC, which is a system-level modeling language that offers a wide range of features to describe concurrent systems at different levels of abstraction. Our tool produces a simulator that uses the result of the formal analysis at runtime to perform partial-order reduction, thereby eliminating context switches that do not affect the result of the test run. Experimental results show simulation speedups of one order of magnitude and better.

Biography: Daniel Kroening joined the Model Checking group in the Computer Science Department at Carnegie Mellon University, Pittsburgh PA, USA, in 2001 as a Post-Doc. He was an assistant professor at the Swiss Technical Institute (ETH) in Zurich, Switzerland, from 2004 to 2007. He is now a Reader at the Computing Laboratory at Oxford University. His research interests include automated formal verification of hardware and software systems, decision procedures, embedded systems, and hardware/software co-design.

Abstract: Rigorous modelling of the intended behaviour of software intensive systems has been shown to be successfull in uncovering requirements and design flaws. However, the impact that behaviour modelling has had among practitioners is limited. The construction of behaviour models remains a difficult and laborious task that requires significant expertise. In addition, traditional approaches to behaviour models require complete descriptions of the system behaviour up to some level of abstraction. This completeness assumption is limiting in the context of software development process best practices which include iterative development, adoption of
use-case and scenario-based techniques and viewpoint- or stakeholder-based analysis; practices which require modelling and analysis in the presence of partial information about system behaviour. Our aim is to support the iterative and incremental construction of behaviour models by means of construction, composition and analysis of partial, heterogeneous, yet formal, descriptions of behaviour. In this talk we discuss how modal transitions systems can provide the basis for such support and present some of the model synthesis and composition techniques we have developed.

Biography: Sebastian Uchitel is a Professor at the Department of Computing, FCEN, University of Buenos Aires, where he obtained his MSc level degree in Computer Science and a researcher of CONICET, Argentina. He also holds a Readership at Imperial College London where he obtained his PhD in 2003. His research interests are in behavior modeling and analysis of requirements and design for complex software-intensive systems. His research focuses on partial behaviour modelling, including scenario- based specifications, behaviour model synthesis and modal transition systems. His research also includes goal-oriented requirements engineering, reliability, software architectures and service-oriented architectures. Dr. Uchitel is currently associate editor of IEEE Transactions on Software Engineering and the Requirements Engineering Journal, he was program co-chair of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006) held in Tokyo and is the program co-chair of the 32nd IEEE/ACM International Conference on Software Engineering (ICSE 2010). Dr Uchitel has recently been distinguished by the Leverhulme Trust and the National Acadamy of Hard and Natural Sciences of Argentina.

Abstract: Satisfiability Modulo Theories (SMT) is about checking the satisfiability of logical formulas over one or more theories. The problem draws on a combination of some of the most fundamental areas in computer science. It combines the problem of Boolean satisfiability with domains, such as, those studied in convex optimization and termmanipulating symbolic systems. It also draws on the most prolific problems in the past century of symbolic logic: the decision problem, completeness and incompleteness of logical theories, and finally complexity theory. The problem of modularly combining special purpose algorithms for each domain is as deep and intriguing as finding new algorithms that work particularly well in the context of a combination. SMT also enjoys a very useful role in software engineering. Modern software, hardware analysis and model-based tools are increasingly complex and multi-faceted software systems. However, at their core is invariably a component using symbolic logic for describing states and transformations between them. A well tuned SMT solver that takes into account the state-of-the-art breakthroughs usually scales orders of magnitude beyond custom ad-hoc solvers.

Biography: Leonardo de Moura is a researcher in the Software Reliability group at Microsoft Research, Redmond WA, USA. He is currently working on the Z3 theorem prover. From 2001-2006, he was a Computer Scientist at SRI International, Menlo Park CA, USA. He obtained his Ph.D. in Computer Science from PUC, Rio de Janeiro RJ, Brazil in 2000. He is interested in theorem provers, decision procedures and software verification.