- FMIndia - example.com

Internship opportunity for formal methods PhD students at GE Aerospace India

by Supratik Chakraborty

I am posting this on behalf of Samhitha Palanganda Poonacha (GE Aerospace) <samhitha.poonacha(a)ge.com>. Please contact Samhitha directly for any queries. ===================== The current V&V process we have for our aircraft engine controls software is fairly involved and manual. The European regulating agencies have mandated a change GE’s V&V process which means much more manual effort for us going forward each time we want to certify our engine controls software. The Research team at Bangalore is currently involved in one such V&V exercise and have identified many opportunities where we can find the right balance between innovation and deploying formal methods that can significantly improve the productivity for the team. We are looking for an intern with a formal methods background who is curious to see what happens to automation in a very complex set up, an aircraft engine, and some of the real-world challenges we need to deal with when designing solutions. To give you an idea: Number of requirements in thousands and written up by a wide variety of people where for many, English is not the primary language, this alone can make things very challenging. The work would involve both supporting some of the V&V activities as well as designing proof-of-concepts for proposed process refinements. Exposure to engineering challenges while being part of a multi-disciplinary unit will be some things the intern can stand to gain. The team itself has folks from a variety of technical backgrounds and additionally solving an array of AI/NLP applications for GE Aerosapce. Ideally we would like someone who can work with us for ~6 months. Job Posting: https://ge.wd5.myworkdayjobs.com/GE_ExternalSite/job/Bengaluru/Research-Int… We can also make the option of a post-doc possible in case someone is interested to see what applied research at GE Aerospace looks like.

1 year, 6 months

1
0
0 0

FAACS 2024 - Call for Research Papers

by Nadeem Abbas

Dear all, We hope you will be doing great. We are writing this to you for the 8th International Workshop on Formal Approaches for Advanced Computing Systems. Please consider the below call, submit your work and join us for the workshop. Also please help us to circulate the call by sharing with your network. Call for Papers: FAACS 2024 The 8th International Workshop on Formal Approaches for Advanced Computing Systems (FAACS 2024), co-located with the 21st IEEE International Conference on Software Architecture (ICSA 2024), will be held in IIIT Hyderabad, India June 4-8, 2024. Web: https://faacs-workshop.github.io/2024/ Twitter/X handle: @faacs_ws Important Dates: – Submission Deadline: February 18, 2024 – Notification of Papers: March 17, 2024 – Camera Ready: March 31, 2024 – Workshop Date: June 4 – 5, 2024 *** Motivation and Scope *** Cutting-edge technologies, infrastructures, and computational paradigms such as digital twin, cloud, fog, edge computing, IoT, digitalization, Industry 5.0, and cyber-physical systems are changing how data and services are delivered and used. Such systems have a significant and elaborate societal impact, making it paramount to guarantee essential qualities of the delivered product, such as dependability, reliability, safety, and availability. As new paradigms become pervasive in our everyday lives, new challenges also emerge in dealing with uncertainty, untrustworthiness, and information loss, affecting the software life cycle in different phases. Ensuring critical qualities requires a joint effort in devising advanced software architecture designs by the software architecture community and formal modeling and verification approaches by the formal methods community. The main goal of the workshop is to foster integration between formal methods and software architecture promoting new connections and synergies between the two communities to address the challenges of the upcoming generation of computing systems. Aligned with the theme of the ICSA 2024, we welcome contributions on the potential and risks of generative AI in developing advanced software architectures and ensuring qualities like dependability, reliability, safety, and availability through formal modeling and verification. *** Topics of Interest include (but are not limited to) the following: *** - requirements formalization and formal specification, with or without the use of generative AI; - formal/semi-formal architecture design, validation and verification, quality analysis and evaluation; - formal/semi-formal approaches to digitalization, development of digital society and Digital Twins; - methodologies and approaches focusing on addressing challenges of modern computing systems that are currently addressed ad-hoc; - architecture description languages and metamodels; - architectural patterns, styles and tactics, viewpoints and views; - architecture transformation and refinement, architecture based synthesis; - model-driven engineering; - approaches and tools for verification and validation; - performance analysis based on formal approaches; - compliance assurance using formal methods; - application of methodologies, theories, approaches and techniques specific to the aforementioned areas to AI-based, autonomous, robotic, cyber-physical, and self-adaptive systems; - use of generative AI for aforementioned areas - reports on practical experience in the application of formal methods to industrial case studies. *** Types of Papers *** FAACS 2024 solicits: Full papers (Max 8 pages including references): original research contributions, case studies, or report on work or experiences in industry; Short papers (Max 4 pages including references): work-in-progress, new and emerging ideas, techniques and/or tools or extensions not fully validated yet, or outstanding challenges along with possible approaches for resolving them. *** Best Paper Award *** Based on the reviews and PC discussion, up to two papers will be selected for the Best Paper Award. *** Submission *** All submissions will follow the IEEE Computer Science proceedings format. Submitted papers must be written in English and conform to the the IEEE Guidelines including the guidelines for AI-Generated text. Submissions must be done before the deadline in PDF format via via the EasyChair submission system. *** Panel Discussion *** We are planning to have an expert panel session related to above specified topics of interest. Please contact the program co-chairs if you are interested in joining the expert panel or would like to nominate someone who you would like to be part of the expert panel. Program Co-chairs Nadeem Abbas, Linnaeus University, Sweden, (nadeem.abbas(a)lnu.se<mailto:nadeem.abbas@lnu.se>) Livia Lestingi, Politecnico di Milano, Italy, (livia.lestingi(a)polimi.it<mailto:livia.lestingi@polimi.it>) Patrizia Scandurra, University of Bergamo, Italy, (patrizia.scandurra(a)unibg.it<mailto:patrizia.scandurra@unibg.it>) Steering Committee – Paolo Arcaini, National Institute of Informatics, Japan – Matteo Camilli, Free University of Bozen-Bolzano, Italy – Marina Mongiello, Politecnico di Bari, Italy – Elvinia Riccobene, University of Milan, Italy – Patrizia Scandurra, University of Bergamo, Italy Regards Nadeem __________________________________________ Nadeem Abbas, PhD Senior Lecturer/Assistant Professor Linnaeus University Department of Computer Science and Media Technology 351 95 Växjö Sweden +46-470-767411 (office) +46-702-017249 (Mobile) +46-470-84004 (Fax) nadeem.abbas(a)lnu.se<mailto:nadeem.abbas@lnu.se> https://lnu.se/en/staff/nadeem.abbas/ __________ Call for Submissions: I am Program Chair for the 8th International Workshop on Formal Approaches for Advanced Computing Systems<https://faacs-workshop.github.io/2024/>, which will be colocated with ICSA 2024<https://conf.researchr.org/home/icsa-2024> at IIIT Hyderabad India. The call for submission of papers will be released soon. It will be great if you yourself can make a submission and also request your network to submit. ICSA is a premier conference on software architecture and accepted papers are published in ICSA Companion proceedings, and indexed in IEEE Xplore Digital Library.

1 year, 6 months

1
0
0 0

Call for papers: SAT 2024

by Supratik Chakraborty

(Apologies for cross-postings, if any) SAT 2024 is the 27th edition of the International Conference on Theory and Applications of Satisfiability Testing (SAT). The scope of SAT 2024 includes all aspects of the theory and applications of propositional satisfiability, broadly construed. This also includes Boolean optimization, such as MaxSAT and Pseudo-Boolean (PB) constraints, Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), Model Counting, and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning. Topics of interest include (but are not limited to): * Theoretical advances (including algorithms, proof complexity, parameterized complexity, and other complexity issues) * Practical search algorithms * Knowledge compilation * Implementation-level details of SAT and SMT solving tools and SAT/SMT-based systems * Problem encodings and reformulations * Applications (including novel application domains and improvements to existing applications) * Case studies and reports on insightful findings based on rigorous experimentation Out of Scope Papers claiming to resolve a major long-standing open theoretical question in Mathematics or Computer Science (such as those for which a Millennium Prize is offered), are outside the scope of the conference because there is insufficient time in the schedule to referee such papers; instead, such papers should be submitted to an appropriate technical journal. Paper Categories Submissions to SAT 2024 are invited in the following three categories: * Long papers (9 to 15 pages, excluding references and appendices) * Short papers (up to 8 pages, excluding references and appendices) * Tool papers (up to 8 pages, excluding references and appendices) Long and short papers should contain original research, with sufficient detail to assess the merits and relevance of the contribution. For papers reporting experimental results, authors are strongly encouraged to make their data and implementation available with the submission. Submissions on applications and case studies are encouraged. Such papers should describe details, weaknesses and strengths of the proposed approaches in sufficient depth, but they are not expected to introduce novel solving methods. Long and short papers will be evaluated with the same quality standards, and are expected to contain a similar contribution per page ratio. The authors should choose between a long or a short paper depending on the space they need to fully describe their contribution.The classification between long and short papers impacts the duration of the presentation of the work during the conference. It is the responsibility of the authors to make sure that their paper is self-contained in the chosen limit of pages. There will be no re-classification of submissions by the PC. Tool papers are expected to report on the design and implementation of a tool, its novel features, strengths, limitations and potential applications. A “tool” is interpreted in a broad sense, including descriptions of solvers, preprocessors etc., as well as systems that exploit SAT and related solvers or their extensions for use in a relevant problem domain. A demonstration is expected to accompany a tool presentation. Papers describing tools that have already been presented previously are expected to contain significant and clear enhancements to the tool. Submission Submissions should not be under review elsewhere nor be submitted elsewhere while under review for SAT 2024, and should not consist of previously published material. Submissions not consistent with these guidelines may be returned without review. Papers must be formatted in the LIPIcs LaTeX style available at https://submission.dagstuhl.de/series/details/LIPIcs#author Submissions must be made electronically in PDF format at https://easychair.org/conferences/?conf=sat2024 The reviewing process for SAT 2024 is single-blind. Authors may submit a supplement containing detailed proofs, examples, software, detailed experimental data, or other material related to the submission, to be consulted at the discretion of the reviewers. The supplement should not be used as overflow space for the main paper, which should be self-contained for review purposes. Supplements will be treated with the same degree of confidentiality as the paper itself. The supplement must consist of a single file in one of the following formats: zipped tarball (.tar.gz or .tgz), gzipped file (.gz), or zip archive (.zip). One author of each accepted paper is expected to register for the conference and present it there. Important dates Abstract submission: March 8, 2024 AoE Full paper submission: March 15, 2024 AoE Author response: May 9-13, 2024 AoE Notification of decisions: May 22, 2024 AoE Camera-ready version submission: July 1, 2024 AoE Workshops & Indian SAT+SMT School: August 18-20, 2024 SAT conference: August 21-24, 2024 Best Paper Awards Long and short papers may be considered for a Best Paper Award. If the main author is a student, both in terms of work and writing, the paper may be considered for a Best Student Paper Award. Proceedings All accepted papers will be published as proceedings of the conference in the Leibniz International Proceedings in Informatics (LIPIcs) as a free, open, electronic archive with access to all. Authors will retain full rights over their work. The accepted papers will be published under a CC-BY license. For more information, please visit http://satisfiability.org/SAT24

1 year, 7 months

1
0
0 0

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, 7 months

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, 7 months

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, 7 months

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, 7 months

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, 7 months

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, 7 months

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, 7 months

1
0
0 0

2025

2024

2023

2022

FMIndia