PPaperPicks
← All conferences
Editions20262024

FM 2024

A

International Symposium on Formal Methods

Official site ↗
67
accepted papers
256
authors
September 09-13, 2024
dates
Italy
location

67 / 67 papers

  1. 1
    A Case Study on Formal Equivalence Verification Between a C/C++ Model and Its RTL Design
    Gaetano Raia
    ,
    Gianluca Rigano
    ,
    David Vincenzoni
    ,
    Maurizio Martina
  2. 2
    A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic
    Valentin Promies
    ,
    Erika Ábrahám
  3. 3
    A Local Search Algorithm for MaxSMT(LIA)
    Xiang He
    ,
    Bohan Li
    ,
    Mengyu Zhao
    ,
    Shaowei Cai
  4. 4
    A Pyramid Of (Formal) Software Verification
    Martin Brain
    ,
    Elizabeth Polgreen
  5. 5
    A Tutorial on Stream-Based Monitoring
    Jan Baumeister
    ,
    Bernd Finkbeiner
    ,
    Florian Kohn
    ,
    Frederik Scheerer
  6. 6
    A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
    Eric Goubault
    ,
    Sylvie Putot
  7. 7
    Accurate Static Data Race Detection for C
    Emerson Sales
    ,
    Omar Inverso
    ,
    Emilio Tuosto
  8. 8
    Advancing Quantum Computing with Formal Methods
    Arend-Jan Quist
    ,
    Jingyi Mei
    ,
    Tim Coopmans
    ,
    Alfons Laarman
  9. 9
    Adversarial Robustness Certification for Bayesian Neural Networks
    Matthew Wicker
    ,
    Andrea Patane
    ,
    Luca Laurenti
    ,
    Marta Kwiatkowska
  10. 10
    AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
    Hanfeng Wang
    ,
    Zhibin Yang
    ,
    Yong Zhou
    ,
    Xilong Wang
    ,
    Weilin Deng
    ,
    Wei Li
  11. 11
    Alloy Repair Hint Generation Based on Historical Data
    Ana Barros
    ,
    Henrique Neto
    ,
    Alcino Cunha
    ,
    Nuno Macedo
    ,
    Ana C. R. Paiva
  12. 12
    ASMETA Tool Set for Rigorous System Design
    Andrea Bombarda
    ,
    Silvia Bonfanti
    ,
    Angelo Gargantini
    ,
    Elvinia Riccobene
    ,
    Patrizia Scandurra
  13. 13
    Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
    Abhishek Tiwari
    ,
    Jyoti Prakash
    ,
    Zhen Dong
    ,
    Carlo A. Furia
  14. 14
    Automated Static Analysis of Quality of Service Properties of Communicating Systems
    Carlos Gustavo López Pombo
    ,
    Agustín Eloy Martinez Suñé
    ,
    Emilio Tuosto
  15. 15
    B2SAT: A Bare-Metal Reduction of B to SAT
    Michael Leuschel
  16. 16
    Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
    Juntao Ji
    ,
    Yinyou Gu
    ,
    Yubao Fu
    ,
    Qingshan Lin
  17. 17
    Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
    Yuang Geng
    ,
    Jake Brandon Baldauf
    ,
    Souradeep Dutta
    ,
    Chao Huang
    ,
    Ivan Ruchkin
  18. 18
    CauMon: An Informative Online Monitor for Signal Temporal Logic
    Zhenya Zhang
    ,
    Jie An
    ,
    Paolo Arcaini
    ,
    Ichiro Hasuo
  19. 19
    Certified Quantization Strategy Synthesis for Neural Networks
    Yedi Zhang
    ,
    Guangke Chen
    ,
    Fu Song
    ,
    Jun Sun
    ,
    Jin Song Dong
  20. 20
    cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
    Pedro Orvalho
    ,
    Mikolás Janota
    ,
    Vasco M. Manquinho
  21. 21
    Chamelon : A Delta-Debugger for OCaml
    Milla Valnet
    ,
    Nathanaëlle Courant
    ,
    Guillaume Bury
    ,
    Pierre Chambart
    ,
    Vincent Laviron
  22. 22
    Code-Level Safety Verification for Automated Driving: A Case Study
    Vladislav Nenchev
    ,
    Calum Imrie
    ,
    Simos Gerasimou
    ,
    Radu Calinescu
  23. 23
    Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms
    Pengbo Yan
    ,
    Toby Murray
    ,
    Olga Ohrimenko
    ,
    Van-Thuan Pham
    ,
    Robert Sison
  24. 24
    Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks
    Huiyu Tan
    ,
    Xi Yang
    ,
    Fu Song
    ,
    Taolue Chen
    ,
    Zhilin Wu
  25. 25
    Detecting Speculative Execution Vulnerabilities on Weak Memory Models
    Nicholas Coughlin
    ,
    Kait Lam
    ,
    Graeme Smith
    ,
    Kirsten Winter
  26. 26
    DFAMiner: Mining Minimal Separating DFAs from Labelled Samples
    Daniele Dell'Erba
    ,
    Yong Li
    ,
    Sven Schewe
  27. 27
    Discourje: Run-Time Verification of Communication Protocols in Clojure - Live at Last
    Sung-Shik Jongmans
  28. 28
    Efficient Formally Verified Maximal End Component Decomposition for MDPs
    Arnd Hartmanns
    ,
    Bram Kohlen
    ,
    Peter Lammich
  29. 29
    Extending Isabelle/HOL's Code Generator with Support for the Go Programming Language
    Terru Stübinger
    ,
    Lars Hupel
  30. 30
    Fast Attack Graph Defense Localization via Bisimulation
    Nimrod Busany
    ,
    Rafi Shalom
    ,
    Dan Klein
    ,
    Shahar Maoz
  31. 31
    FM-Weck: Containerized Execution of Formal-Methods Tools
    Dirk Beyer
    ,
    Henrik Wachowitz
  32. 32
    Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
    Jaeseo Lee
    ,
    Kyungmin Bae
  33. 33
    Free Facts: An Alternative to Inefficient Axioms in Dafny
    Tabea Bordis
    ,
    K. Rustan M. Leino
  34. 34
    Getting Chip Card Payments Right
    David A. Basin
    ,
    Xenia Hofmeier
    ,
    Ralf Sasse
    ,
    Jorge Toro-Pozo
  35. 35
    Integrating Loop Acceleration Into Bounded Model Checking
    Florian Frohn
    ,
    Jürgen Giesl
  36. 36
    Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
    Iacopo Colonnelli
    ,
    Doriana Medic
    ,
    Alberto Mulone
    ,
    Viviana Bono
    ,
    Luca Padovani
    ,
    Marco Aldinucci
  37. 37
    Learning Branching-Time Properties in CTL and ATL via Constraint Solving
    Benjamin Bordais
    ,
    Daniel Neider
    ,
    Rajarshi Roy
  38. 38
    Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
    Ben Greenman
    ,
    Siddhartha Prasad
    ,
    Antonio Di Stasio
    ,
    Shufang Zhu
    ,
    Giuseppe De Giacomo
    ,
    Shriram Krishnamurthi
    ,
    Marco Montali
    ,
    Tim Nelson
    ,
    Milda Zizyte
  39. 39
    No Risk, No Fun - A Tutorial on Risk Management
    Mariëlle Stoelinga
  40. 40
    Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets
    Hao Wu
    ,
    Jie Wang
    ,
    Bican Xia
    ,
    Xiakun Li
    ,
    Naijun Zhan
    ,
    Ting Gan
  41. 41
    On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
    Hao Wu
    ,
    Shenghua Feng
    ,
    Ting Gan
    ,
    Jie Wang
    ,
    Bican Xia
    ,
    Naijun Zhan
  42. 42
    Parameterized Verification of Round-Based Distributed Algorithms via Extended Threshold Automata
    Tom Baumeister
    ,
    Paul Eichler
    ,
    Swen Jacobs
    ,
    Mouhammad Sakr
    ,
    Marcus Völp
  43. 43
    Partially Observable Stochastic Games with Neural Perception Mechanisms
    Rui Yan
    ,
    Gabriel Santos
    ,
    Gethin Norman
    ,
    David Parker
    ,
    Marta Kwiatkowska
  44. 44
    Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
    S. Akshay
    ,
    Supratik Chakraborty
    ,
    Amir Kafshdar Goharshady
    ,
    R. Govind
    ,
    Harshit J. Motwani
    ,
    Sai Teja Varanasi
  45. 45
    Practical Deductive Verification of OCaml Programs
    Mário Pereira
  46. 46
    Proving Functional Program Equivalence via Directed Lemma Synthesis
    Yican Sun
    ,
    Ruyi Ji
    ,
    Jian Fang
    ,
    Xuanlin Jiang
    ,
    Mingshuai Chen
    ,
    Yingfei Xiong
  47. 47
    PyBDR: Set-Boundary Based Reachability Analysis Toolkit in Python
    Jianqiang Ding
    ,
    Taoran Wu
    ,
    Zhen Liang
    ,
    Bai Xue
  48. 48
    Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
    Konstantin Britikov
    ,
    Martin Blicha
    ,
    Natasha Sharygina
    ,
    Grigory Fedyukovich
  49. 49
    Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
    Julius Adelt
    ,
    Robert Mensing
    ,
    Paula Herber
  50. 50
    Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
    Laura Titolo
    ,
    Mariano M. Moscato
    ,
    Marco A. Feliú
    ,
    Paolo Masci
    ,
    César A. Muñoz