Continuing the tradition of the previous years, FMCAD 2025 is hosting a Student Forum that provides a platform for students at any career stage (undergraduate or graduate) to introduce their research to the wider Formal Methods community, and solicit feedback.
Accepted Reports
- Nikil Shyamsunder, Francis Pham, Ernest Ng, Adrian Sampson and Kevin Laeufer: Work-in-Progress: Building an Interpreter for an Imperative Hardware Interface Specification Language
- Mason Davis, Bennett Denbleyker, Joshua Smith, Viswanathan Swaminathan and Zhen Zhang: VeRAPAk: Verification of Neural Network Robustness through Refutation and Attack Methods
- Joseph Tafese: Actionable Feedback for eBPF Developers
- Era Thaqi, Dennis Eigner, Arman Ferdowsi and Ulrich Schmid: Symbolic Timing Analysis of Digital Circuits Using Analytic Delay Functions
- Pedro Saccomani and Haniel Barbosa: Towards a Proof-Producing Theory of Finite Fields
- Yao Hsiao and Caroline Trippel: Consistency-Directed Formal Verification of Cache Coherence Protocol Implementations
- Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Shuvendu Lahiri, Shan Lu, David Dill and Clark Barrett: Automated Verification of Data-Structure Modules in Verus
- Liam Davis and Duo Zhou: Lookahead Branching for Neural Network Verification
- Sergei Leonov and Liam Davis: Two Strategies to Improve the Stålmarck Procedure
- Joshua Jeppson, Landon Taylor, Bingqing Hu and Zhen Zhang: Reasoning about Quantitative Rare-Event Reachability in Stochastic Vector Addition Systems via Affine Vector Spaces
- Ian Dardik and Eunsuk Kang: Towards Fully Automated Compositional Inductive Invariant Inference
- Landon Taylor and Zhen Zhang: Tackling Scalability for Transient Reachability Analysis of Chemical Reaction Networks
- Anna Eaton, Nathan Sobotka, Nicholas Mosier, John Mitchell and Caroline Trippel: SimSpect: Automated Litmus Testing for Simulated Spectre Defenses
- William Fishell and Mark Santolucito: Synthesizing State Space Models: Learning Meets Logic
- Bingqing Hu and Zhen Zhang: Error-Guided Predicate Abstraction for Continuous-Time Markov Chains
- Jibiana Jakpor, Hanna Lachnitt and Clark Barrett: Verifying cvc5’s String Rewrite Rules Using Isabelle/HOL
- Alexis Aurandt, Phillip H. Jones and Kristin Yvonne Rozier: Towards Verified Runtime Monitors for Resource-Constrained Embedded Systems
- Sam Akinwande and Clark Barrett: An Inductive Approach To Verifying Neural Feedback Systems
- Nick Waddoups and Zhen Zhang: Verification of Digital Network-on-Chip Systems Using Dafny
- Thomas Hader: Optimization for MCSat
Main Activities
Each student will give a short presentation and present their poster in the poster session.
Submissions for the event must be short reports describing research ideas or ongoing work that the student is currently pursuing and must be within the scope of FMCAD. Work, part of which has been previously published, will be considered; the novel aspect to be addressed in future work must be clearly described in such cases. All submissions will be reviewed by the Student Forum’s program committee.
Important Dates
- Student forum abstract submission:
Monday, July 7, 2025Monday, July 14, 2025 - Student forum submission:
Sunday, July 13, 2025Sunday, July 20, 2025 - Student forum notification: Monday, August 11, 2025
All deadlines are 11:59 pm AoE (Anywhere on Earth)
Format
The event will consist of short presentations by the student authors of each accepted submission, and of a poster that will be on display throughout the duration of the conference. All participants of the conference are encouraged to attend the talks and approach the students during the poster presentation. Instructions for the preparation of the talks and poster sessions will be announced on notification of acceptance.
Visibility
Accepted submissions will be listed, with title and author name, in the event description in the conference proceedings. The authors will also have the option to upload their slide deck/poster/presentation to the FMCAD website. The report itself will not appear in the FMCAD proceedings. Thus, the presentation at the forum should not interfere with potential future submissions of this research (to FMCAD or elsewhere).
Travel Awards
Limited funds may be available to support travel and/or conference registration, which will be reimbursed after the conference. The first author of each contribution will be given priority over other authors. Please ensure you keep all receipts for reimbursement. Further instructions on how to apply for financial support will be provided soon.
Submissions
Submissions must be short reports describing research ideas or ongoing work that the student is currently pursuing. The topic of the reports must be within the scope of the FMCAD conference. These reports will not be published, therefore we welcome reports based on already submitted/published papers. However, the novel aspects to be addressed in future work must be clearly described.
Submissions should follow the same formatting guidelines as those for regular FMCAD conference submissions, except that the length is limited to 2 pages IEEE format (excluding references).
Each student may only submit one report as the main author.
Please submit in the Student Forum track using the Easychair system.
Advice: Focus on the key idea and try to convey it to the reader in an intuitive way. Provide a clear motivation and emphasize novel concepts and contributions. Avoid unnecessary notational clutter unless it is a widely used formalism and helps make the paper more concise and clear. Only describe related work that is absolutely crucial to your contribution: the limited space available should be used to present your work.
Student Forum Chairs
- Tanja Schindler, University of Basel
- Lee A. Barnett, AWS
Feel free to email fmcad2025studentforum@easychair.org if you have any questions about the event.
Program Committee
| Name | Affiliation |
|---|---|
| Armin Biere | University of Freiburg |
| Nikolaj Bjørner | Microsoft |
| Roderick Bloem | Graz University of Technology |
| Julie Cailler | University of Lorraine, CNRS, Inria, LORIA |
| Deepak D’Souza | Indian Institute of Science |
| Rayna Dimitrova | CISPA Helmholtz Center for Information Security |
| Constantin Enea | École Polytechnique |
| Mathias Fleury | University of Freiburg |
| Arie Gurfinkel | University of Waterloo |
| Clemens Hofstadler | Johannes Kepler University Linz |
| Petra Hozzová | Czech Technical University |
| Marie-Christine Jakobs | Ludwig Maximilian University of Munich |
| Tim King | Amazon Web Services |
| Katherine Kosaian | University of Iowa |
| Kasper Luckow | Amazon Web Services |
| Mark Santolucito | Barnard College |
| Jan Strejček | Masaryk University |
| Jiyuan Wang | Tulane University |
| Emily Yu | Institute of Science and Technology Austria |