December 2022 - FMIndia - mail.cmi.ac.in

IARCS Verification Seminar Series -- Talk by Umang Mathur on Jan 3 at 1900 hrs IST
by VSS IARCS 30 Dec '22

30 Dec '22

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Umang Mathur, an Assistant Professor in the School of Computing at the National University of Singapore. The talk is scheduled on Tuesday, January 3, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MWVtZzZuZn…> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/) and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Dynamic Data Race Prediction: Fundamentals and Advance Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. Data races are arguably the most insidious amongst concurrency bugs and extensive research efforts have been dedicated to effectively detect them. A data race occurs when memory-conflicting actions are executed concurrently. Consequently, considerable effort has been made towards developing efficient techniques for race detection. The preferred approach to detect data races is through dynamic analysis, where one observes an execution of a concurrent program and checks for the presence of data races in the execution observed. Traditional dynamic race detectors rely on Lamport's happens-before (HB) partial order, which can be conservative and are often unable to discover simple data races, even after executing the program several times. Dynamic data race prediction aims to expose data races, that can be otherwise missed by traditional dynamic race detectors (such as those based on HB), by inferring data races in alternate executions of the underlying program, without re-executing it. In this talk, I will talk about the fundamentals of and recent algorithmic advances in data race prediction. Bio: Umang Mathur is an Assistant Professor at the National University of Singapore. He received his PhD from the University of Illinois at Urbana Champaign in 2021 and was an NTT Research Fellow at the Simons Institute for the Theory of Computing at Berkeley. His research interests lie in the use of formal methods and logic for answering design, analysis and implementation questions in programming languages, software engineering and systems. He is a recipient of a Google Research Award (2022), Google PhD Fellowship (2019), an ACM SIGSOFT Distinguished Paper Award at ESEC/FSE'18, a Best Paper Award at ASPLOS'22 and was invited as a Young Researcher at the 8th Heidelberg Laureate Forum.

1 0

Deadline extension : ICECCS 2023 (Toulouse, France)
by Étienne André 14 Dec '22

14 Dec '22

ICECCS 2023 - Call for Papers *************************************************************************************** 27th International Conference on Engineering of Complex Computer Systems (ICECCS 2023) 12 - 16 June 2023, Toulouse, France https://www.irit.fr/iceccs2023/ *************************************************************************************** NEW! paper submission deadline extended to 16th January 2023. The 27th International Conference on Engineering of Complex Computer Systems (ICECCS 2023) is a well-established event that has been held around the world for over 25 years. Over the past years, we have seen a rapidly rising emphasis on the design, implementation and management of complex computer systems which are present in every aspect of human activities, such as manufacturing, communications, defence, transportation, aerospace, hazardous environments, energy, and healthcare. These complex systems are frequently distributed over heterogeneous networks and process a large amount of data. Complexity arises from many factors, including the dynamic environment and the scenarios these systems operate in, demanding and sometimes conflicting requirements in functionality, efficiency, scalability, security, dependability and adaptability, as well as the wide range of development methodologies, programming languages and implementation details. Performance, real-time behaviour, fault tolerance, security, adaptability, development time and cost, and long life concerns are some of the key issues arising in the development of such systems. The goal of this conference is to bring together industrial, academic, and government experts from a variety of application domains and software disciplines, to discuss how the disciplines' problems and solution techniques interact within the whole system. Researchers, practitioners, tool developers and users, and technology transfer experts are all welcome. The scope of the conference includes long-term research issues, near-term requirements and challenges, established complex systems, emerging promising tools, and retrospective and prospective reflections of research and development into complex systems. List of Topics -------------- Authors are invited to submit papers describing original, unpublished research results, case studies and tools. Papers are solicited in all areas related to complex computer-based systems, including the causes of complexity and means of avoiding, controlling, or coping with complexity. Topic areas include, but are not limited to: + Requirements analysis and specification + Verification and validation + Security and privacy of complex systems + Model-driven development + Reverse engineering and refactoring + Software Architecture + Human Machine Interaction + Big data management + Ubiquitous computing, context awareness, sensor networks + SAT/SMT solvers for software analysis and testing + Agile methods + Safety-critical and fault-tolerant architectures + Adaptive, self-managing and multi-agent systems + Cyber-physical systems and Internet of Things (IoT) + Industrial case studies Different kinds of contributions are sought, including novel research, lessons learned, experience reports, and discussions of practical problems faced by industry and user domains. The ultimate goal is to build a rich and comprehensive conference program that can fit the interests and needs of different classes of attendees: professionals, researchers, managers, and students. A program goal is to organize several sessions that include both academic and industrial papers on a given topic and culminate panels to discuss relationships between industrial and academic research. Submission and Publication -------------------------- Full papers are divided into two categories: Technical Papers and Experience Reports. The papers submitted to both categories will be reviewed by the program committee members, and papers accepted in either category will be published in the conference proceedings. Technical papers should describe original research, and experience reports should present practical projects carried out in the industry, and reflect on the lessons learnt from them. Short paper submissions describe early-stage, ongoing or PhD research. All short papers will be reviewed by the program committee members, and accepted short papers will be published in the conference proceedings. Submissions to the conference must not have been published or be concurrently considered for publication elsewhere. All submissions will be judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the conference. The proceedings have been published by the Conference Publishing Services (CPS) of the IEEE Computer Society. Submitted manuscripts should be in English and formatted in the style of the double-column IEEE CPS format. Full papers should not exceed 9 pages + 1 page for bibliography, and short papers should not exceed 5 pages + 1 page for bibliography, including figures, references, and appendices. All submissions should be in PDF format. Submissions not adhering to the specified format and length may be rejected immediately without review. Please prepare your manuscripts in accordance with the IEEE CPS guidelines. https://www.ieee.org/conferences/publishing/templates.html We invite all prospective authors to submit their manuscripts via the ICECCS 2023 portal, hosted by the EasyChair conference management system. https://easychair.org/conferences/?conf=iceccs2023 Important Dates --------------- + Abstract Submissions Due: 08 December, 2022 ==> EXTENDED to 9th January 2023 + Full Paper Submissions Due: 15 December, 2022 ==> EXTENDED to 16th January 2023 + Acceptance/Rejection Notification: 15 March, 2023 + Camera-ready Due: 15 April, 2023 + Conference Dates: 12-16 June 2023 General Chair ------------- Dominique Méry, LORIA, Université de Lorraine, Nancy, France Program Committee Co-Chairs --------------------------- Yamine Ait-Ameur, IRIT-ENSEEIHT, Toulouse, France Ferhat Khendek, Concordia University, Montreal, Canada Program Committee ----------------- see https://www.irit.fr/iceccs2023/ ICECCS 2023 is referenced on https://www.conferences-computer.science/

1 0

IARCS Verification Seminar Series -- Talk by Krishna S on Dec. 6 at 1900 hrs IST
by VSS IARCS 05 Dec '22

05 Dec '22

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Krishna S, a faculty member in the Department of Computer Science and Engineering at IIT Bombay. The talk is scheduled on Tuesday, December 6, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MWU1amtjNG…> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/) and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Verification of Concurrent Programs under Release Acquire Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: This is an overview of some recent work on the verification of concurrent programs. Traditionally concurrent programs are interpreted under sequential consistency (SC). Eventhough SC is very intuitive and easy to use, modern multiprocessors do not employ SC for performance reasons, and instead use so called "weak memory models". Some of the well known weak memory models in vogue among modern multiprocessor architectures are Intel x-86, IBM POWER and ARM. The use of weak memory is also prevalent in the C11 model, leading to the release acquire fragment of C11. This talk is on the verification of concurrent programs under the release acquire (RA) semantics. The main focus of the talk will be on non parameterized programs under RA, and I will briefly discuss results in the parameterized setting. In the non parameterized setting, we show that the reachability problem for RA is undecidable even in the case where the input program is finite-state, closing a long standing open problem. What works well for this class is under approximate reachability, in the form of bounded view switching, an analogue of bounded context switching, relevant to RA. In the parameterized setting, the first observation is that the semantics of RA can be simplified, lending to a better complexity for verification. Further, safety verification is PSPACE-complete for the case where the distinguished threads are loop-free, and jumps to NEXPTIME-complete for the setting where an unrestricted distinguished ego thread interacts with the environment threads. This talk is based on papers that appeared in PLDI'19 (joint with Parosh Abdulla, Mohamed Faouzi Atig and Jatin Arora), PODC'22 (joint with Roland Meyer, Adwait Godbole and Soham Chakraborty), and Arxiv'21 (with Roland Meyer and Adwait Godbole). Bio: Krishna S is a faculty member in the Department of Computer Science and Engineering at IIT Bombay. Her areas of research are broadly in Automata, Logics, Games and the formal verification of timed and probabilistic systems.

1 0