


default search action
26th FM 2024: Milan, Italy - Part I
- André Platzer
, Kristin Yvonne Rozier
, Matteo Pradella
, Matteo Rossi
:
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14933, Springer 2025, ISBN 978-3-031-71161-9
Invited Papers
- Matthew Wicker
, Andrea Patane
, Luca Laurenti
, Marta Kwiatkowska
:
Adversarial Robustness Certification for Bayesian Neural Networks. 3-28 - David A. Basin
, Xenia Hofmeier
, Ralf Sasse
, Jorge Toro-Pozo:
Getting Chip Card Payments Right. 29-51
Fundamentals of Formal Verification
- Xiang He
, Bohan Li
, Mengyu Zhao
, Shaowei Cai
:
A Local Search Algorithm for MaxSMT(LIA). 55-72 - Florian Frohn
, Jürgen Giesl
:
Integrating Loop Acceleration Into Bounded Model Checking. 73-91 - Hao Wu
, Jie Wang
, Bican Xia
, Xiakun Li
, Naijun Zhan
, Ting Gan
:
Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets. 92-110 - S. Akshay, Supratik Chakraborty, Amir Kafshdar Goharshady, R. Govind, Harshit J. Motwani, Sai Teja Varanasi:
Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic. 111-130 - Valentin Promies
, Erika Ábrahám
:
A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic. 131-148
Foundations
- Tabea Bordis
, K. Rustan M. Leino
:
Free Facts: An Alternative to Inefficient Axioms in Dafny. 151-169 - Rüdiger Ehlers
:
Understanding Synthesized Reactive Systems Through Invariants. 170-187 - Pengbo Yan
, Toby Murray
, Olga Ohrimenko
, Van-Thuan Pham
, Robert Sison
:
Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms. 188-205 - Arnd Hartmanns
, Bram Kohlen
, Peter Lammich
:
Efficient Formally Verified Maximal End Component Decomposition for MDPs. 206-225 - Iacopo Colonnelli
, Doriana Medic
, Alberto Mulone
, Viviana Bono
, Luca Padovani
, Marco Aldinucci
:
Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows. 226-244 - Nimrod Busany
, Rafi Shalom
, Dan Klein
, Shahar Maoz
:
Fast Attack Graph Defense Localization via Bisimulation. 245-263
Learn and Repair
- Loes Kruger
, Sebastian Junges
, Jurriaan Rot
:
State Matching and Multiple References in Adaptive Active Automata Learning. 267-284 - Abhishek Tiwari, Jyoti Prakash, Zhen Dong, Carlo A. Furia:
Automated Repair of Information Flow Security in Android Implicit Inter-App Communication. 285-303 - Benjamin Bordais
, Daniel Neider, Rajarshi Roy:
Learning Branching-Time Properties in CTL and ATL via Constraint Solving. 304-323 - Eric Goubault
, Sylvie Putot
:
A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks. 324-342 - Yedi Zhang, Guangke Chen
, Fu Song, Jun Sun, Jin Song Dong:
Certified Quantization Strategy Synthesis for Neural Networks. 343-362 - Rui Yan
, Gabriel Santos
, Gethin Norman
, David Parker
, Marta Kwiatkowska
:
Partially Observable Stochastic Games with Neural Perception Mechanisms. 363-380 - Yuang Geng
, Jake Brandon Baldauf
, Souradeep Dutta
, Chao Huang
, Ivan Ruchkin
:
Bridging Dimensions: Confident Reachability for High-Dimensional Controllers. 381-402 - Yanling Lin
, Ji Guan
, Wang Fang
, Mingsheng Ying
, Zhaofeng Su
:
VeriQR: A Robustness Verification Tool for quantum Machine Learning Models. 403-421
Programming Languages
- Jaeseo Lee
, Kyungmin Bae
:
Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption. 425-442 - Emerson Sales
, Omar Inverso
, Emilio Tuosto
:
Accurate Static Data Race Detection for C. 443-462 - Pedro Orvalho
, Mikolás Janota
, Vasco M. Manquinho
:
cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases. 463-481 - Nicholas Coughlin
, Kait Lam
, Graeme Smith
, Kirsten Winter
:
Detecting Speculative Execution Vulnerabilities on Weak Memory Models. 482-500 - Darius Foo
, Yahui Song
, Wei-Ngan Chin
:
Staged Specification Logic for Verifying Higher-Order Imperative Programs. 501-518 - Lara Bargmann
, Brijesh Dongol
, Heike Wehrheim
:
Unifying Weak Memory Verification Using Potentials. 519-537 - Yican Sun, Ruyi Ji, Jian Fang, Xuanlin Jiang, Mingshuai Chen, Yingfei Xiong:
Proving Functional Program Equivalence via Directed Lemma Synthesis. 538-557 - Konstantin Britikov
, Martin Blicha
, Natasha Sharygina
, Grigory Fedyukovich
:
Reachability Analysis for Multiloop Programs Using Transition Power Abstraction. 558-576
Logic and Automata
- Ben Greenman
, Siddhartha Prasad
, Antonio Di Stasio
, Shufang Zhu
, Giuseppe De Giacomo
, Shriram Krishnamurthi
, Marco Montali
, Tim Nelson
, Milda Zizyte
:
Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic. 579-599 - Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Dorde Zikelic:
Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs. 600-619 - Jie An
, Qiang Gao, Lingtai Wang, Naijun Zhan
, Ichiro Hasuo
:
The Opacity of Timed Automata. 620-637 - Tom Baumeister
, Paul Eichler
, Swen Jacobs
, Mouhammad Sakr
, Marcus Völp
:
Parameterized Verification of Round-Based Distributed Algorithms via Extended Threshold Automata. 638-657 - Benjamin Przybocki
, Guilherme Vicentin de Toledo
, Yoni Zohar
, Clark W. Barrett
:
The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem Theorems. 658-675

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.