ETAPS 2013: 16-24 March 2013, Rome, Italy
Category theory is a well-known mathematical modeling language with a wide area of applications in mathematics and computer science, including especially the semantical foundations of topics in software science and development. It is the intention of the ACCAT workshop to bring together leading researchers in the field of ACCAT with those in software science and development in order to transfer categorical concepts and theories in both directions.
Fabio Gadducci (University of Pisa, Italy) Ulrike Golas (Konrad-Zuse-Zentrum für Informationstechnik Berlin, Germany)
Dates: Sunday March 17th, 2013
System-of-Systems describes the large scale integration of many independent self-contained systems to satisfy global needs or multi-system requests. Examples are smart grid, intelligent buildings, smart cities, transport systems, etc. There is a need for new modeling formalisms, analysis methods and tools to help make trade-off decisions during design and evolution avoiding leading to sub-optimal design and rework during integration and in service. The workshop should focus on the modeling and analysis of System of Systems. The workshop Advances in Systems of Systems aims to gather people from different communities in order to encourage exchange of methods and views. The workshop welcomes submissions on new modeling approaches, analysis technique, tool and case studies.
Kim G. Larsen (Aalborg University, Denmark) Axel Legay (INRIA Renne, France and Aalborg University, Denmark) Ulrik Nyman (Aalborg University, Denmark)
Paper submission: 14 January 2013 (extended)Notification: 25 January 2013Camera ready: 15 February 2013
Dates: Saturday March 16th, 2013
The aim of the workshop is to bring together researchers, established and new, interested in bidirectional transformations from different perspectives, such as: language-based approaches, software/model transformations, data/schema co-evolution. Bidirectional transformations (bx) are a mechanism for maintaining the consistency of at least two related sources of information. Such sources can be databases, software models, documents, graphs, and trees. The methodologies used range from classical program transformation to graph transformation techniques, from ad-hoc techniques for data synchronization to the development of domain-specific languages.
Perdita Stevens (University of Edinburgh, UK)James Terwilliger (Microsoft, USA)
Paper submission: 18 December 2012Notification: 22 January 2013Camera ready: 3 February 2013
Bytecode, such as produced by, e.g., Java and .NET compilers, has become an important topic of interest, both for industry and academia. The industrial interest stems from the fact that bytecode is typically used for Internet and mobile device applications (smart cards, phones, etc.), where security is a major issue. Moreover, bytecode is device-independent and allows dynamic loading of classes, which provides an extra challenge for the application of formal methods. Also the unstructuredness of the code and the pervasive presence of the operand stack provide further challenges for the analysis of bytecode. This workshop will focus on theoretical and practical aspects of semantics, verification, analysis, certification and transformation of bytecode.
Miguel Gomez-Zamalloa (Univ. of Madrid, Spain) Germán Puebla (Technical Univ. of Madrid, Spain)
Abstract submission: 16 December 2012Paper submission: 23 December 2012Notification: 21 January 2013Camera ready: 8 February 2013
Dates: Saturday March 23rd, 2013
The technical day will be focused on innovative techniques on timing analysis of programs. Goal is to make the day an active discussion forum for all non conventional work on timing analysis. In particular, the two European Projects Certified Complexity (CerCo) and Probabilistically Analysable Real-Time Systems (PROARTIS) will present and discuss the respective techniques and results towards improving tightness of WCET estimates in comparison to other timing analysis methods. The approach investigated in CerCo consists in enhancing compilation to induce on the source language a certified and tight cost model for all O(1) code fragments. This information is then combined with Hoare logic, invariant generators and automatic theorem provers to certify the actual complexity of the program as a function of its arguments (dependent complexity). The technique have been applied to a compiler for C programs (under formal certification in the Matita interactive theorem prover) and a compiler for Lustre programs. The approach investigated in PROARTIS is the one of Probabilistic Timing Analysis (PTA) that provides WCET bounds with an associated probability of occurrence, known as probabilistic WCET (pWCET) estimates. With PTA, execution timing becomes less dependent on execution history, with drastic reduction in the amount of information required to obtain tight WCET estimates in comparison to other timing analysis methods. PTA can be applied either in a static (SPTA) or measurement-based (MBPTA) manner. MBPTA bases on statistical reasoning, which requires that the random variables describing measurements of end-to-end runs are independent and identically distributed. Independence is obtained by standard statistical techniques. Identical distribution can instead be ensured by construction in PTA-friendly high-performance hardware.
Roberto Amadio (Univ. Paris Diderot, Paris, France)Claudio Sacerdoti Coen (Univ. di Bologna, Italy)Ian Stark (The University of Edinburgh, UK)
The area of Implicit Computational Complexity (ICC) grew out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g., polytime or logspace computation). It aims at studying the computational complexity of programs without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical / computational principles entailing complexity properties. Several approaches have been explored for that purpose, like restrictions on primitive recursion and ramification, rewriting systems, linear logic, types and lambda calculus, interpretations of functional and imperative programs. The workshop is intended to be a forum for researchers interested in ICC to present new results and discuss recent developments in this area.
Simona Ronchi della Rocca (Univ. of Torino, Italy)
Dates: Saturday March 16th and Sunday March 17th, 2013
One strength of FESCA is the link established between the formal methods community and the software engineering community by exploring how formal approaches can be exploited for the analysis of large software architectures.
We encourage submissions on formal techniques and their application that aid reasoning, analysis and certification of component and servicebased applications. In this context, the following topics are of particular concern:
Submissions concentrating on specification techniques should involve an evaluation of the practical merit of their research and clearly state the analysis and reasoning techniques they enable. We also appreciate work of a formal nature with immediate value to for the industrial context. We encourage not only mature research results, submissions presenting innovative ideas and early results are also of interest.
Barbora Bühnová (Masaryk University, Czech Republic)Lucia Kapová (Karlsruhe Inst. of Technology, Germany) Jan Kofroň (Charles Univ. in Prague, Czech Republic)
Dates: Saturday March 23th, 2013
FESCA 2013 KEYNOTE: Vittorio Cortellessa (Università dell'Aquila, Italy), Tradeoff analysis of software quality attributes through optimization models
FESCA 2013 TUTORIAL: Catia Trubiani, Ph.D. (Università dell'Aquila, Italy), Title: Performance antipatterns and feedback in software architectures
The topic of the GRAPHITE workshop is graph analysis in all its forms in computer science. Graphs are used to represent data in many application areas, and they are subjected to various computational algorithms in order to acquire the desired information. These graph algorithms tend to have common characteristics, such as duplicate detection to guarantee their termination, independent of their application domain. Over the past few years, it has been shown that the scalability of such algorithms can be dramatically improved by using, e.g., external memory, by exploiting parallel architectures, such as clusters, multi-core CPUs, and graphics processing units, and by using heuristics to guide the search. Novel techniques to further scale graph search algorithms, and new applications of graph search are within the scope of this workshop. Another topic of interest of the event is more related to the structural properties of graphs: which kind of graph characteristics are relevant for a particular application area, and how can these be measured? Finally, any novel way of using graphs for a particular application area is on topic. The goal of this event is to gather scientists from different communities, such as model checking, artificial intelligence planning, game playing, and algorithm engineering, who do research on graph search algorithms, such that awareness of each others' work is increased.
We encourage submission of works which include but are not limited to the following topics:
Papers on applications and papers bridging multiple application domains are strongly encouraged.
Anton Wijs (Eindhoven Univ. of Technology, Netherlands)Dragan Bošnački (Eindhoven Univ. of Technology, Netherlands)Stefan Edelkamp (Univ. of Bremen, Germany)
Dates: Sunday March 24th, 2013
GT-VMT 2013 is the twelfth workshop of a series that serves as a forum for all researchers and practitioners interested in the use of visual notations (especially graph-based), techniques and tools for the specification, modeling, validation, manipulation and verification of complex systems. The aim of the workshop is to promote engineering approaches that provide effective sound tool support for visual modeling languages, enhancing formal reasoning at the syntactic as well as semantic level (e.g., for model specification, model analysis, model transformation, and model consistency management) in different domains, such as UML, Petri Nets, Graph Transformation or Business Process/Workflow Models.
This year's workshop has a special theme of the analysis of non-functional / extra-functional / quality properties like performance, realtime, safety, reliability, energy consumption. We particularly encourage submissions that focus on the definition and the evaluation of such properties using visual/graph specification techniques, ranging from underlying theory through to their utility in complex system design.
As a summary, topics relevant to the scope of the workshop include (but are not restricted to) the following:
Matthias Tichy (Chalmers Technical University and Gothenburg University, Gothenburg, Sweden) Leila Ribeiro (Univ. Federal do Rio Grande do Sul, Porto Alegre, Brazil)
Abstract submission: 16 december 2012Paper submission: 21 december 2012Notification: 18 January 2013Camera ready: 1 February 2013
Dates: Saturday March 23th, 2013 and Sunday March 24th, 2013
The interest on autonomous systems is increasing both in industry and academia. Such systems must operate with limited human intervention in a changing environment and must be able to compensate for significant system failures without external intervention. The most appropriate models of autonomous systems can be found in the class of hybrid systems (which study continuous-state dynamic processes via discrete-state controllers) that interact with their environment. This workshop brings together researchers interested in all aspects of autonomy and resilience of hybrid systems.
Manuela Bujorianu (Warwick University, UK)Giordano Pola (Univ. of L'Aquila, Italy)Luca Bortolussi (Univ. of Trieste, Italy)
Paper submission: 20 december 2012
This workshop is intended to be a less formal counterpart to the Principles of Security and Trust (POST) conference at ETAPS, and with an emphasis on "hot topics", both of security and of its theoretical foundations and analysis. Like POST, the themes are
Submissions about new and emerging topics (for example, those that have not appeared prominently in conferences and workshops until now) are particularly encouraged. Submissions of preliminary, tentative work are also encouraged. There is no page limit, but the length of your submission should be appropriate to its content. There will be no formal proceedings. Inclusion in informal proceedings is optional.
Mark Ryan (University of Birmingham, UK)
Submission: 4 January 2013 Notification: 25 January 2013 Final version for informal proceedings (optional): 22 February 2013
Aims: To support and promote the systematic development of the fundamental mathematical theory of systems specification. To investigate the theory of formal models for systems specification, development, transformation and verification.
Scope: The theoretical aspects of the specification and development of computing systems that are based on algebraic and logical concepts, and can be studied systematically within a theory of systems specification.
Till Mossakowski (University of Bremen, Germany)
MBT 2013 is devoted to model-based testing of both software and hardware. Model-based testing uses models that describe the behavior of the system under consideration to guide such efforts as test selection and test results evaluation. Model-based testing has gained attention with the popularization of models in software/hardware design and development. Of particular importance are formal models with precise semantics, such as state-based formalisms. Testing with such models allows one to measure the degree of the product's conformance with the model. The intent of this workshop is to bring together researchers and users using different kinds of models for testing and to discuss the state of the art in theory, applications, tools, and industrialization of model-based testing.
Alexander K. Petrenko (Moscow State University, Moscow, Russia) Holger Schlingloff (Fraunhofer FOKUS and Humboldt-Universität, Berlin, Germany)
Computing systems are getting ever more ubiquitous, making us dependent on their proper functioning. MEALS is a European research project under IRSES Exchange Programme focused on designing and developing methods which provide a formal approach to model, understand, and analyze systems, wrt their required behavior: correct (i.e. they conform their intended behaviour), safe (i.e. its operation does not have catastrophic consequences), reliable, available to provide the intended service, and secure (i.e., no user without appropriate clearance can access or modify protected data).
The purpose of this workshop arranged by MEALS is to bring researchers, practitioners and industry together to discuss the issues, challenges and latest solutions for formal techniques for the specification, verification and synthesis of dependable ubiquitous computing systems, with respect to both qualitative (i.e. pure non-deterministic models) as well as quantitative behaviour (i.e. extended with probabilistic information). The workshop is targeted towards researchers interested in formal methods in all their aspects: foundations (their mathematical and logical basis), algorithmic advances (the conceptual basis for software tool support) and practical considerations (tool construction and case studies). The workshop will feature a number of distinguished presentations on newest challenges, new techniques, case studies, and tool demonstrations.
Suzana Andova (Eindhoven Univ. of Technology, The Netherlands) Pedro R. D'Argenio (Univ. Nacional de Cordoba, Argentina)
Models and Logics for Quantitative Analysis are seen as comprising process models that are analysed using logics for quantitative properties. More specifically, we consider process models formally described by transition systems, automata or process calculi, and we consider logics for expressing stochastic and continuous properties as well as discrete ones, we focus on algorithms, theory and tools, and study applications with particular emphasis on embedded systems and service oriented systems but will aim at treating also IT guided workflow systems and biological systems.
The proposed theme for MLQA 2013 is Cyber Physical Systems.
Flemming Nielson (Techn. Univ. of Denmark, Lyngby, Denmark)
Applications today are built using numerous interacting services; soon off-the-shelf CPUs will host thousands of cores, and sensor networks will be composed from a large number of processing units. Many applications need to make effective use of thousands of computing nodes. At some level of granularity, computation in such systems is inherently concurrent and communication-centred. PLACES aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming in the near future, the development of programming methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern.
Submissions are invited in the general area of foundations of programming languages for concurrency, communication and distribution. Specific topics include:
Papers are welcome which present novel and valuable ideas as well as experiences.
Nobuko Yoshida (Imperial College London, UK)Wim Vanderbauwhede (University of Glasgow, UK)
Abstract submission: 14 December 2012Paper submission: 21 December 2012Notification: 23 January 2013Camera ready: 4 February 2013
Quantitative aspects of computation refer to the use of physical quantities (time, bandwidth, etc.) as well as mathematical quantities (for example, probabilities) for the characterisation of the behaviour and for determining the properties of systems. Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of the QAPL workshop series is to discuss the explicit use of time and probability and general quantities either directly in the model or as a tool for the analysis of systems.
Luca Bortolussi (Univ. of Trieste, Italy)Herbert Wiklicky (Imperial College London, UK)
Abstract submission: 16 December 2012Paper submission: 20 December 2012Notification: 20 January 2013Camera ready: 3 February 2013
Strategic reasoning is one of the most active research area in multi-agent system domain. The literature in this field is extensive and provides a plethora of logics for modeling strategic ability. Theoretical results in this area are now being used in many exciting domains, including software tools for information system security, robot teams with sophisticated adaptive strategies, and automatic players capable of beating expert human adversary, to cite a few. All these examples share the challenge of developing novel theories and tools for agent strategies that take into account the likely behavior of adversaries. This workshop aims to bring together researchers working on different aspects of strategic reasoning, both from a theoretical and a practical point of view.
The topics covered by the conference include, but are not limited to, the following:
Aniello Murano (Univ of Napoli Federico II, Naples, Italy) Fabio Mogavero (Univ of Napoli Federico II, Naples, Italy) Moshe Y. Vardi (Rice University, Houston, USA)
Abstract submission: 15 December 2012Paper submission: 20 December 2012Notification: 17 January 2013Camera ready: 31 January 2013
Dates: Saturday March 16th, 2013 and Sunday March 17th, 2013
The advantage of computing with graphs rather than terms is that common subexpressions can be shared, improving the efficiency of computations in space and time. Sharing is ubiquitous in implementations of programming languages : many functional, logic, object-oriented and concurrent calculi are implemented using term graphs. Research in term and graph rewriting ranges from theoretical questions to practical implementation issues. Different research areas include: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the use of graphical frameworks such as interaction nets and sharing graphs (optimal reduction), rewrite calculi for the semantics and analysis of functional programs, graph reduction implementations of programming languages, graphical calculi modelling concurrent and mobile computations, object-oriented systems, graphs as models of biological or chemical abstract machines, and automated reasoning and symbolic computation systems working on shared structures.
Rachid Echahed (IMAG, Grenoble, France) Detlef Plump (Univ. of York, UK)
This workshop focuses on verification and testing of software change and upgrades. Software is usually not written all at once, but is built incrementally, due to several reasons:
Changes are done frequently during the lifetime of most systems and can introduce software errors that were not present in the old version, or expose errors that were present before but did not get exercised. In addition, upgrades are done gradually, so the old and new versions have to co-exist in the same system. This workshop will address the issue of efficient and reliable verification of system changes and upgrades by means of formal verification and dynamic analysis techniques.
Hana Chockler (IBM Research, Haifa, Israel) Giovanni Denaro (Univ. of Milano Bicocca, Italy) Daniel Kroening (Oxford Univ., UK) Leonardo Mariani (Univ. of Milano Bicocca, Italy) Natasha Sharygina (Univ. of Lugano, Switzerland)
Paper submission: 20 December 2012Author notification: 20 January 2013Camera ready version: 30 January 2013
We have 38 guests and no members online