Women in Formal Methods Workshop (WiFM)

Programme, Friday, August 9, 2024

Objective

The goal of this workshop is to provide a dynamic and inclusive gathering that celebrates the achievements of women in formal methods in particular as well as engineering and computer science in general. We aim to empower female engineers, foster collaboration, and provide a platform for sharing cutting-edge research. This workshop will bring together students, researchers, and industry professionals to explore innovative ideas, discuss challenges, and inspire one another.

Format

We intend to organize the workshop as a one-day event on August 9th, 2024, which will include:

• Research Presentations: the workshop shall feature presentations by female students, researchers, and industry experts to showcase their ground-breaking work in the domain of formal methods and intelligent computer mathematics.
• Panel Discussion "Navigating Challenges": Our panel of accomplished women will engage in candid conversations about the unique challenges faced by female engineers. Topics include work-life balance, bias, and mentorship.
• Celebrating Achievements: We believe in recognizing excellence. Awards will be presented for innovation, leadership, and community impact.

Invited Speaker

We are happy to announce the confirmation of Amber Telfer, Principal Formal Methods Engineer at Microsoft as the keynote speaker at WiFM She is a remarkable engineer in the industry who advocates for gender equality in STEM. She will share her journey, and insights to overcome obstacles and reach new frontiers.

Keynote From Math to AI: Lessons Learned from a Formal Verification Career
Abstract Amber Telfer, Principal Formal Verification Engineer at Microsoft, will be taking us through a reflective journey from grappling with mathematical concepts to harnessing the power of Artificial Intelligence (AI) in the formal verification process. Amber shares personal anecdotes of overcoming challenges, underscoring the pivotal role of continuous learning and adaptability in professional growth. The talk delves into the evolution of her formal verification career, highlighting the transformative impact of AI integration and concluding with 4 lessons you can apply to your own career journey.
Bio Amber Telfer is a Principal Formal Verification Engineer at Microsoft driving formal verification usage and methodology for Cobalt CPUs and related IPs. She is an early adopter leveraging Generative AI for formal verification testbench generation. Prior to Microsoft, Amber was a formal verification engineer at Intel where she formally verified arithmetic units for the Pentium Core 1st generation, multiple IPs with FPV, and mentored new formal engineers. Amber is a graduate of Oregon Graduate Institute at OHSU where she received a Masters in Computer Science & Engineering. To relax, she can be found kayaking nearby lakes or rivers.

Topics of Interest

Topics of interest include (but are not limited to):

• Theorem proving and computer algebra
• Mathematical knowledge management
• Digital mathematical libraries
• Formal specification and modeling
• Formal approaches to fault prevention and detection
• Abstraction, refinement, and evolution
• Integration of formal methods and testing
• SAT/SMT solvers for software analysis and testing
• Practical formal methods
• Applications of formal methods
• Formal approaches to software maintenance
• Formal approaches to safety-critical system development
• Industrial case studies

Many mathematical algorithms are used in safety-critical contexts. Correctness of these algorithms, and the mathematical results underlying them, is crucial. In formal methods, a piece of software called a theorem prover can be used to formally verify algorithms. In this approach, code for an algorithm is accompanied by a rigorous proof of correctness that only depends on the logical foundations of the theorem prover. Algorithms that have been verified in this way are highly trustworthy and thus safe for use in safety-critical applications. Real quantifier elimination problems arise in important application domains, including the verification of cyber-physical systems and motion planning, which makes their correctness crucial. Unfortunately, efficient verified support for quantifier elimination is currently lacking, which necessitates the use of unverified software to resolve quantifier elimination problems that are relevant to safety-critical applications. In this talk, I discuss work on verifying two algorithms for real quantifier elimination in Isabelle/HOL, with a focus on the underlying mathematical intuition and the verification challenges.

Somewhat unexpectedly (even to themselves), mathematicians produce data. The types of data are as varied as mathematics, and so are the ways in which collections are organized. In this talk, I will give a short overview of this landscape.

Evaluating traffic safety based on extracted crash data is deemed unreliable. As an alternative, surrogate safety measures such as Traffic Conflict Techniques (TCTs) are emerging to address many shortcomings of the crash data analysis. However, using data-centric approaches such as simulation to identify traffic conflicts events leading to crashes limits the confidence in road safety assessment. With formal verification, the correctness of the property is guaranteed thanks to the mathematical basis and rigorous analysis nature of formal methods. In the presented research, we aim to complement conventional data-oriented methods for traffic safety assessment with the formalization of TCTs and formal verification of safety properties using the KeYmaera theorem prover based on differential Dynamic Logic (dDL). Our main focus is to guarantee the safety of road users through the evaluation of traffic situations and providing safer traffic interactions between vehicles. In order to analyse different traffic situations and conduct a speed-adaptation feedback loop to update vehicles' speeds, we use the SUMO (Simulation of Urban MObility) traffic simulator, which we feed with the verified property by establishing a data exchange via Mathematica.

In modern data-driven decision-making, transparency and clarity in Machine Learning (ML) models are critical. Explainable Artificial Intelligence (XAI) fulfills this demand by offering human-understandable explanations for the predictions and decisions made by complex Artificial Intelligence (AI) algorithms. XAI bridges the gap between algorithmic processes and end-users, enabling stakeholders to trust and comprehend AI system decisions, thus promoting accountability, fairness, and ethical use of technology. The focus of the presented research is integrating formal methods into XAI frameworks, in particular the XReason tool. We have enhanced XReason by implementing class explanations and integrating it with the LightGBM (LGBM) Classifier, an advanced gradient boosting framework. Our focus is on translating complex decision rules into concise yet informative explanations. The developed tool delivers robust, efficient, and interpretable explanations, making it indispensable for the development of trustworthy AI systems.

Formal methods have a broad adoption in Hardware and Software development in the industry. The author has been leading a formal verification team at Intel that uses ACL2 theorem prover for the verification of hardware. The team developed a methodology for hardware verification and added tools to public libraries of ACL2 Several companies and academic researchers benefitted from those libraries. In this presentation, she will describe the day in the life of a formal verification engineer and all the challenges that they face.

The extended (i.e. smart contract-enabled) UTxO cryptocurrency ledger comes with strong formal guarantees. However, this comes at the cost of inflexibility of specification of what the transaction does to the ledger state. We propose a kind of partially-valid transaction application procedure called "intent processing" to address this inflexibility but maintain certain formal guarantees.

Submissions

• Abstract – up to 2 pages
• Regular – up to 6 pages

Important Dates

• Full Paper Submission: Continuous submission until July 12, 2024 (Early submission leads to early notification).
• Camera Ready: July 26, 2024
• Workshop: August 9, 2024

Program Chair

Yassmeen Elderhalli, Synopsys, Ottawa, ON, Canada

Program Committee

Vandana Desai, Qualcomm, USA
Maissa Elleuch, Digital Research Center of Sfax, Tunisia
Katalin Fazekas, TU Wien, Austria
Liya Liu, AMD, Canada
Ibtissem Seghaier, Nvidia, USA
Yasmine Sharoda, AWS, Canada
Yassmeen Elderhalli (Chair), Synopsys, Canada

Sponsorship

The workshop is partly funded by RESMIQ as the main Sponsor with additional funds from Concordia University.