Helmut Veith is a founding member of the Austrian Society for Rigorous Systems Engineering

The Austrian Society for Rigorous Systems Engineering (ARiSE) was founded in 2010 to further the research in formal methods for the design of correct computer systems. It brings together top researchers in formal methods in Austria in order to foster collaboration and a common research platform.

CfP: Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2 2010)

The annual Workshop on Exploiting Concurrency Efficiently and Correctly (EC2) is a forum that brings together researchers working on formal methods for concurrency, and those working on advanced parallel applications. Its goal is to stimulate incubation of ideas leading to future concurrent system design an verification tools that are essential in the multi-core era.

CfP: 7th International Colloquium on Theoretical Aspects of Computing (ICTAC 2010)

ICTAC 2010 is the 7th International Colloquium on Theoretical Aspects of Computing, the latest in a series founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). ICTAC 2010 will bring together practitioners and researchers from academia, industry and government to present research and to exchange ideas and experience addressing challenges in both theoretical aspects of computing and in the exploitation of theory through methods and tools for system development. Our other main purpose is to promote cooperation in research and education between participants and their institutions, from developing and industrial countries, as in the mandate of the United Nations University. The previous ICTAC events were held in Guiyang, China (2004), Hanoi, Vietnam (2005), Tunis, Tunisia (2006), Macau (2007), Istanbul, Turkey (2008) and Kuala Lumpur, Malaysia (2009). ICTAC 2010 includes two special tracks: the first on the Grand Challenge on Verified Software, the second on Formal Approaches to Testing.

CfP: Formal Methods in Computer Aided Design (FMCAD 2010)

FMCAD 2010 is the tenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing. FMCAD 2010 will have several invited speakers, a panel of foremost academic and industrial experts, a high-quality technical program. The first day is reserved for tutorials.

CfPart: Workshop on Invariant Generation (WING 2010)

This third International Workshop on Invariant Generation brings together researchers from abstract interpretation, computational logics, computer algebra and model checking to exchange their newest research on invariant generation techniques and applications.

CfP: 8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010)

The purpose of ATVA is to promote research on theoretical and practical aspects of automated analysis, verification and synthesis in East Asia by providing a forum for interaction between the regional and the international research communities and industry in the field. The previous six events were held in Taiwan (2003-5), Beijing (2006), Tokyo (2007), Seoul (2008) and Macao (2009). The proceedings of ATVA 2010 will be published by Springer as a volume in the LNCS series.

CfPart: 22nd International Conference on Computer Aided Verification (CAV 2010)

CAV 2010 is the 22nd in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. This year, CAV is part of the 5th International Federated Logic Conference (FLoC 2010), which includes CAV and seven other conferences/symposia: CSF, ICLP, IJCAR, ITP, LICS, RTA and SAT.

CAV considers it vital to continue its leadership in hardware verification, maintain its recent momentum in software verification, and consider new domains such as biological systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. A selection of papers will be invited to a special issue of the International Journal on Formal Methods in System Design.

Dagstuhl Seminar on Decision Procedures in Software, Hardware and Bioware

Efficient and scalable decision procedures for satisfiability, or dually validity, of logical formulas are crucial for many applications. For example, domains used in software and hardware analysis, such as arithmetic over integers, real numbers and bit-vectors can each be solved by specialised solvers, and various combination methods allow for integrating such solvers. At the same time, cross-fertilisation is taking place with other research and application areas, with important synergies for sharing theoretical foundations, heuristics and implementation techniques. For example, decision procedures for propositional logic and its extensions are now being applied in fields such as Scheduling, Biology, Medicine, Cryptography, and Linguistics.

Research in the field focuses on three key ingredients: the theory of decision procedures and their combination, implementation of Satisfiability Modulo Theory (SMT) solvers, and their applications in various areas. The area is highly fascinating since it is one where a sophisticated theory meets practice. Recent practical applications have acted as catalysts for theoretical advances that have in terms led to dramatically improved technologies. We firmly believe that new theory and new methods can increase efficiency of systems by orders of magnitude: the area is thriving with ideas. We also expect new applications of solvers to various problems to appear.

This seminar will bring together renowned as well as young aspiring researchers who work on the key ingredients covered in the seminar: theory, implementation, and applications.

CfP: 19th EACSL Annual Conference on Computer Science Logic (CSL 2010)

Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL).

The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science.

CfPart: 5th International Computer Science Symposium in Russia (CSR 2010)

The 5th International Computer Science Symposium in Russia, CSR 2010, will take place on June 16-20 2010 at the Institute of Informatics of the Tatarstan Academy of Sciences, and Kazan State University, located in Kazan, Russia.

Purpose and Scope: This is an annual conference that intends to reflect the broad scope of international cooperation in computer science. In 2006-2009 the symposium consisted of two tracks: Theory Track and Applications and Technology Track, and in 2010 it will have single track. The topics covered vary from year to year, but in general try to cover as much of the contemporary computer science as possible.