November 2023 - FMIndia

Tutorial on Civl verifier for concurrent programs @ POPL 2024, January 14, 2024

by Shaz Qadeer

Constantin Enea and Shaz Qadeer will present a tutorial on the Civl verifier <https://popl24.sigplan.org/details/POPL-2024-tutorialfest/1/Scaling-Verific…> at POPL 2024 on Sunday January 14, 2024. If you are interested in automated and scalable reasoning about concurrent systems, you will find Civl of interest! A brief description of the tutorial contents is included below. ============================== Objectives: The tutorial aims to introduce the functionality of the Civl verifier, discuss its applicability and limitations, and a comparison with the state of the art. We will start with a description of practically important programming models that exhibit concurrency and require attention from verification researchers. Next, we will present an overview of trends in methods and tools for static verification of concurrent systems. Finally, we will present the different components and proof tactics implemented in Civl using illustrative examples and case studies. Topics to be covered: The tutorial will be structured in several sections that address the objectives mentioned above. 1. Classes of concurrent systems whose construction deserve reasoning support: - concurrent tasks operating on shared-memory (locks, non-blocking algorithms, weak memory, GPU programs) - processes communicating via channels, RPCs (distributed systems) - hardware controllers (memory controllers, pipelined processors), mixed hardware-software controllers (embedded systems) 2. Overview of trends in static concurrency reasoning: - Powering up program logics: extensions of Floyd-Hoare such as Owicki-Gries, Rely-Guarantee, Concurrent Separation Logic, etc. - The approach in Civl: amplifying simple program logics via orthogonal methods such as commutativity, linear types, refinement - Proof discovery: heuristic automation of proofs atop a particular proof system (much like the automation of type inference atop type checking) 3. Programming model of Civl: structured programs with possibly parallel and asynchronous procedure calls 4. Verification in Civl: - Yield invariants: noninterference reasoning that is as precise as Owicki-Gries and as compositional as rely-guarantee - Mover types: reduce interference using verification conditions for checking commutativity of atomic actions and a type system based on Lipton’s reduction - Ownership: disjoint distribution of resources ensured via linear types and verification conditions 5. Layered refinement in Civl: - Lifting refinement over transition systems to refinement over structured programs - A refinement chain of structured programs expressed as a single layered program - Each link in the refinement chain justified by a simulation proof supported by verification methods noted in #4 Presentation approach: The presentation will be driven by examples to illustrate challenges, explanation of core methods accessible to non-experts, and tool demonstration. Target audience: Researchers interested in concurrent systems, program analysis, and program verification Prerequisite knowledge: Logic, invariants, verification conditions, program analysis

1 year

1
0
0 0

IARCS Verification Seminar Series -- Talk by Madhusudan Parthasarathy on Nov. 28 at 1900 hrs IST

by VSS IARCS

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Madhusudan Parthasarathy, a Professor of Computer Science at the University of Illinois at Urbana-Champaign. The talk is scheduled on Tuesday, Nov. 28, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MzViZ3N0an…> ). 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: Learning Logical Expressions Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: We consider the problem of learning logical formulas/expressions that work as classifiers of structures. Logic learning has many applications ranging from program synthesis from input-output examples, learning specifications from code (contracts and inductive invariants), interpretable concept learning in AI, synthesizing lemmas to help prove theorems, finding axiomatizations, and, more generally, replacing certain creative tasks that currently require human help in many applications. We will first motivate logic learning using the applications above. We then will turn a theory lens to this problem by considering when the logic learning problem is *decidable*. We show a general technique using tree automata that realize learning algorithms for a variety of logics/languages ranging from fragments of FOL, regular expressions, temporal logics, grammars, to string transformation for Excel (as in Flashfill). We in fact will show a *meta-theorem* that can be used to show a logic is decidable simply by programming a particular kind of evaluator for its semantics. This theory suggests that many logics can be learned by using Version Space Algebras (VSAs) based on tree automata. If time permits, we will also consider the problem of learning logics themselves to aid few-shot learning. Bio: Madhusudan Parthasarathy is a Professor of Computer Science at the University of Illinois at Urbana-Champaign. He has worked on several projects that turn the theory lens to problems in software verification including visibly pushdown languages, ICE-learning for learning inductive invariants, and natural proofs for proving programs that manipulate data structures. His current interests are in software verification, program synthesis, and trustworthy AI.

1 year

1
0
0 0

8th Indian SAT+SMT School -- Second call for participation & short/poster presentation

by Kumar Madhukar

Dear all, The 8th edition of the Indian SAT+SMT School will be held during 15-17 December 2023, at IIIT Hyderabad, co-located with FSTTCS 2023. Please visit the webpage (https://sat-smt.in/index.html) for registration and other details. Regular registration for the school closes on Nov. 28th. We are also inviting entries for short talks and poster presentations, in the broad area of SAT/SMT, through this Google form: https://forms.gle/6NdFgcJUaEedwaTQ8 Please submit your entries by Dec. 3rd (extended). Note that a print-out of the presentation slides may be used in place of posters during the poster presentation. We look forward to your participation. Needless to say, we'd be very happy to clarify any questions you might have in this regard. Feel free to write to us at indian.satsmt.school(a)gmail.com < mailto:indian.satsmt.school@gmail.com <indian.satsmt.school(a)gmail.com>>. Best regards, Supratik Chakraborty, IIT Bombay Ashutosh Gupta, IIT Bombay Saurabh Joshi, SupraOracles Kumar Madhukar, IIT Delhi Kuldeep Meel, NUS Subhajit Roy, IIT Kanpur Subodh Sharma, IIT Delhi

1 year

1
0
0 0

Call For Abstracts for 1st Workshop on GenAI based Software Engineering (https://genai4se.github.io/ISEC-Workshop/)

by Raveendra Medicherla

TCS Confidential Dear All, We are excited to announce 1st Workshop on GenAI based Software engineering. About: The Software Development Life Cycle (SDLC) governs the creation of software systems, encompassing different engineering phases such as requirement specification, design, coding, testing, and maintenance. Software development is an effort-intensive and time-consuming activity. Most complex, large-scale software systems of today derive their requirements from existing (legacy) software and partial (incomplete) descriptions. Thus, expertise from subject matter experts (SMEs) is essential at each phase, which brings in the important component of knowledge. The emergence of Generative AI techniques holds the potential to empower SMEs to construct purposeful engineering artifacts using natural language interactions. Objective: The proposed workshop (https://genai4se.github.io/ISEC-Workshop/) aims to provide a collaborative platform for researchers from the academia industry, and practitioners. Through this platform, we expect to delve into the convergence of Generative AI, Knowledge Engineering, MDE, Software Understanding, and Software Transformation. This workshop is a part of 17th ISEC 2024 conference (https://conf.researchr.org/home/isec-2024) that will be held at Bangalore, India, from 22nd Feb to 24th Feb 2024 . Call for Abstracts: We solicit submissions in the form of one-page (max 500 words) abstracts describing case studies, interesting experiments, best practices, and lessons learned while applying Generative AI to various SE areas, but not limited to the following topics: * Requirements Engineering * Software Design, Architecture * Software Development * AI Code Assistants * Software Verification, Testing and Debugging * Software Evolution and Maintenance * Legacy Modernization * Reverse Engineering from code, documents * Responsible AI * Human interaction with LLMs Submission link: https://forms.gle/4UqNFpSJb6hSbnxq6 Acceptance criteria: Abstracts will be selected based on reviews by members of the workshop organizing committee. The criteria will be the clarity of articulation of the problem being solved, bringing out the specific need for Generative AI to solve the problem and the novelty of the approach. Authors of accepted abstracts will receive further instructions for submitting camera-ready presentations. At least one of the authors MUST register for the ISEC conference to present their paper. Important Dates * Last date for submitting abstracts: 15 Dec 2023 * Notification of Selected Abstracts: 5 Jan 2024 * Camera Ready submission: 10 Jan 2024 Contact: GenAIForSe.ISECWorkshop(a)tcs.com<mailto:GenAIForSe.ISECWorkshop@tcs.com> GenAIForSe(a)gmail.com<mailto:GenAIForSe@gmail.com> Organizers: Raveendra Kumar M , TCS Research Ravindra Naik, TCS Research, Asha Rajbhoj, TCS Research Manasi Patwardhan, TCS Research Regards M. Raveendra Kumar, Principal Scientist, TCS Research, TCS, Bangalore. TCS Confidential =====-----=====-----===== Notice: The information contained in this e-mail message and/or attachments to it may contain confidential or privileged information. If you are not the intended recipient, any dissemination, use, review, distribution, printing or copying of the information contained in this e-mail message and/or attachments to it are strictly prohibited. If you have received this communication in error, please notify us by reply e-mail or telephone and immediately and permanently delete the message and any attachments. Thank you

1 year

1
0
0 0

Student Poster Session, ISEC 2024

by Madhavan Mukund

----- Forwarded message from IMT2019057 Nandakishore S Menon <Nandakishore.Menon(a)iiitb.ac.in> ----- From: IMT2019057 Nandakishore S Menon <Nandakishore.Menon(a)iiitb.ac.in> Date: Sun, 26 Nov 2023 06:26:10 +0000 Greetings all, We hope this message finds you well. We wish to remind you about the approaching deadline for the Student Poster Session at the Innovations in Software Engineering Conference (ISEC) 2024. Please be informed that the submission deadline is Friday, 8th December 2023. Student Posters Session is a forum for students to present their research work to the conference attendees. It is an excellent opportunity for students to get feedback, learn how to clearly communicate their research, and network with the leading experts in the field. For more details regarding eligibility and guidelines to submit your contribution, please visit the Student Posters Session track page: https://conf.researchr.org/track/isec-2024/isec-2024-student-posters-session Don't miss out on this opportunity to showcase your research at ISEC 2024. We look forward to your valuable contributions. Best Regards, ISEC 2024 Publicity Team Organising Team General Chair Sujit Kumar Chakrabarti (IIIT Bangalore) Organising Co-Chairs Raghavan Komondoor (IISc, Bangalore) Raveendra Kumar Medicherla (TCS Research) Program Co-Chairs (Research Track) Sudipto Ghosh (Colorado State University, USA) Aseem Rastogi (Microsoft Research, India) Workshops and Tutorial Track Co-Chairs Manas Thakur (IIT Bombay, India) Sruti Srinivasa Ragavan (IIT Kanpur, India) Software Engineering in Practice Co-Chairs Manoj Dixit (MathWorks, India) Tukaram Muske (Synopsis, India) PhD Symposium Chair Subhajit Roy (IIT Kanpur, India) ----- End forwarded message -----

1 year

1
0
0 0

Internships at SupraOracles

by Madhavan Mukund

----- Forwarded message from Saurabh Joshi <s.joshi(a)supraoracles.com> ----- From: Saurabh Joshi <s.joshi(a)supraoracles.com> To: madhavan(a)cmi.ac.in Date: Tue, 21 Nov 2023 12:44:05 +0530 We would like to hire an intern (for up to 6 months) with FM background being essential (First Order Logic, Hoare Logic, Pre/Post conditions, Loop invariants) and a good command over any one of the imperative programming languages. Knowledge/experience with model checkers and/or SMT solvers would certainly be a plus. With the internship, we plan to explore the expressivity of the Move specification language, to enable Move Prover to prove properties about smart contracts written in the Move programming language. Possibly also explore internals of Move Prover and how Move is being modelled and whether any modifications/improvement would aid in formal verification of the smart contracts. Suitable interested candidates may apply here: https://supraoracles.com/careers/4967045004/ *--------------------------------------------------------------------------* *Saurabh Joshi* *Principal Researcher | SupraOracles* Current Timezone: New Delhi, India (GMT+5:30) Learn more and connect with SupraOracles here <https://linktr.ee/supraoracles>. ----- End forwarded message -----

1 year, 1 month

1
0
0 0

IARCS Verification Seminar Series -- Talk by Madhusudan Parthasarathy on Nov. 28 at 1900 hrs IST

by VSS IARCS

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Madhusudan Parthasarathy, a Professor of Computer Science at the University of Illinois at Urbana-Champaign. The talk is scheduled on Tuesday, Nov. 28, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MzViZ3N0an…> ). 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: Learning Logical Expressions Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: We consider the problem of learning logical formulas/expressions that work as classifiers of structures. Logic learning has many applications ranging from program synthesis from input-output examples, learning specifications from code (contracts and inductive invariants), interpretable concept learning in AI, synthesizing lemmas to help prove theorems, finding axiomatizations, and, more generally, replacing certain creative tasks that currently require human help in many applications. We will first motivate logic learning using the applications above. We then will turn a theory lens to this problem by considering when the logic learning problem is *decidable*. We show a general technique using tree automata that realize learning algorithms for a variety of logics/languages ranging from fragments of FOL, regular expressions, temporal logics, grammars, to string transformation for Excel (as in Flashfill). We in fact will show a *meta-theorem* that can be used to show a logic is decidable simply by programming a particular kind of evaluator for its semantics. This theory suggests that many logics can be learned by using Version Space Algebras (VSAs) based on tree automata. If time permits, we will also consider the problem of learning logics themselves to aid few-shot learning. Bio: Madhusudan Parthasarathy is a Professor of Computer Science at the University of Illinois at Urbana-Champaign. He has worked on several projects that turn the theory lens to problems in software verification including visibly pushdown languages, ICE-learning for learning inductive invariants, and natural proofs for proving programs that manipulate data structures. His current interests are in software verification, program synthesis, and trustworthy AI.

1 year, 1 month

1
0
0 0

Funded PhD Positions at Boston University

by Ankush Das

Hi all, I am excited to announce that I will be joining Boston University as a tenure-track assistant professor, and I am looking for motivated PhD students starting in Fall 2024. My research interests are broadly in the area of programming languages, with applications in cryptography, distributed systems, and recently in probabilistic and machine learning models. More specifically, my research centers around building type systems for verification and quantitative analysis of concurrent programs with applications in aforementioned areas. You can find more details about my research on my webpage: https://ankushdas.github.io/ If you are interested in working with me, please reach out to me directly and/or apply to the PhD program at BU (details below). Beyond my research, the Principles of Programming and Verification group at Boston University (https://www.bu.edu/cs/research/popv/) has funded PhD positions for several exciting projects. Two examples below: Marco Gaboardi (https://cs-people.bu.edu/gaboardi/) works at the intersection of programming languages, formal verification, and differential privacy. Alley Stoughton (https://alleystoughton.us/) works mainly on using the EasyCrypt proof assistant to mechanize proofs of the security of cryptographic protocols. She leads the EasyUC project on mechanizing security proofs in the universally composable security framework ( https://github.com/easyuc/EasyUC). Details on how to apply: - Application deadline: December 15, 2023 - Our PhD applications web info: https://www.bu.edu/cs/phd-program/phd/ - Our Admissions FAQ page: https://www.bu.edu/cs/phd-program/phd/faqs-about-graduate-admissions-financ… - Visit day: March 25, 2024 Thanks, Ankush

1 year, 1 month

1
0
0 0

CFP : Theme Issue: Indic Mathematical Systems - Scientiae Mathematicae Japonicae (SCMJ)

by gopal＠annauniv.edu

Please find the Call For Papers on the theme "Indic Mathematical Systems" at: https://easychair.org/cfp/SCMJIMS24 As you would appreciate this is for one of the most reputed Journals Scientiae Mathematicae Japonicae (SCMJ). I am serving as the Guest Editor for this theme issue on "Indic Mathematical Systems". Sincerely, Gopal T V 0 9840121302 https://vidwan.inflibnet.ac.in/profile/57545 https://www.facebook.com/gopal.tadepalli ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Dr. T V Gopal Professor Department of Computer Science and Engineering College of Engineering Anna University Chennai - 600 025, INDIA Ph : (Off) 22351723 Extn. 3340 (Res) 24454753 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

1 year, 1 month

1
0
0 0

CFP : Theme Issue: Indic Mathematical Systems - Scientiae Mathematicae Japonicae (SCMJ)

by gopal

Please find the Call For Papers on the theme "Indic Mathematical Systems" at: https://easychair.org/cfp/SCMJIMS24 As you would appreciate this is for one of the most reputed Journals Scientiae Mathematicae Japonicae (SCMJ). I am serving as the Guest Editor for this theme issue on "Indic Mathematical Systems". Sincerely, Gopal T V 0 9840121302 https://vidwan.inflibnet.ac.in/profile/57545 https://www.facebook.com/gopal.tadepalli ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Dr. T V Gopal Professor Department of Computer Science and Engineering College of Engineering Anna University Chennai - 600 025, INDIA Ph : (Off) 22351723 Extn. 3340 (Res) 24454753 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

1 year, 1 month

1
1
0 0

2024

2023

2022

FMIndia November 2023