Palestras DANIEL KROENING, Universidade de Oxford, Reino UnidoSpeeding up Simulation of SystemC using Model Checking Resumo: 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.
Biografia: Daniel Kroening juntou-se ao grupo de Verificação de Modelos no Departamento de Ciências da Computação da Universidade Carnegie Mellon, Pittsburgh PA, USA, em 2001 como pós-doutorando. Ele foi professor assistente no Swiss Technical Institute (ETH) em Zurich, na Suíça, de 2004 a 2007. Ele agora é um professor (“Reader”) no Laboratório de Computação da Universidade de Oxford. Seus interesses de pesquisa incluem a verificação formal automática de sistemas de hardware e software, procedimentos de decisão, sistemas embarcados e co-projeto de hardware/software.
SEBASTIAN UCHITEL, Universidade de Buenos Aires, ArgentinaPartial Behaviour Modelling: Foundations for Incremental and Iterative Model-Based Software Engineering Resumo: 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.
Biografia: Sebastian Uchitel é professor do Departamento de Computação da FCEN, Universidade de Buenos Aires, onde obteve seu título de Mestre em Ciências da Computação, e pesquisador do CONICET, Argentina. Ele também ensina no Imperial College London onde obteve seu título de Doutorado em 2003. Seus interesses de pesquisa são em modelagem de comportamento e projeto e análise de requisitos para sistemas intensivos em software complexos. Sua pesquisa é focada na modelagem de comportamento parcial, incluindo especificações baseadas em cenários, síntese de modelo de comportamento e sistemas de transição modal. Sua pesquisa inclui também engenharia de requisitos orientado a objetivos, confiabilidade, arquiteturas de software e arquiteturas orientadas a serviços. O Dr. Uchitel é atualmente editor associado do IEEE Transactions em Engenharia de Software e da revista Requirements Engineering, ele foi co-coordenador do 21o IEEE/ACM International Conference on Automated Software Engineering (ASE 2006) realizada em Tóquio e é o co-coordenador da programação da 32nd IEEE/ACM International Conference on Software Engineering (ICSE 2010). Dr. Uchitel foi recentemente destacado pelo Leverhulme Trust e a National Acadamy of Hard e Natural Sciences da Argentina.
LEONARDO DE MOURA, Microsoft Research, Estado UnidosSatisfiability Modulo Theories: An Appetizer Resumo: 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.
- Biografia: Leonardo de Moura é um pesquisador no grupo de Software Reliability da Microsoft Research, Redmond WA, USA. Ele está atualmente trabalhando no provador de teoremas Z3. De 2001 a 2006, ele foi Cientista da Computação no SRI International, Menlo Park CA, USA. Obteve seu doutorado em Ciência da Computação na PUC, Rio de Janeiro RJ, Brasil em 2000. Seus interesses são em provadores de teoremas, procedimentos de decisão e verificação de software.
|
